mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
properly handle recursive function definitions #898
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e05cee757b
commit
723b507a88
|
@ -149,7 +149,6 @@ namespace sat {
|
|||
}
|
||||
|
||||
void simplifier::operator()(bool learned) {
|
||||
std::cout << s.rlimit().count() << "\n";
|
||||
if (s.inconsistent())
|
||||
return;
|
||||
if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
|
||||
|
|
Loading…
Reference in a new issue