mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

fix regressions #6703

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-04-27 08:43:59 -07:00
parent c48dc69050
commit d5231f8b33
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_lra.cpp
View file

@ -1661,7 +1661,7 @@ public:
} }
bool giveup = false; bool giveup = false;
final_check_status st = FC_DONE; final_check_status st = FC_DONE;
// m_final_check_idx = 0; // remove to experiment. m_final_check_idx = 0; // remove to experiment.
unsigned old_idx = m_final_check_idx; unsigned old_idx = m_final_check_idx;
switch (is_sat) { switch (is_sat) {
case l_true: case l_true:
@ -1713,12 +1713,12 @@ public:
switch (m_final_check_idx) { switch (m_final_check_idx) {
case 0: case 0:
st = check_lia();
break;
case 1:
if (assume_eqs()) if (assume_eqs())
st = FC_CONTINUE; st = FC_CONTINUE;
break; break;
case 1:
st = check_lia();
break;
case 2: case 2:
st = check_nla(); st = check_nla();
break; break;