From 3bcd98b6532fc3a694804f086a26cd5e20541430 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Aug 2024 10:59:27 -0700 Subject: [PATCH] include bounds checks in set random --- src/ast/sls/sls_valuation.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index 7a0edb546..264eefbb1 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -249,26 +249,27 @@ namespace bv { if (!get_at_most(src, m_tmp)) return false; - if (is_zero(m_tmp) || (0 != r(10))) - return try_set(m_tmp); + if (is_zero(m_tmp) && (0 != r(10))) + return try_set(m_tmp) && m_tmp <= src; // random value below tmp set_random_below(m_tmp, r); - return (can_set(m_tmp) || get_at_most(src, m_tmp)) && try_set(m_tmp); + return (can_set(m_tmp) || get_at_most(src, m_tmp)) && m_tmp <= src && try_set(m_tmp); } bool sls_valuation::set_random_at_least(bvect const& src, random_gen& r) { + m_tmp.set_bw(bw); if (!get_at_least(src, m_tmp)) return false; - if (is_ones(m_tmp) || (0 != r(10))) + if (is_ones(m_tmp) && (0 != r(10))) return try_set(m_tmp); // random value at least tmp set_random_above(m_tmp, r); - return (can_set(m_tmp) || get_at_least(src, m_tmp)) && try_set(m_tmp); + return (can_set(m_tmp) || get_at_least(src, m_tmp)) && src <= m_tmp && try_set(m_tmp); } bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r) {