From d2886a46b725f8641ab66b794759fb7fa255cc7d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 19 Mar 2020 10:07:28 -0700
Subject: [PATCH] fix #3402

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

diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index 4f58ea4e9..75ce78860 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -267,6 +267,10 @@ public:
             else {
                 ++kv.m_value; 
             }
+            if (m_bounds.has_lower(kv.m_key, val, strict)) {
+                SASSERT(!strict);
+                if (val.get_unsigned() > kv.m_value) kv.m_value = val.get_unsigned();
+            }
             unsigned p = next_power_of_two(kv.m_value);            
             if (p <= 1) p = 2;
             if (kv.m_value == p) p *= 2;