diff --git a/src/ast/sls/sls_bv_valuation.cpp b/src/ast/sls/sls_bv_valuation.cpp index 6f0620881..2f3d0529d 100644 --- a/src/ast/sls/sls_bv_valuation.cpp +++ b/src/ast/sls/sls_bv_valuation.cpp @@ -94,7 +94,8 @@ namespace sls { rational p(1), r(0); for (unsigned i = 0; i < nw; ++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; }