diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index a5a31709b26..c6bd12f03a1 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1661,7 +1661,7 @@ class theory_lra::imp { } bool giveup = false; 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; switch (is_sat) { case l_true: @@ -1713,12 +1713,12 @@ class theory_lra::imp { switch (m_final_check_idx) { case 0: - st = check_lia(); - break; - case 1: if (assume_eqs()) st = FC_CONTINUE; break; + case 1: + st = check_lia(); + break; case 2: st = check_nla(); break;