mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
provide additional diagnostics for #5009
This commit is contained in:
parent
8ca2de41db
commit
8b5094fe73
|
@ -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) {
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue