fix Z3Prover#4227

Author: NikolajBjorner

src/smt/old_interval.cpp

@@ -473,6 +473,14 @@ interval & interval::operator*=(interval const & other) {
     return *this;
 }
 
+bool interval::empty() const {
+    if (m_lower.is_infinite() || m_upper.is_infinite())
+        return false;
+    if (m_lower < m_upper)
+        return false;
+    return m_lower > m_upper || m_lower_open || m_upper_open;
+}
+
 bool interval::contains_zero() const {
     TRACE("interval_zero_bug", tout << "contains_zero info: " << *this << "\n";
           tout << "m_lower.is_neg(): " << m_lower.is_neg() << "\n";

src/smt/old_interval.h

@@ -102,6 +102,7 @@ class old_interval {
     bool operator==(old_interval const & other) const { return m_lower == other.m_lower && m_upper == other.m_upper && m_lower_open == other.m_lower_open && m_upper_open == other.m_upper_open; }
     bool contains_zero() const;
     bool contains(rational const& v) const;
+    bool empty() const;
     old_interval & inv();
     void expt(unsigned n);
     void neg();

src/smt/theory_arith_nl.h

@@ -226,23 +226,23 @@ interval theory_arith<Ext>::mk_interval_for(theory_var v) {
         }
         return interval(m_dep_manager,
                         l->get_value().get_rational().to_rational(),
-                        !l->get_value().get_infinitesimal().to_rational().is_zero(),
+                        l->get_value().get_infinitesimal().to_rational().is_pos(),
                         m_dep_manager.mk_leaf(l),
                         u->get_value().get_rational().to_rational(),
-                        !u->get_value().get_infinitesimal().to_rational().is_zero(),
+                        u->get_value().get_infinitesimal().to_rational().is_neg(),
                         m_dep_manager.mk_leaf(u));
     }
     else if (l) {
         return interval(m_dep_manager,
                         l->get_value().get_rational().to_rational(),
-                        !l->get_value().get_infinitesimal().to_rational().is_zero(),
+                        l->get_value().get_infinitesimal().to_rational().is_pos(),
                         true,
                         m_dep_manager.mk_leaf(l));
     }
     else if (u) {
         return interval(m_dep_manager,
                         u->get_value().get_rational().to_rational(),
-                        !u->get_value().get_infinitesimal().to_rational().is_zero(),
+                        u->get_value().get_infinitesimal().to_rational().is_neg(),
                         false,
                         m_dep_manager.mk_leaf(u));
     }