From 143b829488f83b8cf10a14aaceb61cf9f519273c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Dec 2012 13:42:01 -0800 Subject: [PATCH] Fix literal duplication bug that was introduced after v4.3.1 release Signed-off-by: Leonardo de Moura --- src/smt/asserted_formulas.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 5552050db..3155d9c58 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -439,6 +439,8 @@ void asserted_formulas::nnf_cnf() { expr_ref r1(m_manager); proof_ref pr1(m_manager); CASSERT("well_sorted",is_well_sorted(m_manager, n)); + push_todo.reset(); + push_todo_prs.reset(); apply_nnf(n, push_todo, push_todo_prs, r1, pr1); CASSERT("well_sorted",is_well_sorted(m_manager, r1)); pr = m_manager.mk_modus_ponens(pr, pr1); @@ -855,3 +857,8 @@ void asserted_formulas::max_bv_sharing() { } +#ifdef Z3DEBUG +void pp(asserted_formulas & f) { + f.display(std::cout); +} +#endif