mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

fix #3694

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-02 08:05:43 -07:00
parent 57d430b3fd
commit 8290cfadcc
2 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -194,12 +194,16 @@ public:
init_reason_unknown(); init_reason_unknown();
m_internalized_converted = false; m_internalized_converted = false;
bool reason_set = false;
try { try {
// IF_VERBOSE(0, m_solver.display(verbose_stream())); // IF_VERBOSE(0, m_solver.display(verbose_stream()));
r = m_solver.check(m_asms.size(), m_asms.c_ptr()); r = m_solver.check(m_asms.size(), m_asms.c_ptr());
} }
catch (z3_exception& ex) { catch (z3_exception& ex) {
IF_VERBOSE(10, verbose_stream() << "exception: " << ex.msg() << "\n";); IF_VERBOSE(10, verbose_stream() << "exception: " << ex.msg() << "\n";);
reason_set = true;
std::string msg = std::string("(sat.giveup ") + ex.msg() + std::string(")");
set_reason_unknown(msg.c_str());
r = l_undef; r = l_undef;
} }
switch (r) { switch (r) {
@ -215,7 +219,9 @@ public:
} }
break; break;
default: default:
set_reason_unknown(m_solver.get_reason_unknown()); if (!reason_set) {
set_reason_unknown(m_solver.get_reason_unknown());
}
break; break;
} }
return r; return r;
@ -604,6 +610,7 @@ private:
} }
catch (tactic_exception & ex) { catch (tactic_exception & ex) {
IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";); IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
set_reason_unknown(ex.msg());
TRACE("sat", tout << "exception: " << ex.msg() << "\n";); TRACE("sat", tout << "exception: " << ex.msg() << "\n";);
m_preprocess = nullptr; m_preprocess = nullptr;
m_bb_rewriter = nullptr; m_bb_rewriter = nullptr;

2
src/solver/parallel_tactic.cpp
View file

@ -271,6 +271,8 @@ class parallel_tactic : public tactic {
std::string r = get_solver().reason_unknown(); std::string r = get_solver().reason_unknown();
std::string inc("(incomplete"); std::string inc("(incomplete");
m_giveup |= r.compare(0, inc.size(), inc) == 0; m_giveup |= r.compare(0, inc.size(), inc) == 0;
inc = "(sat.giveup";
m_giveup |= r.compare(0, inc.size(), inc) == 0;
return m_giveup; return m_giveup;
} }