From b9dd18483c4fcf6d7bf62b923518c4f9c18ac846 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Mar 2020 14:11:36 -0700 Subject: [PATCH] fix #3571 Signed-off-by: Nikolaj Bjorner --- src/tactic/core/reduce_invertible_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index c3fd3b3b7..5467e3af6 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -76,7 +76,7 @@ public: } reduce_q_rw rw(*this); unsigned sz = g->size(); - for (unsigned idx = 0; idx < sz; idx++) { + for (unsigned idx = 0; !g->inconsistent() && idx < sz; idx++) { checkpoint(); expr* f = g->form(idx); expr_ref f_new(m); @@ -86,6 +86,7 @@ public: proof_ref new_pr(m); if (g->proofs_enabled()) { proof * pr = g->pr(idx); + new_pr = m.mk_rewrite(f, f_new); new_pr = m.mk_modus_ponens(pr, new_pr); } g->update(idx, f_new, new_pr, g->dep(idx));