mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
38250fc304
commit
5ca8628e0d
|
@ -214,6 +214,14 @@ namespace euf {
|
|||
TRACE("euf", tout << "explain " << l << " <- " << r << " " << probing << "\n";);
|
||||
DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true););
|
||||
|
||||
#if 0
|
||||
if (r.size() == 5 && r[0] == literal(401, true) && r[1] == literal(259, false) && r[2] == literal(250, false) &&
|
||||
r[3] == literal(631, false) && r[4] == literal(639, false)) {
|
||||
TRACE("euf", s().display(tout););
|
||||
exit(0);
|
||||
}
|
||||
#endif
|
||||
|
||||
if (!probing)
|
||||
log_antecedents(l, r);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue