diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 47aa7485b..b4a63a0f9 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1733,16 +1733,6 @@ public: final_check_status st = FC_DONE; switch (is_sat) { case l_true: - - if (delayed_assume_eqs()) { - ++m_stats.m_assume_eqs; - return FC_CONTINUE; - } - - if (assume_eqs()) { - ++m_stats.m_assume_eqs; - return FC_CONTINUE; - } TRACE("arith", display(tout);); switch (check_lia()) { @@ -1766,6 +1756,14 @@ public: st = FC_GIVEUP; break; } + if (assume_eqs()) { + ++m_stats.m_assume_eqs; + return FC_CONTINUE; + } + if (delayed_assume_eqs()) { + ++m_stats.m_assume_eqs; + return FC_CONTINUE; + } if (m_not_handled != nullptr) { TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";); st = FC_GIVEUP;