mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Fix array lambda final-check livelock (snapshot-regression iss-6364)

Browse source 
Reverting the registration of lambda enodes with the legacy array
solver (added in 63259d8a4) that caused a non-terminating final-check
livelock on nested-array benchmarks such as inputs/issues/iss-6364/small-5.smt2,
which regressed from 'sat' to a timeout.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-11 00:02:45 -07:00 • committed by GitHub
parent efe5e946f1
commit e83e8f695a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_internalizer.cpp
View file

@ -671,10 +671,9 @@ namespace smt {
SASSERT(is_lambda(q)); SASSERT(is_lambda(q));
if (e_internalized(q)) if (e_internalized(q))
return; return;
auto e = mk_enode(q, true, /* do suppress args */ mk_enode(q, true, /* do suppress args */
false, /* it is a term, so it should not be merged with true/false */ false, /* it is a term, so it should not be merged with true/false */
true); true);
apply_sort_cnstr(q, e);
} }
bool context::has_lambda() { bool context::has_lambda() {