diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 66eff73d3..80c39bb52 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -21,13 +21,11 @@
 #include "math/lp/nla_core.h"
 #include "math/lp/factorization_factory_imp.h"
 namespace nla {
-nla_grobner::nla_grobner(core *c
-                         ) :
-    common(c),
-    m_nl_gb_exhausted(false),
-    m_dep_manager(m_val_manager, m_alloc),
-    m_changed_leading_term(false)
-{}
+nla_grobner::nla_grobner(core *c)
+    : common(c),
+      m_nl_gb_exhausted(false),
+      m_dep_manager(m_val_manager, m_alloc),
+      m_changed_leading_term(false) {}
 
 // Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed,
 // then assert bounds for x, and continue
@@ -301,7 +299,7 @@ bool nla_grobner::simplify_target_monomials_sum(equation * source,
         simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j);
     }
     target->exp() = m_nex_creator.simplify(targ_sum);
-    target->dep = m_dep_manager.mk_join(source->dep, target->dep);
+    target->dep() = m_dep_manager.mk_join(source->dep(), target->dep());
     TRACE("grobner", tout << "target = "; display_equation(tout, *target););
     return true;
 }
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 5b7c903bf..3f719dda9 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -113,24 +113,24 @@ bool intervals::check_interval_for_conflict_on_zero_upper(
     if (!separated_from_zero_on_upper(i))
         return false;
         
-     add_empty_lemma();
+     m_core->add_empty_lemma();
      svector<lp::constraint_index> expl;
      dep = m_dep_manager.mk_join(dep, i.m_upper_dep);
      m_dep_manager.linearize(dep, expl); 
-     _().current_expl().add_expl(expl);
-     TRACE("nla_solver", print_lemma(tout););
+     m_core->current_expl().add_expl(expl);
+     TRACE("nla_solver", m_core->print_lemma(tout););
      return true;
 }
 
 bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, ci_dependency* dep) {
     if (!separated_from_zero_on_lower(i))
         return false;
-     add_empty_lemma();
+     m_core->add_empty_lemma();
      svector<lp::constraint_index> expl;
      dep = m_dep_manager.mk_join(dep, i.m_lower_dep);
      m_dep_manager.linearize(dep, expl); 
-     _().current_expl().add_expl(expl);
-     TRACE("nla_solver", print_lemma(tout););
+     m_core->current_expl().add_expl(expl);
+     TRACE("nla_solver", m_core->print_lemma(tout););
      return true;
 }
 
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
index dc3c262df..79b35c1ea 100644
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -28,11 +28,13 @@
 namespace nla {
 class core;
 
-class intervals : common {
+class intervals {
+    typedef common::ci_dependency_manager ci_dependency_manager;
+    typedef ci_dependency_manager::dependency ci_dependency;
 
     class im_config {
         unsynch_mpq_manager&        m_manager;
-        ci_dependency_manager&       m_dep_manager;
+        common::ci_dependency_manager&       m_dep_manager;
 
     public:
         typedef unsynch_mpq_manager numeral_manager;
@@ -135,11 +137,12 @@ class intervals : common {
     };
 
     region                              m_alloc;
-    ci_value_manager                    m_val_manager;
+    common::ci_value_manager            m_val_manager;
     mutable unsynch_mpq_manager         m_num_manager;
     mutable ci_dependency_manager       m_dep_manager;
     im_config                           m_config;
     mutable interval_manager<im_config> m_imanager;
+    core *                              m_core;
 
 public:
     ci_dependency_manager&  dep_manager() { return m_dep_manager; }
@@ -151,11 +154,11 @@ private:
     const lp::lar_solver& ls() const;
 public:
     intervals(core* c, reslimit& lim) :
-        common(c),
         m_alloc(),
         m_dep_manager(m_val_manager, m_alloc),
         m_config(m_num_manager, m_dep_manager),
-        m_imanager(lim, im_config(m_num_manager, m_dep_manager))
+        m_imanager(lim, im_config(m_num_manager, m_dep_manager)),
+        m_core(c)
     {}
     ci_dependency* mk_join(ci_dependency* a, ci_dependency* b) { return m_dep_manager.mk_join(a, b);}
     ci_dependency* mk_leaf(lp::constraint_index ci) { return m_dep_manager.mk_leaf(ci);}