mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

skip last power

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-28 15:03:01 -08:00
parent 8a7d971264
commit 1676378be9
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/sls/sls_bv_valuation.cpp
View file

@ -94,7 +94,8 @@ namespace sls {
rational p(1), r(0); rational p(1), r(0);
for (unsigned i = 0; i < nw; ++i) { for (unsigned i = 0; i < nw; ++i) {
r += p * rational((*this)[i]); r += p * rational((*this)[i]);
p *= rational::power_of_two(8 * sizeof(digit_t)); if (i + 1 < nw)
p *= rational::power_of_two(8 * sizeof(digit_t));
} }
return r; return r;
} }