diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index 5dddf6d7e..75dfac8c2 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -1169,7 +1169,7 @@ void bit_blaster_tpl<Cfg>::mk_const_case1_multiplier(unsigned sz, expr * const *
         if (!m().is_true(a_bits[i]))
             continue;
 
-        ptr_buffer<expr, 128> one, sbits;
+        ptr_buffer<expr, 128> kbits, ibits;
         expr_ref_vector out_bits1(m());
 
         unsigned k = 0;
@@ -1189,8 +1189,8 @@ void bit_blaster_tpl<Cfg>::mk_const_case1_multiplier(unsigned sz, expr * const *
             // shift by k+1, subtract x
             out_bits.reset();
 
-            mul2_i(k + 1, sbits);
-            mk_adder(sz, out_bits.data(), sbits.data(), out_bits1);
+            mul2_i(k + 1, kbits);
+            mk_adder(sz, out_bits.data(), kbits.data(), out_bits1);
             out_bits.reset();
             out_bits.append(out_bits1);
             out_bits1.reset();
@@ -1201,18 +1201,25 @@ void bit_blaster_tpl<Cfg>::mk_const_case1_multiplier(unsigned sz, expr * const *
             out_bits.append(out_bits1);
             out_bits1.reset();
         }
-        else if (i == k) {
-            mul2_i(i, sbits);
-            mk_adder(sz, out_bits.data(), sbits.data(), out_bits1);
+        else if (i <= k && k <= i + 1) {
+            mul2_i(i, ibits);
+            mk_adder(sz, out_bits.data(), ibits.data(), out_bits1);
             out_bits.reset();
             out_bits.append(out_bits1);
             out_bits1.reset();
+            if (i + 1 == k) {
+                mul2_i(k, kbits);
+                mk_adder(sz, out_bits.data(), kbits.data(), out_bits1);
+                out_bits.reset();
+                out_bits.append(out_bits1);
+                out_bits1.reset();
+            }                
         }
         else if (k == sz - 1) {
             // 2^sz - 2^i = - 2^i
             // -= x*2^i
-            mul2_i(i, sbits);
-            mk_subtracter(sz, out_bits.data(), sbits.data(), out_bits1, cout);
+            mul2_i(i, ibits);
+            mk_subtracter(sz, out_bits.data(), ibits.data(), out_bits1, cout);
             out_bits.reset();
             out_bits.append(out_bits1);
         }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index cee367ad7..bdb396916 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1943,7 +1943,7 @@ public:
 
     final_check_status final_check_eh() {
 
-        verbose_stream() << "final " << ctx().get_scope_level() << " " << ctx().assigned_literals().size() << "\n";
+        //        verbose_stream() << "final " << ctx().get_scope_level() << " " << ctx().assigned_literals().size() << "\n";
         //ctx().display(verbose_stream());
         //exit(0);
         
diff --git a/src/test/bit_blaster.cpp b/src/test/bit_blaster.cpp
index 309e3e05c..19a161394 100644
--- a/src/test/bit_blaster.cpp
+++ b/src/test/bit_blaster.cpp
@@ -195,12 +195,6 @@ void tst_const_multiplier(ast_manager& m, bit_blaster & blaster, unsigned sz) {
         expr_ref_vector c(m), out1(m), out2(m);
         for (unsigned j = 0; j < sz; ++j) 
             c.push_back((i & (1ul << j)) ? m.mk_true() : m.mk_false());
-        for (auto xi : x)
-            verbose_stream() << mk_pp(xi, m);
-        verbose_stream() << " ";
-        for (auto ci : c)
-            verbose_stream() << mk_pp(ci, m);
-        verbose_stream() << "\n";
         blaster.mk_const_case1_multiplier(sz, c.data(), x.data(), out1);
         
         blaster.mk_generic_multiplier(sz, c.data(), x.data(), out2);
@@ -211,7 +205,6 @@ void tst_const_multiplier(ast_manager& m, bit_blaster & blaster, unsigned sz) {
         smt::kernel solver(m, fp);
         solver.assert_expr(m.mk_not(fml));
         auto r = solver.check();
-        verbose_stream() << r << "\n";
         VERIFY(r == l_false);
         expr_mark vis1, vis2;
         unsigned sz1 = 0, sz2 = 0;
@@ -272,7 +265,7 @@ void tst_bit_blaster() {
     bit_blaster_params params;
     bit_blaster blaster(m, params);
 
-    tst_const_multiplier(m, blaster, 7);
+    tst_const_multiplier(m, blaster, 8);
     tst_adder(m, blaster);
     tst_multiplier(m, blaster);
     tst_le(m, 4);