diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 020ace414..a03a7bae3 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -613,16 +613,16 @@ namespace euf { return sat::check_result::CR_CONTINUE; } - if (should_continue()) - return sat::check_result::CR_CONTINUE; - if (m_qsolver && !m_config.m_arith_ignore_int) - apply_solver(m_qsolver); if (should_continue()) return sat::check_result::CR_CONTINUE; if (m_synth_solver) apply_solver(m_synth_solver); if (should_continue()) return sat::check_result::CR_CONTINUE; + if (m_qsolver && !m_config.m_arith_ignore_int) + apply_solver(m_qsolver); + if (should_continue()) + return sat::check_result::CR_CONTINUE; TRACE("after_search", s().display(tout);); if (should_giveup()) return sat::check_result::CR_GIVEUP;