mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
This commit is contained in:
parent
e0099150ca
commit
81ce57b5a8
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue