From 7e1e64d027b2d44c5b17e3ea4b8d82c002760175 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 2 Sep 2022 17:43:57 -0700
Subject: [PATCH] fix #6313

remaining new issues
---
 src/qe/mbp/mbp_arith.cpp       | 10 ++++++----
 src/sat/smt/bv_internalize.cpp |  4 ++++
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index 47ee53668..79f931d50 100644
--- 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
index 8199f539e..6d2dc683a 100644
--- 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;