From 180015a5290208cc3f761c5aad8452a65c581578 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Feb 2021 16:24:48 -0800 Subject: [PATCH] fix #5035 --- src/tactic/arith/lia2pb_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 93b387d0e..a94c0dab5 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -270,7 +270,7 @@ class lia2pb_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); expr_dependency * dep = nullptr; m_rw(curr, new_curr, new_pr);