From 81ce57b5a84d8903d51b0a3b639da28d36448e15 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Jan 2023 15:38:13 -0800 Subject: [PATCH] #6429 --- src/sat/smt/euf_solver.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index e34a590f805..b56093eb0ff 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -574,7 +574,7 @@ namespace euf { return sat::check_result::CR_CONTINUE; if (cont) return sat::check_result::CR_CONTINUE; - if (m_qsolver) + if (m_qsolver && !m_config.m_arith_ignore_int) apply_solver(m_qsolver); if (num_nodes < m_egraph.num_nodes()) return sat::check_result::CR_CONTINUE; @@ -582,7 +582,9 @@ namespace euf { return sat::check_result::CR_CONTINUE; TRACE("after_search", s().display(tout);); if (give_up) - return sat::check_result::CR_GIVEUP; + return sat::check_result::CR_GIVEUP; + if (m_qsolver && m_config.m_arith_ignore_int) + return sat::check_result::CR_GIVEUP; return sat::check_result::CR_DONE; }