diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h
index 34571b897..ecc4da6c2 100644
--- a/src/math/polysat/fixplex.h
+++ b/src/math/polysat/fixplex.h
@@ -246,10 +246,8 @@ namespace polysat {
         unsigned get_num_vars() const { return m_vars.size(); }
         void reset();
 
-        svector<std::pair<unsigned, unsigned>> stack;
-        uint_set on_stack;
-        lbool propagate_ineqs(unsigned idx);
-        void propagate_eqs();
+
+        // void propagate_eqs();
         vector<var_eq> const& var_eqs() const { return m_var_eqs; }
 
         void add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs);
@@ -258,6 +256,10 @@ namespace polysat {
 
     private:
 
+        svector<std::pair<unsigned, unsigned>> stack;
+        uint_set on_stack;
+        lbool propagate_ineqs(unsigned idx);
+
         std::ostream& display_row(std::ostream& out, row const& r, bool values = true) const;
         var_t get_base_var(row const& r) const { return m_rows[r.id()].m_base; }
 
diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h
index 6eaf17b03..4eabd8b6f 100644
--- a/src/math/polysat/fixplex_def.h
+++ b/src/math/polysat/fixplex_def.h
@@ -1054,11 +1054,13 @@ namespace polysat {
      * 
      */
 
+#if 0
     template<typename Ext>
     void fixplex<Ext>::propagate_eqs() {
         for (unsigned i = 0; i < m_rows.size(); ++i) 
             get_offset_eqs(row(i));        
     }
+#endif
 
 
     template<typename Ext>
@@ -1105,7 +1107,7 @@ namespace polysat {
         numeral cz, cu;
         for (auto c : M.col_entries(x)) {
             auto r2 = c.get_row();
-            if (r1.id() >= r2.id())
+            if (r1.id() == r2.id())
                 continue;
             if (!is_offset_row(r2, cz, z, cu, u))
                 continue;
diff --git a/src/test/fixplex.cpp b/src/test/fixplex.cpp
index 79048553b..082601917 100644
--- a/src/test/fixplex.cpp
+++ b/src/test/fixplex.cpp
@@ -114,7 +114,7 @@ namespace polysat {
         fp.add_row(z, 3, ys2, coeffs2);
         fp.set_bounds(u, 1, 2, 1);
         fp.run();
-        fp.propagate_eqs();
+        // fp.propagate_eqs();
         for (auto e : fp.var_eqs())
             std::cout << e.x << " == " << e.y << "\n";