From 8b5094fe73a8d645c3dfc0e102ac5fc6e1c496ac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 Feb 2021 10:14:38 -0800 Subject: [PATCH] provide additional diagnostics for #5009 --- src/sat/sat_solver/inc_sat_solver.cpp | 8 +++++--- src/solver/parallel_tactic.cpp | 4 ++++ 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 4e17ec4d8..003d630d8 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -215,9 +215,11 @@ public: r = m_solver.check(m_asms.size(), m_asms.c_ptr()); } catch (z3_exception& ex) { - IF_VERBOSE(10, verbose_stream() << "exception: " << ex.msg() << "\n";); - reason_set = true; - set_reason_unknown(std::string("(sat.giveup ") + ex.msg() + ')'); + IF_VERBOSE(1, verbose_stream() << "exception: " << ex.msg() << "\n";); + if (m.inc()) { + reason_set = true; + set_reason_unknown(std::string("(sat.giveup ") + ex.msg() + ')'); + } r = l_undef; } switch (r) { diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index ef2356678..c8b1c7d3f 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -288,11 +288,15 @@ class parallel_tactic : public tactic { } bool giveup() { + if (m_giveup) + return m_giveup; std::string r = get_solver().reason_unknown(); std::string inc("(incomplete"); m_giveup |= r.compare(0, inc.size(), inc) == 0; inc = "(sat.giveup"; m_giveup |= r.compare(0, inc.size(), inc) == 0; + if (m_giveup) + IF_VERBOSE(0, verbose_stream() << r << "\n"); return m_giveup; }