From 1676378be9330a4dfb10899101ed10060b6aba1e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Jan 2025 15:03:01 -0800
Subject: [PATCH] skip last power
---
src/ast/sls/sls_bv_valuation.cpp | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
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;
}