diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h
index a43f06e18..a2c5450bf 100644
--- a/src/math/polysat/fixplex.h
+++ b/src/math/polysat/fixplex.h
@@ -26,13 +26,15 @@ Author:
 #include "util/rational.h"
 #include "util/lbool.h"
 #include "util/uint_set.h"
+#include "util/dependency.h"
+#include "util/ref.h"
 
 inline rational to_rational(uint64_t n) { return rational(n, rational::ui64()); }
 
 namespace polysat {
 
     typedef unsigned var_t;
-
+    
     struct fixplex_base {
         virtual ~fixplex_base() {}
         virtual lbool make_feasible() = 0;
@@ -93,12 +95,20 @@ namespace polysat {
             S_DEFAULT
         };
 
+#if 0
+        struct dep_config {
+            static const bool ref_count = true;
+            typedef unsigned value;
+        };
+        typedef dependency_manager<dep_config> dep_manager;
+#endif
+
         struct var_info : public mod_interval<numeral> {
-            unsigned    m_base2row:29;
-            unsigned    m_is_base:1;
-            numeral     m_value = 0;
-            unsigned    m_lo_dep = UINT_MAX;
-            unsigned    m_hi_dep = UINT_MAX;
+            unsigned      m_base2row:29;
+            unsigned      m_is_base:1;
+            numeral       m_value = 0;
+            u_dependency* m_lo_dep = nullptr;
+            u_dependency* m_hi_dep = nullptr;
             var_info():
                 m_base2row(0),
                 m_is_base(false)
@@ -164,6 +174,7 @@ namespace polysat {
         unsigned_vector             m_base_vars;
         stats                       m_stats;
         vector<stashed_bound>       m_stashed_bounds;
+        u_dependency_manager        m_deps;
         map<numeral, fix_entry, typename manager::hash, typename manager::eq> m_value2fixed_var;
 
         // inequalities
diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h
index 45d889079..e335bc204 100644
--- a/src/math/polysat/fixplex_def.h
+++ b/src/math/polysat/fixplex_def.h
@@ -490,9 +490,9 @@ namespace polysat {
         auto hi0 = m_vars[v].hi;
         m_vars[v] &= mod_interval(l, h);
         if (lo0 != m_vars[v].lo)
-            m_vars[v].m_lo_dep = dep;
+            m_vars[v].m_lo_dep = nullptr; // TODO set_atom(dep);
         if (hi0 != m_vars[v].hi)
-            m_vars[v].m_hi_dep = dep;
+            m_vars[v].m_hi_dep = nullptr; // TODO .set_atom(dep);
         if (in_bounds(v))
             return;
         if (is_base(v))
@@ -523,11 +523,15 @@ namespace polysat {
 
     template<typename Ext>
     void fixplex<Ext>::restore_bound() {
-        auto const& b = m_stashed_bounds.back();
+        auto& b = m_stashed_bounds.back();
+        auto* lo = m_vars[b.m_var].m_lo_dep;
+        auto* hi = m_vars[b.m_var].m_hi_dep;
         m_vars[b.m_var].lo = b.lo;
         m_vars[b.m_var].hi = b.hi;
         m_vars[b.m_var].m_lo_dep = b.m_lo_dep;
         m_vars[b.m_var].m_hi_dep = b.m_hi_dep;
+//        m_deps.dec_ref(lo);
+//        m_deps.dec_ref(hi);
         m_stashed_bounds.pop_back();
     }
 
@@ -799,15 +803,13 @@ namespace polysat {
         m_unsat_core.reset();
         SASSERT(is_base(v));
         auto row = base2row(v);
+        ptr_vector<u_dependency> todo;
         for (auto const& e : M.row_entries(row)) {
             var_t v = e.var();
-            auto lo = m_vars[v].m_lo_dep;
-            auto hi = m_vars[v].m_hi_dep;
-            if (lo != UINT_MAX)
-                m_unsat_core.push_back(lo);
-            if (hi != UINT_MAX)
-                m_unsat_core.push_back(hi);
+            todo.push_back(m_vars[v].m_lo_dep);
+            todo.push_back(m_vars[v].m_hi_dep);
         }
+        m_deps.linearize(todo, m_unsat_core);
     }
 
     /**