mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 19:00:25 +00:00
Code Activity

reserve for multiplication

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-27 10:06:10 -07:00
parent a0ae5c8d5e
commit 6b0a10637c
2 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/sls/bv_sls_eval.cpp
View file

@ -352,13 +352,13 @@ namespace bv {
break; break;
} }
case OP_BMUL: { case OP_BMUL: {
SASSERT(e->get_num_args() > 1);
auto const& a = wval(e->get_arg(0)); auto const& a = wval(e->get_arg(0));
auto const& b = wval(e->get_arg(1)); 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(), false);
val.set_mul(val.eval, a.bits(), b.bits());
for (unsigned j = 2; j < e->get_num_args(); ++j) { for (unsigned j = 2; j < e->get_num_args(); ++j) {
auto const& c = wval(e->get_arg(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; break;
} }

2
src/ast/sls/sls_valuation.cpp
View file

@ -705,6 +705,8 @@ namespace bv {
} }
bool sls_valuation::set_mul(bvect& out, bvect const& a, bvect const& b, bool check_overflow) const { 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()); mpn_manager().mul(a.data(), nw, b.data(), nw, out.data());
bool ovfl = false; bool ovfl = false;
if (check_overflow) { if (check_overflow) {