From e56a5787dc734d6122f25dccad4a96b1cfa65ac8 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 2 Mar 2020 19:47:17 -0800
Subject: [PATCH] remove a too strict debug check and fix a bug in intervals on
 terms

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_intervals.cpp | 17 +++++++++++++++--
 src/smt/theory_lra.cpp        | 19 +++++++++++--------
 2 files changed, 26 insertions(+), 10 deletions(-)

diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 488a402b8..15abac98b 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -77,7 +77,14 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
         return false;
     }
     auto interv_wd = interval_of_expr<e_with_deps::with_deps>(n, 1);
-    TRACE("grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) <<"expr = " << *n << "\n, initial deps\n"; print_dependencies(initial_deps, tout););
+    TRACE("grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) <<"expr = " << *n << "\n, initial deps\n"; print_dependencies(initial_deps, tout);
+          tout << ", expressions vars = \n";
+          for(lpvar j: m_core->get_vars_of_expr_with_opening_terms(n)) {
+              m_core->print_var(j, tout);
+          }
+          tout << "\n";
+          );
+    
     std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
                                                          m_core->add_empty_lemma();
                                                          m_core->current_expl().add(e);
@@ -268,6 +275,12 @@ bool intervals::interval_from_term(const nex& e, interval& i) {
     lp::explanation exp;
     if (m_core->explain_by_equiv(norm_t, exp)) {
         set_zero_interval(i);
+        if (wd == e_with_deps::with_deps) {
+            for (auto p : exp) {
+                i.m_lower_dep = mk_join(i.m_lower_dep, mk_leaf(p.second));
+            }
+            i.m_upper_dep = i.m_lower_dep;
+        }
         TRACE("nla_intervals", tout << "explain_by_equiv\n";);
         return true;
     }
@@ -275,7 +288,7 @@ bool intervals::interval_from_term(const nex& e, interval& i) {
     if (j + 1 == 0)
         return false;
 
-    set_var_interval<e_with_deps::without_deps>(j, i);
+    set_var_interval<wd>(j, i);
     interval bi;
     m_dep_intervals.mul<wd>(a, i, bi);
     m_dep_intervals.add(b, bi);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index f0f516bfa..2ad825505 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3333,14 +3333,17 @@ public:
                 c.neg();
                 ctx().mark_as_relevant(c);
             }
-            TRACE("arith", ctx().display_literals_verbose(tout, m_core) << "\n";);
-            DEBUG_CODE(
-                for (literal const& c : m_core) {
-                    if (ctx().get_assignment(c) == l_true) {
-                        TRACE("arith", ctx().display_literal_verbose(tout, c) << " is true\n";);
-                        SASSERT(false);
-                    }
-                });
+
+            // DEBUG_CODE(
+            //     for (literal const& c : m_core) {
+            //         if (ctx().get_assignment(c) == l_true) {
+            //             TRACE("arith", ctx().display_literal_verbose(tout, c) << " is true\n";);
+            //             SASSERT(false);
+            //         }
+            //     });   // TODO: this check seems to be too strict.
+            // The lemmas can come in batches
+            // and the same literal can appear in several lemmas in a batch: it becomes l_true
+            // in earlier processing, but it was not so when the lemma was produced
             ctx().mk_th_axiom(get_id(), m_core.size(), m_core.c_ptr());
         }
     }