diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h
index bcc76c64f..f7125588e 100644
--- a/src/math/simplex/simplex.h
+++ b/src/math/simplex/simplex.h
@@ -97,6 +97,7 @@ namespace simplex {
         unsigned                    m_blands_rule_threshold;
         random_gen                  m_random;
         uint_set                    m_left_basis;
+        unsigned                    m_infeasible_var;
 
     public:
         simplex():
@@ -112,6 +113,7 @@ namespace simplex {
 
         void  ensure_var(var_t v);
         row   add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs);
+        row   get_infeasible_row();
         void  del_row(row const& r);
         void  set_lower(var_t var, eps_numeral const& b);
         void  set_upper(var_t var, eps_numeral const& b);
diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h
index 631b89ce7..b08d4d0ff 100644
--- a/src/math/simplex/simplex_def.h
+++ b/src/math/simplex/simplex_def.h
@@ -24,11 +24,6 @@ namespace simplex {
     template<typename Ext>
     typename simplex<Ext>::row 
     simplex<Ext>::add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs) {
-        DEBUG_CODE(
-            bool found = false;
-            for (unsigned i = 0; !found && i < num_vars; ++i) found = vars[i] == base;
-            SASSERT(found);
-            );
         scoped_numeral base_coeff(m);
         scoped_eps_numeral value(em), tmp(em);
         row r = M.mk_row();
@@ -49,7 +44,7 @@ namespace simplex {
         em.neg(value);
         em.div(value, base_coeff, value);
         SASSERT(!m.is_zero(base_coeff));
-        SASSERT(!m_vars[base].m_is_base);
+        SASSERT(!is_base(base));
         while (m_row2base.size() <= r.id()) {
             m_row2base.push_back(null_var);
         }
@@ -63,6 +58,14 @@ namespace simplex {
         return r;
     }
 
+    template<typename Ext>
+    typename simplex<Ext>::row 
+    simplex<Ext>::get_infeasible_row() {
+        SASSERT(is_base(m_infeasible_var));
+        unsigned row_id = m_vars[m_infeasible_var].m_base2row;
+        return row(row_id);
+    }
+
     template<typename Ext>
     void simplex<Ext>::add_patch(var_t v) {
         SASSERT(is_base(v));
@@ -140,10 +143,10 @@ namespace simplex {
             if (vi.m_upper_valid) out << em.to_string(vi.m_upper); else out << "oo";
             out << "] ";
             if (vi.m_is_base) out << "b:" << vi.m_base2row << " ";
-            col_iterator it = M.col_begin(i), end = M.col_end(i);
-            for (; it != end; ++it) {
-                out << "r" << it.get_row().id() << " ";
-            }
+            //col_iterator it = M.col_begin(i), end = M.col_end(i);
+            //for (; it != end; ++it) {
+            //    out << "r" << it.get_row().id() << " ";
+            //}
             out << "\n";
         }
     }
@@ -159,6 +162,7 @@ namespace simplex {
     template<typename Ext>
     lbool simplex<Ext>::make_feasible() {
         m_left_basis.reset();
+        m_infeasible_var = null_var;
         unsigned num_iterations = 0;
         unsigned num_repeated = 0;
         var_t v = null_var;
@@ -169,6 +173,7 @@ namespace simplex {
             }
             check_blands_rule(v, num_repeated);
             if (!make_var_feasible(v)) {
+                m_infeasible_var = v;
                 return l_false;
             }
             ++num_iterations;
@@ -529,6 +534,7 @@ namespace simplex {
 
             pivot(x_i, x_j, a_ij);
             move_to_bound(x_i, inc == m.is_pos(a_ij));            
+            SASSERT(well_formed_row(row(m_vars[x_j].m_base2row)));
         }
         return l_true;
     }
diff --git a/src/test/simplex.cpp b/src/test/simplex.cpp
index 986caa30b..37d4501f7 100644
--- a/src/test/simplex.cpp
+++ b/src/test/simplex.cpp
@@ -78,9 +78,6 @@ void add_row(Simplex& S, vector<R> const& _v, R const& _b, bool is_eq = false) {
     mpq_inf one(mpq(1),mpq(0));
     mpq_inf zero(mpq(0),mpq(0));
     SASSERT(vars.size() == coeffs.size());
-    std::cout << coeffs.size() << " " << nv << "\n";
-    for (unsigned i = 0; i < vars.size(); ++i) std::cout << vars[i] << " ";
-    std::cout << "\n";
     S.set_lower(nv, zero);
     if (is_eq) S.set_upper(nv, zero);
     S.set_lower(nv+1, one);
@@ -119,6 +116,16 @@ static void test3() {
     feas(S);
 }
 
+static void test4() {
+    Simplex S;
+    add_row(S, vec(1, 0), R(1));
+    add_row(S, vec(0, -1), R(-1));
+    add_row(S, vec(1, 1), R(1), true);
+    feas(S);
+}
+
+
+
 void tst_simplex() {
     Simplex S;
 
@@ -153,4 +160,5 @@ void tst_simplex() {
     test1();
     test2();
     test3();
+    test4();
 }