mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fix #3571

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-30 14:11:36 -07:00
parent d4aa850412
commit b9dd18483c
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/core/reduce_invertible_tactic.cpp
View file

@ -76,7 +76,7 @@ public:
} }
reduce_q_rw rw(*this); reduce_q_rw rw(*this);
unsigned sz = g->size(); unsigned sz = g->size();
for (unsigned idx = 0; idx < sz; idx++) { for (unsigned idx = 0; !g->inconsistent() && idx < sz; idx++) {
checkpoint(); checkpoint();
expr* f = g->form(idx); expr* f = g->form(idx);
expr_ref f_new(m); expr_ref f_new(m);
@ -86,6 +86,7 @@ public:
proof_ref new_pr(m); proof_ref new_pr(m);
if (g->proofs_enabled()) { if (g->proofs_enabled()) {
proof * pr = g->pr(idx); proof * pr = g->pr(idx);
new_pr = m.mk_rewrite(f, f_new);
new_pr = m.mk_modus_ponens(pr, new_pr); new_pr = m.mk_modus_ponens(pr, new_pr);
} }
g->update(idx, f_new, new_pr, g->dep(idx)); g->update(idx, f_new, new_pr, g->dep(idx));