@@ -109,17 +109,20 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
109109        break ;
110110    case  OP_BNEG_OVFL:
111111        SASSERT (num_args == 1 );
112-         return  mk_bvneg_overflow (args[0 ], result);
113- 
112+         st =  mk_bvneg_overflow (args[0 ], result);
113+          break ; 
114114    case  OP_BSHL:
115115        SASSERT (num_args == 2 );
116-         return  mk_bv_shl (args[0 ], args[1 ], result);
116+         st = mk_bv_shl (args[0 ], args[1 ], result);
117+         break ;
117118    case  OP_BLSHR:
118119        SASSERT (num_args == 2 );
119-         return  mk_bv_lshr (args[0 ], args[1 ], result);
120+         st = mk_bv_lshr (args[0 ], args[1 ], result);
121+         break ;
120122    case  OP_BASHR:
121123        SASSERT (num_args == 2 );
122-         return  mk_bv_ashr (args[0 ], args[1 ], result);
124+         st = mk_bv_ashr (args[0 ], args[1 ], result);
125+         break ;
123126    case  OP_BSDIV:
124127        SASSERT (num_args == 2 );
125128        return  mk_bv_sdiv (args[0 ], args[1 ], result);
@@ -151,13 +154,16 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
151154        SASSERT (num_args == 2 );
152155        return  mk_bv_smod_i (args[0 ], args[1 ], result);
153156    case  OP_CONCAT:
154-         return  mk_concat (num_args, args, result);
157+         st = mk_concat (num_args, args, result);
158+         break ;
155159    case  OP_EXTRACT:
156160        SASSERT (num_args == 1 );
157-         return  mk_extract (m_util.get_extract_high (f), m_util.get_extract_low (f), args[0 ], result);
161+         st = mk_extract (m_util.get_extract_high (f), m_util.get_extract_low (f), args[0 ], result);
162+         break ;
158163    case  OP_REPEAT:
159164        SASSERT (num_args == 1 );
160-         return  mk_repeat (f->get_parameter (0 ).get_int (), args[0 ], result);
165+         st = mk_repeat (f->get_parameter (0 ).get_int (), args[0 ], result);
166+         break ;
161167    case  OP_ZERO_EXT:
162168        SASSERT (num_args == 1 );
163169        return  mk_zero_extend (f->get_parameter (0 ).get_int (), args[0 ], result);
@@ -596,53 +602,45 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
596602        // 
597603        //  a <=_u #x000f
598604        // 
599-         unsigned  bv_sz = m_util.get_bv_size (b);
600-         unsigned  i     = bv_sz;
601-         unsigned  first_non_zero = UINT_MAX;
602-         while  (i > 0 ) {
603-             --i;
604-             if  (!is_zero_bit (b, i)) {
605-                 first_non_zero = i;
606-                 break ;
607-             }
608-         }
605+         unsigned  bv_sz = m_util.get_bv_size (a);
606+         auto  last_non_zero = [&](expr* x) {
607+             for  (unsigned  i = bv_sz; i-- > 0 ; ) 
608+                 if  (!is_zero_bit (x, i)) 
609+                     return  i;
610+             return  UINT_MAX;
611+         };
612+         
613+         unsigned  lnz = last_non_zero (b);
609614
610-         if  (first_non_zero  == UINT_MAX) {
615+         if  (lnz  == UINT_MAX) {
611616            //  all bits are zero
612617            result = m.mk_eq (a, mk_zero (bv_sz));
613618            return  BR_REWRITE1;
614619        }
615-         else  if  (first_non_zero < bv_sz - 1  && m_le2extract) {
616-             result = m.mk_and (m.mk_eq (m_mk_extract (bv_sz - 1 , first_non_zero + 1 , a), mk_zero (bv_sz - first_non_zero - 1 )),
617-                                 m_util.mk_ule (m_mk_extract (first_non_zero, 0 , a), m_mk_extract (first_non_zero, 0 , b)));
620+         else  if  (lnz < bv_sz - 1  && m_le2extract) {
621+             //  a[sz-1:lnz+1] = 0 & a[lnz:0] <= b[lnz:0]
622+             result = m.mk_and (m.mk_eq (m_mk_extract (bv_sz - 1 , lnz + 1 , a), mk_zero (bv_sz - lnz - 1 )),
623+                               m_util.mk_ule (m_mk_extract (lnz, 0 , a), m_mk_extract (lnz, 0 , b)));
624+ 
618625            return  BR_REWRITE3;
619626        }
620627
621-         //  #x000f <=_u a <=> not (a <=_u #x000f) or a = #x000f
622-         i = bv_sz;
623-         first_non_zero = UINT_MAX;
624-         while  (i > 0 ) {
625-             --i;
626-             if  (!is_zero_bit (a, i)) {
627-                 first_non_zero = i;
628-                 break ;
629-             }
630-         }        
631628
632-         if  (first_non_zero == UINT_MAX) {
629+         lnz = last_non_zero (a);
630+ 
631+         if  (lnz == UINT_MAX) {
633632            //  all bits are zero
634-             result = m.mk_eq (b,  mk_zero (bv_sz) );
635-             return  BR_REWRITE1 ;
633+             result = m.mk_true ( );
634+             return  BR_DONE ;
636635        }
637-         else  if  (first_non_zero < bv_sz - 1  && m_le2extract) {
638-             result = m.mk_and (m.mk_eq (m_mk_extract (bv_sz - 1 , first_non_zero + 1 , b), mk_zero (bv_sz - first_non_zero - 1 )),
639-                                 m_util.mk_ule (m_mk_extract (first_non_zero, 0 , b), m_mk_extract (first_non_zero, 0 , a)));
640-             result = m.mk_or (m.mk_not (result), m.mk_eq (a, b));
636+         else  if  (lnz < bv_sz - 1  && m_le2extract) {
637+             //  use the equivalence to simplify:
638+             //  #x000f <=_u b <=> b[sz-1:lnz+1] != 0 or #xf <= b[lnz:0])
639+ 
640+             result = m.mk_implies (m.mk_eq (m_mk_extract (bv_sz - 1 , lnz + 1 , b), mk_zero (bv_sz - lnz - 1 )),
641+                                   m_util.mk_ule (m_mk_extract (lnz, 0 , a), m_mk_extract (lnz, 0 , b)));
641642            return  BR_REWRITE_FULL;
642643        }
643- 
644- 
645- 
646644    }
647645#endif 
648646
0 commit comments