diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h
index 29fce95bc..5c7fdcf97 100644
--- a/src/math/polysat/fixplex.h
+++ b/src/math/polysat/fixplex.h
@@ -185,6 +185,7 @@ namespace polysat {
         unsigned get_num_vars() const { return m_vars.size(); }
         void  reset();
         void  propagate_bounds();
+        void  propagate_eqs();
         lbool make_feasible();
         row add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs);
         std::ostream& display(std::ostream& out) const;
diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h
index 51bc03093..354bab72c 100644
--- a/src/math/polysat/fixplex_def.h
+++ b/src/math/polysat/fixplex_def.h
@@ -811,6 +811,13 @@ namespace polysat {
      * 
      */
 
+    template<typename Ext>
+    void fixplex<Ext>::propagate_eqs() {
+        for (unsigned i = 0; i < m_rows.size(); ++i) 
+            get_offset_eqs(row(i));        
+    }
+
+
     template<typename Ext>
     void fixplex<Ext>::get_offset_eqs(row const& r) {
         var_t x, y;
@@ -855,7 +862,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;
@@ -863,8 +870,11 @@ namespace polysat {
                 std::swap(z, u);
                 std::swap(cz, cu);
             }
-            if (z == x && cx == cz && u != y && cu == cy && value(u) == value(y)) 
+            if (z == x && u != y && cx == cz && cu == cy && value(u) == value(y)) 
                 eq_eh(u, y, r1, r2);                
+            if (z == x && u != y && cx + cz == 0 && cu + cy == 0 && value(u) == value(y)) 
+                eq_eh(u, y, r1, r2);                
+
         }
     }
 
@@ -883,6 +893,7 @@ namespace polysat {
 
     template<typename Ext>
     void fixplex<Ext>::eq_eh(var_t x, var_t y, row const& r1, row const& r2) {
+        std::cout << "eq " << x << " == " << y << "\n";
         m_var_eqs.push_back(var_eq(x, y, r1, r2));
     }    
 
@@ -990,9 +1001,8 @@ namespace polysat {
     template<typename Ext>                                     
     bool fixplex<Ext>::well_formed_row(row const& r) const { 
         var_t s = m_rows[r.id()].m_base;
-        (void)s;
-        SASSERT(base2row(s) == r.id());
-        SASSERT(m_vars[s].m_is_base);
+        VERIFY(base2row(s) == r.id());
+        VERIFY(m_vars[s].m_is_base);
         numeral sum = 0;
         numeral base_coeff = m_rows[r.id()].m_base_coeff;
         for (auto const& e : M.row_entries(r)) {
@@ -1004,6 +1014,7 @@ namespace polysat {
             TRACE("polysat", display(tout << "non-well formed row\n"); M.display_row(tout << "row: ", r););
             throw default_exception("non-well formed row");
         }
+        SASSERT(sum == m_rows[r.id()].m_value + base_coeff * value(s));
         return true;
     }
 
diff --git a/src/test/fixplex.cpp b/src/test/fixplex.cpp
index 2b00973b3..d5da95071 100644
--- a/src/test/fixplex.cpp
+++ b/src/test/fixplex.cpp
@@ -97,6 +97,22 @@ namespace polysat {
         std::cout << fp << "\n";
     }
 
+    static void test_eq() {
+        scoped_fp fp;
+        var_t x = 0, y = 1, z = 2, u = 3;        
+        var_t ys1[3] = { x, y, u };
+        numeral m1 = 0ull - 1ull;
+        numeral coeffs1[3] = { 1, m1, m1 };        
+        var_t ys2[3] = { y, z, u };
+        numeral coeffs2[3] = { 1, m1, 1 };        
+        fp.add_row(x, 3, ys1, coeffs1);
+        fp.add_row(z, 3, ys2, coeffs2);
+        fp.set_bounds(u, 1, 2);
+        fp.run();
+        fp.propagate_eqs();
+
+    }
+
 
     static void test_interval() {
         interval<uint64_t> i1(1, 2);
@@ -119,8 +135,6 @@ namespace polysat {
         std::cout << 30 << " " << e.mul_inverse(30) << " " << 30*e.mul_inverse(30) << "\n";
         std::cout << 60 << " " << e.mul_inverse(60) << " " << 60*e.mul_inverse(60) << "\n";
         std::cout << 29 << " " << e.mul_inverse(29) << " " << 29*e.mul_inverse(29) << "\n";
-
-
     }
 }
 
@@ -133,4 +147,5 @@ void tst_fixplex() {
 
     polysat::test_interval();
     polysat::test_gcd();
+    polysat::test_eq();
 }