diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h
index 2972e0086..9b3f670e8 100644
--- a/src/math/dd/pdd_interval.h
+++ b/src/math/dd/pdd_interval.h
@@ -25,27 +25,27 @@ typedef dep_intervals::interval interval;
 typedef dep_intervals::with_deps_t w_dep;
 // calculates the interval of a pdd expression based on the given intervals of the variables
 class pdd_interval {
-    dep_intervals m_dep_intervals;
-    std::function<interval (unsigned, bool)> m_var2interval;
+    dep_intervals& m_dep_intervals;
+    std::function<void (unsigned, bool, scoped_dep_interval&)> m_var2interval;
     
 public:
     
-    pdd_interval(reslimit& lim): m_dep_intervals(lim) {}
+    pdd_interval(dep_intervals& d): m_dep_intervals(d) {}
 
     dep_intervals& m() { return m_dep_intervals; }
 
-    std::function<interval (unsigned, bool)>& var2interval() { return m_var2interval; } // setter
-    const std::function<interval (unsigned, bool)>& var2interval() const { return m_var2interval; } // getter
+    std::function<void (unsigned, bool, scoped_dep_interval&)>& var2interval() { return m_var2interval; } // setter
+    const std::function<void (unsigned, bool, scoped_dep_interval&)>& var2interval() const { return m_var2interval; } // getter
 
     template <w_dep wd>
     void get_interval(pdd const& p, scoped_dep_interval& ret) {
         if (p.is_val()) {
-            m_dep_intervals.set_interval_for_scalar(ret.get(), p.val());
+            m_dep_intervals.set_interval_for_scalar(ret, p.val());
             return;
         }
         bool deps = wd == w_dep::with_deps;
-        interval a = m_var2interval(p.var(), deps);
-        scoped_dep_interval hi(m()), lo(m()), t(m());
+        scoped_dep_interval hi(m()), lo(m()), t(m()), a(m());
+        m_var2interval(p.var(), deps, a);
         get_interval<wd>(p.hi(), hi);
         get_interval<wd>(p.lo(), lo);
         if (deps) {
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index a38de126d..2b4fd38f6 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1485,24 +1485,24 @@ std::ostream& core::diagnose_pdd_miss(std::ostream& out) {
 }
 
 bool core::check_pdd_eq(const dd::solver::equation* e) {
-    dd::pdd_interval eval(m_reslim);
+    auto& di = m_intervals.get_dep_intervals();
+    dd::pdd_interval eval(di);
     eval.var2interval() =
-        [this](lpvar j, bool deps) {
-            intervals::interval a;
-            if (deps) m_intervals.set_var_interval<dd::w_dep::with_deps>(j, a);
-            else m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
-            return a;
-        };
-    scoped_dep_interval i(eval.m()), i_wd(eval.m());
+        [this](lpvar j, bool deps, scoped_dep_interval& a) {
+        if (deps) m_intervals.set_var_interval<dd::w_dep::with_deps>(j, a);
+        else m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
+    };
+    scoped_dep_interval i(di), i_wd(di);
     eval.get_interval<dd::w_dep::without_deps>(e->poly(), i);    
-    if (!eval.m().separated_from_zero(i))
+    if (!di.separated_from_zero(i))
         return false;
     eval.get_interval<dd::w_dep::with_deps>(e->poly(), i_wd);  
-    std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
-                                                         add_empty_lemma();
-                                                         current_expl().add(e);
-                                                     };
-    if (eval.m().check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) {
+    std::function<void (const lp::explanation&)> f = 
+        [this](const lp::explanation& e) {
+        add_empty_lemma();
+        current_expl().add(e);
+    };
+    if (di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) {
         lp_settings().stats().m_grobner_conflicts++;
         return true;
     }