From 0e1def5bd6950e7e967348335e04be5905e99626 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Oct 2020 01:54:42 -0700 Subject: [PATCH] fix #4736 --- src/tactic/arith/factor_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 18f11906b..c32063f4f 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -264,7 +264,7 @@ class factor_tactic : public tactic { expr_ref new_curr(m); proof_ref new_pr(m); unsigned size = g->size(); - for (unsigned idx = 0; idx < size; idx++) { + for (unsigned idx = 0; !g->inconsistent() && idx < size; idx++) { expr * curr = g->form(idx); m_rw(curr, new_curr, new_pr); if (produce_proofs) {