Merge branch 'fcexplanations'

21 files changed, 948 insertions, 621 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 3c664d806..e6ef6fdc2 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -11,6 +11,7 @@ libarith_la_SOURCES = \
 	arithvar.h \
 	arithvar.cpp \
 	bound_counts.h \
+	bound_counts.cpp \
 	arith_rewriter.h \
 	arith_rewriter.cpp \
 	arith_static_learner.h \
diff --git a/src/theory/arith/bound_counts.cpp b/src/theory/arith/bound_counts.cpp
new file mode 100644
index 000000000..27e9a35dc
--- /dev/null
+++ b/src/theory/arith/bound_counts.cpp
@@ -0,0 +1,16 @@
+#include "theory/arith/bound_counts.h"
+#include "theory/arith/tableau.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const {
+  RowIndex ridx = d_tab->basicToRowIndex(basic);
+  Assert(d_bc->isKey(ridx));
+  return (*d_bc)[ridx];
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h
index 954cc056a..d82fff3eb 100644
--- a/src/theory/arith/bound_counts.h
+++ b/src/theory/arith/bound_counts.h
@@ -10,62 +10,92 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-/**
- * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j
- *
- * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)}
- * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)}
- */
 class BoundCounts {
 private:
-  uint32_t d_atLowerBounds;
-  uint32_t d_atUpperBounds;
+  uint32_t d_lowerBoundCount;
+  uint32_t d_upperBoundCount;
 
 public:
-  BoundCounts() : d_atLowerBounds(0), d_atUpperBounds(0) {}
+  BoundCounts() : d_lowerBoundCount(0), d_upperBoundCount(0) {}
   BoundCounts(uint32_t lbs, uint32_t ubs)
-  : d_atLowerBounds(lbs), d_atUpperBounds(ubs) {}
+  : d_lowerBoundCount(lbs), d_upperBoundCount(ubs) {}
 
   bool operator==(BoundCounts bc) const {
-    return d_atLowerBounds == bc.d_atLowerBounds
-      && d_atUpperBounds == bc.d_atUpperBounds;
+    return d_lowerBoundCount == bc.d_lowerBoundCount
+      && d_upperBoundCount == bc.d_upperBoundCount;
   }
   bool operator!=(BoundCounts bc) const {
-    return  d_atLowerBounds != bc.d_atLowerBounds
-      || d_atUpperBounds != bc.d_atUpperBounds;
+    return  d_lowerBoundCount != bc.d_lowerBoundCount
+      || d_upperBoundCount != bc.d_upperBoundCount;
   }
-  inline bool isZero() const{ return d_atLowerBounds == 0 && d_atUpperBounds == 0; }
-  inline uint32_t atLowerBounds() const{
-    return d_atLowerBounds;
+  /** This is not a total order! */
+  bool operator>=(BoundCounts bc) const {
+    return d_lowerBoundCount >= bc.d_lowerBoundCount &&
+      d_upperBoundCount >= bc.d_upperBoundCount;
   }
-  inline uint32_t atUpperBounds() const{
-    return d_atUpperBounds;
+
+  inline bool isZero() const{ return d_lowerBoundCount == 0 && d_upperBoundCount == 0; }
+  inline uint32_t lowerBoundCount() const{
+    return d_lowerBoundCount;
+  }
+  inline uint32_t upperBoundCount() const{
+    return d_upperBoundCount;
   }
 
   inline BoundCounts operator+(BoundCounts bc) const{
-    return BoundCounts(d_atLowerBounds + bc.d_atLowerBounds,
-                       d_atUpperBounds + bc.d_atUpperBounds);
+    return BoundCounts(d_lowerBoundCount + bc.d_lowerBoundCount,
+                       d_upperBoundCount + bc.d_upperBoundCount);
   }
 
   inline BoundCounts operator-(BoundCounts bc) const {
-    Assert(d_atLowerBounds >= bc.d_atLowerBounds);
-    Assert(d_atUpperBounds >= bc.d_atUpperBounds);
-    return BoundCounts(d_atLowerBounds - bc.d_atLowerBounds,
-                       d_atUpperBounds - bc.d_atUpperBounds);
+    Assert( *this >= bc );
+    return BoundCounts(d_lowerBoundCount - bc.d_lowerBoundCount,
+                       d_upperBoundCount - bc.d_upperBoundCount);
+  }
+
+
+  inline BoundCounts& operator+=(BoundCounts bc) {
+    d_upperBoundCount += bc.d_upperBoundCount;
+    d_lowerBoundCount += bc.d_lowerBoundCount;
+    return *this;
+  }
+
+  inline BoundCounts& operator-=(BoundCounts bc) {
+    Assert(d_lowerBoundCount >= bc.d_lowerBoundCount);
+    Assert(d_upperBoundCount >= bc.d_upperBoundCount);
+    d_upperBoundCount -= bc.d_upperBoundCount;
+    d_lowerBoundCount -= bc.d_lowerBoundCount;
+
+    return *this;
+  }
+
+  /** Based on the sign coefficient a variable is multiplied by,
+   * the effects the bound counts either has no effect (sgn == 0),
+   * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
+   */
+  inline BoundCounts multiplyBySgn(int sgn) const{
+    if(sgn > 0){
+      return *this;
+    }else if(sgn == 0){
+      return BoundCounts(0,0);
+    }else{
+      return BoundCounts(d_upperBoundCount, d_lowerBoundCount);
+    }
   }
 
   inline void addInChange(int sgn, BoundCounts before, BoundCounts after){
-    Assert(before != after);
-    if(sgn < 0){
-      Assert(d_atUpperBounds >= before.d_atLowerBounds);
-      Assert(d_atLowerBounds >= before.d_atUpperBounds);
-      d_atUpperBounds += after.d_atLowerBounds - before.d_atLowerBounds;
-      d_atLowerBounds += after.d_atUpperBounds - before.d_atUpperBounds;
+    if(before == after){
+      return;
+    }else if(sgn < 0){
+      Assert(d_upperBoundCount >= before.d_lowerBoundCount);
+      Assert(d_lowerBoundCount >= before.d_upperBoundCount);
+      d_upperBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
+      d_lowerBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
     }else if(sgn > 0){
-      Assert(d_atUpperBounds >= before.d_atUpperBounds);
-      Assert(d_atLowerBounds >= before.d_atLowerBounds);
-      d_atUpperBounds += after.d_atUpperBounds - before.d_atUpperBounds;
-      d_atLowerBounds += after.d_atLowerBounds - before.d_atLowerBounds;
+      Assert(d_upperBoundCount >= before.d_upperBoundCount);
+      Assert(d_lowerBoundCount >= before.d_lowerBoundCount);
+      d_upperBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
+      d_lowerBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
     }
   }
 
@@ -74,69 +104,129 @@ public:
     Assert(!bc.isZero());
 
     if(before < 0){
-      d_atUpperBounds -= bc.d_atLowerBounds;
-      d_atLowerBounds -= bc.d_atUpperBounds;
+      d_upperBoundCount -= bc.d_lowerBoundCount;
+      d_lowerBoundCount -= bc.d_upperBoundCount;
     }else if(before > 0){
-      d_atUpperBounds -= bc.d_atUpperBounds;
-      d_atLowerBounds -= bc.d_atLowerBounds;
+      d_upperBoundCount -= bc.d_upperBoundCount;
+      d_lowerBoundCount -= bc.d_lowerBoundCount;
     }
     if(after < 0){
-      d_atUpperBounds += bc.d_atLowerBounds;
-      d_atLowerBounds += bc.d_atUpperBounds;
+      d_upperBoundCount += bc.d_lowerBoundCount;
+      d_lowerBoundCount += bc.d_upperBoundCount;
     }else if(after > 0){
-      d_atUpperBounds += bc.d_atUpperBounds;
-      d_atLowerBounds += bc.d_atLowerBounds;
+      d_upperBoundCount += bc.d_upperBoundCount;
+      d_lowerBoundCount += bc.d_lowerBoundCount;
     }
   }
+};
 
-  inline BoundCounts& operator+=(BoundCounts bc) {
-    d_atUpperBounds += bc.d_atUpperBounds;
-    d_atLowerBounds += bc.d_atLowerBounds;
-    return *this;
+class BoundsInfo {
+private:
+
+  /**
+   * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j
+   *
+   * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)}
+   * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)}
+   */
+  BoundCounts d_atBounds;
+
+  /** This is for counting how many upper and lower bounds a row has. */
+  BoundCounts d_hasBounds;
+
+public:
+  BoundsInfo() : d_atBounds(), d_hasBounds() {}
+  BoundsInfo(BoundCounts atBounds, BoundCounts hasBounds)
+    : d_atBounds(atBounds), d_hasBounds(hasBounds) {}
+
+  BoundCounts atBounds() const { return d_atBounds; }
+  BoundCounts hasBounds() const { return d_hasBounds; }
+
+  /** This corresponds to adding in another variable to the row. */
+  inline BoundsInfo operator+(const BoundsInfo& bc) const{
+    return BoundsInfo(d_atBounds + bc.d_atBounds,
+                      d_hasBounds + bc.d_hasBounds);
+  }
+  /** This corresponds to removing a variable from the row. */
+  inline BoundsInfo operator-(const BoundsInfo& bc) const {
+    Assert(*this >= bc);
+    return BoundsInfo(d_atBounds - bc.d_atBounds,
+                      d_hasBounds - bc.d_hasBounds);
   }
 
-  inline BoundCounts& operator-=(BoundCounts bc) {
-    Assert(d_atLowerBounds >= bc.d_atLowerBounds);
-    Assert(d_atUpperBounds >= bc.d_atUpperBounds);
-    d_atUpperBounds -= bc.d_atUpperBounds;
-    d_atLowerBounds -= bc.d_atLowerBounds;
+  inline BoundsInfo& operator+=(const BoundsInfo& bc) {
+    d_atBounds += bc.d_atBounds;
+    d_hasBounds += bc.d_hasBounds;
+    return (*this);
+  }
 
-    return *this;
+  /** Based on the sign coefficient a variable is multiplied by,
+   * the effects the bound counts either has no effect (sgn == 0),
+   * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
+   */
+  inline BoundsInfo multiplyBySgn(int sgn) const{
+    return BoundsInfo(d_atBounds.multiplyBySgn(sgn), d_hasBounds.multiplyBySgn(sgn));
   }
 
-  inline BoundCounts multiplyBySgn(int sgn) const{
-    if(sgn > 0){
-      return *this;
-    }else if(sgn == 0){
-      return BoundCounts(0,0);
-    }else{
-      return BoundCounts(d_atUpperBounds, d_atLowerBounds);
-    }
+  bool operator==(const BoundsInfo& other) const{
+    return d_atBounds == other.d_atBounds && d_hasBounds == other.d_hasBounds;
+  }
+  bool operator!=(const BoundsInfo& other) const{
+    return !(*this == other);
+  }
+  /** This is not a total order! */
+  bool operator>=(const BoundsInfo& other) const{
+    return d_atBounds >= other.d_atBounds && d_hasBounds >= other.d_hasBounds;
+  }
+  void addInChange(int sgn, const BoundsInfo& before, const BoundsInfo& after){
+    addInAtBoundChange(sgn, before.d_atBounds, after.d_atBounds);
+    addInHasBoundChange(sgn, before.d_hasBounds, after.d_hasBounds);
+  }
+  void addInAtBoundChange(int sgn, BoundCounts before, BoundCounts after){
+    d_atBounds.addInChange(sgn, before, after);
+  }
+  void addInHasBoundChange(int sgn, BoundCounts before, BoundCounts after){
+    d_hasBounds.addInChange(sgn, before, after);
+  }
+
+  inline void addInSgn(const BoundsInfo& bc, int before, int after){
+    if(!bc.d_atBounds.isZero()){ d_atBounds.addInSgn(bc.d_atBounds, before, after);}
+    if(!bc.d_hasBounds.isZero()){ d_hasBounds.addInSgn(bc.d_hasBounds, before, after);}
   }
 };
 
-typedef DenseMap<BoundCounts> BoundCountingVector;
+/** This is intended to map each row to its relevant bound information. */
+typedef DenseMap<BoundsInfo> BoundInfoMap;
+
+class Tableau;
 
 class BoundCountingLookup {
 private:
-  BoundCountingVector* d_bc;
+  BoundInfoMap* d_bc;
+  Tableau* d_tab;
 public:
-  BoundCountingLookup(BoundCountingVector* bc) : d_bc(bc) {}
-  BoundCounts boundCounts(ArithVar v) const {
-    Assert(d_bc->isKey(v));
-    return (*d_bc)[v];
+  BoundCountingLookup(BoundInfoMap* bc, Tableau* tab) : d_bc(bc), d_tab(tab) {}
+  const BoundsInfo& boundsInfo(ArithVar basic) const;
+  BoundCounts atBounds(ArithVar basic) const{
+    return boundsInfo(basic).atBounds();
+  }
+  BoundCounts hasBounds(ArithVar basic) const {
+    return boundsInfo(basic).hasBounds();
   }
 };
 
 inline std::ostream& operator<<(std::ostream& os, const BoundCounts& bc){
-  os << "[bc " << bc.atLowerBounds() << ", "
-     << bc.atUpperBounds() << "]";
+  os << "[bc " << bc.lowerBoundCount() << ", " << bc.upperBoundCount() << "]";
   return os;
 }
 
-class BoundCountsCallback {
+inline std::ostream& operator<<(std::ostream& os, const BoundsInfo& inf){
+  os << "[bi : @ " << inf.atBounds() << ", " << inf.hasBounds() << "]";
+  return os;
+}
+class BoundUpdateCallback {
 public:
-  virtual void operator()(ArithVar v, BoundCounts bc) = 0;
+  virtual void operator()(ArithVar v, const BoundsInfo&  up) = 0;
 };
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index e26687bf1..78b9d3494 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -922,6 +922,28 @@ bool ConstraintValue::proofIsEmpty() const{
   return result;
 }
 
+Node ConstraintValue::makeImplication(const std::vector<Constraint>& b) const{
+  Node antecedent = makeConjunction(b);
+  Node implied = getLiteral();
+  return antecedent.impNode(implied);
+}
+
+
+Node ConstraintValue::makeConjunction(const std::vector<Constraint>& b){
+  NodeBuilder<> nb(kind::AND);
+  for(vector<Constraint>::const_iterator i = b.begin(), end = b.end(); i != end; ++i){
+    Constraint b_i = *i;
+    b_i->explainBefore(nb, AssertionOrderSentinel);
+  }
+  if(nb.getNumChildren() >= 2){
+    return nb;
+  }else if(nb.getNumChildren() == 1){
+    return nb[0];
+  }else{
+    return mkBoolNode(true);
+  }
+}
+
 void ConstraintValue::explainBefore(NodeBuilder<>& nb, AssertionOrder order) const{
   Assert(hasProof());
   Assert(!isSelfExplaining() || assertedToTheTheory());
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index a5d64a652..4966115d2 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -598,6 +598,8 @@ public:
   void impliedBy(Constraint a, Constraint b);
   void impliedBy(const std::vector<Constraint>& b);
 
+  Node makeImplication(const std::vector<Constraint>& b) const;
+  static Node makeConjunction(const std::vector<Constraint>& b);
 
   /** The node must have a proof already and be eligible for propagation! */
   void propagate();
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 91d7e49ea..27ac6ccd2 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -377,8 +377,8 @@ public:
 
   uint32_t sumMetric(ArithVar a) const{
     Assert(inError(a));
-    BoundCounts bcs = d_boundLookup.boundCounts(a);
-    uint32_t count = getSgn(a) > 0 ? bcs.atUpperBounds() : bcs.atLowerBounds();
+    BoundCounts bcs = d_boundLookup.atBounds(a);
+    uint32_t count = getSgn(a) > 0 ? bcs.upperBoundCount() : bcs.lowerBoundCount();
 
     uint32_t length = d_tableauSizes.getRowLength(a);
 
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index ac4625ba3..d264be978 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -289,7 +289,7 @@ UpdateInfo FCSimplexDecisionProcedure::selectPrimalUpdate(ArithVar basic, Linear
   Debug("arith::selectPrimalUpdate")
     << "selectPrimalUpdate " << instance << endl
     << basic << " " << d_tableau.basicRowLength(basic)
-    << " " << d_linEq._countBounds(basic) << endl;
+    << " " << d_linEq.debugBasicAtBoundCount(basic) << endl;
 
   static const int s_maxCandidatesAfterImprove = 3;
   bool isFocus = basic == d_focusErrorVar;
@@ -505,7 +505,7 @@ void FCSimplexDecisionProcedure::debugPrintSignal(ArithVar updated) const{
   int dir = !d_variables.assignmentIsConsistent(updated) ?
     d_errorSet.getSgn(updated) : 0;
   Debug("updateAndSignal") << " dir " << dir;
-  Debug("updateAndSignal") << " _countBounds " << d_linEq._countBounds(updated) << endl;
+  Debug("updateAndSignal") << " debugBasicAtBoundCount " << d_linEq.debugBasicAtBoundCount(updated) << endl;
 }
 
 bool debugUpdatedBasic(const UpdateInfo& selected, ArithVar updated){
@@ -530,7 +530,7 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit
       ArithVar leaving = selected.leaving();
       ss << "leaving " << leaving
          << " " << d_tableau.basicRowLength(leaving)
-         << " " << d_linEq._countBounds(leaving)
+         << " " << d_linEq.debugBasicAtBoundCount(leaving)
          << endl;
     }
     if(degenerate(w) && selected.describesPivot()){
@@ -539,7 +539,7 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit
         << "degenerate " << leaving
         << ", atBounds " << d_linEq.basicsAtBounds(selected)
         << ", len " << d_tableau.basicRowLength(leaving)
-        << ", bc " << d_linEq._countBounds(leaving)
+        << ", bc " << d_linEq.debugBasicAtBoundCount(leaving)
         << endl;
     }
   }
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 42d8b41f8..bde771102 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -31,12 +31,6 @@ template void LinearEqualityModule::propagateNonbasics<false>(ArithVar basic, Co
 template ArithVar LinearEqualityModule::selectSlack<true>(ArithVar x_i, VarPreferenceFunction pf) const;
 template ArithVar LinearEqualityModule::selectSlack<false>(ArithVar x_i, VarPreferenceFunction pf) const;
 
-// template bool LinearEqualityModule::preferNonDegenerate<true>(const UpdateInfo& a, const UpdateInfo& b) const;
-// template bool LinearEqualityModule::preferNonDegenerate<false>(const UpdateInfo& a, const UpdateInfo& b) const;
-
-// template bool LinearEqualityModule::preferErrorsFixed<true>(const UpdateInfo& a, const UpdateInfo& b) const;
-// template bool LinearEqualityModule::preferErrorsFixed<false>(const UpdateInfo& a, const UpdateInfo& b) const;
-
 template bool LinearEqualityModule::preferWitness<true>(const UpdateInfo& a, const UpdateInfo& b) const;
 template bool LinearEqualityModule::preferWitness<false>(const UpdateInfo& a, const UpdateInfo& b) const;
 
@@ -57,14 +51,14 @@ void Border::output(std::ostream& out) const{
       << "}";
 }
 
-LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundCountingVector& boundTracking, BasicVarModelUpdateCallBack f):
+LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundInfoMap& boundsTracking, BasicVarModelUpdateCallBack f):
   d_variables(vars),
   d_tableau(t),
   d_basicVariableUpdates(f),
   d_increasing(1),
   d_decreasing(-1),
   d_relevantErrorBuffer(),
-  d_boundTracking(boundTracking),
+  d_btracking(boundsTracking),
   d_areTracking(false),
   d_trackCallback(this)
 {}
@@ -103,31 +97,24 @@ LinearEqualityModule::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_weakenings);
   StatisticsRegistry::unregisterStat(&d_weakenTime);
 }
-void LinearEqualityModule::includeBoundCountChange(ArithVar nb, BoundCounts prev){
-  if(d_tableau.isBasic(nb)){
-    return;
-  }
-  Assert(!d_tableau.isBasic(nb));
+void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev){
   Assert(!d_areTracking);
 
-  BoundCounts curr = d_variables.boundCounts(nb);
+  BoundsInfo curr = d_variables.boundsInfo(v);
 
   Assert(prev != curr);
-  Tableau::ColIterator basicIter = d_tableau.colIterator(nb);
+  Tableau::ColIterator basicIter = d_tableau.colIterator(v);
   for(; !basicIter.atEnd(); ++basicIter){
     const Tableau::Entry& entry = *basicIter;
-    Assert(entry.getColVar() == nb);
+    Assert(entry.getColVar() == v);
     int a_ijSgn = entry.getCoefficient().sgn();
 
-    ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex());
-
-    BoundCounts& counts = d_boundTracking.get(basic);
-    Debug("includeBoundCountChange") << basic << " " << counts << " to " ;
-    counts -= prev.multiplyBySgn(a_ijSgn);
-    counts += curr.multiplyBySgn(a_ijSgn);
-    Debug("includeBoundCountChange") << counts << " " << a_ijSgn << std::endl;
+    RowIndex ridx = entry.getRowIndex();
+    BoundsInfo& counts = d_btracking.get(ridx);
+    Debug("includeBoundUpdate") << d_tableau.rowIndexToBasic(ridx) << " " << counts << " to " ;
+    counts.addInChange(a_ijSgn, prev, curr);
+    Debug("includeBoundUpdate") << counts << " " << a_ijSgn << std::endl;
   }
-  d_boundTracking.set(nb, curr);
 }
 
 void LinearEqualityModule::updateMany(const DenseMap<DeltaRational>& many){
@@ -231,9 +218,9 @@ void LinearEqualityModule::updateTracked(ArithVar x_i, const DeltaRational& v){
                  << d_variables.getAssignment(x_i) << "|-> " << v << endl;
 
 
-  BoundCounts before = d_variables.boundCounts(x_i);
+  BoundCounts before = d_variables.atBoundCounts(x_i);
   d_variables.setAssignment(x_i, v);
-  BoundCounts after = d_variables.boundCounts(x_i);
+  BoundCounts after = d_variables.atBoundCounts(x_i);
 
   bool anyChange = before != after;
 
@@ -242,17 +229,24 @@ void LinearEqualityModule::updateTracked(ArithVar x_i, const DeltaRational& v){
     const Tableau::Entry& entry = *colIter;
     Assert(entry.getColVar() == x_i);
 
-    ArithVar x_j = d_tableau.rowIndexToBasic(entry.getRowIndex());
+    RowIndex ridx = entry.getRowIndex();
+    ArithVar x_j = d_tableau.rowIndexToBasic(ridx);
     const Rational& a_ji = entry.getCoefficient();
 
     const DeltaRational& assignment = d_variables.getAssignment(x_j);
     DeltaRational  nAssignment = assignment+(diff * a_ji);
     Debug("update") << x_j << " " << a_ji << assignment << " -> " << nAssignment << endl;
+    BoundCounts xjBefore = d_variables.atBoundCounts(x_j);
     d_variables.setAssignment(x_j, nAssignment);
+    BoundCounts xjAfter = d_variables.atBoundCounts(x_j);
 
-    if(anyChange && basicIsTracked(x_j)){
-      BoundCounts& next_bc_k = d_boundTracking.get(x_j);
-      next_bc_k.addInChange(a_ji.sgn(), before, after);
+    Assert(rowIndexIsTracked(ridx));
+    BoundsInfo& next_bc_k = d_btracking.get(ridx);
+    if(anyChange){
+      next_bc_k.addInAtBoundChange(a_ji.sgn(), before, after);
+    }
+    if(xjBefore != xjAfter){
+      next_bc_k.addInAtBoundChange(-1, xjBefore, xjAfter);
     }
 
     d_basicVariableUpdates(x_j);
@@ -332,7 +326,7 @@ void LinearEqualityModule::debugCheckTracking(){
       ArithVar var = entry.getColVar();
       const Rational& coeff = entry.getCoefficient();
       DeltaRational beta = d_variables.getAssignment(var);
-      Debug("arith::tracking") << var << " " << d_variables.boundCounts(var)
+      Debug("arith::tracking") << var << " " << d_variables.boundsInfo(var)
                                << " " << beta << coeff;
       if(d_variables.hasLowerBound(var)){
         Debug("arith::tracking") << "(lb " << d_variables.getLowerBound(var) << ")";
@@ -345,11 +339,12 @@ void LinearEqualityModule::debugCheckTracking(){
     Debug("arith::tracking") << "end row"<< endl;
 
     if(basicIsTracked(basic)){
-      BoundCounts computed = computeBoundCounts(basic);
+      RowIndex ridx = d_tableau.basicToRowIndex(basic);
+      BoundsInfo computed = computeRowBoundInfo(ridx, false);
       Debug("arith::tracking")
         << "computed " << computed
-        << " tracking " << d_boundTracking[basic] << endl;
-      Assert(computed == d_boundTracking[basic]);
+        << " tracking " << d_btracking[ridx] << endl;
+      Assert(computed == d_btracking[ridx]);
 
     }
   }
@@ -426,19 +421,42 @@ bool LinearEqualityModule::debugEntireLinEqIsConsistent(const string& s){
   return result;
 }
 
-DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){
+// DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){
+//   DeltaRational sum(0,0);
+//   for(Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd(); ++i){
+//     const Tableau::Entry& entry = (*i);
+//     ArithVar nonbasic = entry.getColVar();
+//     if(nonbasic == basic) continue;
+//     const Rational& coeff =  entry.getCoefficient();
+//     int sgn = coeff.sgn();
+//     bool ub = upperBound ? (sgn > 0) : (sgn < 0);
+
+//     const DeltaRational& bound = ub ?
+//       d_variables.getUpperBound(nonbasic):
+//       d_variables.getLowerBound(nonbasic);
+
+//     DeltaRational diff = bound * coeff;
+//     sum = sum + diff;
+//   }
+//   return sum;
+// }
+DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound) const {
+  RowIndex rid = d_tableau.basicToRowIndex(basic);
+  return computeRowBound(rid, upperBound, basic);
+}
+DeltaRational LinearEqualityModule::computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const {
   DeltaRational sum(0,0);
-  for(Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd(); ++i){
+  for(Tableau::RowIterator i = d_tableau.ridRowIterator(ridx); !i.atEnd(); ++i){
     const Tableau::Entry& entry = (*i);
-    ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == basic) continue;
+    ArithVar v = entry.getColVar();
+    if(v == skip){ continue; }
+
     const Rational& coeff =  entry.getCoefficient();
-    int sgn = coeff.sgn();
-    bool ub = upperBound ? (sgn > 0) : (sgn < 0);
+    bool vUb = (rowUb == (coeff.sgn() > 0));
 
-    const DeltaRational& bound = ub ?
-      d_variables.getUpperBound(nonbasic):
-      d_variables.getLowerBound(nonbasic);
+    const DeltaRational& bound = vUb ?
+      d_variables.getUpperBound(v):
+      d_variables.getLowerBound(v);
 
     DeltaRational diff = bound * coeff;
     sum = sum + diff;
@@ -449,7 +467,7 @@ DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound
 /**
  * Computes the value of a basic variable using the current assignment.
  */
-DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){
+DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe) const{
   Assert(d_tableau.isBasic(x));
   DeltaRational sum(0);
 
@@ -465,28 +483,54 @@ DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){
   return sum;
 }
 
+// bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){
+//   for(Tableau::RowIterator iter = d_tableau.basicRowIterator(basic); !iter.atEnd(); ++iter){
+//     const Tableau::Entry& entry = *iter;
+
+//     ArithVar var = entry.getColVar();
+//     if(var == basic) continue;
+//     int sgn = entry.getCoefficient().sgn();
+//     if(upperBound){
+//       if( (sgn < 0 && !d_variables.hasLowerBound(var)) ||
+//           (sgn > 0 && !d_variables.hasUpperBound(var))){
+//         return false;
+//       }
+//     }else{
+//       if( (sgn < 0 && !d_variables.hasUpperBound(var)) ||
+//           (sgn > 0 && !d_variables.hasLowerBound(var))){
+//         return false;
+//       }
+//     }
+//   }
+//   return true;
+// }
+
 bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){
-  for(Tableau::RowIterator iter = d_tableau.basicRowIterator(basic); !iter.atEnd(); ++iter){
+  RowIndex ridx = d_tableau.basicToRowIndex(basic);
+  return rowLacksBound(ridx, upperBound, basic) == NULL;
+}
+
+const Tableau::Entry* LinearEqualityModule::rowLacksBound(RowIndex ridx, bool rowUb, ArithVar skip){
+  Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
+  for(; !iter.atEnd(); ++iter){
     const Tableau::Entry& entry = *iter;
 
     ArithVar var = entry.getColVar();
-    if(var == basic) continue;
+    if(var == skip) { continue; }
+
     int sgn = entry.getCoefficient().sgn();
-    if(upperBound){
-      if( (sgn < 0 && !d_variables.hasLowerBound(var)) ||
-          (sgn > 0 && !d_variables.hasUpperBound(var))){
-        return false;
-      }
-    }else{
-      if( (sgn < 0 && !d_variables.hasUpperBound(var)) ||
-          (sgn > 0 && !d_variables.hasLowerBound(var))){
-        return false;
-      }
+    bool selectUb = (rowUb == (sgn > 0));
+    bool hasBound = selectUb ?
+      d_variables.hasUpperBound(var):
+      d_variables.hasLowerBound(var);
+    if(!hasBound){
+      return &entry;
     }
   }
-  return true;
+  return NULL;
 }
 
+
 template <bool upperBound>
 void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
   Assert(d_tableau.isBasic(basic));
@@ -537,6 +581,39 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
                                    << basic << ") done" << endl;
 }
 
+void LinearEqualityModule::propagateRow(vector<Constraint>& into, RowIndex ridx, bool rowUp, Constraint c){
+  Assert(!c->assertedToTheTheory());
+  Assert(c->canBePropagated());
+  Assert(!c->hasProof());
+
+  ArithVar v = c->getVariable();
+  Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
+                                   << v <<") start" << endl;
+  //vector<Constraint> bounds;
+
+  Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
+  for(; !iter.atEnd(); ++iter){
+    const Tableau::Entry& entry = *iter;
+    ArithVar nonbasic = entry.getColVar();
+    if(nonbasic == v){ continue; }
+
+    const Rational& a_ij = entry.getCoefficient();
+
+    int sgn = a_ij.sgn();
+    Assert(sgn != 0);
+    bool selectUb = rowUp ? (sgn > 0) : (sgn < 0);
+    Constraint bound = selectUb
+      ? d_variables.getUpperBoundConstraint(nonbasic)
+      : d_variables.getLowerBoundConstraint(nonbasic);
+
+    Assert(bound != NullConstraint);
+    Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl;
+    into.push_back(bound);
+  }
+  Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
+                                   << v << ") done" << endl;
+}
+
 Constraint LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic) const {
 
   int sgn = coeff.sgn();
@@ -745,60 +822,35 @@ void LinearEqualityModule::stopTrackingBoundCounts(){
 }
 
 
-void LinearEqualityModule::trackVariable(ArithVar x_i){
-  Assert(!basicIsTracked(x_i));
-  BoundCounts counts(0,0);
-
-  for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd();  ++iter){
-    const Tableau::Entry& entry = *iter;
-    ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == x_i) continue;
-
-    const Rational& a_ij = entry.getCoefficient();
-    counts += (d_variables.oldBoundCounts(nonbasic)).multiplyBySgn(a_ij.sgn());
-  }
-  d_boundTracking.set(x_i, counts);
+void LinearEqualityModule::trackRowIndex(RowIndex ridx){
+  Assert(!rowIndexIsTracked(ridx));
+  BoundsInfo bi = computeRowBoundInfo(ridx, true);
+  d_btracking.set(ridx, bi);
 }
 
-BoundCounts LinearEqualityModule::computeBoundCounts(ArithVar x_i) const{
-  BoundCounts counts(0,0);
+BoundsInfo LinearEqualityModule::computeRowBoundInfo(RowIndex ridx, bool inQueue) const{
+  BoundsInfo bi;
 
-  for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd();  ++iter){
+  Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
+  for(; !iter.atEnd();  ++iter){
     const Tableau::Entry& entry = *iter;
-    ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == x_i) continue;
-
+    ArithVar v = entry.getColVar();
     const Rational& a_ij = entry.getCoefficient();
-    counts += (d_variables.boundCounts(nonbasic)).multiplyBySgn(a_ij.sgn());
+    bi += (d_variables.selectBoundsInfo(v, inQueue)).multiplyBySgn(a_ij.sgn());
   }
-
-  return counts;
+  return bi;
 }
 
-// BoundCounts LinearEqualityModule::cachingCountBounds(ArithVar x_i) const{
-//   if(d_boundTracking.isKey(x_i)){
-//     return d_boundTracking[x_i];
-//   }else{
-//     return computeBoundCounts(x_i);
-//   }
-// }
-BoundCounts LinearEqualityModule::_countBounds(ArithVar x_i) const {
-  Assert(d_boundTracking.isKey(x_i));
-  return d_boundTracking[x_i];
+BoundCounts LinearEqualityModule::debugBasicAtBoundCount(ArithVar x_i) const {
+  return d_btracking[d_tableau.basicToRowIndex(x_i)].atBounds();
 }
 
-// BoundCounts LinearEqualityModule::countBounds(ArithVar x_i){
-//   if(d_boundTracking.isKey(x_i)){
-//     return d_boundTracking[x_i];
-//   }else{
-//     BoundCounts bc = computeBoundCounts(x_i);
-//     if(d_areTracking){
-//       d_boundTracking.set(x_i,bc);
-//     }
-//     return bc;
-//   }
-// }
-
+/**
+ * If the pivot described in u were performed,
+ * then the row would qualify as being either at the minimum/maximum
+ * to the non-basics being at their bounds.
+ * The minimum/maximum is determined by the direction the non-basic is changing.
+ */
 bool LinearEqualityModule::basicsAtBounds(const UpdateInfo& u) const {
   Assert(u.describesPivot());
 
@@ -814,79 +866,78 @@ bool LinearEqualityModule::basicsAtBounds(const UpdateInfo& u) const {
   int toLB = (c->getType() == LowerBound ||
               c->getType() == Equality) ? 1 : 0;
 
+  RowIndex ridx = d_tableau.basicToRowIndex(basic);
 
-  BoundCounts bcs = d_boundTracking[basic];
+  BoundCounts bcs = d_btracking[ridx].atBounds();
   // x = c*n + \sum d*m
-  // n = 1/c * x + -1/c * (\sum d*m)  
-  BoundCounts nonb = bcs - d_variables.boundCounts(nonbasic).multiplyBySgn(coeffSgn);
+  // 0 = -x + c*n + \sum d*m
+  // n = 1/c * x + -1/c * (\sum d*m)
+  BoundCounts nonb = bcs - d_variables.atBoundCounts(nonbasic).multiplyBySgn(coeffSgn);
+  nonb.addInChange(-1, d_variables.atBoundCounts(basic), BoundCounts(toLB, toUB));
   nonb = nonb.multiplyBySgn(-coeffSgn);
-  nonb += BoundCounts(toLB, toUB).multiplyBySgn(coeffSgn);
 
   uint32_t length = d_tableau.basicRowLength(basic);
   Debug("basicsAtBounds")
     << "bcs " << bcs
     << "nonb " << nonb
     << "length " << length << endl;
-
+  // nonb has nb excluded.
   if(nbdir < 0){
-    return bcs.atLowerBounds() + 1 == length;
+    return nonb.lowerBoundCount() + 1 == length;
   }else{
     Assert(nbdir > 0);
-    return bcs.atUpperBounds() + 1 == length;
+    return nonb.upperBoundCount() + 1 == length;
   }
 }
 
 bool LinearEqualityModule::nonbasicsAtLowerBounds(ArithVar basic) const {
   Assert(basicIsTracked(basic));
-  BoundCounts bcs = d_boundTracking[basic];
+  RowIndex ridx = d_tableau.basicToRowIndex(basic);
+
+  BoundCounts bcs = d_btracking[ridx].atBounds();
   uint32_t length = d_tableau.basicRowLength(basic);
 
-  return bcs.atLowerBounds() + 1 == length;
+  // return true if excluding the basic is every element is at its "lowerbound"
+  // The psuedo code is:
+  //   bcs -= basic.count(basic, basic's sgn)
+  //   return bcs.lowerBoundCount() + 1 == length
+  // As basic's sign is always -1, we can pull out the pieces of the count:
+  //   bcs.lowerBoundCount() - basic.atUpperBoundInd() + 1 == length
+  // basic.atUpperBoundInd() is either 0 or 1
+  uint32_t lbc = bcs.lowerBoundCount();
+  return  (lbc == length) ||
+    (lbc + 1 == length && d_variables.cmpAssignmentUpperBound(basic) != 0);
 }
 
 bool LinearEqualityModule::nonbasicsAtUpperBounds(ArithVar basic) const {
   Assert(basicIsTracked(basic));
-  BoundCounts bcs = d_boundTracking[basic];
+  RowIndex ridx = d_tableau.basicToRowIndex(basic);
+  BoundCounts bcs = d_btracking[ridx].atBounds();
   uint32_t length = d_tableau.basicRowLength(basic);
+  uint32_t ubc = bcs.upperBoundCount();
+  // See the comment for nonbasicsAtLowerBounds()
 
-  return bcs.atUpperBounds() + 1 == length;
+  return (ubc == length) ||
+    (ubc + 1 == length && d_variables.cmpAssignmentLowerBound(basic) != 0);
 }
 
-void LinearEqualityModule::trackingSwap(ArithVar basic, ArithVar nb, int nbSgn) {
-  Assert(basicIsTracked(basic));
-
-  // z = a*x + \sum b*y
-  // x = (1/a) z + \sum (-1/a)*b*y
-  // basicCount(z) = bc(a*x) +  bc(\sum b y)
-  // basicCount(x) = bc(z/a) + bc(\sum -b/a * y)
-
-  // sgn(1/a) = sgn(a)
-  // bc(a*x) = bc(x).multiply(sgn(a))
-  // bc(z/a) = bc(z).multiply(sgn(a))
-  // bc(\sum -b/a * y) = bc(\sum b y).multiplyBySgn(-sgn(a))
-  // bc(\sum b y) = basicCount(z) - bc(a*x)
-  // basicCount(x) =
-  //  = bc(z).multiply(sgn(a)) + (basicCount(z) - bc(a*x)).multiplyBySgn(-sgn(a))
-
-  BoundCounts bc = d_boundTracking[basic];
-  bc -= (d_variables.boundCounts(nb)).multiplyBySgn(nbSgn);
-  bc = bc.multiplyBySgn(-nbSgn);
-  bc += d_variables.boundCounts(basic).multiplyBySgn(nbSgn);
-  d_boundTracking.set(nb, bc);
-  d_boundTracking.remove(basic);
+void LinearEqualityModule::trackingMultiplyRow(RowIndex ridx, int sgn) {
+  Assert(rowIndexIsTracked(ridx));
+  Assert(sgn != 0);
+  if(sgn < 0){
+    BoundsInfo& bi = d_btracking.get(ridx);
+    bi = bi.multiplyBySgn(sgn);
+  }
 }
 
 void LinearEqualityModule::trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){
   Assert(oldSgn != currSgn);
-  BoundCounts nb_bc = d_variables.boundCounts(nb);
+  BoundsInfo nb_inf = d_variables.boundsInfo(nb);
 
-  if(!nb_bc.isZero()){
-    ArithVar basic = d_tableau.rowIndexToBasic(ridx);
-    Assert(basicIsTracked(basic));
+  Assert(rowIndexIsTracked(ridx));
 
-    BoundCounts& basic_bc = d_boundTracking.get(basic);
-    basic_bc.addInSgn(nb_bc, oldSgn, currSgn);
-  }
+  BoundsInfo& row_bi = d_btracking.get(ridx);
+  row_bi.addInSgn(nb_inf, oldSgn, currSgn);
 }
 
 void LinearEqualityModule::computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction pref){
@@ -895,9 +946,6 @@ void LinearEqualityModule::computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunct
   Assert(sgn != 0);
   Assert(!d_tableau.isBasic(nb));
 
-  //inf.setErrorsChange(0);
-  //inf.setlimiting = NullConstraint;
-
 
   // Error variables moving in the correct direction
   Assert(d_relevantErrorBuffer.empty());
@@ -1188,8 +1236,9 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr
 
   // Assume past this point, nb will be in error if this pivot is done
   ArithVar nb = entry.getColVar();
-  ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex());
-  Assert(basicIsTracked(basic));
+  RowIndex ridx = entry.getRowIndex();
+  ArithVar basic = d_tableau.rowIndexToBasic(ridx);
+  Assert(rowIndexIsTracked(ridx));
   int coeffSgn = entry.getCoefficient().sgn();
 
 
@@ -1201,12 +1250,11 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr
   // 2) -a * x = -y + \sum b * z
   // 3) x = (-1/a) * ( -y + \sum b * z)
 
-  Assert(basicIsTracked(basic));
-  BoundCounts bc = d_boundTracking[basic];
+  BoundCounts bc = d_btracking[ridx].atBounds();
 
   // 1) y = a * x + \sum b * z
   // Get bc(\sum b * z)
-  BoundCounts sumOnly = bc - d_variables.boundCounts(nb).multiplyBySgn(coeffSgn);
+  BoundCounts sumOnly = bc - d_variables.atBoundCounts(nb).multiplyBySgn(coeffSgn);
 
   // y's bounds in the proposed model
   int yWillBeAtUb = (bToUB || d_variables.boundsAreEqual(basic)) ? 1 : 0;
@@ -1215,19 +1263,19 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr
 
   // 2) -a * x = -y + \sum b * z
   // Get bc(-y + \sum b * z)
-  BoundCounts withNegY = sumOnly + ysBounds.multiplyBySgn(-1);
+  sumOnly.addInChange(-1, d_variables.atBoundCounts(basic), ysBounds);
 
   // 3) x = (-1/a) * ( -y + \sum b * z)
   // Get bc((-1/a) * ( -y + \sum b * z))
-  BoundCounts xsBoundsAfterPivot = withNegY.multiplyBySgn(-coeffSgn);
+  BoundCounts xsBoundsAfterPivot = sumOnly.multiplyBySgn(-coeffSgn);
 
   uint32_t length = d_tableau.basicRowLength(basic);
   if(nbSgn > 0){
     // Only check for the upper bound being violated
-    return xsBoundsAfterPivot.atLowerBounds() + 1 == length;
+    return xsBoundsAfterPivot.lowerBoundCount() + 1 == length;
   }else{
     // Only check for the lower bound being violated
-    return xsBoundsAfterPivot.atUpperBounds() + 1 == length;
+    return xsBoundsAfterPivot.upperBoundCount() + 1 == length;
   }
 }
 
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 8b9b888f2..b1f3d00d7 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -192,9 +192,6 @@ public:
 };
 
 
-
-
-
 class LinearEqualityModule {
 public:
   typedef ArithVar (LinearEqualityModule::*VarPreferenceFunction)(ArithVar, ArithVar) const;
@@ -226,14 +223,12 @@ public:
    * Initializes a LinearEqualityModule with a partial model, a tableau,
    * and a callback function for when basic variables update their values.
    */
-  LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundCountingVector& boundTracking, BasicVarModelUpdateCallBack f);
+  LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundInfoMap& boundTracking, BasicVarModelUpdateCallBack f);
 
   /**
    * Updates the assignment of a nonbasic variable x_i to v.
    * Also updates the assignment of basic variables accordingly.
    */
-  void updateUntracked(ArithVar x_i, const DeltaRational& v);
-  void updateTracked(ArithVar x_i, const DeltaRational& v);
   void update(ArithVar x_i, const DeltaRational& v){
     if(d_areTracking){
       updateTracked(x_i,v);
@@ -241,6 +236,17 @@ public:
       updateUntracked(x_i,v);
     }
   }
+
+  /** Specialization of update if the module is not tracking yet (for Assert*). */
+  void updateUntracked(ArithVar x_i, const DeltaRational& v);
+
+  /** Specialization of update if the module is not tracking yet (for Simplex). */
+  void updateTracked(ArithVar x_i, const DeltaRational& v);
+
+  /**
+   * Updates every non-basic to reflect the assignment in many.
+   * For use with ApproximateSimplex.
+   */
   void updateMany(const DenseMap<DeltaRational>& many);
 
   /**
@@ -249,26 +255,30 @@ public:
    * Updates the assignment of the other basic variables accordingly.
    */
   void pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& v);
-  //void pivotAndUpdateAdj(ArithVar x_i, ArithVar x_j, const DeltaRational& v);
 
   ArithVariables& getVariables() const{ return d_variables; }
   Tableau& getTableau() const{ return d_tableau; }
 
   void forceNewBasis(const DenseSet& newBasis);
 
+#warning "Remove legacy code."
   bool hasBounds(ArithVar basic, bool upperBound);
-  bool hasLowerBounds(ArithVar basic){
-    return hasBounds(basic, false);
-  }
-  bool hasUpperBounds(ArithVar basic){
-    return hasBounds(basic, true);
-  }
+
+  /**
+   * Returns a pointer to the first Tableau entry on the row ridx that does not
+   * have an either a lower bound/upper bound for proving a bound on skip.
+   * The variable skip is always excluded. Returns NULL if there is no such element.
+   *
+   * If skip == ARITHVAR_SENTINEL, this is equivalent to considering the whole row.
+   */
+  const Tableau::Entry* rowLacksBound(RowIndex ridx, bool upperBound, ArithVar skip);
+
 
   void startTrackingBoundCounts();
   void stopTrackingBoundCounts();
 
 
-  void includeBoundCountChange(ArithVar nb, BoundCounts prev);
+  void includeBoundUpdate(ArithVar nb, const BoundsInfo& prev);
 
   void computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction basic);
 
@@ -334,40 +344,6 @@ public:
     }
   }
 
-  // template<bool heuristic>
-  // bool preferNonDegenerate(const UpdateInfo& a, const UpdateInfo& b) const{
-  //   if(a.focusDirection() == b.focusDirection()){
-  //     if(heuristic){
-  //       return preferNeitherBound(a,b);
-  //     }else{
-  //       return minNonBasicVarOrder(a,b);
-  //     }
-  //   }else{
-  //     return a.focusDirection() < b.focusDirection();
-  //   }
-  // }
-
-  // template <bool heuristic>
-  // bool preferErrorsFixed(const UpdateInfo& a, const UpdateInfo& b) const{
-  //   if( a.errorsChange() == b.errorsChange() ){
-  //     return preferNonDegenerate<heuristic>(a,b);
-  //   }else{
-  //     return a.errorsChange() > b.errorsChange();
-  //   }
-  // }
-
-  // template <bool heuristic>
-  // bool preferConflictFound(const UpdateInfo& a, const UpdateInfo& b) const{
-  //   if(a.d_foundConflict && b.d_foundConflict){
-  //     // if both are true, determinize the preference
-  //     return minNonBasicVarOrder(a,b);
-  //   }else if( a.d_foundConflict || b.d_foundConflict ){
-  //     return b.d_foundConflict;
-  //   }else{
-  //     return preferErrorsFixed<heuristic>(a,b);
-  //   }
-  // }
-
   bool modifiedBlands(const UpdateInfo& a, const UpdateInfo& b) const {
     Assert(a.focusDirection() == 0 && b.focusDirection() == 0);
     Assert(a.describesPivot());
@@ -434,14 +410,13 @@ private:
   //uint32_t computedFixed(ArithVar nb, int sgn, const DeltaRational& am);
   void computedFixed(UpdateInfo&);
 
-  // RowIndex -> BoundCount
-  BoundCountingVector& d_boundTracking;
+  /**
+   * This maps each row index to its relevant bounds info.
+   * This tracks the */
+  BoundInfoMap& d_btracking;
   bool d_areTracking;
 
-  /**
-   * Exports either the explanation of an upperbound or a lower bound
-   * of the basic variable basic, using the non-basic variables in the row.
-   */
+#warning "Remove legacy code"
   template <bool upperBound>
   void propagateNonbasics(ArithVar basic, Constraint c);
 
@@ -452,6 +427,11 @@ public:
   void propagateNonbasicsUpperBound(ArithVar basic, Constraint c){
     propagateNonbasics<true>(basic, c);
   }
+  /**
+   * Exports either the explanation of an upperbound or a lower bound
+   * of the basic variable basic, using the non-basic variables in the row.
+   */
+  void propagateRow(std::vector<Constraint>& into, RowIndex ridx, bool rowUp, Constraint c);
 
   /**
    * Computes the value of a basic variable using the assignments
@@ -460,12 +440,12 @@ public:
    * - the the current assignment (useSafe=false) or
    * - the safe assignment (useSafe = true).
    */
-  DeltaRational computeRowValue(ArithVar x, bool useSafe);
+  DeltaRational computeRowValue(ArithVar x, bool useSafe) const;
 
-  inline DeltaRational computeLowerBound(ArithVar basic){
+  inline DeltaRational computeLowerBound(ArithVar basic) const{
     return computeBound(basic, false);
   }
-  inline DeltaRational computeUpperBound(ArithVar basic){
+  inline DeltaRational computeUpperBound(ArithVar basic) const{
     return computeBound(basic, true);
   }
 
@@ -548,35 +528,42 @@ public:
 
   const Tableau::Entry* selectSlackEntry(ArithVar x_i, bool above) const;
 
+  inline bool rowIndexIsTracked(RowIndex ridx) const {
+    return d_btracking.isKey(ridx);
+  }
   inline bool basicIsTracked(ArithVar v) const {
-    return d_boundTracking.isKey(v);
+    return rowIndexIsTracked(d_tableau.basicToRowIndex(v));
   }
-  void trackVariable(ArithVar x_i);
-
-  void maybeRemoveTracking(ArithVar v){
-    Assert(!d_tableau.isBasic(v));
-    if(d_boundTracking.isKey(v)){
-      d_boundTracking.remove(v);
-    }
+  void trackRowIndex(RowIndex ridx);
+  void stopTrackingRowIndex(RowIndex ridx){
+    Assert(rowIndexIsTracked(ridx));
+    d_btracking.remove(ridx);
   }
 
-  // void trackVariable(ArithVar x_i){
-  //   Assert(!basicIsTracked(x_i));
-  //   d_boundTracking.set(x_i,computeBoundCounts(x_i));
-  // }
+  /**
+   * If the pivot described in u were performed,
+   * then the row would qualify as being either at the minimum/maximum
+   * to the non-basics being at their bounds.
+   * The minimum/maximum is determined by the direction the non-basic is changing.
+   */
   bool basicsAtBounds(const UpdateInfo& u) const;
 private:
-  BoundCounts computeBoundCounts(ArithVar x_i) const;
+  BoundsInfo computeRowBoundInfo(RowIndex ridx, bool inQueue) const;
 public:
-  //BoundCounts cachingCountBounds(ArithVar x_i) const;
-  BoundCounts _countBounds(ArithVar x_i) const;
+  BoundCounts debugBasicAtBoundCount(ArithVar x_i) const;
   void trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn);
+  void trackingMultiplyRow(RowIndex ridx, int sgn);
 
-  void trackingSwap(ArithVar basic, ArithVar nb, int sgn);
+  BoundCounts hasBoundCount(RowIndex ri) const {
+    Assert(d_variables.boundsQueueEmpty());
+    return d_btracking[ri].hasBounds();
+  }
 
+#warning "Remove legacy code"
   bool nonbasicsAtLowerBounds(ArithVar x_i) const;
   bool nonbasicsAtUpperBounds(ArithVar x_i) const;
 
+#warning "Remove legacy code"
   ArithVar _anySlackLowerBound(ArithVar x_i) const {
     return selectSlack<true>(x_i, &LinearEqualityModule::noPreference);
   }
@@ -593,8 +580,8 @@ private:
     void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){
       d_linEq->trackingCoefficientChange(ridx, nb, oldSgn, currSgn);
     }
-    void swap(ArithVar basic, ArithVar nb, int oldNbSgn){
-      d_linEq->trackingSwap(basic, nb, oldNbSgn);
+    void multiplyRow(RowIndex ridx, int sgn){
+      d_linEq->trackingMultiplyRow(ridx, sgn);
     }
     bool canUseRow(RowIndex ridx) const {
       ArithVar basic = d_linEq->getTableau().rowIndexToBasic(ridx);
@@ -629,8 +616,10 @@ public:
     return minimallyWeakConflict(false, conflictVar);
   }
 
+  DeltaRational computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const;
+
 private:
-  DeltaRational computeBound(ArithVar basic, bool upperBound);
+  DeltaRational computeBound(ArithVar basic, bool upperBound) const;
 
 public:
   void substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult);
@@ -737,13 +726,13 @@ public:
   }
 };
 
-class UpdateTrackingCallback : public BoundCountsCallback {
+class UpdateTrackingCallback : public BoundUpdateCallback {
 private:
   LinearEqualityModule* d_mod;
 public:
   UpdateTrackingCallback(LinearEqualityModule* mod): d_mod(mod){}
-  void operator()(ArithVar v, BoundCounts bc){
-    d_mod->includeBoundCountChange(v, bc);
+  void operator()(ArithVar v, const BoundsInfo& bi){
+    d_mod->includeBoundUpdate(v, bi);
   }
 };
 
diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp
index 7136c3fa8..b8bd68488 100644
--- a/src/theory/arith/matrix.cpp
+++ b/src/theory/arith/matrix.cpp
@@ -24,7 +24,7 @@ namespace theory {
 namespace arith {
 
 void NoEffectCCCB::update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) {}
-void NoEffectCCCB::swap(ArithVar basic, ArithVar nb, int nbSgn){}
+void NoEffectCCCB::multiplyRow(RowIndex ridx, int sgn){}
 bool NoEffectCCCB::canUseRow(RowIndex ridx) const { return false; }
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h
index 100f999e0..d93b6986e 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -39,15 +39,15 @@ const RowIndex ROW_INDEX_SENTINEL  = std::numeric_limits<RowIndex>::max();
 
 class CoefficientChangeCallback {
 public:
-  virtual void update(RowIndex basic, ArithVar nb, int oldSgn, int currSgn) = 0;
-  virtual void swap(ArithVar basic, ArithVar nb, int nbSgn) = 0;
+  virtual void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) = 0;
+  virtual void multiplyRow(RowIndex ridx, int Sgn) = 0;
   virtual bool canUseRow(RowIndex ridx) const = 0;
 };
 
 class NoEffectCCCB : public CoefficientChangeCallback {
 public:
   void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn);
-  void swap(ArithVar basic, ArithVar nb, int nbSgn);
+  void multiplyRow(RowIndex ridx, int Sgn);
   bool canUseRow(RowIndex ridx) const;
 };
 
diff --git a/src/theory/arith/options b/src/theory/arith/options
index 977d6cb32..1366addae 100644
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -91,4 +91,10 @@ option fancyFinal --fancy-final bool :default false :read-write
 option exportDioDecompositions --dio-decomps bool :default false :read-write
  Let skolem variables for integer divisibility constraints leak from the dio solver.
 
+option newProp --new-prop bool :default false :read-write
+ Use the new row propagation system
+
+option arithPropAsLemmaLength --arith-prop-clauses int :default 8 :read-write
+ Rows shorter than this are propagated as clauses
+
 endmodule
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 695d9df25..3fae3751c 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -35,12 +35,13 @@ ArithVariables::ArithVariables(context::Context* c, DeltaComputeCallback deltaCo
    d_released(),
    d_releasedIterator(d_released.begin()),
    d_nodeToArithVarMap(),
+   d_boundsQueue(),
+   d_enqueueingBoundCounts(true),
    d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
    d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
    d_deltaIsSafe(false),
    d_delta(-1,1),
-   d_deltaComputingFunc(deltaComputingFunc),
-   d_enqueueingBoundCounts(true)
+   d_deltaComputingFunc(deltaComputingFunc)
 { }
 
 ArithVariables::VarInfo::VarInfo()
@@ -55,6 +56,10 @@ ArithVariables::VarInfo::VarInfo()
     d_slack(false)
 { }
 
+bool ArithVariables::VarInfo::initialized() const {
+  return d_var != ARITHVAR_SENTINEL;
+}
+
 void ArithVariables::VarInfo::initialize(ArithVar v, Node n, bool slack){
   Assert(!initialized());
   Assert(d_lb == NullConstraint);
@@ -82,7 +87,7 @@ void ArithVariables::VarInfo::uninitialize(){
   d_node = Node::null();
 }
 
-bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundCounts & prev){
+bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundsInfo& prev){
   Assert(initialized());
   d_assignment = a;
   int cmpUB = (d_ub == NullConstraint) ? -1 :
@@ -97,7 +102,7 @@ bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundCounts
     (cmpUB == 0 || d_cmpAssignmentUB == 0);
 
   if(lbChanged || ubChanged){
-    prev = boundCounts();
+    prev = boundsInfo();
   }
 
   d_cmpAssignmentUB = cmpUB;
@@ -119,33 +124,59 @@ void ArithVariables::releaseArithVar(ArithVar v){
   }
 }
 
-bool ArithVariables::VarInfo::setUpperBound(Constraint ub, BoundCounts& prev){
+bool ArithVariables::VarInfo::setUpperBound(Constraint ub, BoundsInfo& prev){
   Assert(initialized());
-  d_ub = ub;
-  int cmpUB = (d_ub == NullConstraint) ? -1 : d_assignment.cmp(d_ub->getValue());
-  bool ubChanged = cmpUB != d_cmpAssignmentUB &&
-    (cmpUB == 0 || d_cmpAssignmentUB == 0);
+  bool wasNull = d_ub == NullConstraint;
+  bool isNull = ub == NullConstraint;
+
+  int cmpUB = isNull ? -1 : d_assignment.cmp(ub->getValue());
+  bool ubChanged = (wasNull != isNull) ||
+    (cmpUB != d_cmpAssignmentUB && (cmpUB == 0 || d_cmpAssignmentUB == 0));
   if(ubChanged){
-    prev = boundCounts();
+    prev = boundsInfo();
   }
+  d_ub = ub;
   d_cmpAssignmentUB = cmpUB;
   return ubChanged;
 }
 
-bool ArithVariables::VarInfo::setLowerBound(Constraint lb, BoundCounts& prev){
+bool ArithVariables::VarInfo::setLowerBound(Constraint lb, BoundsInfo& prev){
   Assert(initialized());
-  d_lb = lb;
-  int cmpLB = (d_lb == NullConstraint) ? 1 : d_assignment.cmp(d_lb->getValue());
+  bool wasNull = d_lb == NullConstraint;
+  bool isNull = lb == NullConstraint;
 
-  bool lbChanged = cmpLB != d_cmpAssignmentLB &&
-    (cmpLB == 0 || d_cmpAssignmentLB == 0);
+  int cmpLB = isNull ? 1 : d_assignment.cmp(lb->getValue());
+
+  bool lbChanged = (wasNull != isNull) ||
+    (cmpLB != d_cmpAssignmentLB && (cmpLB == 0 || d_cmpAssignmentLB == 0));
   if(lbChanged){
-    prev = boundCounts();
+    prev = boundsInfo();
   }
+  d_lb = lb;
   d_cmpAssignmentLB = cmpLB;
   return lbChanged;
 }
 
+BoundCounts ArithVariables::VarInfo::atBoundCounts() const {
+  uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
+  uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
+  return BoundCounts(lbIndc, ubIndc);
+}
+
+BoundCounts ArithVariables::VarInfo::hasBoundCounts() const {
+  uint32_t lbIndc = (d_lb != NullConstraint) ? 1 : 0;
+  uint32_t ubIndc = (d_ub != NullConstraint) ? 1 : 0;
+  return BoundCounts(lbIndc, ubIndc);
+}
+
+BoundsInfo ArithVariables::VarInfo::boundsInfo() const{
+  return BoundsInfo(atBoundCounts(), hasBoundCounts());
+}
+
+bool ArithVariables::VarInfo::canBeReclaimed() const{
+  return d_pushCount == 0;
+}
+
 void ArithVariables::attemptToReclaimReleased(){
   std::list<ArithVar>::iterator i_end = d_released.end();
   for(int iter = 0; iter < 20 && d_releasedIterator != i_end; ++d_releasedIterator){
@@ -170,7 +201,7 @@ ArithVar ArithVariables::allocateVariable(){
     attemptToReclaimReleased();
   }
   bool reclaim = !d_pool.empty();
-  
+
   ArithVar varX;
   if(reclaim){
     varX = d_pool.back();
@@ -210,7 +241,7 @@ void ArithVariables::setAssignment(ArithVar x, const DeltaRational& r){
   }
   invalidateDelta();
 
-  BoundCounts prev;
+  BoundsInfo prev;
   if(vi.setAssignment(r, prev)){
     addToBoundQueue(x, prev);
   }
@@ -229,7 +260,7 @@ void ArithVariables::setAssignment(ArithVar x, const DeltaRational& safe, const
 
   invalidateDelta();
   VarInfo& vi = d_vars.get(x);
-  BoundCounts prev;
+  BoundsInfo prev;
   if(vi.setAssignment(r, prev)){
     addToBoundQueue(x, prev);
   }
@@ -314,7 +345,7 @@ void ArithVariables::setLowerBoundConstraint(Constraint c){
   invalidateDelta();
   VarInfo& vi = d_vars.get(x);
   pushLowerBound(vi);
-  BoundCounts prev;
+  BoundsInfo prev;
   if(vi.setLowerBound(c, prev)){
     addToBoundQueue(x, prev);
   }
@@ -333,37 +364,12 @@ void ArithVariables::setUpperBoundConstraint(Constraint c){
   invalidateDelta();
   VarInfo& vi = d_vars.get(x);
   pushUpperBound(vi);
-  BoundCounts prev;
+  BoundsInfo prev;
   if(vi.setUpperBound(c, prev)){
     addToBoundQueue(x, prev);
   }
 }
 
-// void ArithVariables::forceRelaxLowerBound(ArithVar v){
-//   AssertArgument(inMaps(v), "Calling forceRelaxLowerBound on a variable that is not properly setup.");
-//   AssertArgument(hasLowerBound(v), "Calling forceRelaxLowerBound on a variable without a lowerbound.");
-
-//   Debug("partial_model") << "forceRelaxLowerBound(" << v << ") dropping :" << getLowerBoundConstraint(v) << endl;
-
-//   invalidateDelta();
-//   VarInfo& vi = d_vars.get(v);
-//   pushLowerBound(vi);
-//   vi.setLowerBound(NullConstraint);
-// }
-
-
-// void ArithVariables::forceRelaxUpperBound(ArithVar v){
-//   AssertArgument(inMaps(v), "Calling forceRelaxUpperBound on a variable that is not properly setup.");
-//   AssertArgument(hasUpperBound(v), "Calling forceRelaxUpperBound on a variable without an upper bound.");
-
-//   Debug("partial_model") << "forceRelaxUpperBound(" << v << ") dropping :" << getUpperBoundConstraint(v) << endl;
-
-//   invalidateDelta();
-//   VarInfo& vi = d_vars.get(v);
-//   pushUpperBound(vi);
-//   vi.setUpperBound(NullConstraint);
-// }
-
 int ArithVariables::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{
   if(!hasLowerBound(x)){
     // l = -\intfy
@@ -405,30 +411,16 @@ bool ArithVariables::hasEitherBound(ArithVar x) const{
 
 bool ArithVariables::strictlyBelowUpperBound(ArithVar x) const{
   return d_vars[x].d_cmpAssignmentUB < 0;
-  // if(!hasUpperBound(x)){ // u = \infty
-  //   return true;
-  // }else{
-  //   return d_assignment[x] < getUpperBound(x);
-  // }
 }
 
 bool ArithVariables::strictlyAboveLowerBound(ArithVar x) const{
   return d_vars[x].d_cmpAssignmentLB > 0;
-  // if(!hasLowerBound(x)){ // l = -\infty
-  //   return true;
-  // }else{
-  //   return getLowerBound(x) < d_assignment[x];
-  // }
 }
 
 bool ArithVariables::assignmentIsConsistent(ArithVar x) const{
   return
     d_vars[x].d_cmpAssignmentLB >= 0 &&
     d_vars[x].d_cmpAssignmentUB <= 0;
-  // const DeltaRational& beta = getAssignment(x);
-
-  // //l_i <= beta(x_i) <= u_i
-  // return  greaterThanLowerBound(x,beta) && lessThanUpperBound(x,beta);
 }
 
 
@@ -442,7 +434,7 @@ void ArithVariables::clearSafeAssignments(bool revert){
     ArithVar atBack = d_safeAssignment.back();
     if(revert){
       VarInfo& vi = d_vars.get(atBack);
-      BoundCounts prev;
+      BoundsInfo prev;
       if(vi.setAssignment(d_safeAssignment[atBack], prev)){
         addToBoundQueue(atBack, prev);
       }
@@ -489,33 +481,6 @@ void ArithVariables::printModel(ArithVar x) const{
   printModel(x,  Debug("model"));
 }
 
-// BoundRelationship ArithVariables::boundRelationship(Constraint lb, const DeltaRational& d, Constraint ub){
-//   if(lb == NullConstraint && ub == NullConstraint){
-//     return BetweenBounds;
-//   }else if(lb == NullConstraint){
-//     int cmp = d.cmp(ub->getValue());
-//     return (cmp < 0) ? BetweenBounds :
-//       (cmp == 0 ? AtUpperBound  : AboveUpperBound);
-//   }else if(ub == NullConstraint){
-//     int cmp = d.cmp(lb->getValue());
-//     return (cmp > 0) ? BetweenBounds :
-//       (cmp == 0 ? AtLowerBound  : BelowLowerBound);    
-//   }else{
-//     Assert(lb->getValue() <= ub->getValue());
-//     int cmpToLB = d.cmp(lb->getValue());
-//     if(cmpToLB < 0){
-//       return BelowLowerBound;
-//     }else if(cmpToLB == 0){
-//       return (d == ub->getValue()) ? AtBothBounds : AtLowerBound;
-//     }else{
-//       // d > 0
-//       int cmpToUB = d.cmp(ub->getValue());
-//       return (cmpToUB > 0) ? BetweenBounds :
-//         (cmpToUB == 0 ? AtLowerBound  : BelowLowerBound);    
-//     }
-//   }
-// }
-
 void ArithVariables::pushUpperBound(VarInfo& vi){
   ++vi.d_pushCount;
   d_ubRevertHistory.push_back(make_pair(vi.d_var, vi.d_ub));
@@ -528,7 +493,7 @@ void ArithVariables::pushLowerBound(VarInfo& vi){
 void ArithVariables::popUpperBound(AVCPair* c){
   ArithVar x = c->first;
   VarInfo& vi = d_vars.get(x);
-  BoundCounts prev;
+  BoundsInfo prev;
   if(vi.setUpperBound(c->second, prev)){
     addToBoundQueue(x, prev);
   }
@@ -538,62 +503,42 @@ void ArithVariables::popUpperBound(AVCPair* c){
 void ArithVariables::popLowerBound(AVCPair* c){
   ArithVar x = c->first;
   VarInfo& vi = d_vars.get(x);
-  BoundCounts prev;
+  BoundsInfo prev;
   if(vi.setLowerBound(c->second, prev)){
     addToBoundQueue(x, prev);
   }
   --vi.d_pushCount;
 }
 
-/* To ensure that the final deallocation stuff works,
- * we need to ensure that we need to not reference any of the other vectors
- */
-// void ArithVariables::relaxUpperBound(Constraint curr, Constraint afterPop){
-//   BoundRelation next = Undefined;
-//   switch(d_boundRel[x]){
-//   case BelowLowerBound:
-//   case BetweenBounds:
-//   case AtLowerBound:
-//     return; // do nothing
-//   case AtUpperBound:
-//     if(afterPop != NullConstraint
-//        && curr->getValue() == afterPop->getValue()){
-//       next = AtUpperBound;
-//     }else{
-//       next = BetweenBounds;
-//     }
-//     break;
-//   case AtBothBounds:
-//     if(afterPop != NullConstraint
-//        && curr->getValue() == afterPop->getValue()){
-//       next = AtUpperBound;
-//     }else{
-//       next = AtLowerBound;
-//     }
-//     break;
-//   case AboveUpperBound:
-//     if(afterPop == NullConstraint){
-//       next = BetweenBounds;
-//     }else{
-//       int cmp = d_assignment[x].cmp(afterPop->getValue());
-//       next = (cmp < 0) ? BetweenBounds :
-//         (cmp == 0) ? AtUpperBound  : AboveUpperBound;
-//     }
-//     break;
-//   default:
-//     Unreachable();
-//   }
-//   d_boundRel[x] = next;
-// }
+void ArithVariables::addToBoundQueue(ArithVar v, const BoundsInfo& prev){
+  if(d_enqueueingBoundCounts && !d_boundsQueue.isKey(v)){
+    d_boundsQueue.set(v, prev);
+  }
+}
 
+BoundsInfo ArithVariables::selectBoundsInfo(ArithVar v, bool old) const {
+  if(old && d_boundsQueue.isKey(v)){
+    return d_boundsQueue[v];
+  }else{
+    return boundsInfo(v);
+  }
+}
 
+bool ArithVariables::boundsQueueEmpty() const {
+  return d_boundsQueue.empty();
+}
 
-// void ArithVariables::relaxLowerBound(Constraint curr, Constraint afterPop){
-//   // TODO this can be optimized using the automata induced by d_boundRel and
-//   // the knowledge that lb <= ub
-//   ArithVar x = curr->getVariable();
-//   d_boundRel[x] = boundRelationship(afterPop, d_assignment[x], d_ubc[x]);    
-// }
+void ArithVariables::processBoundsQueue(BoundUpdateCallback& changed){
+  while(!boundsQueueEmpty()){
+    ArithVar v = d_boundsQueue.back();
+    BoundsInfo prev = d_boundsQueue[v];
+    d_boundsQueue.pop_back();
+    BoundsInfo curr = boundsInfo(v);
+    if(prev != curr){
+      changed(v, prev);
+    }
+  }
+}
 
 void ArithVariables::LowerBoundCleanUp::operator()(AVCPair* p){
   d_pm->popLowerBound(p);
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index dcfe97079..953c8c0d3 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -44,6 +44,7 @@ namespace arith {
 
 class ArithVariables {
 private:
+
   class VarInfo {
     friend class ArithVariables;
     ArithVar d_var;
@@ -62,29 +63,36 @@ private:
   public:
     VarInfo();
 
-    bool setAssignment(const DeltaRational& r, BoundCounts& prev);
-    bool setLowerBound(Constraint c, BoundCounts& prev);
-    bool setUpperBound(Constraint c, BoundCounts& prev);
+    bool setAssignment(const DeltaRational& r, BoundsInfo& prev);
+    bool setLowerBound(Constraint c, BoundsInfo& prev);
+    bool setUpperBound(Constraint c, BoundsInfo& prev);
 
-    bool initialized() const {
-      return d_var != ARITHVAR_SENTINEL;
-    }
+    /** Returns true if this VarInfo has been initialized. */
+    bool initialized() const;
+
+    /**
+     * Initializes the VarInfo with the ArithVar index it is associated with,
+     * the node that the variable represents, and whether it is a slack variable.
+     */
     void initialize(ArithVar v, Node n, bool slack);
+    /** Uninitializes the VarInfo. */
     void uninitialize();
 
-    bool canBeReclaimed() const{
-      return d_pushCount == 0;
-    }
+    bool canBeReclaimed() const;
 
-    BoundCounts boundCounts() const {
-      uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
-      uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
-      return BoundCounts(lbIndc, ubIndc);
-    }
+    /** Indicator variables for if the assignment is equal to the upper and lower bounds. */
+    BoundCounts atBoundCounts() const;
+
+    /** Combination of indicator variables for whether it has upper and lower bounds.  */
+    BoundCounts hasBoundCounts() const;
+
+    /** Stores both atBoundCounts() and hasBoundCounts().  */
+    BoundsInfo boundsInfo() const;
   };
 
-  //Maps from ArithVar -> VarInfo
+  /**Maps from ArithVar -> VarInfo */
   typedef DenseMap<VarInfo> VarInfoVec;
+  /** This maps an ArithVar to its Variable information.*/
   VarInfoVec d_vars;
 
   // Partial Map from Arithvar -> PreviousAssignment
@@ -104,7 +112,15 @@ private:
   // Inverse of d_vars[x].d_node
   NodeToArithVarMap d_nodeToArithVarMap;
 
-  DenseMap<BoundCounts> d_atBoundsQueue;
+
+  /** The queue of constraints where the assignment is at the bound.*/
+  DenseMap<BoundsInfo> d_boundsQueue;
+
+  /**
+   * If this is true, record the incoming changes to the bound information.
+   * If this is false, the responsibility of recording the changes is LinearEqualities's.
+   */
+  bool d_enqueueingBoundCounts;
 
  public:
 
@@ -225,7 +241,6 @@ private:
   // Function to call if the value of delta needs to be recomputed.
   DeltaComputeCallback d_deltaComputingFunc;
 
-  bool d_enqueueingBoundCounts;
 
 public:
 
@@ -252,22 +267,7 @@ public:
     return d_vars[x].d_lb;
   }
 
-  /**
-   * This forces the lower bound for a variable to be relaxed in the current context.
-   * This is done by forcing the lower bound to be NullConstraint.
-   * This is an expert only operation! (See primal simplex for an example.)
-   */
-  //void forceRelaxLowerBound(ArithVar x);
-
-  /**
-   * This forces the upper bound for a variable to be relaxed in the current context.
-   * This is done by forcing the upper bound to be NullConstraint.
-   * This is an expert only operation! (See primal simplex for an example.)
-   */
-  //void forceRelaxUpperBound(ArithVar x);
-
   /* Initializes a variable to a safe value.*/
-  //void initialize(ArithVar x, const DeltaRational& r);
   void initialize(ArithVar x, Node n, bool slack);
 
   ArithVar allocate(Node n, bool slack = false);
@@ -360,8 +360,14 @@ public:
     return d_vars[x].d_cmpAssignmentUB;
   }
 
-  inline BoundCounts boundCounts(ArithVar x) const {
-    return d_vars[x].boundCounts();
+  inline BoundCounts atBoundCounts(ArithVar x) const {
+    return d_vars[x].atBoundCounts();
+  }
+  inline BoundCounts hasBoundCounts(ArithVar x) const {
+    return d_vars[x].hasBoundCounts();
+  }
+  inline BoundsInfo boundsInfo(ArithVar x) const{
+    return d_vars[x].boundsInfo();
   }
 
   bool strictlyBelowUpperBound(ArithVar x) const;
@@ -391,38 +397,14 @@ public:
     d_deltaIsSafe = true;
   }
 
-  // inline bool initialized(ArithVar x) const {
-  //   return d_vars[x].initialized();
-  // }
-
-  void addToBoundQueue(ArithVar v, BoundCounts prev){
-    if(d_enqueueingBoundCounts && !d_atBoundsQueue.isKey(v)){
-      d_atBoundsQueue.set(v, prev);
-    }
-  }
+  void startQueueingBoundCounts(){ d_enqueueingBoundCounts = true; }
+  void stopQueueingBoundCounts(){ d_enqueueingBoundCounts = false; }
+  void addToBoundQueue(ArithVar v, const BoundsInfo& prev);
 
-  BoundCounts oldBoundCounts(ArithVar v) const {
-    if(d_atBoundsQueue.isKey(v)){
-      return d_atBoundsQueue[v];
-    }else{
-      return boundCounts(v);
-    }
-  }
+  BoundsInfo selectBoundsInfo(ArithVar v, bool old) const;
 
-  void startQueueingAtBoundQueue(){ d_enqueueingBoundCounts = true; }
-  void stopQueueingAtBoundQueue(){ d_enqueueingBoundCounts = false; }
-
-  void processAtBoundQueue(BoundCountsCallback& changed){
-    while(!d_atBoundsQueue.empty()){
-      ArithVar v = d_atBoundsQueue.back();
-      BoundCounts prev = d_atBoundsQueue[v];
-      d_atBoundsQueue.pop_back();
-      BoundCounts curr = boundCounts(v);
-      if(prev != curr){
-        changed(v, prev);
-      }
-    }
-  }
+  bool boundsQueueEmpty() const;
+  void processBoundsQueue(BoundUpdateCallback& changed);
 
   void printEntireModel(std::ostream& out) const;
 
diff --git a/src/theory/arith/pure_update_simplex.cpp b/src/theory/arith/pure_update_simplex.cpp
index 9b3edfa6f..233fc292f 100644
--- a/src/theory/arith/pure_update_simplex.cpp
+++ b/src/theory/arith/pure_update_simplex.cpp
@@ -175,7 +175,7 @@ bool PureUpdateSimplexDecisionProcedure::attemptPureUpdates(){
 
       worthwhile = proposal.errorsChange() < 0 ||
         (proposal.focusDirection() > 0 &&
-         d_variables.boundCounts(curr).isZero() &&
+         d_variables.atBoundCounts(curr).isZero() &&
          !proposal.describesPivot());
 
       Debug("pu::refined")
@@ -188,11 +188,11 @@ bool PureUpdateSimplexDecisionProcedure::attemptPureUpdates(){
     if(worthwhile){
       Debug("pu") << d_variables.getAssignment(d_focusErrorVar) << endl;
 
-      BoundCounts before = d_variables.boundCounts(curr);
+      BoundCounts before = d_variables.atBoundCounts(curr);
       DeltaRational newAssignment =
         d_variables.getAssignment(curr) + proposal.nonbasicDelta();
       d_linEq.updateTracked(curr, newAssignment);
-      BoundCounts after = d_variables.boundCounts(curr);
+      BoundCounts after = d_variables.atBoundCounts(curr);
 
       ++d_statistics.d_pureUpdates;
       ++boundImprovements;
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 02e49258c..707c8d029 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -130,6 +130,8 @@ void SimplexDecisionProcedure::tearDownInfeasiblityFunction(TimerStat& timer, Ar
   Assert(tmp != ARITHVAR_SENTINEL);
   Assert(d_tableau.isBasic(tmp));
 
+  RowIndex ri = d_tableau.basicToRowIndex(tmp);
+  d_linEq.stopTrackingRowIndex(ri);
   d_tableau.removeBasicRow(tmp);
   releaseVariable(tmp);
 }
@@ -193,9 +195,10 @@ ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& time
   DeltaRational newAssignment = d_linEq.computeRowValue(inf, false);
   d_variables.setAssignment(inf, newAssignment);
 
-  d_linEq.trackVariable(inf);
+  //d_linEq.trackVariable(inf);
+  d_linEq.trackRowIndex(d_tableau.basicToRowIndex(inf));
 
-  Debug("Inf") << inf << " " << newAssignment << endl;
+  Debug("constructInfeasiblityFunction") << inf << " " << newAssignment << endl;
 
   return inf;
 }
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 7255d92ef..b6949c526 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -237,7 +237,7 @@ UpdateInfo SumOfInfeasibilitiesSPD::selectUpdate(LinearEqualityModule::UpdatePre
   Debug("soi::selectPrimalUpdate")
     << "selectPrimalUpdate " << instance << endl
     << d_soiVar << " " << d_tableau.basicRowLength(d_soiVar)
-    << " " << d_linEq._countBounds(d_soiVar) << endl;
+    << " " << d_linEq.debugBasicAtBoundCount(d_soiVar) << endl;
 
   typedef std::vector<Cand> CandVector;
   CandVector candidates;
@@ -349,7 +349,7 @@ void SumOfInfeasibilitiesSPD::debugPrintSignal(ArithVar updated) const{
   int dir = !d_variables.assignmentIsConsistent(updated) ?
     d_errorSet.getSgn(updated) : 0;
   Debug("updateAndSignal") << " dir " << dir;
-  Debug("updateAndSignal") << " _countBounds " << d_linEq._countBounds(updated) << endl;
+  Debug("updateAndSignal") << " debugBasicAtBoundCount " << d_linEq.debugBasicAtBoundCount(updated) << endl;
 }
 
 
@@ -367,7 +367,7 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes
       ArithVar leaving = selected.leaving();
       ss << "leaving " << leaving
          << " " << d_tableau.basicRowLength(leaving)
-         << " " << d_linEq._countBounds(leaving)
+         << " " << d_linEq.debugBasicAtBoundCount(leaving)
          << endl;
     }
     if(degenerate(w) && selected.describesPivot()){
@@ -376,7 +376,7 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes
         << "degenerate " << leaving
         << ", atBounds " << d_linEq.basicsAtBounds(selected)
         << ", len " << d_tableau.basicRowLength(leaving)
-        << ", bc " << d_linEq._countBounds(leaving)
+        << ", bc " << d_linEq.debugBasicAtBoundCount(leaving)
         << endl;
     }
   }
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index c54b0857a..9d06fadc4 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -75,7 +75,7 @@ void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCa
   d_basic2RowIndex.set(basicNew, rid);
   d_rowIndex2basic.set(rid, basicNew);
 
-  cb.swap(basicOld, basicNew, a_rs_sgn);
+  cb.multiplyRow(rid, -a_rs_sgn);
 }
 
 
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 8b6ef1df6..deed7e7be 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -72,8 +72,12 @@ public:
     return getColumn(x).begin();
   }
 
+  RowIterator ridRowIterator(RowIndex rid) const {
+    return getRow(rid).begin();
+  }
+
   RowIterator basicRowIterator(ArithVar basic) const {
-    return getRow(basicToRowIndex(basic)).begin();
+    return ridRowIterator(basicToRowIndex(basic));
   }
 
   const Entry& basicFindEntry(ArithVar basic, ArithVar col) const {
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 263f9536b..31b6cd032 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -83,7 +83,7 @@ namespace arith {
 TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   d_containing(containing),
   d_nlIncomplete( false),
-  d_boundTracking(),
+  d_rowTracking(),
   d_constraintDatabase(c, u, d_partialModel, d_congruenceManager, RaiseConflict(*this)),
   d_qflraStatus(Result::SAT_UNKNOWN),
   d_unknownsInARow(0),
@@ -96,9 +96,9 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_currentPropagationList(),
   d_learnedBounds(c),
   d_partialModel(c, DeltaComputeCallback(*this)),
-  d_errorSet(d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(&d_boundTracking)),
+  d_errorSet(d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(&d_rowTracking, &d_tableau)),
   d_tableau(),
-  d_linEq(d_partialModel, d_tableau, d_boundTracking, BasicVarModelUpdateCallBack(*this)),
+  d_linEq(d_partialModel, d_tableau, d_rowTracking, BasicVarModelUpdateCallBack(*this)),
   d_diosolver(c),
   d_restartsCounter(0),
   d_tableauSizeHasBeenModified(false),
@@ -116,6 +116,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_cutInContext(c),
   d_statistics()
 {
+  srand(79);
 }
 
 TheoryArithPrivate::~TheoryArithPrivate(){ }
@@ -489,9 +490,7 @@ bool TheoryArithPrivate::AssertUpper(Constraint constraint){
         }else if(!lb->negationHasProof()){
           Constraint negLb = lb->getNegation();
           negLb->impliedBy(constraint, diseq);
-          //if(!negLb->canBePropagated()){
           d_learnedBounds.push_back(negLb);
-          //}//otherwise let this be propagated/asserted later
         }
       }
     }
@@ -1100,7 +1099,7 @@ void TheoryArithPrivate::setupPolynomial(const Polynomial& poly) {
     ArithVar varSlack = requestArithVar(polyNode, true);
     d_tableau.addRow(varSlack, coefficients, variables);
     setupBasicValue(varSlack);
-    d_linEq.trackVariable(varSlack);
+    d_linEq.trackRowIndex(d_tableau.basicToRowIndex(varSlack));
 
     //Add differences to the difference manager
     Polynomial::iterator i = poly.begin(), end = poly.end();
@@ -1176,7 +1175,6 @@ void TheoryArithPrivate::releaseArithVar(ArithVar v){
 
   d_constraintDatabase.removeVariable(v);
   d_partialModel.releaseArithVar(v);
-  d_linEq.maybeRemoveTracking(v);
 }
 
 ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool slack){
@@ -1188,70 +1186,19 @@ ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool slack){
   Assert(!d_partialModel.hasArithVar(x));
   Assert(x.getType().isReal()); // real or integer
 
-  // ArithVar varX = d_variables.size();
-  // d_variables.push_back(Node(x));
-
   ArithVar max = d_partialModel.getNumberOfVariables();
   ArithVar varX = d_partialModel.allocate(x, slack);
 
   bool reclaim =  max >= d_partialModel.getNumberOfVariables();;
 
-  if(reclaim){
-    // varX = d_pool.back();
-    // d_pool.pop_back();
-
-    // d_partialModel.setAssignment(varX, d_DELTA_ZERO, d_DELTA_ZERO);
-  }else{
-    // varX = d_numberOfVariables;
-    // ++d_numberOfVariables;
-
-    // d_slackVars.push_back(true);
-    // d_variableTypes.push_back(ATReal);
-
+  if(!reclaim){
     d_dualSimplex.increaseMax();
 
     d_tableau.increaseSize();
     d_tableauSizeHasBeenModified = true;
-
-    //d_partialModel.initialize(varX, d_DELTA_ZERO);
   }
-
-  // ArithType type;
-  // if(slack){
-  //   //The type computation is not quite accurate for Rationals that are integral.
-  //   //We'll use the isIntegral check from the polynomial package instead.
-  //   Polynomial p = Polynomial::parsePolynomial(x);
-  //   type = p.isIntegral() ? ATInteger : ATReal;
-  // }else{
-  //   type = nodeToArithType(x);
-  // }
-  // d_variableTypes[varX] = type;
-  // d_slackVars[varX] = slack;
-
   d_constraintDatabase.addVariable(varX);
 
-  //d_partialModel.setArithVar(x,varX);
-
-  // Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl;
-
-  // if(slack){
-  //   //The type computation is not quite accurate for Rationals that are integral.
-  //   //We'll use the isIntegral check from the polynomial package instead.
-  //   Polynomial p = Polynomial::parsePolynomial(x);
-  //   d_variableTypes.push_back(p.isIntegral() ? ATInteger : ATReal);
-  // }else{
-  //   d_variableTypes.push_back(nodeToArithType(x));
-  // }
-
-  // d_slackVars.push_back(slack);
-
-  // d_simplex.increaseMax();
-
-  // d_tableau.increaseSize();
-  // d_tableauSizeHasBeenModified = true;
-
-  // d_constraintDatabase.addVariable(varX);
-
   Debug("arith::arithvar") << x << " |-> " << varX << endl;
 
   Assert(!d_partialModel.hasUpperBound(varX));
@@ -1609,9 +1556,9 @@ void TheoryArithPrivate::branchVector(const std::vector<ArithVar>& lemmas){
 bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
   Assert(d_qflraStatus != Result::SAT);
 
-  d_partialModel.stopQueueingAtBoundQueue();
+  d_partialModel.stopQueueingBoundCounts();
   UpdateTrackingCallback utcb(&d_linEq);
-  d_partialModel.processAtBoundQueue(utcb);
+  d_partialModel.processBoundsQueue(utcb);
   d_linEq.startTrackingBoundCounts();
 
   bool noPivotLimit = Theory::fullEffort(effortLevel) ||
@@ -1701,7 +1648,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
 
   // TODO Save zeroes with no conflicts
   d_linEq.stopTrackingBoundCounts();
-  d_partialModel.startQueueingAtBoundQueue();
+  d_partialModel.startQueueingBoundCounts();
 
   return emmittedConflictOrSplit;
 }
@@ -2161,7 +2108,11 @@ void TheoryArithPrivate::propagate(Theory::Effort e) {
      (options::arithPropagationMode() == BOUND_INFERENCE_PROP ||
       options::arithPropagationMode() == BOTH_PROP)
      && hasAnyUpdates()){
-    propagateCandidates();
+    if(options::newProp()){
+      propagateCandidatesNew();
+    }else{
+      propagateCandidates();
+    }
   }else{
     clearUpdates();
   }
@@ -2432,37 +2383,6 @@ void TheoryArithPrivate::notifyRestart(){
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
 
   ++d_restartsCounter;
-#warning "removing restart"
-  // return;
-
-  // uint32_t currSize = d_tableau.size();
-  // uint32_t copySize = d_smallTableauCopy.size();
-
-  // Debug("arith::reset") << "resetting" << d_restartsCounter << endl;
-  // Debug("arith::reset") << "curr " << currSize << " copy " << copySize << endl;
-  // Debug("arith::reset") << "tableauSizeHasBeenModified " << d_tableauSizeHasBeenModified << endl;
-
-  // if(d_tableauSizeHasBeenModified){
-  //   Debug("arith::reset") << "row has been added must copy " << d_restartsCounter << endl;
-  //   d_smallTableauCopy = d_tableau;
-  //   d_tableauSizeHasBeenModified = false;
-  // }else if( d_restartsCounter >= RESET_START){
-  //   if(copySize >= currSize * 1.1 ){
-  //     Debug("arith::reset") << "size has shrunk " << d_restartsCounter << endl;
-  //     ++d_statistics.d_smallerSetToCurr;
-  //     d_smallTableauCopy = d_tableau;
-  //   }else if(d_tableauResetDensity * copySize <=  currSize){
-  //     d_errorSet.popAllSignals();
-  //     if(safeToReset()){
-  //       Debug("arith::reset") << "resetting " << d_restartsCounter << endl;
-  //       ++d_statistics.d_currSetToSmaller;
-  //       d_tableau = d_smallTableauCopy;
-  //     }else{
-  //       Debug("arith::reset") << "not safe to reset at the moment " << d_restartsCounter << endl;
-  //     }
-  //   }
-  // }
-  // Assert(unenqueuedVariablesAreConsistent());
 }
 
 bool TheoryArithPrivate::entireStateIsConsistent(const string& s){
@@ -2629,19 +2549,31 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound
         }
         // I think this can be skipped if canBePropagated is true
         //d_learnedBounds.push(bestImplied);
+        if(Debug.isOn("arith::prop")){
+          Debug("arith::prop") << "success " << bestImplied << endl;
+          d_partialModel.printModel(basic, Debug("arith::prop"));
+        }
         return true;
       }
+      if(Debug.isOn("arith::prop")){
+        Debug("arith::prop") << "failed " << basic << " " << bound << assertedToTheTheory << " " <<
+          canBePropagated << " " << hasProof << endl;
+        d_partialModel.printModel(basic, Debug("arith::prop"));
+      }
     }
+  }else if(Debug.isOn("arith::prop")){
+    Debug("arith::prop") << "false " << bound << " ";
+    d_partialModel.printModel(basic, Debug("arith::prop"));
   }
   return false;
 }
 
 void TheoryArithPrivate::propagateCandidate(ArithVar basic){
   bool success = false;
-  if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasLowerBounds(basic)){
+  if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasBounds(basic, false)){
     success |= propagateCandidateLowerBound(basic);
   }
-  if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasUpperBounds(basic)){
+  if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasBounds(basic, true)){
     success |= propagateCandidateUpperBound(basic);
   }
   if(success){
@@ -2652,6 +2584,8 @@ void TheoryArithPrivate::propagateCandidate(ArithVar basic){
 void TheoryArithPrivate::propagateCandidates(){
   TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
 
+  Debug("arith::prop") << "propagateCandidates begin" << endl;
+
   Assert(d_candidateBasics.empty());
 
   if(d_updatedBounds.empty()){ return; }
@@ -2685,6 +2619,278 @@ void TheoryArithPrivate::propagateCandidates(){
     Assert(d_tableau.isBasic(candidate));
     propagateCandidate(candidate);
   }
+  Debug("arith::prop") << "propagateCandidates end" << endl << endl << endl;
+}
+
+void TheoryArithPrivate::propagateCandidatesNew(){
+  /* Four criteria must be met for progagation on a variable to happen using a row:
+   * 0: A new bound has to have been added to the row.
+   * 1: The hasBoundsCount for the row must be "full" or be full minus one variable
+   *    (This is O(1) to check, but requires book keeping.)
+   * 2: The current assignment must be strictly smaller/greater than the current bound.
+   *    assign(x) < upper(x)
+   *    (This is O(1) to compute.)
+   * 3: There is a bound that is strictly smaller/greater than the current assignment.
+   *    assign(x) < c for some x <= c literal
+   *    (This is O(log n) to compute.)
+   * 4: The implied bound on x is strictly smaller/greater than the current bound.
+   *    (This is O(n) to compute.)
+   */
+
+  TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
+  Debug("arith::prop") << "propagateCandidatesNew begin" << endl;
+
+  Assert(d_qflraStatus == Result::SAT);
+  if(d_updatedBounds.empty()){ return; }
+  dumpUpdatedBoundsToRows();
+  Assert(d_updatedBounds.empty());
+
+  if(!d_candidateRows.empty()){
+    UpdateTrackingCallback utcb(&d_linEq);
+    d_partialModel.processBoundsQueue(utcb);
+  }
+
+  while(!d_candidateRows.empty()){
+    RowIndex candidate = d_candidateRows.back();
+    d_candidateRows.pop_back();
+    propagateCandidateRow(candidate);
+  }
+  Debug("arith::prop") << "propagateCandidatesNew end" << endl << endl << endl;
+}
+
+bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{
+  int cmp = ub ? d_partialModel.cmpAssignmentUpperBound(v)
+    : d_partialModel.cmpAssignmentLowerBound(v);
+  bool hasSlack = ub ? cmp < 0 : cmp > 0;
+  if(hasSlack){
+    ConstraintType t = ub ? UpperBound : LowerBound;
+    const DeltaRational& a = d_partialModel.getAssignment(v);
+
+    Constraint strongestPossible = d_constraintDatabase.getBestImpliedBound(v, t, a);
+    if(strongestPossible == NullConstraint){
+      return false;
+    }else{
+      bool assertedToTheTheory = strongestPossible->assertedToTheTheory();
+      bool canBePropagated = strongestPossible->canBePropagated();
+      bool hasProof = strongestPossible->hasProof();
+
+      return !assertedToTheTheory && canBePropagated && !hasProof;
+    }
+  }else{
+    return false;
+  }
+}
+
+bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){
+  Debug("arith::prop") << "  attemptSingleton" << ridx;
+
+  const Tableau::Entry* ep;
+  ep = d_linEq.rowLacksBound(ridx, rowUp, ARITHVAR_SENTINEL);
+  Assert(ep != NULL);
+
+  ArithVar v = ep->getColVar();
+  const Rational& coeff = ep->getCoefficient();
+
+  // 0 = c * v + \sum rest
+  // Suppose rowUp
+  // - c * v = \sum rest \leq D
+  // if c > 0, v \geq -D/c so !vUp
+  // if c < 0, v \leq -D/c so  vUp
+  // Suppose not rowUp
+  // - c * v = \sum rest \geq D
+  // if c > 0, v \leq -D/c so  vUp
+  // if c < 0, v \geq -D/c so !vUp
+  bool vUp = (rowUp == ( coeff.sgn() < 0));
+
+  Debug("arith::prop") << "  " << rowUp << " " << v << " " << coeff << " " << vUp << endl;
+  Debug("arith::prop") << "  " << propagateMightSucceed(v, vUp) << endl;
+
+  if(propagateMightSucceed(v, vUp)){
+    DeltaRational dr = d_linEq.computeRowBound(ridx, rowUp, v);
+    DeltaRational bound = dr / (- coeff);
+    return tryToPropagate(ridx, rowUp, v, vUp, bound);
+  }
+  return false;
+}
+
+bool TheoryArithPrivate::attemptFull(RowIndex ridx, bool rowUp){
+  Debug("arith::prop") << "  attemptFull" << ridx << endl;
+
+  vector<const Tableau::Entry*> candidates;
+
+  for(Tableau::RowIterator i = d_tableau.ridRowIterator(ridx); !i.atEnd(); ++i){
+    const Tableau::Entry& e =*i;
+    const Rational& c = e.getCoefficient();
+    ArithVar v = e.getColVar();
+    bool vUp = (rowUp == (c.sgn() < 0));
+    if(propagateMightSucceed(v, vUp)){
+      candidates.push_back(&e);
+    }
+  }
+  if(candidates.empty()){ return false; }
+
+  const DeltaRational slack =
+    d_linEq.computeRowBound(ridx, rowUp, ARITHVAR_SENTINEL);
+  bool any = false;
+  vector<const Tableau::Entry*>::const_iterator i, iend;
+  for(i = candidates.begin(), iend = candidates.end(); i != iend; ++i){
+    const Tableau::Entry* ep = *i;
+    const Rational& c = ep->getCoefficient();
+    ArithVar v = ep->getColVar();
+
+    // See the comment for attemptSingleton()
+    bool activeUp = (rowUp == (c.sgn() > 0));
+    bool vUb = (rowUp == (c.sgn() < 0));
+
+    const DeltaRational& activeBound = activeUp ?
+      d_partialModel.getUpperBound(v):
+      d_partialModel.getLowerBound(v);
+
+    DeltaRational contribution = activeBound * c;
+    DeltaRational impliedBound = (slack - contribution)/(-c);
+
+    bool success = tryToPropagate(ridx, rowUp, v, vUb, impliedBound);
+    any |= success;
+  }
+  return any;
+}
+
+bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, bool vUb, const DeltaRational& bound){
+
+  bool weaker = vUb ? d_partialModel.strictlyLessThanUpperBound(v, bound):
+    d_partialModel.strictlyGreaterThanLowerBound(v, bound);
+  if(weaker){
+    ConstraintType t = vUb ? UpperBound : LowerBound;
+    Constraint implied = d_constraintDatabase.getBestImpliedBound(v, t, bound);
+    if(implied != NullConstraint){
+      return rowImplicationCanBeApplied(ridx, rowUp, implied);
+    }
+  }
+  return false;
+}
+
+Node flattenImplication(Node imp){
+  NodeBuilder<> nb(kind::OR);
+  Node left = imp[0];
+  Node right = imp[1];
+
+  if(left.getKind() == kind::AND){
+    for(Node::iterator i = left.begin(), iend = left.end(); i != iend; ++i) {
+      nb << (*i).negate();
+    }
+  }else{
+    nb << left.negate();
+  }
+
+  if(right.getKind() == kind::OR){
+    for(Node::iterator i = right.begin(), iend = right.end(); i != iend; ++i) {
+      nb << *i;
+    }
+  }else{
+    nb << right;
+  }
+
+  return nb;
+}
+
+bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, Constraint implied){
+  Assert(implied != NullConstraint);
+  ArithVar v = implied->getVariable();
+
+  bool assertedToTheTheory = implied->assertedToTheTheory();
+  bool canBePropagated = implied->canBePropagated();
+  bool hasProof = implied->hasProof();
+
+  Debug("arith::prop") << "arith::prop" << v
+                       << " " << assertedToTheTheory
+                       << " " << canBePropagated
+                       << " " << hasProof
+                       << endl;
+
+  if(implied->negationHasProof()){
+    Warning() << "the negation of " <<  implied << " : " << endl
+              << "has proof " << implied->getNegation() << endl
+              << implied->getNegation()->explainForConflict() << endl;
+  }
+
+  if(!assertedToTheTheory && canBePropagated && !hasProof ){
+    vector<Constraint> explain;
+    d_linEq.propagateRow(explain, ridx, rowUp, implied);
+    if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){
+      Node implication = implied->makeImplication(explain);
+      Node clause = flattenImplication(implication);
+      outputLemma(clause);
+    }else{
+      implied->impliedBy(explain);
+    }
+    return true;
+  }
+
+  if(Debug.isOn("arith::prop")){
+    Debug("arith::prop")
+      << "failed " << v << " " << assertedToTheTheory << " "
+      << canBePropagated << " " << hasProof << " " << implied << endl;
+    d_partialModel.printModel(v, Debug("arith::prop"));
+  }
+  return false;
+}
+
+double fRand(double fMin, double fMax)
+{
+    double f = (double)rand() / RAND_MAX;
+    return fMin + f * (fMax - fMin);
+}
+
+bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
+  BoundCounts hasCount = d_linEq.hasBoundCount(ridx);
+  uint32_t rowLength = d_tableau.getRowLength(ridx);
+
+  bool success = false;
+  static int instance = 0;
+  ++instance;
+
+  Debug("arith::prop")
+    << "propagateCandidateRow " << instance << " attempt " << rowLength << " " <<  hasCount << endl;
+
+  if(rowLength >= options::arithPropagateMaxLength()){
+    if(fRand(0.0,1.0) >= double(options::arithPropagateMaxLength())/rowLength){
+      return false;
+    }
+  }
+
+  if(hasCount.lowerBoundCount() == rowLength){
+    success |= attemptFull(ridx, false);
+  }else if(hasCount.lowerBoundCount() + 1 == rowLength){
+    success |= attemptSingleton(ridx, false);
+  }
+
+  if(hasCount.upperBoundCount() == rowLength){
+    success |= attemptFull(ridx, true);
+  }else if(hasCount.upperBoundCount() + 1 == rowLength){
+    success |= attemptSingleton(ridx, true);
+  }
+  return success;
+}
+
+void TheoryArithPrivate::dumpUpdatedBoundsToRows(){
+  Assert(d_candidateRows.empty());
+  DenseSet::const_iterator i = d_updatedBounds.begin();
+  DenseSet::const_iterator end = d_updatedBounds.end();
+  for(; i != end; ++i){
+    ArithVar var = *i;
+    if(d_tableau.isBasic(var)){
+      RowIndex ridx = d_tableau.basicToRowIndex(var);
+      d_candidateRows.softAdd(ridx);
+    }else{
+      Tableau::ColIterator basicIter = d_tableau.colIterator(var);
+      for(; !basicIter.atEnd(); ++basicIter){
+        const Tableau::Entry& entry = *basicIter;
+        RowIndex ridx = entry.getRowIndex();
+        d_candidateRows.softAdd(ridx);
+      }
+    }
+  }
+  d_updatedBounds.purge();
 }
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 7b37a813f..e522bb8c8 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -105,7 +105,7 @@ private:
   // TODO A better would be:
   //context::CDO<bool> d_nlIncomplete;
 
-  BoundCountingVector d_boundTracking;
+  BoundInfoMap d_rowTracking;
 
   /**
    * The constraint database associated with the theory.
@@ -463,12 +463,25 @@ private:
 
   /** Tracks the basic variables where propagation might be possible. */
   DenseSet d_candidateBasics;
+  DenseSet d_candidateRows;
 
   bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
   void clearUpdates();
 
   void revertOutOfConflict();
 
+  void propagateCandidatesNew();
+  void dumpUpdatedBoundsToRows();
+  bool propagateCandidateRow(RowIndex rid);
+  bool propagateMightSucceed(ArithVar v, bool ub) const;
+  /** Attempt to perform a row propagation where there is at most 1 possible variable.*/
+  bool attemptSingleton(RowIndex ridx, bool rowUp);
+  /** Attempt to perform a row propagation where every variable is a potential candidate.*/
+  bool attemptFull(RowIndex ridx, bool rowUp);
+  bool tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, bool vUp, const DeltaRational& bound);
+  bool rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, Constraint bestImplied);
+
+
   void propagateCandidates();
   void propagateCandidate(ArithVar basic);
   bool propagateCandidateBound(ArithVar basic, bool upperBound);