fix #3953

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 14, 2020 · 5e0c34c · 5e0c34c
1 parent 2a0537a
commit 5e0c34c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 5 deletions.
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -971,7 +971,6 @@ class inc_sat_solver : public solver {
                 IF_VERBOSE(0, verbose_stream() << "evaluated to " << tmp << "\n");
                 all_true = false;
             }
-            //IF_VERBOSE(0, verbose_stream() << (i++) << ": " << mk_pp(f, m) << "\n");
         }
         if (!all_true) {
             IF_VERBOSE(0, verbose_stream() << m_params << "\n");

diff --git a/src/tactic/arith/bv2int_rewriter.cpp b/src/tactic/arith/bv2int_rewriter.cpp
@@ -234,7 +234,7 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
     if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
         align_sizes(s1, t1, false);
         result = m_bv.mk_bv2int(m_bv.mk_bv_urem(s1, t1));
-        TRACE("bv2int_rewriter", tout << mk_pp(result,m()) << "\n";);
+        TRACE("bv2int_rewriter", tout << result << "\n";);
         return BR_DONE;
     }
 
@@ -243,13 +243,13 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
     //
     if (is_bv2int_diff(s, s1, s2) && is_bv2int(t, t1)) {
         expr_ref u1(m());
-        align_sizes(s1, t1, false);
-        u1 = m_bv.mk_bv_urem(s1, t1);
+        align_sizes(s2, t1, false);
+        u1 = m_bv.mk_bv_urem(s2, t1);
         u1 = m_bv.mk_bv_sub(t1, u1);
         u1 = mk_bv_add(s1, u1, false);
         align_sizes(u1, t1, false);
         result = m_bv.mk_bv2int(m_bv.mk_bv_urem(u1, t1));
-        TRACE("bv2int_rewriter", tout << mk_pp(result,m()) << "\n";);
+        TRACE("bv2int_rewriter", tout << result << "\n";);
         return BR_DONE;
     }