From 657aaf9a0fd9d6e427aca3f8228e77fd3472927a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 Mar 2024 10:15:44 -0800 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/sls/bv_sls_eval.cpp | 2 +- src/ast/sls/sls_valuation.cpp | 9 +++------ 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 592c92b1c39..cc5911905c4 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -976,7 +976,7 @@ namespace bv { bool sls_eval::try_repair_band(bvect const& e, bvval& a, bvval const& b) { for (unsigned i = 0; i < a.nw; ++i) - m_tmp[i] = (e[i] & ~a.fixed[i]) | (~b.bits()[i] & ~a.fixed[i] & random_bits()); + m_tmp[i] = ~a.fixed[i] & (e[i] | (~b.bits()[i] & random_bits())); return a.set_repair(random_bool(), m_tmp); } diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index f7ce41f8b74..b656a341bf7 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -347,7 +347,7 @@ namespace bv { dst.set(i, true); } else { - for (unsigned i = 0; !in_range(dst); ++i) + for (unsigned i = 0; i < bw && !in_range(dst); ++i) if (!fixed.get(i) && !dst.get(i)) dst.set(i, true); for (unsigned i = bw; !in_range(dst) && i-- > 0;) @@ -431,7 +431,6 @@ namespace bv { // bool sls_valuation::can_set(bvect const& new_bits) const { SASSERT(!has_overflow(new_bits)); - // verbose_stream() << "can set " << bw << " " << new_bits[0] << " " << in_range(new_bits) << "\n"; for (unsigned i = 0; i < nw; ++i) if (0 != ((new_bits[i] ^ m_bits[i]) & fixed[i])) return false; @@ -548,10 +547,8 @@ namespace bv { set(tmp, m_lo); unsigned max_diff = bw; for (unsigned i = 0; i < bw; ++i) { - if (fixed.get(i) && (m_bits.get(i) ^ m_lo.get(i))) { - tmp.set(i, m_bits.get(i)); - max_diff = i; - } + if (fixed.get(i) && (m_bits.get(i) ^ m_lo.get(i))) + max_diff = i; } SASSERT(max_diff != bw);