From f76c6424f204051de117e1053a019bf78e90b3ba Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 19 Apr 2020 12:58:42 -0700
Subject: [PATCH] another memory managment leak fix. Relates to different leak
 exposed by #3997

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/interval/dep_intervals.h | 4 +---
 src/math/lp/nla_intervals.cpp     | 7 ++++---
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h
index 9d0f69882..fa294c9ba 100644
--- a/src/math/interval/dep_intervals.h
+++ b/src/math/interval/dep_intervals.h
@@ -297,11 +297,9 @@ public:
 
     void del(interval& i) { m_imanager.del(i); }
     
-    template <enum with_deps_t wd> interval intersect(const interval& a, const interval& b) const {
-        interval i;
+    template <enum with_deps_t wd> void intersect(const interval& a, const interval& b, interval& i) const {
         update_lower_for_intersection<wd>(a, b, i);
         update_upper_for_intersection<wd>(a, b, i);
-        return i;
     }
 
     template <enum with_deps_t wd>
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 4d131b798..53917390b 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -375,7 +375,8 @@ bool intervals::interval_of_sum(const nex_sum& e, scoped_dep_interval& a, const
         SASSERT(e.is_sum() && e.size() > 1);
         scoped_dep_interval i_from_term(get_dep_intervals());
         if (interval_from_term<wd>(e, i_from_term)) {
-            interval r = m_dep_intervals.intersect<wd>(a, i_from_term);
+            scoped_dep_interval r(get_dep_intervals());
+            m_dep_intervals.intersect<wd>(a, i_from_term, r);
             TRACE("nla_intervals_details", tout << "intersection="; display(tout, r) << "\n";);
             
             if (m_dep_intervals.is_empty(r)) {
@@ -384,9 +385,9 @@ bool intervals::interval_of_sum(const nex_sum& e, scoped_dep_interval& a, const
                     T expl;
                     if (conflict_u_l(a, i_from_term)) {
                         get_dep_intervals().linearize(a.get().m_upper_dep, expl);
-                        get_dep_intervals().linearize(r.m_lower_dep, expl);                        
+                        get_dep_intervals().linearize(r.get().m_lower_dep, expl);                        
                     } else {
-                        get_dep_intervals().linearize(r.m_upper_dep, expl);
+                        get_dep_intervals().linearize(r.get().m_upper_dep, expl);
                         get_dep_intervals().linearize(a.get().m_lower_dep, expl);                        
                     }                        
                     f(expl);