From 4922d62311c3a2a7d3c455b5a6ebc38f808854c7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Feb 2013 11:02:13 -0800 Subject: [PATCH] Fix bug reported at http://z3.codeplex.com/workitem/23 Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 2 ++ src/tactic/goal.cpp | 20 +++++++++++++++----- 2 files changed, 17 insertions(+), 5 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 13957064e..7aaaf2f8d 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -61,6 +61,8 @@ Version 4.3.2 - Fixed bugs in the C++ API (Thanks to Andrey Kupriyanov). +- Fixed bug reported at http://z3.codeplex.com/workitem/23 (Thanks to Paul Jackson). + Version 4.3.1 ============= diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index c6dad42b2..03a13aba5 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -111,19 +111,29 @@ void goal::push_back(expr * f, proof * pr, expr_dependency * d) { if (m().is_true(f)) return; if (m().is_false(f)) { + // Make sure pr and d are not deleted by the m().del(...) statements. + proof_ref saved_pr(m()); + expr_dependency_ref saved_d(m()); + saved_pr = pr; + saved_d = d; m().del(m_forms); m().del(m_proofs); m().del(m_dependencies); m_inconsistent = true; + m().push_back(m_forms, m().mk_false()); + if (proofs_enabled()) + m().push_back(m_proofs, saved_pr); + if (unsat_core_enabled()) + m().push_back(m_dependencies, saved_d); } else { SASSERT(!m_inconsistent); + m().push_back(m_forms, f); + if (proofs_enabled()) + m().push_back(m_proofs, pr); + if (unsat_core_enabled()) + m().push_back(m_dependencies, d); } - m().push_back(m_forms, f); - if (proofs_enabled()) - m().push_back(m_proofs, pr); - if (unsat_core_enabled()) - m().push_back(m_dependencies, d); } void goal::quick_process(bool save_first, expr * & f, expr_dependency * d) {