diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp
index 75e982a85..36bedcc5e 100644
--- a/src/tactic/bv/elim_small_bv_tactic.cpp
+++ b/src/tactic/bv/elim_small_bv_tactic.cpp
@@ -247,7 +247,7 @@ public:
         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) {