diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h
index 9b3f670e8..81153e4b5 100644
--- a/src/math/dd/pdd_interval.h
+++ b/src/math/dd/pdd_interval.h
@@ -63,7 +63,9 @@ public:
 	// f meant to be called when the separation happens
     template <typename T>
     bool separated_from_zero(pdd const& p, u_dependency*& dep, std::function<void (const T)>& f) {
-        return m_dep_intervals.check_interval_for_conflict_on_zero(get_interval<w_dep::with_deps>(p), dep, f);
+        scoped_dep_interval i(m());
+        get_interval<w_dep::with_deps>(p, i);
+        return m_dep_intervals.check_interval_for_conflict_on_zero(i, dep, f);
     }
 
 };
diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index 61a619169..a89201129 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -55,7 +55,7 @@ void emonics::pop(unsigned n) {
         lpvar last_var = UINT_MAX;
         for (lpvar v : m.vars()) {
             if (v != last_var) {
-                remove_cell(m_use_lists[v], i);
+                remove_cell(m_use_lists[v]);
                 last_var = v;
             }
         }
@@ -69,7 +69,7 @@ void emonics::pop(unsigned n) {
     m_u_f_stack.pop_scope(n);
 }
 
-void emonics::remove_cell(head_tail& v, unsigned mIndex) {
+void emonics::remove_cell(head_tail& v) {
     cell*& cur_head = v.m_head;
     cell*& cur_tail = v.m_tail;
     cell* old_head = cur_head->m_next;
diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h
index 260c29159..4931c90e6 100644
--- a/src/math/lp/emonics.h
+++ b/src/math/lp/emonics.h
@@ -97,7 +97,7 @@ class emonics {
 
     void inc_visited() const;
 
-    void remove_cell(head_tail& v, unsigned mIndex);
+    void remove_cell(head_tail& v);
     void insert_cell(head_tail& v, unsigned mIndex);
     void merge_cells(head_tail& root, head_tail& other);
     void unmerge_cells(head_tail& root, head_tail& other);
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 2b4fd38f6..13c402e08 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1487,8 +1487,7 @@ std::ostream& core::diagnose_pdd_miss(std::ostream& out) {
 bool core::check_pdd_eq(const dd::solver::equation* e) {
     auto& di = m_intervals.get_dep_intervals();
     dd::pdd_interval eval(di);
-    eval.var2interval() =
-        [this](lpvar j, bool deps, scoped_dep_interval& a) {
+    eval.var2interval() = [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);
     };
@@ -1497,8 +1496,7 @@ bool core::check_pdd_eq(const dd::solver::equation* e) {
     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) {
+    std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
         add_empty_lemma();
         current_expl().add(e);
     };