From 5e9131042ac83d8983a9afd0393779e1b96b211d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Aug 2023 12:17:37 -0700 Subject: [PATCH] re-order when synth is invoked compared to q-solver Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_solver.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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;