mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fix #2158

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-26 15:13:47 -08:00
parent c4ee4ffae4
commit ea9e2f6642
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/qe/qe_lite.cpp
View file

@ -694,7 +694,8 @@ namespace eq {
if (m.proofs_enabled() && r != q) { if (m.proofs_enabled() && r != q) {
pr = m.mk_transitivity(pr, curr_pr); pr = m.mk_transitivity(pr, curr_pr);
} }
} while (q != r && is_quantifier(r)); }
while (q != r && is_quantifier(r));
m_new_exprs.reset(); m_new_exprs.reset();
} }
@ -2441,7 +2442,7 @@ class qe_lite_tactic : public tactic {
continue; continue;
new_f = f; new_f = f;
m_qe(new_f, new_pr); m_qe(new_f, new_pr);
if (produce_proofs) { if (new_pr) {
expr* fact = m.get_fact(new_pr); expr* fact = m.get_fact(new_pr);
if (to_app(fact)->get_arg(0) != to_app(fact)->get_arg(1)) { if (to_app(fact)->get_arg(0) != to_app(fact)->get_arg(1)) {
new_pr = m.mk_modus_ponens(g->pr(i), new_pr); new_pr = m.mk_modus_ponens(g->pr(i), new_pr);