fix #3524

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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) {

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) {

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);

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);
     }