mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
more useful diagnostics
This commit is contained in:
parent
968717a532
commit
9e306e3b6e
|
@ -371,7 +371,7 @@ namespace smt {
|
|||
case l_true:
|
||||
if (!m_proto_model->eval(n, res, false))
|
||||
return true;
|
||||
CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n";);
|
||||
CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n" << *m_proto_model << "\n";);
|
||||
if (m.is_false(res)) {
|
||||
return false;
|
||||
}
|
||||
|
@ -379,7 +379,7 @@ namespace smt {
|
|||
case l_false:
|
||||
if (!m_proto_model->eval(n, res, false))
|
||||
return true;
|
||||
CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n";);
|
||||
CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n" << *m_proto_model << "\n";);
|
||||
if (m.is_true(res)) {
|
||||
return false;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue