fix #4048: incorrect bvurem rewrite when divisor=0

also, always enable this rewrite, since it shrinks formula size globally
Z3Prover · Apr 22, 2020 · 220bc7f · 220bc7f
1 parent dd064a5
commit 220bc7f
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 5 deletions.
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
@@ -29,7 +29,6 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
     m_elim_sign_ext = p.elim_sign_ext();
     m_mul2concat = p.mul2concat();
     m_bit2bool = p.bit2bool();
-    m_urem_simpl = p.bv_urem_simpl();
     m_blast_eq_value = p.blast_eq_value();
     m_split_concat_eq = p.split_concat_eq();
     m_bvnot2arith = p.bvnot2arith();
@@ -2608,15 +2607,15 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             return st;
     }
 
-    if (m_urem_simpl) {
+    {
         expr * dividend;
         expr * divisor;
         numeral divisor_val, rhs_val;
         unsigned divisor_sz, rhs_sz;
         if (is_urem_any(lhs, dividend, divisor)
             && is_numeral(rhs, rhs_val, rhs_sz)
             && is_numeral(divisor, divisor_val, divisor_sz)) {
-            if (rhs_val >= divisor_val) {//(= (bvurem x c1) c2) where c2 >= c1
+            if (!divisor_val.is_zero() && rhs_val >= divisor_val) {//(= (bvurem x c1) c2) where c2 >= c1
                 result = m().mk_false();
                 return BR_DONE;
             }

diff --git a/src/ast/rewriter/bv_rewriter_params.pyg b/src/ast/rewriter/bv_rewriter_params.pyg
@@ -12,6 +12,5 @@ def_module_params(module_name='rewriter',
                           ("bv_extract_prop", BOOL, False, "attempt to partially propagate extraction inwards"),
                           ("bv_not_simpl", BOOL, False, "apply simplifications for bvnot"),
                           ("bv_ite2id", BOOL, False, "rewrite ite that can be simplified to identity"),
-                          ("bv_le_extra", BOOL, False, "additional bu_(u/s)le simplifications"),
-                          ("bv_urem_simpl", BOOL, False, "additional simplification for bvurem")
+                          ("bv_le_extra", BOOL, False, "additional bu_(u/s)le simplifications")
                           ))