From 1957b4d991a821aed70b32e1a71e7ea91e2e81ba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 Nov 2024 12:48:03 -0700 Subject: [PATCH] fix reporting on cancelation when based on cancel flag --- src/smt/smt_context.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 5bfcdfd9567..3b42f6ea6d5 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4077,7 +4077,11 @@ namespace smt { IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"" << th->get_name() << "\")\n";); ok = th->final_check_eh(); 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; m_incomplete_theories.push_back(th); }