fix random update to a legal one

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 27, 2024 · 1f55ec5 · 1f55ec5
1 parent c82518c
commit 1f55ec5
Showing 1 changed file with 12 additions and 5 deletions.
diff --git 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<expr> 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);