From 5da2169a0e925b438889a91ae9c432dbf4ab6b94 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 26 Mar 2020 10:38:13 -0700
Subject: [PATCH] fix #3524

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp            |  1 +
 src/tactic/arith/bound_manager.cpp | 17 +++++++++++++++++
 src/tactic/arith/bound_manager.h   |  2 ++
 src/tactic/arith/eq2bv_tactic.cpp  |  9 ++++++++-
 4 files changed, 28 insertions(+), 1 deletion(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 05dc63efa..4a151bb37 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -828,6 +828,7 @@ namespace opt {
         SASSERT(result.size() == 1);
         goal* r = result[0];
         m_model_converter = r->mc();
+        CTRACE("opt", r->mc(), r->mc()->display(tout););
         fmls.reset();
         expr_ref tmp(m);
         for (unsigned i = 0; i < r->size(); ++i) {
diff --git a/src/tactic/arith/bound_manager.cpp b/src/tactic/arith/bound_manager.cpp
index 7f662810b..abde88a19 100644
--- a/src/tactic/arith/bound_manager.cpp
+++ b/src/tactic/arith/bound_manager.cpp
@@ -259,6 +259,23 @@ void bound_manager::reset() {
     m_upper_deps.finalize();
 }
 
+bool bound_manager::inconsistent() const {
+    for (auto const& kv : m_lowers) {
+        limit const& lim1 = kv.m_value;
+        limit lim2;        
+        if (m_uppers.find(kv.m_key, lim2)) {
+            if (lim1.first > lim2.first) {
+                return true;
+            }
+            if (lim1.first == lim2.first &&
+                !lim1.second && lim2.second) {
+                return true;
+            }
+        }
+    }
+    return false;
+}
+
 void bound_manager::display(std::ostream & out) const {
     numeral n; bool strict;
     for (iterator it = begin(); it != end(); ++it) {
diff --git a/src/tactic/arith/bound_manager.h b/src/tactic/arith/bound_manager.h
index 5a22778d4..a1ff456ce 100644
--- a/src/tactic/arith/bound_manager.h
+++ b/src/tactic/arith/bound_manager.h
@@ -87,6 +87,8 @@ public:
             return d;
         return nullptr;
     }
+
+    bool inconsistent() const;
     
     bool has_lower(expr * c) const {
         return m_lowers.contains(c);
diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index bfb907e9f..597adc191 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -184,6 +184,12 @@ public:
 
         m_bounds(*g);
 
+        if (m_bounds.inconsistent()) {
+            g->inc_depth();
+            result.push_back(g.get());
+            return;
+        }
+        
         for (unsigned i = 0; i < g->size(); i++) {            
             collect_fd(g->form(i));
         }
@@ -194,7 +200,7 @@ public:
             return;
         }
 
-        for (unsigned i = 0; i < g->size(); i++) {            
+        for (unsigned i = 0; !g->inconsistent() && i < g->size(); i++) {            
             expr_ref   new_curr(m);
             proof_ref  new_pr(m);  
             func_decl_ref var(m);
@@ -319,6 +325,7 @@ public:
         return false;
     }
 
+
     bool is_bound(expr* f, func_decl_ref& var, unsigned& val) {
         return is_lower(f, var, val) || is_upper(f, var, val);
     }