diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h
index b08d4d0ff..3f1d7cdb0 100644
--- a/src/math/simplex/simplex_def.h
+++ b/src/math/simplex/simplex_def.h
@@ -41,10 +41,10 @@ namespace simplex {
                 }
             }
         }
-        em.neg(value);
-        em.div(value, base_coeff, value);
         SASSERT(!m.is_zero(base_coeff));
         SASSERT(!is_base(base));
+        em.neg(value);
+        em.div(value, base_coeff, value);
         while (m_row2base.size() <= r.id()) {
             m_row2base.push_back(null_var);
         }
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 22f872978..c721224b0 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -190,6 +190,37 @@ namespace smt {
         return alloc(theory_pb, new_ctx->get_manager(), m_params); 
     }
 
+    class theory_pb::remove_var : public trail<context> {
+        theory_pb& pb;
+        unsigned   v;
+    public:
+        remove_var(theory_pb& pb, unsigned v): pb(pb), v(v) {}
+        virtual void undo(context& ctx) {
+            pb.m_vars.remove(v);
+            pb.m_simplex.unset_lower(v);
+            pb.m_simplex.unset_upper(v);
+        }        
+    };
+
+    class reset_bound : public trail<context> {
+        theory_pb& pb;
+        unsigned   v;
+        bool       is_lower;
+    public:
+        reset_bound(theory_pb& pb, unsigned v, bool is_lower):pb(pb), v(v), is_lower(is_lower) {}
+        virtual void undo(context& ctx) {
+        }
+    };
+
+    class undo_bound : public trail<context> {
+        theory_pb& pb;
+        unsigned   v;
+        bool       is_lower;
+    public:
+        undo_bound(theory_pb& pb, unsigned v, bool is_lower):pb(pb), v(v), is_lower(is_lower) {}
+        virtual void undo(context& ctx) {
+        }
+    };
 
     bool theory_pb::internalize_atom(app * atom, bool gate_ctx) {
         SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom) || 
@@ -243,7 +274,7 @@ namespace smt {
 
         literal lit(abv);
 
-        TRACE("pb", display(tout << mk_pp(atom, m), *c); tout << " := " << lit << "\n";);        
+        TRACE("pb", display(tout, *c); tout << " := " << lit << "\n";);        
         switch(is_true) {
         case l_false: 
             lit = ~lit;
@@ -317,7 +348,10 @@ namespace smt {
             if (m_ineq_rep.find(rep, abv2)) {
                 slack = abv2; 
                 r = m_ineq_row_info.find(abv2).m_row;
-                TRACE("pb", tout << "Found: " << abv << " |-> " << slack << " " << m_ineq_row_info.find(abv2).m_bound << " vs. " << k << "\n";);
+                TRACE("pb", 
+                      tout << "Old row: " << abv << " |-> " << slack << " ";
+                      tout << m_ineq_row_info.find(abv2).m_bound << " vs. " << k << "\n";
+                      display(tout, rep););
             }
             else {
                 m_ineq_rep.insert(rep, abv);
@@ -326,15 +360,23 @@ namespace smt {
                 scoped_mpz_vector coeffs(mgr);
                 for (unsigned i = 0; i < rep.size(); ++i) {
                     unsigned v = rep.lit(i).var();
-                    std::cout << v << "\n";
                     m_simplex.ensure_var(v);
                     vars.push_back(v);
+                    if (!m_vars.contains(v)) {
+                        mpq_inf zero(mpq(0),mpq(0)), one(mpq(1),mpq(0));
+                        m_simplex.set_lower(v, zero);
+                        m_simplex.set_upper(v, one);
+                        m_vars.insert(v);
+                        ctx.push_trail(remove_var(*this, v));                        
+                    }
                     coeffs.push_back(rep.coeff(i).to_mpq().numerator());
                 }
                 slack = abv;
-                m_simplex.ensure_var(abv);
-                r = m_simplex.add_row(vars.size(), slack, vars.c_ptr(), coeffs.c_ptr());
-                TRACE("pb", tout << "New row: " << abv << " " << k << "\n";);
+                m_simplex.ensure_var(slack);
+                vars.push_back(slack);
+                coeffs.push_back(mpz(-1));
+                r = m_simplex.add_row(slack, vars.size(), vars.c_ptr(), coeffs.c_ptr());
+                TRACE("pb", tout << "New row: " << abv << " " << k << "\n"; display(tout, rep););
             }
             m_ineq_row_info.insert(abv, row_info(slack, k, rep, r));
         }
@@ -550,6 +592,18 @@ namespace smt {
             else {
                 assign_eq(*c, is_true);
             }
+            if (m_enable_simplex) {
+                row_info const& info = m_ineq_row_info.find(v);
+                if (is_true) {
+                    // m_simplex.set_lower(info.m_slack, info.m_coeff);
+                    // ctx.push_trail(reset_lower(info.m_slack));
+                }
+                else {
+                    // m_simplex.set_upper(info.m_slack, info.m_coeff - 1);
+                    // ctx.push_trail(reset_upper(info.m_slack));
+                }
+                // m_simplex.feasiable();
+            }
         }
     }
 
@@ -1184,6 +1238,16 @@ namespace smt {
             clear_watch(*c);
             m_ineqs.remove(v);
             m_ineqs_trail.pop_back();
+            if (m_enable_simplex) {
+                row_info r_info;
+                VERIFY(m_ineq_row_info.find(v, r_info));
+                m_simplex.del_row(r_info.m_row);
+                m_ineq_row_info.erase(v);
+                bool_var v2 = m_ineq_rep.find(r_info.m_rep);
+                if (v == v2) {
+                    m_ineq_rep.erase(r_info.m_rep);
+                }
+            }
             dealloc(c);
         }
         m_ineqs_lim.resize(new_lim);
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index 5b1adbd25..a77561304 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -36,6 +36,9 @@ namespace smt {
         class  unwatch_ge;
         class  rewatch_vars;
         class  negate_ineq;
+        class  remove_var;
+        class  reset_bound;
+        class  undo_bound;
         typedef rational numeral;
         typedef vector<std::pair<literal, numeral> > arg_t;
         typedef simplex::simplex<simplex::mpz_ext> simplex;
@@ -159,14 +162,16 @@ namespace smt {
         };
 
         typedef ptr_vector<ineq> watch_list;
+        typedef map<ineq, bool_var, ineq::hash, ineq::eq> ineq_map;
 
         theory_pb_params         m_params;        
         u_map<watch_list*>       m_lwatch;      // per literal.
         u_map<watch_list*>       m_vwatch;      // per variable.
         u_map<ineq*>             m_ineqs;       // per inequality.
-        map<ineq, bool_var, ineq::hash, ineq::eq>      m_ineq_rep;       // Simplex: representative inequality
-        u_map<row_info>          m_ineq_row_info;  // Simplex: row information per variable.
-        simplex                  m_simplex;        // Simplex
+        ineq_map                 m_ineq_rep;       // Simplex: representative inequality
+        u_map<row_info>          m_ineq_row_info;  // Simplex: row information per variable
+        uint_set                 m_vars;           // Simplex: 0-1 variables.
+        simplex                  m_simplex;        // Simplex: tableau
         unsigned_vector          m_ineqs_trail;
         unsigned_vector          m_ineqs_lim;
         literal_vector           m_literals;    // temporary vector