From afce09efe4848f35d84106200db4859dbbb550fd Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 2 Apr 2020 12:10:31 -0700
Subject: [PATCH] assert that the sdi is infinite by default

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_intervals.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index e33ceabdd..82be4afef 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -305,8 +305,10 @@ bool intervals::interval_from_term(const nex& e, scoped_dep_interval& i) {
 
 template <e_with_deps wd>
 void intervals::interval_of_sum_no_term(const nex_sum& e, scoped_dep_interval & sdi) {
-    if (has_inf_interval(e))
+    if (has_inf_interval(e)) {
+        SASSERT(m_dep_intervals.lower_is_inf(sdi) && m_dep_intervals.upper_is_inf(sdi));
         return;
+    }
     
     interval_of_expr<wd>(e[0], 1, sdi);
     for (unsigned k = 1; k < e.size(); k++) {