diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
index cbf04f058..7b7e32612 100644
--- a/src/ast/sls/bv_sls_eval.cpp
+++ b/src/ast/sls/bv_sls_eval.cpp
@@ -352,13 +352,13 @@ namespace bv {
             break;
         }
         case OP_BMUL: {
+            SASSERT(e->get_num_args() > 1);
             auto const& a = wval(e->get_arg(0));
             auto const& b = wval(e->get_arg(1));
-            for (unsigned i = 0; i < a.nw; ++i)
-                val.set_mul(val.eval, a.bits(), b.bits());
+            val.set_mul(val.eval, a.bits(), b.bits(), false);
             for (unsigned j = 2; j < e->get_num_args(); ++j) {
                 auto const& c = wval(e->get_arg(j));
-                val.set_mul(val.eval, val.eval, c.bits());
+                val.set_mul(val.eval, val.eval, c.bits(), false);
             }
             break;
         }
diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp
index 7f35cbb8d..7a0edb546 100644
--- a/src/ast/sls/sls_valuation.cpp
+++ b/src/ast/sls/sls_valuation.cpp
@@ -705,6 +705,8 @@ namespace bv {
     }
 
     bool sls_valuation::set_mul(bvect& out, bvect const& a, bvect const& b, bool check_overflow) const {
+        out.reserve(2 * nw);
+        SASSERT(out.size() >= 2 * nw);
         mpn_manager().mul(a.data(), nw, b.data(), nw, out.data());
         bool ovfl = false;
         if (check_overflow) {