mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Fix literal duplication bug that was introduced after v4.3.1 release

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-17 13:42:01 -08:00
parent 7e66a65e98
commit 143b829488
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/asserted_formulas.cpp
View file

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