fix #6313

remaining new issues
Z3Prover · Sep 3, 2022 · 7e1e64d · 7e1e64d
1 parent 9dca8d1
commit 7e1e64d
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 4 deletions.
diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
@@ -183,7 +183,9 @@ namespace mbp {
                 return c0;
             };
 
-            if (a.is_mul(t, t1, t2) && is_numeral(t1, mul1))
+            if (tids.contains(t))
+                insert_mul(t, mul, ts);
+            else if (a.is_mul(t, t1, t2) && is_numeral(t1, mul1))
                 linearize(mbo, eval, mul * mul1, t2, c, fmls, ts, tids);
             else if (a.is_mul(t, t1, t2) && is_numeral(t2, mul1))
                 linearize(mbo, eval, mul * mul1, t1, c, fmls, ts, tids);
@@ -221,6 +223,7 @@ namespace mbp {
                 vars coeffs;
                 rational c0 = add_def(t1, mul1, coeffs);
                 tids.insert(t, mbo.add_mod(coeffs, c0, mul1));
+
             }
             else if (a.is_idiv(t, t1, t2) && is_numeral(t2, mul1) && mul1 > 0) {
                 // v = t1 div mul1
@@ -278,9 +281,8 @@ namespace mbp {
 
         expr_ref var2expr(ptr_vector<expr> const& index2expr, var const& v) {
             expr_ref t(index2expr[v.m_id], m);
-            if (!v.m_coeff.is_one()) {
-                t = a.mk_mul(a.mk_numeral(v.m_coeff, a.is_int(t)), t);
-            }
+            if (!v.m_coeff.is_one()) 
+                t = a.mk_mul(a.mk_numeral(v.m_coeff, a.is_int(t)), t);            
             return t;
         }
 

diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
@@ -450,6 +450,10 @@ namespace bv {
      * Create the axioms:
      *   bit2bool(i,n) == ((e div 2^i) mod 2 != 0)
      * for i = 0,.., sz-1
+     *
+     * Alternative axiomatization:
+     * e = sum bit2bool(i,n)*2^i + 2^n * (div(e, 2^n))
+     * possibly term div(e,2^n) is not 
      */
     void solver::assert_int2bv_axiom(app* n) {
         expr* e = nullptr;