mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Fix bug reported at http://z3.codeplex.com/workitem/23

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-02-21 11:02:13 -08:00
parent 70192b66e9
commit 4922d62311
2 changed files with 17 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/tactic/goal.cpp
View file

@ -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) {