From e43854d4aa51b36dd46bab6338748810df84fe01 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 4 Mar 2026 15:37:51 +0000
Subject: [PATCH] Fix array refinement crash with CaDiCaL SAT solver

Commit 6ff2ce40b8 ("Use get_value() instead of get() in array
refinement loop", PR #8842) introduced get_value() calls in
arrays_overapproximated() that read actual values from the SAT
model (via CaDiCaL's val()). The loop interleaved these calls with
modifications to the main solver (adding clauses via
prop.l_set_to_true(convert(...))). CaDiCaL 3.0.0 strictly enforces
that val() can only be called in the satisfied state, and adding
clauses invalidates that state, causing a fatal error:
  'can only get value in satisfied state'

This was observed on the macOS-14 CI job (which uses CaDiCaL) for
Array_UF3, Array_UF4, Array_UF5, Array_UF7, Array_UF8, Array_UF9,
and Array_UF16 tests, all of which use --refine-arrays.

Fix: split the loop into two phases. First, evaluate all lazy
constraints using get_value() while the solver is still in SAT
state. Then, check each evaluated constraint with a local solver
and activate violated ones by adding clauses to the main solver.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 src/solvers/refinement/refine_arrays.cpp | 46 ++++++++++++++++--------
 1 file changed, 32 insertions(+), 14 deletions(-)

diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp
index e8e6816bcfc..1456410dc7f 100644
--- a/src/solvers/refinement/refine_arrays.cpp
+++ b/src/solvers/refinement/refine_arrays.cpp
@@ -40,14 +40,25 @@ void bv_refinementt::arrays_overapproximated()
 
   unsigned nb_active=0;
 
-  std::list<lazy_constraintt>::iterator it=lazy_array_constraints.begin();
-  while(it!=lazy_array_constraints.end())
+  // Evaluate all lazy constraints while the solver is still in SAT state.
+  // We must not interleave get_value() calls with modifications to the
+  // main solver (prop) because some SAT solvers (e.g., CaDiCaL) only
+  // permit reading model values while in the satisfied state, and adding
+  // clauses invalidates that state.
+  struct evaluated_constraintt
   {
-    satcheck_no_simplifiert sat_check{log.get_message_handler()};
-    bv_pointerst solver{ns, sat_check, log.get_message_handler()};
-    solver.unbounded_array=bv_pointerst::unbounded_arrayt::U_ALL;
-
-    exprt current=(*it).lazy;
+    exprt constraint;
+    exprt simplified;
+    std::list<lazy_constraintt>::iterator list_it;
+  };
+  std::vector<evaluated_constraintt> to_check;
+  to_check.reserve(lazy_array_constraints.size());
+
+  for(auto it = lazy_array_constraints.begin();
+      it != lazy_array_constraints.end();
+      ++it)
+  {
+    const exprt &current = it->lazy;
 
     // some minor simplifications
     // check if they are worth having
@@ -57,7 +68,6 @@ void bv_refinementt::arrays_overapproximated()
       exprt implies_simplified = get_value(imp.op0());
       if(implies_simplified==false_exprt())
       {
-        ++it;
         continue;
       }
     }
@@ -71,23 +81,31 @@ void bv_refinementt::arrays_overapproximated()
       exprt o2 = get_value(orexp.op1());
       if(o1==true_exprt() || o2 == true_exprt())
       {
-        ++it;
         continue;
       }
     }
 
-    exprt simplified = get_value(current);
-    solver << simplified;
+    to_check.push_back({current, get_value(current), it});
+  }
+
+  // Now check each evaluated constraint using a local solver and activate
+  // violated ones. This phase may modify the main solver (prop).
+  for(auto &entry : to_check)
+  {
+    satcheck_no_simplifiert sat_check{log.get_message_handler()};
+    bv_pointerst solver{ns, sat_check, log.get_message_handler()};
+    solver.unbounded_array = bv_pointerst::unbounded_arrayt::U_ALL;
+
+    solver << entry.simplified;
 
     switch(static_cast<decision_proceduret::resultt>(sat_check.prop_solve()))
     {
     case decision_proceduret::resultt::D_SATISFIABLE:
-      ++it;
       break;
     case decision_proceduret::resultt::D_UNSATISFIABLE:
-      prop.l_set_to_true(convert(current));
+      prop.l_set_to_true(convert(entry.constraint));
       nb_active++;
-      lazy_array_constraints.erase(it++);
+      lazy_array_constraints.erase(entry.list_it);
       break;
     case decision_proceduret::resultt::D_ERROR:
       INVARIANT(false, "error in array over approximation check");