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);