mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix #6410

Browse source 
regression after introducing beta-redex optimization
This commit is contained in:
Nikolaj Bjorner 2022-10-18 12:34:45 -07:00
parent f0b85716a9
commit 464d52babe
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_array.cpp
View file

@ -380,9 +380,8 @@ namespace smt {
} }
else { else {
if (m_final_check_idx % 2 == 1) { if (m_final_check_idx % 2 == 1) {
if (assert_delayed_axioms() == FC_CONTINUE) r = assert_delayed_axioms();
r = FC_CONTINUE; if (r == FC_DONE)
else
r = mk_interface_eqs_at_final_check(); r = mk_interface_eqs_at_final_check();
} }
else { else {