From 4f22e8c6989696d71ae6d4652fbb57eac8921386 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Apr 2020 11:57:07 -0700
Subject: [PATCH] fix #3663

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/arith/eq2bv_tactic.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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;