mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

fix reporting on cancelation when based on cancel flag

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-11-02 12:48:03 -07:00
parent 604714ba40
commit 1957b4d991
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_context.cpp
View file

@ -4077,7 +4077,11 @@ namespace smt {
IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"" << th->get_name() << "\")\n";); IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"" << th->get_name() << "\")\n";);
ok = th->final_check_eh(); ok = th->final_check_eh();
TRACE("final_check_step", tout << "final check '" << th->get_name() << " ok: " << ok << " inconsistent " << inconsistent() << "\n";); TRACE("final_check_step", tout << "final check '" << th->get_name() << " ok: " << ok << " inconsistent " << inconsistent() << "\n";);
if (ok == FC_GIVEUP) { if (get_cancel_flag()) {
f = CANCELED;
ok = FC_GIVEUP;
}
else if (ok == FC_GIVEUP) {
f = THEORY; f = THEORY;
m_incomplete_theories.push_back(th); m_incomplete_theories.push_back(th);
} }