diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index 597adc191..1e1b259fc 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -184,7 +184,7 @@ public:
 
         m_bounds(*g);
 
-        if (m_bounds.inconsistent()) {
+        if (m_bounds.inconsistent() || g->proofs_enabled()) {
             g->inc_depth();
             result.push_back(g.get());
             return;