From 1f55ec5cefca2e42e8fe8eee871710e9f1551d9a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Dec 2024 13:01:47 -0800 Subject: [PATCH] fix random update to a legal one Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_lookahead.cpp | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index dde03265d..37ca06b26 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -70,11 +70,17 @@ namespace sls { } bool bv_lookahead::apply_random_update(ptr_vector const& vars) { - expr* e = vars[ctx.rand(vars.size())]; - auto& v = wval(e); - m_v_updated.set_bw(v.bw); - v.get_variant(m_v_updated, m_ev.m_rand); - apply_update(e, m_v_updated); + while (true) { + expr* e = vars[ctx.rand(vars.size())]; + auto& v = wval(e); + m_v_updated.set_bw(v.bw); + v.get_variant(m_v_updated, m_ev.m_rand); + v.eval = m_v_updated; + if (!v.commit_eval()) + continue; + apply_update(e, m_v_updated); + break; + } return true; } @@ -221,6 +227,7 @@ namespace sls { SASSERT(is_uninterp(e)); SASSERT(m_restore.empty()); wval(e).eval = new_value; + VERIFY(wval(e).commit_eval()); insert_update_stack(e); unsigned max_depth = get_depth(e);