mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
testing bdd for elim-vars
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
dc6ed64da1
commit
553bf74f47
|
@ -1622,7 +1622,7 @@ namespace sat {
|
|||
}
|
||||
SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size()));
|
||||
//SASSERT(!missed_conflict());
|
||||
VERIFY(!missed_propagation());
|
||||
//VERIFY(!missed_propagation());
|
||||
TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n"););
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue