From 6b0a10637c7aa7c188be674d5625c8d291ee2cb0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Aug 2024 10:06:10 -0700 Subject: [PATCH] reserve for multiplication Signed-off-by: Nikolaj Bjorner --- src/ast/sls/bv_sls_eval.cpp | 6 +++--- src/ast/sls/sls_valuation.cpp | 2 ++ 2 files changed, 5 insertions(+), 3 deletions(-) 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) {