Fix array refinement crash with CaDiCaL SAT solver

[tautschnig]

Commit 6ff2ce4 ("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.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

Fixes a CaDiCaL crash during array refinement by avoiding get_value() model reads after mutating the main SAT solver state.

Changes:

• Splits lazy array constraint handling into two phases: (1) evaluate with get_value() in SAT state, (2) locally check and then activate violated constraints in the main solver.
• Introduces a small staging structure (evaluated_constraintt) to carry the simplified constraint and its originating list iterator across phases.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.01%. Comparing base (5059d48) to head (e43854d).
⚠️ Report is 13 commits behind head on develop.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8849   +/-   ##
========================================
  Coverage    80.01%   80.01%           
========================================
  Files         1700     1700           
  Lines       188316   188316           
  Branches        73       73           
========================================
  Hits        150677   150677           
  Misses       37639    37639           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[kroening]

Follow-up: I am considering to make the usual states (unknown, SAT, UNSAT) part of the decision_proceduret and propt APIs, first by documenting, and then possibly even enforce these by adding explicit checks.

[tautschnig]

Follow-up: I am considering to make the usual states (unknown, SAT, UNSAT) part of the decision_proceduret and propt APIs, first by documenting, and then possibly even enforce these by adding explicit checks.

See #8852 for a proposed implementation thereof.