This commit merges the branch arithmetic/propagation-again into trunk.

	- This adds code for bounds refinement, and conflict weakening.
	- This adds util/boolean_simplification.h.
	- This adds a propagation manager to theory of arithmetic.
	- Propagation is disabled by default.
	- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
	- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.

22 files changed, 1894 insertions, 500 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 12088b493..c5534560b 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -11,6 +11,9 @@ libarith_la_SOURCES = \
 	arith_rewriter.cpp \
 	arith_static_learner.h \
 	arith_static_learner.cpp \
+	arith_prop_manager.h \
+	arith_prop_manager.cpp \
+	arithvar_node_map.h \
 	normal_form.h\
 	normal_form.cpp \
 	arith_utilities.h \
diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index 4905f4dc5..872c25e3b 100644
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -160,7 +160,7 @@ void ArithPriorityQueue::transitionToDifferenceMode() {
   Assert(d_diffQueue.empty());
 
   Debug("arith::priorityqueue") << "transitionToDifferenceMode()" << endl;
-  d_varSet.clear();
+  d_varSet.purge();
 
   ArithVarArray::const_iterator i = d_candidates.begin(), end = d_candidates.end();
   for(; i != end; ++i){
@@ -232,18 +232,18 @@ void ArithPriorityQueue::clear(){
   switch(d_modeInUse){
   case Collection:
     d_candidates.clear();
-    d_varSet.clear();
+    d_varSet.purge();
     break;
   case VariableOrder:
     if(!d_varOrderQueue.empty()) {
       d_varOrderQueue.clear();
-      d_varSet.clear();
+      d_varSet.purge();
     }
     break;
   case Difference:
     if(!d_diffQueue.empty()){
       d_diffQueue.clear();
-      d_varSet.clear();
+      d_varSet.purge();
     }
     break;
   default:
diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp
new file mode 100644
index 000000000..a09bed8e8
--- /dev/null
+++ b/src/theory/arith/arith_prop_manager.cpp
@@ -0,0 +1,174 @@
+
+#include "theory/arith/arith_prop_manager.h"
+
+#include "theory/arith/arith_utilities.h"
+#include "context/context.h"
+#include "context/cdlist.h"
+#include "context/cdmap.h"
+#include "context/cdo.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+using namespace CVC4::kind;
+using namespace std;
+
+
+bool ArithPropManager::isAsserted(TNode n) const{
+  Node satValue = d_valuation.getSatValue(n);
+  if(satValue.isNull()){
+    return false;
+  }else{
+    //Assert(satValue.getConst<bool>());
+    return true;
+  }
+}
+
+// Node ArithPropManager::strictlyWeakerAssertedUpperBound(TNode n) const{
+//   Node weaker = n;
+//   do {
+//     weaker = d_propagator.getWeakerImpliedUpperBound(weaker);
+//   }while(!weaker.isNull() && !isAsserted(weaker));
+//   Assert(weaker != n);
+//   return weaker;
+// }
+
+// Node ArithPropManager::strictlyWeakerAssertedLowerBound(TNode n) const{
+//   Node weaker = n;
+//   do {
+//     weaker = d_propagator.getWeakerImpliedLowerBound(weaker);
+//   }while(!weaker.isNull() && !isAsserted(weaker));
+//   Assert(weaker != n);
+//   return weaker;
+// }
+
+Node ArithPropManager::strictlyWeakerAssertedUpperBound(ArithVar v, const DeltaRational& b) const{
+  Node bound = boundAsNode(true, v, b);
+
+  Assert(b.getInfinitesimalPart() <= 0);
+  bool largeEpsilon = (b.getInfinitesimalPart() < -1);
+
+  Node weaker = bound;
+  do {
+    if(largeEpsilon){
+      weaker = d_propagator.getBestImpliedUpperBound(weaker);
+      largeEpsilon = false;
+    }else{
+      weaker = d_propagator.getWeakerImpliedUpperBound(weaker);
+    }
+  }while(!weaker.isNull() && !isAsserted(weaker));
+  return weaker;
+}
+
+Node ArithPropManager::strictlyWeakerAssertedLowerBound(ArithVar v, const DeltaRational& b) const{
+  Debug("ArithPropManager") << "strictlyWeakerAssertedLowerBound" << endl;
+  Node bound = boundAsNode(false, v, b);
+
+  Assert(b.getInfinitesimalPart() >= 0);
+  bool largeEpsilon = (b.getInfinitesimalPart() > 1);
+
+  Node weaker = bound;
+  Debug("ArithPropManager") << bound << b << endl;
+  do {
+    if(largeEpsilon){
+      weaker = d_propagator.getBestImpliedLowerBound(weaker);
+      largeEpsilon = false;
+    }else{
+      weaker = d_propagator.getWeakerImpliedLowerBound(weaker);
+    }
+  }while(!weaker.isNull() && !isAsserted(weaker));
+  Debug("ArithPropManager") << "res: " << weaker << endl;
+  return weaker;
+}
+
+Node ArithPropManager::getBestImpliedLowerBound(ArithVar v, const DeltaRational& b) const{
+  Node bound = boundAsNode(false, v, b);
+  return d_propagator.getBestImpliedLowerBound(bound);
+}
+Node ArithPropManager::getBestImpliedUpperBound(ArithVar v, const DeltaRational& b) const{
+  Node bound = boundAsNode(true, v, b);
+  return d_propagator.getBestImpliedUpperBound(bound);
+}
+
+bool ArithPropManager::hasStrongerLowerBound(TNode n) const{
+  bool haveAcompilerWarning;
+  return true;
+}
+bool ArithPropManager::hasStrongerUpperBound(TNode n) const{
+  return true;
+}
+
+Node ArithPropManager::boundAsNode(bool upperbound, ArithVar var, const DeltaRational& b) const {
+  Assert((!upperbound) || (b.getInfinitesimalPart() <= 0) );
+  Assert(upperbound || (b.getInfinitesimalPart() >= 0) );
+
+  Node varAsNode = d_arithvarNodeMap.asNode(var);
+  Kind kind;
+  bool negate;
+  if(upperbound){
+    negate = b.getInfinitesimalPart() < 0;
+    kind = negate ? GEQ : LEQ;
+  } else{
+    negate = b.getInfinitesimalPart() > 0;
+    kind = negate ? LEQ : GEQ;
+  }
+
+  Node righthand = mkRationalNode(b.getNoninfinitesimalPart());
+  Node bAsNode = NodeBuilder<2>(kind) << varAsNode << righthand;
+
+  if(negate){
+    bAsNode = NodeBuilder<1>(NOT) << bAsNode;
+  }
+
+  return bAsNode;
+}
+
+bool ArithPropManager::propagateArithVar(bool upperbound, ArithVar var, const DeltaRational& b, TNode reason){
+  bool success = false;
+
+  ++d_statistics.d_propagateArithVarCalls;
+
+  Node bAsNode = boundAsNode(upperbound, var ,b);
+
+  Node bestImplied = upperbound ?
+    d_propagator.getBestImpliedUpperBound(bAsNode):
+    d_propagator.getBestImpliedLowerBound(bAsNode);
+
+  Debug("ArithPropManager") << upperbound <<","<< var <<","<< b <<","<< reason << endl
+                            << bestImplied << endl;
+
+  if(!bestImplied.isNull()){
+    bool asserted = isAsserted(bestImplied);
+
+    if( !asserted && !isPropagated(bestImplied)){
+      propagate(bestImplied, reason);
+      ++d_statistics.d_addedPropagation;
+      success = true;
+    }else if(!asserted){
+      ++d_statistics.d_alreadyPropagatedNode;
+    }else if(!isPropagated(bestImplied)){
+      ++d_statistics.d_alreadySetSatLiteral;
+    }
+  }
+  return success;
+}
+
+ArithPropManager::Statistics::Statistics():
+  d_propagateArithVarCalls("arith::prop-manager::propagateArithVarCalls",0),
+  d_addedPropagation("arith::prop-manager::addedPropagation",0),
+  d_alreadySetSatLiteral("arith::prop-manager::alreadySetSatLiteral",0),
+  d_alreadyPropagatedNode("arith::prop-manager::alreadyPropagatedNode",0)
+{
+  StatisticsRegistry::registerStat(&d_propagateArithVarCalls);
+  StatisticsRegistry::registerStat(&d_alreadySetSatLiteral);
+  StatisticsRegistry::registerStat(&d_alreadyPropagatedNode);
+  StatisticsRegistry::registerStat(&d_addedPropagation);
+}
+
+ArithPropManager::Statistics::~Statistics()
+{
+  StatisticsRegistry::unregisterStat(&d_propagateArithVarCalls);
+  StatisticsRegistry::unregisterStat(&d_alreadySetSatLiteral);
+  StatisticsRegistry::unregisterStat(&d_alreadyPropagatedNode);
+  StatisticsRegistry::unregisterStat(&d_addedPropagation);
+}
diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h
new file mode 100644
index 000000000..1fd23dd62
--- /dev/null
+++ b/src/theory/arith/arith_prop_manager.h
@@ -0,0 +1,144 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H
+#define __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H
+
+#include "theory/valuation.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar_node_map.h"
+#include "theory/arith/unate_propagator.h"
+#include "theory/arith/delta_rational.h"
+#include "context/context.h"
+#include "context/cdlist.h"
+#include "context/cdmap.h"
+#include "context/cdo.h"
+
+#include "util/stats.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class PropManager {
+private:
+  context::CDList<TNode> d_propagated;
+  context::CDO<uint32_t> d_propagatedPos;
+  typedef context::CDMap<TNode, TNode, TNodeHashFunction> ExplainMap;
+
+  ExplainMap d_explanationMap;
+
+  context::CDList<Node> d_reasons;
+
+public:
+
+  PropManager(context::Context* c):
+    d_propagated(c),
+    d_propagatedPos(c, 0),
+    d_explanationMap(c),
+    d_reasons(c)
+  { }
+
+  bool isPropagated(TNode n) const {
+    return d_explanationMap.find(n) != d_explanationMap.end();
+  }
+
+  void propagate(TNode n, Node reason) {
+    Assert(!isPropagated(n));
+    Assert(reason.getKind() == kind::AND);
+
+    d_explanationMap.insert(n, reason);
+
+    d_reasons.push_back(reason);
+    d_propagated.push_back(n);
+
+    //std::cout << n  << std::endl << "<="<< reason<< std::endl;
+  }
+
+  bool hasMorePropagations() const {
+    return d_propagatedPos < d_propagated.size();
+  }
+
+  TNode getPropagation() {
+    Assert(hasMorePropagations());
+    TNode prop = d_propagated[d_propagatedPos];
+    d_propagatedPos = d_propagatedPos + 1;
+    return prop;
+  }
+
+  TNode explain(TNode n) const {
+    Assert(isPropagated(n));
+    ExplainMap::iterator p = d_explanationMap.find(n);
+    return (*p).second;
+  }
+
+};/* class PropManager */
+
+class ArithPropManager : public PropManager {
+private:
+  const ArithVarNodeMap& d_arithvarNodeMap;
+  const ArithUnatePropagator& d_propagator;
+  Valuation d_valuation;
+
+public:
+  ArithPropManager(context::Context* c,
+                   const ArithVarNodeMap& map,
+                   const ArithUnatePropagator& prop,
+                   Valuation v):
+    PropManager(c), d_arithvarNodeMap(map), d_propagator(prop), d_valuation(v)
+  {}
+
+  /**
+   * Returns true if the node has a value in sat solver in the current context.
+   * In debug mode this fails an Assert() if the node has a negative assignment.
+   */
+  bool isAsserted(TNode n) const;
+
+  /** Returns true if a bound was added. */
+  bool propagateArithVar(bool upperbound, ArithVar var, const DeltaRational& b, TNode reason);
+
+  Node boundAsNode(bool upperbound, ArithVar var, const DeltaRational& b) const;
+
+  Node strictlyWeakerLowerBound(TNode n) const{
+    return d_propagator.getWeakerImpliedLowerBound(n);
+  }
+  Node strictlyWeakerUpperBound(TNode n) const{
+    return d_propagator.getWeakerImpliedUpperBound(n);
+  }
+
+
+  //Node strictlyWeakerAssertedUpperBound(TNode n) const;
+  //Node strictlyWeakerAssertedLowerBound(TNode n) const;
+
+  Node strictlyWeakerAssertedUpperBound(ArithVar v, const DeltaRational& b) const;
+
+  Node strictlyWeakerAssertedLowerBound(ArithVar v, const DeltaRational& b) const;
+
+  Node getBestImpliedLowerBound(ArithVar v, const DeltaRational& b) const;
+  Node getBestImpliedUpperBound(ArithVar v, const DeltaRational& b) const;
+
+  bool hasStrongerLowerBound(TNode current) const;
+  bool hasStrongerUpperBound(TNode current) const;
+
+  bool containsLiteral(TNode n) const {
+    return d_propagator.containsLiteral(n);
+  }
+
+private:
+  class Statistics {
+  public:
+    IntStat d_propagateArithVarCalls;
+    IntStat d_addedPropagation;
+    IntStat d_alreadySetSatLiteral;
+    IntStat d_alreadyPropagatedNode;
+
+    Statistics();
+    ~Statistics();
+  };
+  Statistics d_statistics;
+};
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H */
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 59b4e9bef..78b77eb00 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -25,6 +25,7 @@
 #include "util/rational.h"
 #include "expr/node.h"
 #include "expr/attribute.h"
+#include "theory/arith/delta_rational.h"
 #include <vector>
 #include <stdint.h>
 #include <limits>
@@ -204,6 +205,38 @@ inline int deltaCoeff(Kind k){
   }
 }
 
+template <bool selectLeft>
+inline TNode getSide(TNode assertion, Kind simpleKind){
+  switch(simpleKind){
+  case kind::LT:
+  case kind::GT:
+  case kind::DISTINCT:
+    return selectLeft ? (assertion[0])[0] : (assertion[0])[1];
+  case kind::LEQ:
+  case kind::GEQ:
+  case kind::EQUAL:
+    return selectLeft ? assertion[0] : assertion[1];
+  default:
+    Unreachable();
+    return TNode::null();
+  }
+}
+
+inline DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){
+  TNode right = getSide<false>(assertion, simpleKind);
+
+  Assert(right.getKind() == kind::CONST_RATIONAL);
+  const Rational& noninf = right.getConst<Rational>();
+
+  Rational inf = Rational(Integer(deltaCoeff(simpleKind)));
+  return DeltaRational(noninf, inf);
+}
+
+inline DeltaRational asDeltaRational(TNode n){
+  Kind simp = simplifiedKind(n);
+  return determineRightConstant(n, simp);
+}
+
  /**
   * Takes two nodes with exactly 2 children,
   * the second child of both are of kind CONST_RATIONAL,
@@ -236,6 +269,19 @@ inline Node negateConjunctionAsClause(TNode conjunction){
   return orBuilder;
 }
 
+inline Node maybeUnaryConvert(NodeBuilder<>& builder){
+  Assert(builder.getKind() == kind::OR ||
+         builder.getKind() == kind::AND ||
+         builder.getKind() == kind::PLUS ||
+         builder.getKind() == kind::MULT);
+  Assert(builder.getNumChildren() >= 1);
+  if(builder.getNumChildren() == 1){
+    return builder[0];
+  }else{
+    return builder;
+  }
+}
+
 }; /* namesapce arith */
 }; /* namespace theory */
 }; /* namespace CVC4 */
diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h
new file mode 100644
index 000000000..aca61878d
--- /dev/null
+++ b/src/theory/arith/arithvar_node_map.h
@@ -0,0 +1,59 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
+#define __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
+
+
+#include "theory/arith/arith_utilities.h"
+#include "context/context.h"
+#include "context/cdlist.h"
+#include "context/cdmap.h"
+#include "context/cdo.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class ArithVarNodeMap {
+private:
+  /**
+   * Bidirectional map between Nodes and ArithVars.
+   */
+  NodeToArithVarMap d_nodeToArithVarMap;
+  ArithVarToNodeMap d_arithVarToNodeMap;
+
+public:
+  ArithVarNodeMap() {}
+
+  inline bool hasArithVar(TNode x) const {
+    return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
+  }
+
+  inline ArithVar asArithVar(TNode x) const{
+    Assert(hasArithVar(x));
+    Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL);
+    return (d_nodeToArithVarMap.find(x))->second;
+  }
+  inline Node asNode(ArithVar a) const{
+    Assert(d_arithVarToNodeMap.find(a) != d_arithVarToNodeMap.end());
+    return (d_arithVarToNodeMap.find(a))->second;
+  }
+
+  inline void setArithVar(TNode x, ArithVar a){
+    Assert(!hasArithVar(x));
+    Assert(d_arithVarToNodeMap.find(a) == d_arithVarToNodeMap.end());
+    d_arithVarToNodeMap[a] = x;
+    d_nodeToArithVarMap[x] = a;
+  }
+
+  const ArithVarToNodeMap& getArithVarToNodeMap() const {
+    return d_arithVarToNodeMap;
+  }
+
+};/* class ArithVarNodeMap */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */
diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h
index 0d59e3aea..4cd205172 100644
--- a/src/theory/arith/arithvar_set.h
+++ b/src/theory/arith/arithvar_set.h
@@ -72,9 +72,12 @@ public:
     return d_posVector.size();
   }
 
-  void clear(){
+  void purge() {
+    for(VarList::const_iterator i=d_list.begin(), endIter=d_list.end();i!= endIter; ++i){
+      d_posVector[*i] = ARITHVAR_SENTINEL;
+    }
     d_list.clear();
-    d_posVector.clear();
+    Assert(empty());
   }
 
   void increaseSize(ArithVar max){
@@ -117,6 +120,16 @@ public:
   const_iterator begin() const{ return d_list.begin(); }
   const_iterator end() const{ return d_list.end(); }
 
+  /**
+   * Invalidates iterators.
+   * Adds x to the set if it is not already in the set.
+   */
+  void softAdd(ArithVar x){
+    if(!isMember(x)){
+      add(x);
+    }
+  }
+
   const VarList& getList() const{
     return d_list;
   }
@@ -125,8 +138,16 @@ public:
   void remove(ArithVar x){
     Assert(isMember(x));
     swapToBack(x);
-    d_posVector[x] = ARITHVAR_SENTINEL;
+    Assert(d_list.back() == x);
+    pop_back();
+  }
+
+  ArithVar pop_back() {
+    Assert(!empty());
+    ArithVar atBack = d_list.back();
+    d_posVector[atBack] = ARITHVAR_SENTINEL;
     d_list.pop_back();
+    return atBack;
   }
 
  private:
diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h
index 68c5e18c9..43ccd7815 100644
--- a/src/theory/arith/ordered_set.h
+++ b/src/theory/arith/ordered_set.h
@@ -1,3 +1,4 @@
+#include <map>
 #include <set>
 #include "expr/kind.h"
 #include "expr/node.h"
@@ -9,16 +10,84 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
+inline const Rational& rightHandRational(TNode ineq){
+  Assert(ineq.getKind() == kind::LEQ
+         || ineq.getKind() == kind::GEQ
+         || ineq.getKind() == kind::EQUAL);
+  TNode righthand = ineq[1];
+  Assert(righthand.getKind() == kind::CONST_RATIONAL);
+  return righthand.getConst<Rational>();
+}
 
-typedef std::set<TNode, RightHandRationalLT> OrderedSet;
+class BoundValueEntry {
+private:
+  const Rational& value;
+  TNode d_leq, d_geq;
 
-struct SetCleanupStrategy{
-  static void cleanup(OrderedSet* l){
-    Debug("arithgc") << "cleaning up  " << l << "\n";
-    delete l;
+  BoundValueEntry(const Rational& v, TNode l, TNode g):
+    value(v),
+    d_leq(l),
+    d_geq(g)
+  {}
+
+public:
+  Node getLeq() const{
+    Assert(hasLeq());
+    return d_leq;
+  }
+  Node getGeq() const{
+    Assert(hasGeq());
+    return d_geq;
+  }
+
+  static BoundValueEntry mkFromLeq(TNode leq){
+    Assert(leq.getKind() == kind::LEQ);
+    return BoundValueEntry(rightHandRational(leq), leq, TNode::null());
+  }
+
+  static BoundValueEntry mkFromGeq(TNode geq){
+    Assert(geq.getKind() == kind::GEQ);
+    return BoundValueEntry(rightHandRational(geq), TNode::null(), geq);
+  }
+
+  void addLeq(TNode leq){
+    Assert(leq.getKind() == kind::LEQ);
+    Assert(rightHandRational(leq) == getValue());
+    Assert(!hasLeq());
+    d_leq = leq;
+  }
+
+  void addGeq(TNode geq){
+    Assert(geq.getKind() == kind::GEQ);
+    Assert(rightHandRational(geq) == getValue());
+    Assert(!hasGeq());
+    d_geq = geq;
+  }
+
+  bool hasGeq() const { return d_geq != TNode::null(); }
+  bool hasLeq() const { return d_leq != TNode::null(); }
+
+
+  const Rational& getValue() const{
+    return value;
+  }
+
+  bool operator<(const BoundValueEntry& other){
+    return value < other.value;
   }
 };
 
+typedef std::map<Rational, BoundValueEntry> BoundValueSet;
+
+typedef std::set<TNode, RightHandRationalLT> EqualValueSet;
+
+// struct SetCleanupStrategy{
+//   static void cleanup(OrderedSet* l){
+//     Debug("arithgc") << "cleaning up  " << l << "\n";
+//     delete l;
+//   }
+// };
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 39685a2a1..3cd8ed926 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -184,6 +184,21 @@ bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool
   }
 }
 
+bool ArithPartialModel::equalsLowerBound(ArithVar x, const DeltaRational& c){
+  if(!hasLowerBound(x)){
+    return false;
+  }else{
+    return c == d_lowerBound[x];
+  }
+}
+bool ArithPartialModel::equalsUpperBound(ArithVar x, const DeltaRational& c){
+  if(!hasUpperBound(x)){
+    return false;
+  }else{
+    return c == d_upperBound[x];
+  }
+}
+
 bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){
   if(!hasUpperBound(x)){
     // u = \intfy
@@ -216,6 +231,30 @@ bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){
   return  d_lowerBound[x] < d_assignment[x];
 }
 
+/**
+ * x <= u
+ * ? c < u
+ */
+bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){
+  Assert(inMaps(x));
+  if(!hasUpperBound(x)){ // u = \infty
+    return true;
+  }
+  return c < d_upperBound[x];
+}
+
+/**
+ * x <= u
+ * ? c < u
+ */
+bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){
+  Assert(inMaps(x));
+  if(!hasLowerBound(x)){ // l = -\infty
+    return true;
+  }
+  return  d_lowerBound[x] < c;
+}
+
 bool ArithPartialModel::assignmentIsConsistent(ArithVar x){
   const DeltaRational& beta = getAssignment(x);
 
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 2edfdebca..171c74942 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -48,8 +48,8 @@ private:
 
   context::CDVector<DeltaRational> d_upperBound;
   context::CDVector<DeltaRational> d_lowerBound;
-  context::CDVector<TNode> d_upperConstraint;
-  context::CDVector<TNode> d_lowerConstraint;
+  context::CDVector<Node> d_upperConstraint;
+  context::CDVector<Node> d_lowerConstraint;
 
   bool d_deltaIsSafe;
   Rational d_delta;
@@ -68,10 +68,10 @@ public:
     d_hasSafeAssignment(),
     d_assignment(),
     d_safeAssignment(),
-    d_upperBound(c, false),
-    d_lowerBound(c, false),
-    d_upperConstraint(c,false),
-    d_lowerConstraint(c,false),
+    d_upperBound(c, true),
+    d_lowerBound(c, true),
+    d_upperConstraint(c,true),
+    d_lowerConstraint(c,true),
     d_deltaIsSafe(false),
     d_delta(-1,1),
     d_history()
@@ -114,17 +114,32 @@ public:
 
 
   /**
-   * x <= l
+   * x >= l
    * ? c < l
    */
   bool belowLowerBound(ArithVar x, const DeltaRational& c, bool strict);
 
   /**
    * x <= u
-   * ? c < u
+   * ? c > u
    */
   bool aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict);
 
+  bool equalsLowerBound(ArithVar x, const DeltaRational& c);
+  bool equalsUpperBound(ArithVar x, const DeltaRational& c);
+
+  /**
+   * x <= u
+   * ? c < u
+   */
+  bool strictlyBelowUpperBound(ArithVar x, const DeltaRational& c);
+
+  /**
+   * x <= u
+   * ? c < u
+   */
+  bool strictlyAboveLowerBound(ArithVar x, const DeltaRational& c);
+
   bool strictlyBelowUpperBound(ArithVar x);
   bool strictlyAboveLowerBound(ArithVar x);
   bool assignmentIsConsistent(ArithVar x);
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 1a9c39984..b804cb1aa 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -14,6 +14,33 @@ static const uint32_t NUM_CHECKS = 10;
 static const bool CHECK_AFTER_PIVOT = true;
 static const uint32_t VARORDER_CHECK_PERIOD = 200;
 
+SimplexDecisionProcedure::SimplexDecisionProcedure(ArithPropManager& propManager,
+                                                   ArithPartialModel& pm,
+                                                   Tableau& tableau) :
+  d_partialModel(pm),
+  d_tableau(tableau),
+  d_queue(pm, tableau),
+  d_propManager(propManager),
+  d_numVariables(0),
+  d_delayedLemmas(),
+  d_ZERO(0),
+  d_DELTA_ZERO(0,0)
+{
+  switch(Options::ArithPivotRule rule = Options::current()->pivotRule) {
+  case Options::MINIMUM:
+    d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
+    break;
+  case Options::BREAK_TIES:
+    d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES);
+    break;
+  case Options::MAXIMUM:
+    d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM);
+    break;
+  default:
+    Unhandled(rule);
+  }
+}
+
 SimplexDecisionProcedure::Statistics::Statistics():
   d_statPivots("theory::arith::pivots",0),
   d_statUpdates("theory::arith::updates",0),
@@ -31,6 +58,13 @@ SimplexDecisionProcedure::Statistics::Statistics():
   d_successDuringVarOrderSearch("theory::arith::qi::DuringVarOrderSearch::success",0),
   d_attemptAfterVarOrderSearch("theory::arith::qi::AfterVarOrderSearch::attempt",0),
   d_successAfterVarOrderSearch("theory::arith::qi::AfterVarOrderSearch::success",0),
+  d_weakeningAttempts("theory::arith::weakening::attempts",0),
+  d_weakeningSuccesses("theory::arith::weakening::success",0),
+  d_weakenings("theory::arith::weakening::total",0),
+  d_weakenTime("theory::arith::weakening::time"),
+  d_boundComputationTime("theory::arith::bound::time"),
+  d_boundComputations("theory::arith::bound::boundComputations",0),
+  d_boundPropagations("theory::arith::bound::boundPropagations",0),
   d_delayedConflicts("theory::arith::delayedConflicts",0),
   d_pivotTime("theory::arith::pivotTime"),
   d_avgNumRowsNotContainingOnUpdate("theory::arith::avgNumRowsNotContainingOnUpdate"),
@@ -55,6 +89,15 @@ SimplexDecisionProcedure::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_attemptAfterVarOrderSearch);
   StatisticsRegistry::registerStat(&d_successAfterVarOrderSearch);
 
+  StatisticsRegistry::registerStat(&d_weakeningAttempts);
+  StatisticsRegistry::registerStat(&d_weakeningSuccesses);
+  StatisticsRegistry::registerStat(&d_weakenings);
+  StatisticsRegistry::registerStat(&d_weakenTime);
+
+  StatisticsRegistry::registerStat(&d_boundComputationTime);
+  StatisticsRegistry::registerStat(&d_boundComputations);
+  StatisticsRegistry::registerStat(&d_boundPropagations);
+
   StatisticsRegistry::registerStat(&d_delayedConflicts);
 
   StatisticsRegistry::registerStat(&d_pivotTime);
@@ -83,6 +126,15 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_attemptAfterVarOrderSearch);
   StatisticsRegistry::unregisterStat(&d_successAfterVarOrderSearch);
 
+  StatisticsRegistry::unregisterStat(&d_weakeningAttempts);
+  StatisticsRegistry::unregisterStat(&d_weakeningSuccesses);
+  StatisticsRegistry::unregisterStat(&d_weakenings);
+  StatisticsRegistry::unregisterStat(&d_weakenTime);
+
+  StatisticsRegistry::unregisterStat(&d_boundComputationTime);
+  StatisticsRegistry::unregisterStat(&d_boundComputations);
+  StatisticsRegistry::unregisterStat(&d_boundPropagations);
+
   StatisticsRegistry::unregisterStat(&d_delayedConflicts);
   StatisticsRegistry::unregisterStat(&d_pivotTime);
 
@@ -94,9 +146,21 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
 Node SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
   Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
 
-  if(d_partialModel.belowLowerBound(x_i, c_i, false)){
+  if(d_partialModel.belowLowerBound(x_i, c_i, true)){
     return Node::null();
   }
+  // if(d_partialModel.equalsLowerBound(x_i, c_i) && original.getKind() != AND){
+  //   TNode prevConstraint =  d_partialModel.getLowerConstraint(x_i);
+  //   if(prevConstraint.getKind() == EQUAL){
+  //     return Node::null();
+  //   }else{
+  //     Debug("beat::ya") << x_i << " "<< c_i << original << prevConstraint << endl;
+  //     Assert(prevConstraint.getKind() == AND);
+  //     d_partialModel.setLowerConstraint(x_i,original);
+  //     return Node::null();
+  //   }
+  // }
+
   if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
     Node ubc = d_partialModel.getUpperConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
@@ -109,6 +173,8 @@ Node SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_
   d_partialModel.setLowerConstraint(x_i,original);
   d_partialModel.setLowerBound(x_i, c_i);
 
+  d_updatedBounds.softAdd(x_i);
+
   if(!d_tableau.isBasic(x_i)){
     if(d_partialModel.getAssignment(x_i) < c_i){
       update(x_i, c_i);
@@ -127,23 +193,34 @@ Node SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_
 
   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
 
-  if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i
-    //return false; //sat
-    return Node::null();
+  if(d_partialModel.aboveUpperBound(x_i, c_i, true) ){ // \upperbound(x_i) <= c_i
+    return Node::null(); //sat
   }
+
+  // if(d_partialModel.equalsUpperBound(x_i, c_i) && original.getKind() != AND){
+  //   TNode prevConstraint = d_partialModel.getUpperConstraint(x_i);
+  //   if(prevConstraint.getKind() == EQUAL){
+  //     return Node::null();
+  //   }else{
+  //     Debug("beat::ya") << x_i << " "<< c_i << original << prevConstraint  << endl;
+  //     Assert(prevConstraint.getKind() == AND);
+  //     d_partialModel.setUpperConstraint(x_i,original);
+  //     return Node::null();
+  //   }
+  // }
   if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i
     Node lbc = d_partialModel.getLowerConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
     Debug("arith") << "AssertUpper conflict " << conflict << endl;
     ++(d_statistics.d_statAssertUpperConflicts);
-    //d_out->conflict(conflict);
     return conflict;
-    //return true;
   }
 
   d_partialModel.setUpperConstraint(x_i,original);
   d_partialModel.setUpperBound(x_i, c_i);
 
+  d_updatedBounds.softAdd(x_i);
+
   if(!d_tableau.isBasic(x_i)){
     if(d_partialModel.getAssignment(x_i) > c_i){
       update(x_i, c_i);
@@ -155,7 +232,6 @@ Node SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_
   if(Debug.isOn("model")) { d_partialModel.printModel(x_i); }
 
   return Node::null();
-  //return false;
 }
 
 
@@ -168,16 +244,13 @@ Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
   // This can happen if both c_i <= x_i and x_i <= c_i are in the system.
   if(d_partialModel.belowLowerBound(x_i, c_i, false) &&
      d_partialModel.aboveUpperBound(x_i, c_i, false)){
-    //return false; //sat
-    return Node::null();
+    return Node::null(); //sat
   }
 
   if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
     Node ubc = d_partialModel.getUpperConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
-    //d_out->conflict(conflict);
     Debug("arith") << "AssertLower conflict " << conflict << endl;
-    //return true;
     return conflict;
   }
 
@@ -185,8 +258,6 @@ Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
     Node lbc = d_partialModel.getLowerConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
     Debug("arith") << "AssertUpper conflict " << conflict << endl;
-    //d_out->conflict(conflict);
-    //return true;
     return conflict;
   }
 
@@ -196,52 +267,18 @@ Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
   d_partialModel.setUpperConstraint(x_i,original);
   d_partialModel.setUpperBound(x_i, c_i);
 
+  d_updatedBounds.softAdd(x_i);
+
   if(!d_tableau.isBasic(x_i)){
     if(!(d_partialModel.getAssignment(x_i) == c_i)){
       update(x_i, c_i);
     }
   }else{
     d_queue.enqueueIfInconsistent(x_i);
-    //checkBasicVariable(x_i);
   }
-
-  //return false;
   return Node::null();
 }
 
-// set<ArithVar> tableauAndHasSet(Tableau& tab, ArithVar v){
-//   set<ArithVar> has;
-//   for(ArithVarSet::const_iterator basicIter = tab.beginBasic();
-//       basicIter != tab.endBasic();
-//       ++basicIter){
-//     ArithVar basic = *basicIter;
-//     ReducedRowVector& row = tab.lookup(basic);
-
-//     if(row.has(v)){
-//       has.insert(basic);
-//     }
-//   }
-//   return has;
-// }
-
-// set<ArithVar> columnIteratorSet(Tableau& tab,ArithVar v){
-//   set<ArithVar> has;
-//   Column::iterator basicIter = tab.beginColumn(v);
-//   Column::iterator endIter = tab.endColumn(v);
-//   for(; basicIter != endIter; ++basicIter){
-//     ArithVar basic = *basicIter;
-//     has.insert(basic);
-//   }
-//   return has;
-// }
-
-
-/*
-bool matchingSets(Tableau& tab, ArithVar v){
-  return tableauAndHasSet(tab, v) == columnIteratorSet(tab, v);
-}
-*/
-
 void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
   Assert(!d_tableau.isBasic(x_i));
   DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
@@ -279,6 +316,116 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
   if(Debug.isOn("paranoid:check_tableau")){  debugCheckTableau(); }
 }
 
+
+bool SimplexDecisionProcedure::propagateCandidateBound(ArithVar basic, bool upperBound){
+
+  DeltaRational bound = upperBound ?
+    computeUpperBound(basic):
+    computeLowerBound(basic);
+
+  if((upperBound && d_partialModel.strictlyBelowUpperBound(basic, bound)) ||
+     (!upperBound && d_partialModel.strictlyAboveLowerBound(basic, bound))){
+    Node bestImplied = upperBound ?
+      d_propManager.getBestImpliedUpperBound(basic, bound):
+      d_propManager.getBestImpliedLowerBound(basic, bound);
+
+    if(!bestImplied.isNull()){
+      bool asserted = d_propManager.isAsserted(bestImplied);
+      bool propagated = d_propManager.isPropagated(bestImplied);
+      if( !asserted && !propagated){
+
+        NodeBuilder<> nb(kind::AND);
+        if(upperBound){
+          explainNonbasicsUpperBound(basic, nb);
+        }else{
+          explainNonbasicsLowerBound(basic, nb);
+        }
+        Node explanation = nb;
+        d_propManager.propagate(bestImplied, explanation);
+        return true;
+      }else{
+        Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl;
+      }
+    }
+  }
+  return false;
+}
+
+
+bool SimplexDecisionProcedure::hasBounds(ArithVar basic, bool upperBound){
+  for(Tableau::RowIterator iter = d_tableau.rowIterator(basic); !iter.atEnd(); ++iter){
+    const TableauEntry& entry = *iter;
+
+    ArithVar var = entry.getColVar();
+    if(var == basic) continue;
+    int sgn = entry.getCoefficient().sgn();
+    if(upperBound){
+      if( (sgn < 0 && !d_partialModel.hasLowerBound(var)) ||
+          (sgn > 0 && !d_partialModel.hasUpperBound(var))){
+        return false;
+      }
+    }else{
+      if( (sgn < 0 && !d_partialModel.hasUpperBound(var)) ||
+          (sgn > 0 && !d_partialModel.hasLowerBound(var))){
+        return false;
+      }
+    }
+  }
+  return true;
+}
+void SimplexDecisionProcedure::propagateCandidate(ArithVar basic){
+  bool success = false;
+  if(d_partialModel.strictlyAboveLowerBound(basic) &&
+     (!d_partialModel.hasLowerBound(basic) || d_propManager.hasStrongerLowerBound(d_partialModel.getLowerConstraint(basic))) &&
+     hasLowerBounds(basic)){
+    ++d_statistics.d_boundComputations;
+    success |= propagateCandidateLowerBound(basic);
+  }
+  if(d_partialModel.strictlyBelowUpperBound(basic) &&
+     (!d_partialModel.hasUpperBound(basic) || d_propManager.hasStrongerUpperBound(d_partialModel.getUpperConstraint(basic))) &&
+     hasUpperBounds(basic)){
+    ++d_statistics.d_boundComputations;
+    success |= propagateCandidateUpperBound(basic);
+  }
+  if(success){
+    ++d_statistics.d_boundPropagations;
+  }
+}
+
+void SimplexDecisionProcedure::propagateCandidates(){
+  TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
+
+  Assert(d_candidateBasics.empty());
+
+  if(d_updatedBounds.empty()){ return; }
+
+  PermissiveBackArithVarSet::const_iterator i = d_updatedBounds.begin();
+  PermissiveBackArithVarSet::const_iterator end = d_updatedBounds.end();
+  for(; i != end; ++i){
+    ArithVar var = *i;
+    if(d_tableau.isBasic(var)){
+      d_candidateBasics.softAdd(var);
+    }else{
+      Tableau::ColIterator basicIter = d_tableau.colIterator(var);
+      for(; !basicIter.atEnd(); ++basicIter){
+        const TableauEntry& entry = *basicIter;
+        ArithVar rowVar = entry.getRowVar();
+        Assert(entry.getColVar() == var);
+        Assert(d_tableau.isBasic(rowVar));
+        d_candidateBasics.softAdd(rowVar);
+      }
+    }
+  }
+  d_updatedBounds.purge();
+
+  while(!d_candidateBasics.empty()){
+    ArithVar candidate = d_candidateBasics.pop_back();
+    Assert(d_tableau.isBasic(candidate));
+    propagateCandidate(candidate);
+  }
+}
+
+
 void SimplexDecisionProcedure::debugPivotSimplex(ArithVar x_i, ArithVar x_j){
   Debug("arith::simplex:row") << "debugRowSimplex("
                               << x_i  << "|->" << x_j
@@ -545,14 +692,14 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
   const DeltaRational& beta = d_partialModel.getAssignment(basic);
 
   if(d_partialModel.belowLowerBound(basic, beta, true)){
-    ArithVar x_j = selectSlackBelow<minVarOrder>(basic);
+    ArithVar x_j = selectSlackUpperBound<minVarOrder>(basic);
     if(x_j == ARITHVAR_SENTINEL ){
-      return generateConflictBelow(basic);
+      return generateConflictBelowLowerBound(basic);
     }
   }else if(d_partialModel.aboveUpperBound(basic, beta, true)){
-    ArithVar x_j = selectSlackAbove<minVarOrder>(basic);
+    ArithVar x_j = selectSlackLowerBound<minVarOrder>(basic);
     if(x_j == ARITHVAR_SENTINEL ){
-      return generateConflictAbove(basic);
+      return generateConflictAboveUpperBound(basic);
     }
   }
   return Node::null();
@@ -580,30 +727,43 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
     ArithVar x_j = ARITHVAR_SENTINEL;
 
     if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
-      x_j = selectSlackBelow<pf>(x_i);
+      x_j = selectSlackUpperBound<pf>(x_i);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
-        return generateConflictBelow(x_i); //unsat
+        return generateConflictBelowLowerBound(x_i); //unsat
       }
       DeltaRational l_i = d_partialModel.getLowerBound(x_i);
       pivotAndUpdate(x_i, x_j, l_i);
 
     }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
-      x_j = selectSlackAbove<pf>(x_i);
+      x_j = selectSlackLowerBound<pf>(x_i);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
-        return generateConflictAbove(x_i); //unsat
+        return generateConflictAboveUpperBound(x_i); //unsat
       }
       DeltaRational u_i = d_partialModel.getUpperBound(x_i);
       pivotAndUpdate(x_i, x_j, u_i);
     }
     Assert(x_j != ARITHVAR_SENTINEL);
+
     //Check to see if we already have a conflict with x_j to prevent wasteful work
     if(CHECK_AFTER_PIVOT){
-      Node earlyConflict = checkBasicForConflict(x_j);
-      if(!earlyConflict.isNull()){
-        return earlyConflict;
+      Node possibleConflict = checkBasicForConflict(x_j);
+      if(!possibleConflict.isNull()){
+        return possibleConflict;
       }
+      // if(selectSlackUpperBound<pf>(x_j) == ARITHVAR_SENTINEL){
+      //   Node possibleConflict  = deduceUpperBound(x_j);
+      //   if(!possibleConflict.isNull()){
+      //     return possibleConflict;
+      //   }
+      // }
+      // if(selectSlackLowerBound<pf>(x_j) == ARITHVAR_SENTINEL){
+      //   Node possibleConflict  = deduceLowerBound(x_j);
+      //   if(!possibleConflict.isNull()){
+      //     return possibleConflict;
+      //   }
+      // }
     }
   }
   Assert(remainingIterations == 0);
@@ -611,93 +771,289 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
   return Node::null();
 }
 
+template <bool upperBound>
+void SimplexDecisionProcedure::explainNonbasics(ArithVar basic, NodeBuilder<>& output){
+  Assert(d_tableau.isBasic(basic));
 
-Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){
-
-  NodeBuilder<> nb(kind::AND);
-  TNode bound = d_partialModel.getUpperConstraint(conflictVar);
-
-  Debug("arith")  << "generateConflictAbove "
-                  << "conflictVar " << conflictVar
-                  << " " << d_partialModel.getAssignment(conflictVar)
-                  << " " << bound << endl;
+  Debug("arith::explainNonbasics") << "SimplexDecisionProcedure::explainNonbasics("
+                                   << basic <<") start" << endl;
 
-  nb << bound;
 
-  Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar);
+  Tableau::RowIterator iter = d_tableau.rowIterator(basic);
   for(; !iter.atEnd(); ++iter){
     const TableauEntry& entry = *iter;
     ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == conflictVar) continue;
+    if(nonbasic == basic) continue;
 
     const Rational& a_ij = entry.getCoefficient();
     Assert(a_ij != d_ZERO);
+    TNode bound = TNode::null();
 
     int sgn = a_ij.sgn();
     Assert(sgn != 0);
-    if(sgn < 0){
-      bound =  d_partialModel.getUpperConstraint(nonbasic);
-      Debug("arith") << "below 0 " << nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic)
-                     << " " << bound << endl;
-      nb << bound;
+    if(upperBound){
+      if(sgn < 0){
+        bound = d_partialModel.getLowerConstraint(nonbasic);
+      }else{
+        Assert(sgn > 0);
+        bound = d_partialModel.getUpperConstraint(nonbasic);
+      }
     }else{
-      Assert(sgn > 0);
-      bound =  d_partialModel.getLowerConstraint(nonbasic);
-      Debug("arith") << " above 0 " << nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic)
-                     << " " << bound << endl;
-      nb << bound;
+      if(sgn < 0){
+        bound =  d_partialModel.getUpperConstraint(nonbasic);
+      }else{
+        Assert(sgn > 0);
+        bound =  d_partialModel.getLowerConstraint(nonbasic);
+      }
     }
+    Assert(!bound.isNull());
+    Debug("arith::explainNonbasics") << "\t" << nonbasic << " " << sgn << " " << bound
+                                     << endl;
+    output << bound;
   }
-  Node conflict = nb;
-  return conflict;
+  Debug("arith::explainNonbasics") << "SimplexDecisionProcedure::explainNonbasics("
+                                   << basic << ") done" << endl;
 }
 
-Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
-  NodeBuilder<> nb(kind::AND);
-  TNode bound = d_partialModel.getLowerConstraint(conflictVar);
-
-  Debug("arith") << "generateConflictBelow "
-                 << "conflictVar " << conflictVar
-                 << d_partialModel.getAssignment(conflictVar) << " "
-                 << " " << bound << endl;
-  nb << bound;
 
+TNode SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic){
+
+  int sgn = coeff.sgn();
+  bool ub = aboveUpper?(sgn < 0) : (sgn > 0);
+  TNode exp = ub ?
+    d_partialModel.getUpperConstraint(v) :
+    d_partialModel.getLowerConstraint(v);
+  DeltaRational bound = ub?
+    d_partialModel.getUpperBound(v) :
+    d_partialModel.getLowerBound(v);
+
+  bool weakened;
+  do{
+    weakened = false;
+
+    Node weaker = ub?
+      d_propManager.strictlyWeakerAssertedUpperBound(v, bound):
+      d_propManager.strictlyWeakerAssertedLowerBound(v, bound);
+
+    if(!weaker.isNull()){
+      DeltaRational weakerBound = asDeltaRational(weaker);
+
+      DeltaRational diff = aboveUpper ? bound - weakerBound : weakerBound - bound;
+      //if var == basic,
+      //  if aboveUpper, weakerBound > bound, multiply by -1
+      //  if !aboveUpper, weakerBound < bound, multiply by -1
+      diff = diff * coeff;
+      if(surplus > diff){
+        ++d_statistics.d_weakenings;
+        weakened = true;
+        anyWeakening = true;
+        surplus = surplus - diff;
+
+        Debug("weak") << "found:" << endl;
+        if(v == basic){
+          Debug("weak") << "  basic: ";
+        }
+        Debug("weak") << "  " << surplus << " "<< diff  << endl
+                      << "  " << bound << exp << endl
+                      << "  " << weakerBound << weaker << endl;
 
-  Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar);
-  for(; !iter.atEnd(); ++iter){
-    const TableauEntry& entry = *iter;
-    ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == conflictVar) continue;
+        if(exp.getKind() == AND){
+          Debug("weak") << "VICTORY" << endl;
+        }
 
-    const Rational& a_ij = entry.getCoefficient();
+        Assert(diff > d_DELTA_ZERO);
+        exp = weaker;
+        bound = weakerBound;
+      }
+    }
+  }while(weakened);
 
-    int sgn = a_ij.sgn();
-    Assert(a_ij != d_ZERO);
-    Assert(sgn != 0);
+  if(exp.getKind() == AND){
+    Debug("weak") << "boo: " << exp << endl;
+  }
+  return exp;
+}
 
-    if(sgn < 0){
-      TNode bound = d_partialModel.getLowerConstraint(nonbasic);
-      Debug("arith") << "Lower "<< nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic) << " "
-                     << bound << endl;
+Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar){
+  TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime);
 
-      nb << bound;
-    }else{
-      Assert(sgn > 0);
-      TNode bound = d_partialModel.getUpperConstraint(nonbasic);
-      Debug("arith") << "Upper "<< nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic) << " "
-                     << bound << endl;
+  const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
+  DeltaRational surplus;
+  if(aboveUpper){
+    Assert(d_partialModel.hasUpperBound(basicVar));
+    Assert(assignment > d_partialModel.getUpperBound(basicVar));
+    surplus = assignment - d_partialModel.getUpperBound(basicVar);
+  }else{
+    Assert(d_partialModel.hasLowerBound(basicVar));
+    Assert(assignment < d_partialModel.getLowerBound(basicVar));
+    surplus = d_partialModel.getLowerBound(basicVar) - assignment;
+  }
 
-      nb << bound;
-    }
+  NodeBuilder<> conflict(kind::AND);
+  bool anyWeakenings = false;
+  for(Tableau::RowIterator i = d_tableau.rowIterator(basicVar); !i.atEnd(); ++i){
+    const TableauEntry& entry = *i;
+    ArithVar v = entry.getColVar();
+    const Rational& coeff = entry.getCoefficient();
+    conflict << weakestExplanation(aboveUpper, surplus, v, coeff, anyWeakenings, basicVar);
+  }
+  ++d_statistics.d_weakeningAttempts;
+  if(anyWeakenings){
+    ++d_statistics.d_weakeningSuccesses;
   }
-  Node conflict (nb.constructNode());
   return conflict;
 }
 
+
+// Node SimplexDecisionProcedure::weakenLowerBoundConflict(ArithVar basicVar){
+//   TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime);
+
+//   bool anyWeakenings = false;
+//   const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
+//   Assert(d_partialModel.hasLowerBound(basicVar));
+//   Assert(assignment < d_partialModel.getLowerBound(basicVar));
+
+//   DeltaRational surplus = d_partialModel.getLowerBound(basicVar) - assignment;
+
+//   vector<WeakeningElem> weakeningElements;
+//   queue<uint32_t> potentialWeakingings;
+//   for(Tableau::RowIterator i = d_tableau.rowIterator(basicVar); !i.atEnd(); ++i){
+//     const TableauEntry& entry = *i;
+//     ArithVar v = entry.getColVar();
+//     const Rational& coeff = entry.getCoefficient();
+
+//     int sgn = coeff.sgn();
+//     bool ub = (sgn > 0);
+//     Node exp = ub ?
+//       d_partialModel.getUpperConstraint(v) :
+//       d_partialModel.getLowerConstraint(v);
+//     DeltaRational bound = ub?
+//       d_partialModel.getUpperBound(v) :
+//       d_partialModel.getLowerBound(v);
+//     potentialWeakingings.push(weakeningElements.size());
+//     weakeningElements.push_back(WeakeningElem(v, &coeff, ub, bound, exp));
+//   }
+
+//   vector<Node> conflict;
+
+//   Debug("weak") << "weakenLowerBoundConflict" << endl;
+//   while(!potentialWeakingings.empty()){
+//     uint32_t pos = potentialWeakingings.front();
+//     potentialWeakingings.pop();
+
+//     WeakeningElem& curr = weakeningElements[pos];
+
+//     Node weaker = curr.upperBound?
+//       d_propManager.strictlyWeakerAssertedUpperBound(curr.var, curr.bound):
+//       d_propManager.strictlyWeakerAssertedLowerBound(curr.var, curr.bound);
+
+//     bool weakened = false;
+//     if(!weaker.isNull()){
+//       DeltaRational weakerBound = asDeltaRational(weaker);
+//       DeltaRational diff = weakerBound -  curr.bound;
+//       //if var == basic, weakerBound < curr.bound
+//       // multiply by -1
+//       diff = diff * (*curr.coeff);
+
+//       if(surplus > diff){
+//         ++d_statistics.d_weakenings;
+//         anyWeakenings = true;
+//         weakened = true;
+//         surplus = surplus - diff;
+
+//         Debug("weak") << "found:" << endl;
+//         if(curr.var == basicVar){
+//           Debug("weak") << "  basic: ";
+//         }
+//         Debug("weak") << "  " << surplus << " "<< diff  << endl
+//                       << "  " << curr.bound << weakerBound << endl
+//                       << "  " << curr.explanation << weaker << endl;
+
+//         if(curr.explanation.getKind() == AND){
+//           Debug("weak") << "VICTORY" << endl;
+//         }
+
+//         Assert(diff > d_DELTA_ZERO);
+//         curr.explanation = weaker;
+//         curr.bound = weakerBound;
+//       }
+//     }
+
+//     if(weakened){
+//       potentialWeakingings.push(pos);
+//     }else{
+//       if(curr.explanation.getKind() == AND){
+//         Debug("weak") << "boo: " << curr.explanation << endl;
+//       }
+//       conflict.push_back(curr.explanation);
+//     }
+//   }
+
+//   ++d_statistics.d_weakeningAttempts;
+//   if(anyWeakenings){
+//     ++d_statistics.d_weakeningSuccesses;
+//   }
+
+//   NodeBuilder<> nb(AND);
+//   nb.append(conflict);
+//   return nb;
+// }
+
+// Node SimplexDecisionProcedure::deduceUpperBound(ArithVar basicVar){
+//   Assert(d_tableau.isBasic(basicVar));
+//   Assert(selectSlackUpperBound<minVarOrder>(basicVar) == ARITHVAR_SENTINEL);
+
+//   const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
+
+//   Assert(assignment.getInfinitesimalPart() <= 0);
+
+//   if(d_partialModel.strictlyBelowUpperBound(basicVar, assignment)){
+//     NodeBuilder<> nb(kind::AND);
+//     explainNonbasicsUpperBound(basicVar, nb);
+//     Node explanation = maybeUnaryConvert(nb);
+//     Debug("waka-waka") << basicVar << " ub " << assignment << " "<< explanation << endl;
+//     Node res = AssertUpper(basicVar, assignment, explanation);
+//     if(res.isNull()){
+//       d_propManager.propagateArithVar(true, basicVar, assignment, explanation);
+//     }
+//     return res;
+//   }else{
+//     return Node::null();
+//   }
+// }
+
+// Node SimplexDecisionProcedure::deduceLowerBound(ArithVar basicVar){
+//   Assert(d_tableau.isBasic(basicVar));
+//   Assert(selectSlackLowerBound<minVarOrder>(basicVar) == ARITHVAR_SENTINEL);
+//   const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
+
+//   if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); }
+
+//   Assert(assignment.getInfinitesimalPart() >= 0);
+
+//   if(d_partialModel.strictlyAboveLowerBound(basicVar, assignment)){
+//     NodeBuilder<> nb(kind::AND);
+//     explainNonbasicsLowerBound(basicVar, nb);
+//     Node explanation = maybeUnaryConvert(nb);
+//     Debug("waka-waka") << basicVar << " lb " << assignment << " "<< explanation << endl;
+//     Node res = AssertLower(basicVar, assignment, explanation);
+//     if(res.isNull()){
+//       d_propManager.propagateArithVar(false, basicVar, assignment, explanation);
+//     }
+//     return res;
+//   }else{
+//     return Node::null();
+//   }
+// }
+
+Node SimplexDecisionProcedure::generateConflictAboveUpperBound(ArithVar conflictVar){
+  return weakenConflict(true, conflictVar);
+}
+
+Node SimplexDecisionProcedure::generateConflictBelowLowerBound(ArithVar conflictVar){
+  return weakenConflict(false, conflictVar);
+}
+
 /**
  * Computes the value of a basic variable using the current assignment.
  */
@@ -717,6 +1073,26 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe
   return sum;
 }
 
+DeltaRational SimplexDecisionProcedure::computeBound(ArithVar basic, bool upperBound){
+  DeltaRational sum(0,0);
+  for(Tableau::RowIterator i = d_tableau.rowIterator(basic); !i.atEnd(); ++i){
+    const TableauEntry& 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_partialModel.getUpperBound(nonbasic):
+      d_partialModel.getLowerBound(nonbasic);
+
+    DeltaRational diff = bound * coeff;
+    sum = sum + diff;
+  }
+  return sum;
+}
+
 /**
  * This check is quite expensive.
  * It should be wrapped in a Debug.isOn() guard.
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index b1ebe2972..f0dc5d62e 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -10,6 +10,7 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/tableau.h"
 #include "theory/arith/partial_model.h"
+#include "theory/arith/arith_prop_manager.h"
 
 #include "util/options.h"
 
@@ -33,36 +34,23 @@ private:
   Tableau& d_tableau;
   ArithPriorityQueue d_queue;
 
+  ArithPropManager& d_propManager;
+
   ArithVar d_numVariables;
 
   std::queue<Node> d_delayedLemmas;
 
+  PermissiveBackArithVarSet d_updatedBounds;
+  PermissiveBackArithVarSet d_candidateBasics;
+
   Rational d_ZERO;
+  DeltaRational d_DELTA_ZERO;
 
 public:
-  SimplexDecisionProcedure(ArithPartialModel& pm,
-                           Tableau& tableau) :
-    d_partialModel(pm),
-    d_tableau(tableau),
-    d_queue(pm, tableau),
-    d_numVariables(0),
-    d_delayedLemmas(),
-    d_ZERO(0)
-  {
-    switch(Options::ArithPivotRule rule = Options::current()->pivotRule) {
-    case Options::MINIMUM:
-      d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
-      break;
-    case Options::BREAK_TIES:
-      d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES);
-      break;
-    case Options::MAXIMUM:
-      d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM);
-      break;
-    default:
-      Unhandled(rule);
-    }
-  }
+  SimplexDecisionProcedure(ArithPropManager& propManager,
+                           ArithPartialModel& pm,
+                           Tableau& tableau);
+
 
   /**
    * Assert*(n, orig) takes an bound n that is implied by orig.
@@ -165,32 +153,49 @@ private:
    * This returns ARITHVAR_SENTINEL if none exists.
    *
    * More formally one of the following conditions must be satisfied:
-   * -  above && a_ij < 0 && assignment(x_j) < upperbound(x_j)
-   * -  above && a_ij > 0 && assignment(x_j) > lowerbound(x_j)
-   * - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j)
-   * - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
+   * -  lowerBound && a_ij < 0 && assignment(x_j) < upperbound(x_j)
+   * -  lowerBound && a_ij > 0 && assignment(x_j) > lowerbound(x_j)
+   * - !lowerBound && a_ij > 0 && assignment(x_j) < upperbound(x_j)
+   * - !lowerBound && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
    *
    */
-  template <bool above, PreferenceFunction>  ArithVar selectSlack(ArithVar x_i);
-  template <PreferenceFunction pf> ArithVar selectSlackBelow(ArithVar x_i) {
-    return selectSlack<false, pf>(x_i);
-  }
-  template <PreferenceFunction pf> ArithVar selectSlackAbove(ArithVar x_i) {
+  template <bool lowerBound, PreferenceFunction>  ArithVar selectSlack(ArithVar x_i);
+  template <PreferenceFunction pf> ArithVar selectSlackLowerBound(ArithVar x_i) {
     return selectSlack<true, pf>(x_i);
   }
+  template <PreferenceFunction pf> ArithVar selectSlackUpperBound(ArithVar x_i) {
+    return selectSlack<false, pf>(x_i);
+  }
   /**
    * Returns the smallest basic variable whose assignment is not consistent
    * with its upper and lower bounds.
    */
   ArithVar selectSmallestInconsistentVar();
 
+
+  /**
+   * Exports either the explanation of an upperbound or a lower bound
+   * of the basic variable basic, using the non-basic variables in the row.
+   */
+  template <bool upperBound>
+  void explainNonbasics(ArithVar basic, NodeBuilder<>& output);
+  void explainNonbasicsLowerBound(ArithVar basic, NodeBuilder<>& output){
+    explainNonbasics<false>(basic, output);
+  }
+  void explainNonbasicsUpperBound(ArithVar basic, NodeBuilder<>& output){
+    explainNonbasics<true>(basic, output);
+  }
+
+  Node deduceUpperBound(ArithVar basicVar);
+  Node deduceLowerBound(ArithVar basicVar);
+
   /**
    * Given a non-basic variable that is know to not be updatable
    * to a consistent value, construct and return a conflict.
    * Follows section 4.2 in the CAV06 paper.
    */
-  Node generateConflictAbove(ArithVar conflictVar);
-  Node generateConflictBelow(ArithVar conflictVar);
+  Node generateConflictAboveUpperBound(ArithVar conflictVar);
+  Node generateConflictBelowLowerBound(ArithVar conflictVar);
 
 public:
   /**
@@ -210,6 +215,11 @@ public:
    */
   DeltaRational computeRowValue(ArithVar x, bool useSafe);
 
+  bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
+  void clearUpdates(){
+    d_updatedBounds.purge();
+  }
+  void propagateCandidates();
 
   void increaseMax() {d_numVariables++;}
 
@@ -234,7 +244,7 @@ private:
 
   /** Adds a conflict as a lemma to the queue. */
   void delayConflictAsLemma(Node conflict){
-    Node negatedConflict = negateConjunctionAsClause(conflict);
+   Node negatedConflict = negateConjunctionAsClause(conflict);
     pushLemma(negatedConflict);
   }
 
@@ -254,6 +264,36 @@ private:
    */
   Node checkBasicForConflict(ArithVar b);
 
+  Node weakenConflict(bool aboveUpper, ArithVar basicVar);
+  TNode weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic);
+
+  void propagateCandidate(ArithVar basic);
+  bool propagateCandidateBound(ArithVar basic, bool upperBound);
+
+  inline bool propagateCandidateLowerBound(ArithVar basic){
+    return propagateCandidateBound(basic, false);
+  }
+  inline bool propagateCandidateUpperBound(ArithVar basic){
+    return propagateCandidateBound(basic, true);
+  }
+
+  bool hasBounds(ArithVar basic, bool upperBound);
+  bool hasLowerBounds(ArithVar basic){
+    return hasBounds(basic, false);
+  }
+  bool hasUpperBounds(ArithVar basic){
+    return hasBounds(basic, true);
+  }
+  DeltaRational computeBound(ArithVar basic, bool upperBound);
+
+  inline DeltaRational computeLowerBound(ArithVar basic){
+    return computeBound(basic, false);
+  }
+  inline DeltaRational computeUpperBound(ArithVar basic){
+    return computeBound(basic, true);
+  }
+
+
   /** These fields are designed to be accessable to TheoryArith methods. */
   class Statistics {
   public:
@@ -270,6 +310,12 @@ private:
     IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch;
     IntStat d_attemptAfterVarOrderSearch, d_successAfterVarOrderSearch;
 
+    IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings;
+    TimerStat d_weakenTime;
+
+    TimerStat d_boundComputationTime;
+    IntStat d_boundComputations, d_boundPropagations;
+
     IntStat d_delayedConflicts;
 
     TimerStat d_pivotTime;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c22b0019d..3c275fae0 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -26,6 +26,8 @@
 
 #include "util/rational.h"
 #include "util/integer.h"
+#include "util/boolean_simplification.h"
+
 
 #include "theory/rewriter.h"
 
@@ -40,6 +42,7 @@
 
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/normal_form.h"
+#include "theory/arith/arith_prop_manager.h"
 
 #include <stdint.h>
 
@@ -54,7 +57,7 @@ using namespace CVC4::theory::arith;
 static const uint32_t RESET_START = 2;
 
 struct SlackAttrID;
-typedef expr::Attribute<SlackAttrID, Node> Slack;
+typedef expr::Attribute<SlackAttrID, bool> Slack;
 
 TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation) :
   Theory(THEORY_ARITH, c, out, valuation),
@@ -67,7 +70,8 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valu
   d_tableauResetDensity(1.6),
   d_tableauResetPeriod(10),
   d_propagator(c, out),
-  d_simplex(d_partialModel, d_tableau),
+  d_propManager(c, d_arithvarNodeMap, d_propagator, valuation),
+  d_simplex(d_propManager, d_partialModel, d_tableau),
   d_DELTA_ZERO(0),
   d_statistics()
 {}
@@ -171,6 +175,7 @@ void TheoryArith::preRegisterTerm(TNode n) {
   if(isRelationOperator(k)){
     Assert(Comparison::isNormalAtom(n));
 
+    //cout << n << endl;
 
     d_propagator.addAtom(n);
 
@@ -179,7 +184,7 @@ void TheoryArith::preRegisterTerm(TNode n) {
     if(left.getKind() == PLUS){
       //We may need to introduce a slack variable.
       Assert(left.getNumChildren() >= 2);
-      if(!left.hasAttribute(Slack())){
+      if(!left.getAttribute(Slack())){
         setupSlack(left);
       }
     }
@@ -189,15 +194,15 @@ void TheoryArith::preRegisterTerm(TNode n) {
 
 
 ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
-  Assert(isLeaf(x));
-  Assert(!hasArithVar(x));
+  Assert(isLeaf(x) || x.getKind() == PLUS);
+  Assert(!d_arithvarNodeMap.hasArithVar(x));
 
   ArithVar varX = d_variables.size();
   d_variables.push_back(Node(x));
 
   d_simplex.increaseMax();
 
-  setArithVar(x,varX);
+  d_arithvarNodeMap.setArithVar(x,varX);
 
   d_userVariables.init(varX, !basic);
   d_tableau.increaseSize();
@@ -218,9 +223,9 @@ void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::v
     Debug("rewriter") << "should be var: " << n << endl;
 
     Assert(isLeaf(n));
-    Assert(hasArithVar(n));
+    Assert(d_arithvarNodeMap.hasArithVar(n));
 
-    ArithVar av = asArithVar(n);
+    ArithVar av = d_arithvarNodeMap.asArithVar(n);
 
     coeffs.push_back(constant.getValue());
     variables.push_back(av);
@@ -228,13 +233,12 @@ void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::v
 }
 
 void TheoryArith::setupSlack(TNode left){
+  Assert(!left.getAttribute(Slack()));
 
   ++(d_statistics.d_statSlackVariables);
-  TypeNode real_type = NodeManager::currentNM()->realType();
-  Node slack = NodeManager::currentNM()->mkVar(real_type);
-  left.setAttribute(Slack(), slack);
+  left.setAttribute(Slack(), true);
 
-  ArithVar varSlack = requestArithVar(slack, true);
+  ArithVar varSlack = requestArithVar(left, true);
 
   Polynomial polyLeft = Polynomial::parsePolynomial(left);
 
@@ -273,44 +277,18 @@ void TheoryArith::registerTerm(TNode tn){
   Debug("arith") << "registerTerm(" << tn << ")" << endl;
 }
 
-template <bool selectLeft>
-TNode getSide(TNode assertion, Kind simpleKind){
-  switch(simpleKind){
-  case LT:
-  case GT:
-  case DISTINCT:
-    return selectLeft ? (assertion[0])[0] : (assertion[0])[1];
-  case LEQ:
-  case GEQ:
-  case EQUAL:
-    return selectLeft ? assertion[0] : assertion[1];
-  default:
-    Unreachable();
-    return TNode::null();
-  }
-}
 
 ArithVar TheoryArith::determineLeftVariable(TNode assertion, Kind simpleKind){
   TNode left = getSide<true>(assertion, simpleKind);
 
   if(isLeaf(left)){
-    return asArithVar(left);
+    return d_arithvarNodeMap.asArithVar(left);
   }else{
     Assert(left.hasAttribute(Slack()));
-    TNode slack = left.getAttribute(Slack());
-    return asArithVar(slack);
+    return d_arithvarNodeMap.asArithVar(left);
   }
 }
 
-DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){
-  TNode right = getSide<false>(assertion, simpleKind);
-
-  Assert(right.getKind() == CONST_RATIONAL);
-  const Rational& noninf = right.getConst<Rational>();
-
-  Rational inf = Rational(Integer(deltaCoeff(simpleKind)));
-  return DeltaRational(noninf, inf);
-}
 
 Node TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){
   NodeBuilder<3> conflict(kind::AND);
@@ -390,19 +368,28 @@ void TheoryArith::check(Effort effortLevel){
 
     if(!possibleConflict.isNull()){
       d_partialModel.revertAssignmentChanges();
+      //Node simpleConflict  = BooleanSimplification::simplifyConflict(possibleConflict);
+
+      Debug("arith::conflict") << "conflict   " << possibleConflict << endl;
+
+      d_simplex.clearUpdates();
       d_out->conflict(possibleConflict);
       return;
     }
   }
 
-  if(Debug.isOn("arith::print_assertions") && fullEffort(effortLevel)) {
+  if(Debug.isOn("arith::print_assertions")) {
     debugPrintAssertions();
   }
 
   Node possibleConflict = d_simplex.updateInconsistentVars();
   if(possibleConflict != Node::null()){
-
     d_partialModel.revertAssignmentChanges();
+    d_simplex.clearUpdates();
+
+    //Node simpleConflict  = BooleanSimplification::simplifyConflict(possibleConflict);
+
+    Debug("arith::conflict") << "conflict   " << possibleConflict << endl;
 
     d_out->conflict(possibleConflict);
   }else{
@@ -489,14 +476,137 @@ void TheoryArith::debugPrintModel(){
   }
 }
 
+/*
+bool TheoryArith::isImpliedUpperBound(ArithVar var, Node exp){
+  Node varAsNode = asNode(var);
+  const DeltaRational& ub = d_partialModel.getUpperBound(var);
+  Assert(ub.getInfinitesimalPart() <= 0 );
+  Kind kind = ub.getInfinitesimalPart() < 0 ? LT : LEQ;
+  Node ubAsNode = NodeBuilder<2>(kind) << varAsNode << mkRationalNode(ub.getNoninfinitesimalPart());
+  Node bestImplied = d_propagator.getBestImpliedUpperBound(ubAsNode);
+
+  return bestImplied == exp;
+}
+
+bool TheoryArith::isImpliedLowerBound(ArithVar var, Node exp){
+  Node varAsNode = asNode(var);
+  const DeltaRational& lb = d_partialModel.getLowerBound(var);
+  Assert(lb.getInfinitesimalPart() >= 0 );
+  Kind kind = lb.getInfinitesimalPart() > 0 ? GT : GEQ;
+  Node lbAsIneq = NodeBuilder<2>(kind) << varAsNode << mkRationalNode(lb.getNoninfinitesimalPart());
+  Node bestImplied = d_propagator.getBestImpliedLowerBound(lbAsIneq);
+  return bestImplied == exp;
+}
+*/
+
 void TheoryArith::explain(TNode n) {
+  Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
+  //Assert(n.hasAttribute(Propagated()));
+
+  //NodeBuilder<> explainBuilder(AND);
+  //internalExplain(n,explainBuilder);
+  Assert(d_propManager.isPropagated(n));
+  Node explanation = d_propManager.explain(n);
+  //Node flatExplanation = BooleanSimplification::simplifyConflict(explanation);
+
+  d_out->explanation(explanation, true);
+}
+/*
+void TheoryArith::internalExplain(TNode n, NodeBuilder<>& explainBuilder){
+  Assert(n.hasAttribute(Propagated()));
+  Node bound = n.getAttribute(Propagated());
+
+  AlwaysAssert(bound.getKind() == kind::AND);
+
+  for(Node::iterator i = bound.begin(), end = bound.end(); i != end; ++i){
+    Node lit = *i;
+    if(lit.hasAttribute(Propagated())){
+      cout << "hoop the sadjklasdj" << endl;
+      internalExplain(lit, explainBuilder);
+    }else{
+      explainBuilder << lit;
+    }
+  }
+}
+*/
+/*
+static const bool EXPORT_LEMMA_INSTEAD_OF_PROPAGATE = false;
+void TheoryArith::propagateArithVar(bool upperbound, ArithVar var ){
+  Node varAsNode = asNode(var);
+  const DeltaRational& b = upperbound ?
+    d_partialModel.getUpperBound(var) : d_partialModel.getLowerBound(var);
+
+  Assert((!upperbound) || (b.getInfinitesimalPart() <= 0) );
+  Assert(upperbound || (b.getInfinitesimalPart() >= 0) );
+  Kind kind;
+  if(upperbound){
+    kind = b.getInfinitesimalPart() < 0 ? LT : LEQ;
+  } else{
+    kind = b.getInfinitesimalPart() > 0 ? GT : GEQ;
+  }
+
+  Node bAsNode = NodeBuilder<2>(kind) << varAsNode
+                                      << mkRationalNode(b.getNoninfinitesimalPart());
+
+  Node bestImplied = upperbound ?
+    d_propagator.getBestImpliedUpperBound(bAsNode):
+    d_propagator.getBestImpliedLowerBound(bAsNode);
+
+  if(!bestImplied.isNull()){
+    Node satValue = d_valuation.getSatValue(bestImplied);
+    if(satValue.isNull()){
+
+      Node reason = upperbound ?
+        d_partialModel.getUpperConstraint(var) :
+        d_partialModel.getLowerConstraint(var);
+
+      //cout << getContext()->getLevel() << " " << bestImplied << " " << reason  << endl;
+      if(EXPORT_LEMMA_INSTEAD_OF_PROPAGATE){
+        Node lemma = NodeBuilder<2>(IMPLIES) << reason
+                                             << bestImplied;
+
+        //Temporary
+        Node clause = BooleanSimplification::simplifyHornClause(lemma);
+        d_out->lemma(clause);
+      }else{
+        Assert(!bestImplied.hasAttribute(Propagated()));
+        bestImplied.setAttribute(Propagated(), reason);
+        d_reasons.push_back(reason);
+        d_out->propagate(bestImplied);
+      }
+    }else{
+      Assert(!satValue.isNull());
+      Assert(satValue.getKind() == CONST_BOOLEAN);
+      Assert(satValue.getConst<bool>());
+    }
+  }
 }
+*/
 
 void TheoryArith::propagate(Effort e) {
   if(quickCheckOrMore(e)){
-    while(d_simplex.hasMoreLemmas()){
-      Node lemma = d_simplex.popLemma();
-      d_out->lemma(lemma);
+    bool propagated = false;
+    if(Options::current()->arithPropagation && d_simplex.hasAnyUpdates()){
+      d_simplex.propagateCandidates();
+    }else{
+      d_simplex.clearUpdates();
+    }
+
+    while(d_propManager.hasMorePropagations()){
+      TNode toProp = d_propManager.getPropagation();
+      Node satValue = d_valuation.getSatValue(toProp);
+      AlwaysAssert(satValue.isNull());
+      TNode exp = d_propManager.explain(toProp);
+      propagated = true;
+      d_out->propagate(toProp);
+    }
+
+    if(!propagated){
+      //Opportunistically export previous conflicts
+      while(d_simplex.hasMoreLemmas()){
+        Node lemma = d_simplex.popLemma();
+        d_out->lemma(lemma);
+      }
     }
   }
 }
@@ -506,7 +616,7 @@ Node TheoryArith::getValue(TNode n) {
 
   switch(n.getKind()) {
   case kind::VARIABLE: {
-    ArithVar var = asArithVar(n);
+    ArithVar var = d_arithvarNodeMap.asArithVar(n);
 
     if(d_removedRows.find(var) != d_removedRows.end()){
       Node eq = d_removedRows.find(var)->second;
@@ -634,7 +744,7 @@ void TheoryArith::notifyRestart(){
 bool TheoryArith::entireStateIsConsistent(){
   typedef std::vector<Node>::const_iterator VarIter;
   for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
-    ArithVar var = asArithVar(*i);
+    ArithVar var = d_arithvarNodeMap.asArithVar(*i);
     if(!d_partialModel.assignmentIsConsistent(var)){
       d_partialModel.printModel(var);
       cerr << "Assignment is not consistent for " << var << *i << endl;
@@ -669,7 +779,7 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){
     Assert(!noRow);
 
     //remove the row from the tableau
-    Node eq =  d_tableau.rowAsEquality(v, d_arithVarToNodeMap);
+    Node eq =  d_tableau.rowAsEquality(v, d_arithvarNodeMap.getArithVarToNodeMap());
     d_tableau.removeRow(v);
 
     if(Debug.isOn("tableau")) d_tableau.printTableau();
@@ -681,8 +791,8 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){
     d_removedRows[v] = eq;
   }
 
-  Debug("arith::permanentlyRemoveVariable") << "Permanently removed variable "
-                                            << v << ":" << asNode(v) << endl;
+  Debug("arith::permanentlyRemoveVariable") << "Permanently removed variable " << v
+                                            << ":" << d_arithvarNodeMap.asNode(v) <<endl;
   ++(d_statistics.d_permanentlyRemovedVariables);
 }
 
@@ -692,7 +802,7 @@ void TheoryArith::presolve(){
   typedef std::vector<Node>::const_iterator VarIter;
   for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
     Node variableNode = *i;
-    ArithVar var = asArithVar(variableNode);
+    ArithVar var = d_arithvarNodeMap.asArithVar(variableNode);
     if(d_userVariables.isMember(var) && !d_propagator.hasAnyAtoms(variableNode)){
       //The user variable is unconstrained.
       //Remove this variable permanently
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 85f554849..9580a6c71 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -36,6 +36,8 @@
 #include "theory/arith/unate_propagator.h"
 #include "theory/arith/simplex.h"
 #include "theory/arith/arith_static_learner.h"
+#include "theory/arith/arith_prop_manager.h"
+#include "theory/arith/arithvar_node_map.h"
 
 #include "util/stats.h"
 
@@ -64,6 +66,8 @@ private:
    */
   std::vector<Node> d_variables;
 
+  ArithVarNodeMap d_arithvarNodeMap;
+
   /**
    * If ArithVar v maps to the node n in d_removednode,
    * then n = (= asNode(v) rhs) where rhs is a term that
@@ -82,32 +86,7 @@ private:
    */
   ArithVarSet d_userVariables;
 
-  /**
-   * Bidirectional map between Nodes and ArithVars.
-   */
-  NodeToArithVarMap d_nodeToArithVarMap;
-  ArithVarToNodeMap d_arithVarToNodeMap;
-
-  inline bool hasArithVar(TNode x) const {
-    return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
-  }
-
-  inline ArithVar asArithVar(TNode x) const{
-    Assert(hasArithVar(x));
-    Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL);
-    return (d_nodeToArithVarMap.find(x))->second;
-  }
-  inline Node asNode(ArithVar a) const{
-    Assert(d_arithVarToNodeMap.find(a) != d_arithVarToNodeMap.end());
-    return (d_arithVarToNodeMap.find(a))->second;
-  }
-
-  inline void setArithVar(TNode x, ArithVar a){
-    Assert(!hasArithVar(x));
-    Assert(d_arithVarToNodeMap.find(a) == d_arithVarToNodeMap.end());
-    d_arithVarToNodeMap[a] = x;
-    d_nodeToArithVarMap[x] = a;
-  }
+
 
   /**
    * List of all of the inequalities asserted in the current context.
@@ -141,6 +120,9 @@ private:
   Tableau d_smallTableauCopy;
 
   ArithUnatePropagator d_propagator;
+
+  ArithPropManager d_propManager;
+
   SimplexDecisionProcedure d_simplex;
 
 public:
@@ -175,6 +157,9 @@ private:
   /** The constant zero. */
   DeltaRational d_DELTA_ZERO;
 
+  /** propagates an arithvar */
+  void propagateArithVar(bool upperbound, ArithVar var );
+
   /**
    * Using the simpleKind return the ArithVar associated with the
    * left hand side of assertion.
@@ -228,6 +213,11 @@ private:
    */
   void permanentlyRemoveVariable(ArithVar v);
 
+  bool isImpliedUpperBound(ArithVar var, Node exp);
+  bool isImpliedLowerBound(ArithVar var, Node exp);
+
+  void internalExplain(TNode n, NodeBuilder<>& explainBuilder);
+
 
   void asVectors(Polynomial& p,
                  std::vector<Rational>& coeffs,
diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/unate_propagator.cpp
index 069f4f0f3..2785f0773 100644
--- a/src/theory/arith/unate_propagator.cpp
+++ b/src/theory/arith/unate_propagator.cpp
@@ -31,36 +31,47 @@ using namespace CVC4::kind;
 using namespace std;
 
 ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt, OutputChannel& out) :
-  d_arithOut(out), d_orderedListMap()
+  d_arithOut(out), d_setsMap()
 { }
 
-bool ArithUnatePropagator::leftIsSetup(TNode left){
-  return d_orderedListMap.find(left) != d_orderedListMap.end();
+bool ArithUnatePropagator::leftIsSetup(TNode left) const{
+  return d_setsMap.find(left) != d_setsMap.end();
 }
 
-ArithUnatePropagator::OrderedSetTriple& ArithUnatePropagator::getOrderedSetTriple(TNode left){
+const ArithUnatePropagator::VariablesSets& ArithUnatePropagator::getVariablesSets(TNode left) const{
   Assert(leftIsSetup(left));
-  return d_orderedListMap[left];
+  NodeToSetsMap::const_iterator i = d_setsMap.find(left);
+  return i->second;
+}
+ArithUnatePropagator::VariablesSets& ArithUnatePropagator::getVariablesSets(TNode left){
+  Assert(leftIsSetup(left));
+  NodeToSetsMap::iterator i = d_setsMap.find(left);
+  return i->second;
+}
+EqualValueSet& ArithUnatePropagator::getEqualValueSet(TNode left){
+  Assert(leftIsSetup(left));
+  return getVariablesSets(left).d_eqValueSet;
 }
 
-OrderedSet& ArithUnatePropagator::getEqSet(TNode left){
+const EqualValueSet& ArithUnatePropagator::getEqualValueSet(TNode left) const{
   Assert(leftIsSetup(left));
-  return getOrderedSetTriple(left).d_eqSet;
+  return getVariablesSets(left).d_eqValueSet;
 }
-OrderedSet& ArithUnatePropagator::getLeqSet(TNode left){
+
+BoundValueSet& ArithUnatePropagator::getBoundValueSet(TNode left){
   Assert(leftIsSetup(left));
-  return getOrderedSetTriple(left).d_leqSet;
+  return getVariablesSets(left).d_boundValueSet;
 }
-OrderedSet& ArithUnatePropagator::getGeqSet(TNode left){
+
+const BoundValueSet& ArithUnatePropagator::getBoundValueSet(TNode left) const{
   Assert(leftIsSetup(left));
-  return getOrderedSetTriple(left).d_geqSet;
+  return getVariablesSets(left).d_boundValueSet;
 }
 
-bool ArithUnatePropagator::hasAnyAtoms(TNode v){
+bool ArithUnatePropagator::hasAnyAtoms(TNode v) const{
   Assert(!leftIsSetup(v)
-         || !(getEqSet(v)).empty()
-         || !(getLeqSet(v)).empty()
-         || !(getGeqSet(v)).empty());
+         || !(getEqualValueSet(v)).empty()
+         || !(getBoundValueSet(v)).empty());
 
   return leftIsSetup(v);
 }
@@ -68,7 +79,58 @@ bool ArithUnatePropagator::hasAnyAtoms(TNode v){
 void ArithUnatePropagator::setupLefthand(TNode left){
   Assert(!leftIsSetup(left));
 
-  d_orderedListMap[left] = OrderedSetTriple();
+  d_setsMap[left] = VariablesSets();
+}
+
+bool ArithUnatePropagator::containsLiteral(TNode lit) const{
+  switch(lit.getKind()){
+  case NOT: return containsAtom(lit[0]);
+  default: return containsAtom(lit);
+  }
+}
+
+bool ArithUnatePropagator::containsAtom(TNode atom) const{
+  switch(atom.getKind()){
+  case EQUAL: return containsEquality(atom);
+  case LEQ: return containsLeq(atom);
+  case GEQ: return containsGeq(atom);
+  default:
+    Unreachable();
+  }
+}
+
+bool ArithUnatePropagator::containsEquality(TNode atom) const{
+  TNode left = atom[0];
+  const EqualValueSet& eqSet = getEqualValueSet(left);
+  return eqSet.find(atom) != eqSet.end();
+}
+
+bool ArithUnatePropagator::containsLeq(TNode atom) const{
+  TNode left = atom[0];
+  const Rational& value = rightHandRational(atom);
+
+  const BoundValueSet& bvSet = getBoundValueSet(left);
+  BoundValueSet::const_iterator i = bvSet.find(value);
+  if(i == bvSet.end()){
+    return false;
+  }else{
+    const BoundValueEntry& entry = i->second;
+    return entry.hasLeq();
+  }
+}
+
+bool ArithUnatePropagator::containsGeq(TNode atom) const{
+  TNode left = atom[0];
+  const Rational& value = rightHandRational(atom);
+
+  const BoundValueSet& bvSet = getBoundValueSet(left);
+  BoundValueSet::const_iterator i = bvSet.find(value);
+  if(i == bvSet.end()){
+    return false;
+  }else{
+    const BoundValueEntry& entry = i->second;
+    return entry.hasGeq();
+  }
 }
 
 void ArithUnatePropagator::addAtom(TNode atom){
@@ -79,39 +141,47 @@ void ArithUnatePropagator::addAtom(TNode atom){
     setupLefthand(left);
   }
 
-  OrderedSet& eqSet = getEqSet(left);
-  OrderedSet& leqSet = getLeqSet(left);
-  OrderedSet& geqSet = getGeqSet(left);
+  const Rational& value = rightHandRational(atom);
 
   switch(atom.getKind()){
   case EQUAL:
     {
-      pair<OrderedSet::iterator, bool> res = eqSet.insert(atom);
+      Assert(!containsEquality(atom));
+      addImplicationsUsingEqualityAndEqualityValues(atom);
+      addImplicationsUsingEqualityAndBoundValues(atom);
+
+      pair<EqualValueSet::iterator, bool> res = getEqualValueSet(left).insert(atom);
       Assert(res.second);
-      addImplicationsUsingEqualityAndEqualityList(atom, eqSet);
-      addImplicationsUsingEqualityAndLeqList(atom, leqSet);
-      addImplicationsUsingEqualityAndGeqList(atom, geqSet);
       break;
     }
   case LEQ:
     {
-      pair<OrderedSet::iterator, bool> res = leqSet.insert(atom);
-      Assert(res.second);
-
-      addImplicationsUsingLeqAndEqualityList(atom, eqSet);
-      addImplicationsUsingLeqAndLeqList(atom, leqSet);
-      addImplicationsUsingLeqAndGeqList(atom, geqSet);
+      addImplicationsUsingLeqAndEqualityValues(atom);
+      addImplicationsUsingLeqAndBoundValues(atom);
+
+      BoundValueSet& bvSet = getBoundValueSet(left);
+      if(hasBoundValueEntry(atom)){
+        BoundValueSet::iterator i = bvSet.find(value);
+        BoundValueEntry& inSet = i->second;
+        inSet.addLeq(atom);
+      }else{
+        bvSet.insert(make_pair(value, BoundValueEntry::mkFromLeq(atom)));
+      }
       break;
     }
   case GEQ:
     {
-      pair<OrderedSet::iterator, bool> res = geqSet.insert(atom);
-      Assert(res.second);
-
-      addImplicationsUsingGeqAndEqualityList(atom, eqSet);
-      addImplicationsUsingGeqAndLeqList(atom, leqSet);
-      addImplicationsUsingGeqAndGeqList(atom, geqSet);
-
+      addImplicationsUsingGeqAndEqualityValues(atom);
+      addImplicationsUsingGeqAndBoundValues(atom);
+
+      BoundValueSet& bvSet = getBoundValueSet(left);
+      if(hasBoundValueEntry(atom)){
+        BoundValueSet::iterator i = bvSet.find(value);
+        BoundValueEntry& inSet = i->second;
+        inSet.addGeq(atom);
+      }else{
+        bvSet.insert(make_pair(value, BoundValueEntry::mkFromGeq(atom)));
+      }
       break;
     }
   default:
@@ -119,6 +189,13 @@ void ArithUnatePropagator::addAtom(TNode atom){
   }
 }
 
+bool ArithUnatePropagator::hasBoundValueEntry(TNode atom){
+  TNode left = atom[0];
+  const Rational& value = rightHandRational(atom);
+  BoundValueSet& bvSet = getBoundValueSet(left);
+  return bvSet.find(value) != bvSet.end();
+}
+
 bool rightHandRationalIsEqual(TNode a, TNode b){
   TNode secondA = a[1];
   TNode secondB = b[1];
@@ -135,162 +212,146 @@ bool rightHandRationalIsLT(TNode a, TNode b){
   return RightHandRationalLT()(a,b);
 }
 
-//void addImplicationsUsingEqualityAndEqualityList(TNode eq, OrderedSet* eqSet);
-
-void ArithUnatePropagator::addImplicationsUsingEqualityAndEqualityList(TNode atom, OrderedSet& eqSet){
+void ArithUnatePropagator::addImplicationsUsingEqualityAndEqualityValues(TNode atom){
   Assert(atom.getKind() == EQUAL);
-  OrderedSet::iterator eqPos = eqSet.find(atom);
-  Assert(eqPos != eqSet.end());
-  Assert(*eqPos == atom);
+  TNode left = atom[0];
+  EqualValueSet& eqSet = getEqualValueSet(left);
 
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
-  for(OrderedSet::iterator eqIter = eqSet.begin();
-      eqIter != eqSet.end(); ++eqIter){
-    if(eqIter == eqPos) continue;
+
+  for(EqualValueSet::iterator eqIter = eqSet.begin(), endIter = eqSet.end();
+      eqIter != endIter; ++eqIter){
     TNode eq = *eqIter;
-    Assert(!rightHandRationalIsEqual(eq, atom));
+    Assert(eq != atom);
     addImplication(eq, negation);
   }
 }
 
-void ArithUnatePropagator::addImplicationsUsingEqualityAndLeqList(TNode atom, OrderedSet& leqSet){
-
-  Assert(atom.getKind() == EQUAL);
-  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+// if weaker, do not return an equivalent node
+// if strict, get the strongest bound implied by  (< x value)
+// if !strict, get the strongest bound implied by  (<= x value)
+Node getUpperBound(const BoundValueSet& bvSet, const Rational& value, bool strict, bool weaker){
+  BoundValueSet::const_iterator bv = bvSet.lower_bound(value);
+  if(bv == bvSet.end()){
+    return Node::null();
+  }
 
-  OrderedSet::iterator leqIter = leqSet.lower_bound(atom);
-  if(leqIter != leqSet.end()){
-    TNode lowerBound = *leqIter;
-    if(rightHandRationalIsEqual(atom, lowerBound)){
-      addImplication(atom, lowerBound);  // x=b /\ b = b' => x <= b'
-      if(leqIter != leqSet.begin()){
-        --leqIter;
-        Assert(rightHandRationalIsLT(*leqIter, atom));
-        addImplication(*leqIter, negation); // x=b /\ b > b' => x > b'
-      }
-    }else{
-      //probably wrong
-      Assert(rightHandRationalIsLT(atom, lowerBound));
-      addImplication(atom, lowerBound);// x=b /\ b < b' => x <= b'
-
-      if(leqIter != leqSet.begin()){
-        --leqIter;
-        Assert(rightHandRationalIsLT(*leqIter, atom));
-        addImplication(*leqIter, negation);// x=b /\ b > b' => x > b'
-      }
+  if((bv->second).getValue() == value){
+    const BoundValueEntry& entry = bv->second;
+    if(strict && entry.hasGeq() && !weaker){
+      return NodeBuilder<1>(NOT) << entry.getGeq();
+    }else if(entry.hasLeq() && (strict || !weaker)){
+      return entry.getLeq();
     }
-  }else if(leqIter != leqSet.begin()){
-    --leqIter;
-    TNode strictlyLessThan = *leqIter;
-    Assert(rightHandRationalIsLT(strictlyLessThan, atom));
-    addImplication(*leqIter, negation); // x=b /\ b < b' => x <= b'
+  }
+  ++bv;
+  if(bv == bvSet.end()){
+    return Node::null();
+  }
+  Assert(bv->second.getValue() > value);
+  const BoundValueEntry& entry = bv->second;
+  if(entry.hasGeq()){
+    return NodeBuilder<1>(NOT) << entry.getGeq();
   }else{
-    Assert(leqSet.empty());
+    Assert(entry.hasLeq());
+    return entry.getLeq();
   }
 }
 
-void ArithUnatePropagator::addImplicationsUsingEqualityAndGeqList(TNode atom, OrderedSet& geqSet){
 
-  Assert(atom.getKind() == EQUAL);
-  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
 
-  OrderedSet::iterator geqIter = geqSet.lower_bound(atom);
-  if(geqIter != geqSet.end()){
-    TNode lowerBound = *geqIter;
-    if(rightHandRationalIsEqual(atom, lowerBound)){
-      addImplication(atom, lowerBound);  // x=b /\ b = b' => x >= b'
-      ++geqIter;
-      if(geqIter != geqSet.end()){ // x=b /\ b < b' => x < b'
-        TNode strictlyGt = *geqIter;
-        Assert(rightHandRationalIsLT( atom, strictlyGt ));
-        addImplication(strictlyGt, negation);
-      }
-    }else{
-      Assert(rightHandRationalIsLT(atom, lowerBound));
-      addImplication(lowerBound, negation);// x=b /\ b < b' => x < b'
-      if(geqIter != geqSet.begin()){
-        --geqIter;
-        TNode strictlyLessThan = *geqIter;
-        Assert(rightHandRationalIsLT(strictlyLessThan, atom));
-        addImplication(atom, strictlyLessThan);// x=b /\ b > b' => x >= b'
-      }
+
+// if weaker, do not return an equivalent node
+// if strict, get the strongest bound implied by  (> x value)
+// if !strict, get the strongest bound implied by  (>= x value)
+Node getLowerBound(const BoundValueSet& bvSet, const Rational& value, bool strict, bool weaker){
+  static int time = 0;
+  ++time;
+
+  if(bvSet.empty()){
+    return Node::null();
+  }
+  Debug("getLowerBound") << "getLowerBound" << bvSet.size() << " " << value << " " << strict << weaker << endl;
+
+  BoundValueSet::const_iterator bv = bvSet.lower_bound(value);
+  if(bv == bvSet.end()){
+    Debug("getLowerBound") << "got end " << value << " " << (bvSet.rbegin()->second).getValue() << endl;
+    Assert(value > (bvSet.rbegin()->second).getValue());
+  }else{
+    Debug("getLowerBound") << value << ", " << bv->second.getValue() << endl;
+    Assert(value <= bv->second.getValue());
+  }
+
+  if(bv != bvSet.end() && (bv->second).getValue() == value){
+    const BoundValueEntry& entry = bv->second;
+    Debug("getLowerBound") << entry.hasLeq() << entry.hasGeq() << endl;
+    if(strict && entry.hasLeq() && !weaker){
+      return NodeBuilder<1>(NOT) << entry.getLeq();
+    }else if(entry.hasGeq() && (strict || !weaker)){
+      return entry.getGeq();
     }
-  }else if(geqIter != geqSet.begin()){
-    --geqIter;
-    TNode strictlyLT = *geqIter;
-    Assert(rightHandRationalIsLT(strictlyLT, atom));
-    addImplication(atom, strictlyLT);// x=b /\ b > b' => x >= b'
+  }
+  if(bv == bvSet.begin()){
+    return Node::null();
   }else{
-    Assert(geqSet.empty());
+    --bv;
+    // (and (>= x v) (>= v v')) then (> x v')
+    Assert(bv->second.getValue() < value);
+    const BoundValueEntry& entry = bv->second;
+    if(entry.hasLeq()){
+      return NodeBuilder<1>(NOT) << entry.getLeq();
+    }else{
+      Assert(entry.hasGeq());
+      return entry.getGeq();
+    }
   }
 }
 
-void ArithUnatePropagator::addImplicationsUsingLeqAndLeqList(TNode atom, OrderedSet& leqSet)
-{
-  Assert(atom.getKind() == LEQ);
-  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+void ArithUnatePropagator::addImplicationsUsingEqualityAndBoundValues(TNode atom){
+  Assert(atom.getKind() == EQUAL);
+  Node left = atom[0];
 
-  OrderedSet::iterator atomPos = leqSet.find(atom);
-  Assert(atomPos != leqSet.end());
-  Assert(*atomPos == atom);
+  const Rational& value = rightHandRational(atom);
 
-  if(atomPos != leqSet.begin()){
-    --atomPos;
-    TNode beforeLeq = *atomPos;
-    Assert(rightHandRationalIsLT(beforeLeq, atom));
-    addImplication(beforeLeq, atom);// x<=b' /\ b' < b => x <= b
-    ++atomPos;
+  BoundValueSet& bvSet = getBoundValueSet(left);
+  Node ub = getUpperBound(bvSet, value, false, false);
+  Node lb = getLowerBound(bvSet, value, false, false);
+
+  if(!ub.isNull()){
+    addImplication(atom, ub);
   }
-  ++atomPos;
-  if(atomPos != leqSet.end()){
-    TNode afterLeq = *atomPos;
-    Assert(rightHandRationalIsLT(atom, afterLeq));
-    addImplication(atom, afterLeq);// x<=b /\ b < b' => x <= b'
+
+  if(!lb.isNull()){
+    addImplication(atom, lb);
   }
 }
-void ArithUnatePropagator::addImplicationsUsingLeqAndGeqList(TNode atom, OrderedSet& geqSet) {
 
+void ArithUnatePropagator::addImplicationsUsingLeqAndBoundValues(TNode atom)
+{
   Assert(atom.getKind() == LEQ);
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
 
-  OrderedSet::iterator geqIter = geqSet.lower_bound(atom);
-  if(geqIter != geqSet.end()){
-    TNode lowerBound = *geqIter;
-    if(rightHandRationalIsEqual(atom, lowerBound)){
-      Assert(rightHandRationalIsEqual(atom, lowerBound));
-      addImplication(negation, lowerBound);// (x > b) => (x >= b)
-      ++geqIter;
-      if(geqIter != geqSet.end()){
-        TNode next = *geqIter;
-        Assert(rightHandRationalIsLT(atom, next));
-        addImplication(next, negation);// x>=b' /\ b' > b => x > b
-      }
-    }else{
-      Assert(rightHandRationalIsLT(atom, lowerBound));
-      addImplication(lowerBound, negation);// x>=b' /\ b' > b => x > b
-      if(geqIter != geqSet.begin()){
-        --geqIter;
-        TNode prev = *geqIter;
-        Assert(rightHandRationalIsLT(prev, atom));
-        addImplication(negation, prev);// (x>b /\ b > b') => x >= b'
-      }
-    }
-  }else if(geqIter != geqSet.begin()){
-    --geqIter;
-    TNode strictlyLT = *geqIter;
-    Assert(rightHandRationalIsLT(strictlyLT, atom));
-    addImplication(negation, strictlyLT);// (x>b /\ b > b') => x >= b'
-  }else{
-    Assert(geqSet.empty());
+  Node ub = getImpliedUpperBoundUsingLeq(atom, false);
+  Node lb = getImpliedLowerBoundUsingGT(negation, false);
+
+  if(!ub.isNull()){
+    addImplication(atom, ub);
+  }
+
+  if(!lb.isNull()){
+    addImplication(negation, lb);
   }
 }
 
-void ArithUnatePropagator::addImplicationsUsingLeqAndEqualityList(TNode atom, OrderedSet& eqSet) {
+void ArithUnatePropagator::addImplicationsUsingLeqAndEqualityValues(TNode atom) {
   Assert(atom.getKind() == LEQ);
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
 
+  TNode left = atom[0];
+  EqualValueSet& eqSet = getEqualValueSet(left);
+
   //TODO Improve this later
-  for(OrderedSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){
+  for(EqualValueSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){
     TNode eq = *eqIter;
     if(rightHandRationalIsEqual(atom, eq)){
       // (x = b' /\ b = b') =>  x <= b
@@ -306,73 +367,30 @@ void ArithUnatePropagator::addImplicationsUsingLeqAndEqualityList(TNode atom, Or
 }
 
 
-void ArithUnatePropagator::addImplicationsUsingGeqAndGeqList(TNode atom, OrderedSet& geqSet){
+void ArithUnatePropagator::addImplicationsUsingGeqAndBoundValues(TNode atom){
   Assert(atom.getKind() == GEQ);
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
 
-  OrderedSet::iterator atomPos = geqSet.find(atom);
-  Assert(atomPos != geqSet.end());
-  Assert(*atomPos == atom);
+  Node lb = getImpliedLowerBoundUsingGeq(atom, false); //What is implied by (>= left value)
+  Node ub = getImpliedUpperBoundUsingLT(negation, false);
 
-  if(atomPos != geqSet.begin()){
-    --atomPos;
-    TNode beforeGeq = *atomPos;
-    Assert(rightHandRationalIsLT(beforeGeq, atom));
-    addImplication(atom, beforeGeq);// x>=b /\ b > b' => x >= b'
-    ++atomPos;
-  }
-  ++atomPos;
-  if(atomPos != geqSet.end()){
-    TNode afterGeq = *atomPos;
-    Assert(rightHandRationalIsLT(atom, afterGeq));
-    addImplication(afterGeq, atom);// x>=b' /\ b' > b => x >= b
+  if(!lb.isNull()){
+    addImplication(atom, lb);
   }
-}
-
-void ArithUnatePropagator::addImplicationsUsingGeqAndLeqList(TNode atom, OrderedSet& leqSet){
 
-  Assert(atom.getKind() == GEQ);
-  Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
-
-  OrderedSet::iterator leqIter = leqSet.lower_bound(atom);
-  if(leqIter != leqSet.end()){
-    TNode lowerBound = *leqIter;
-    if(rightHandRationalIsEqual(atom, lowerBound)){
-      Assert(rightHandRationalIsEqual(atom, lowerBound));
-      addImplication(negation, lowerBound);// (x < b) => (x <= b)
-
-      if(leqIter != leqSet.begin()){
-        --leqIter;
-        TNode prev = *leqIter;
-        Assert(rightHandRationalIsLT(prev, atom));
-        addImplication(prev, negation);// x<=b' /\ b' < b => x < b
-      }
-    }else{
-      Assert(rightHandRationalIsLT(atom, lowerBound));
-      addImplication(negation, lowerBound);// (x < b /\ b < b') => x <= b'
-      ++leqIter;
-      if(leqIter != leqSet.end()){
-        TNode next = *leqIter;
-        Assert(rightHandRationalIsLT(atom, next));
-        addImplication(negation, next);// (x < b /\ b < b') => x <= b'
-      }
-    }
-  }else if(leqIter != leqSet.begin()){
-    --leqIter;
-    TNode strictlyLT = *leqIter;
-    Assert(rightHandRationalIsLT(strictlyLT, atom));
-    addImplication(strictlyLT, negation);// (x <= b' /\ b' < b) => x < b
-  }else{
-    Assert(leqSet.empty());
+  if(!ub.isNull()){
+    addImplication(negation, ub);
   }
 }
-void ArithUnatePropagator::addImplicationsUsingGeqAndEqualityList(TNode atom, OrderedSet& eqSet){
+void ArithUnatePropagator::addImplicationsUsingGeqAndEqualityValues(TNode atom){
 
   Assert(atom.getKind() == GEQ);
   Node negation = NodeManager::currentNM()->mkNode(NOT, atom);
+  Node left = atom[0];
+  EqualValueSet& eqSet = getEqualValueSet(left);
 
   //TODO Improve this later
-  for(OrderedSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){
+  for(EqualValueSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){
     TNode eq = *eqIter;
     if(rightHandRationalIsEqual(atom, eq)){
       // (x = b' /\ b = b') =>  x >= b
@@ -390,8 +408,132 @@ void ArithUnatePropagator::addImplicationsUsingGeqAndEqualityList(TNode atom, Or
 void ArithUnatePropagator::addImplication(TNode a, TNode b){
   Node imp = NodeBuilder<2>(IMPLIES) << a << b;
 
-  Debug("arith-propagate") << "ArithUnatePropagator::addImplication";
-  Debug("arith-propagate") << "(" << a << ", " << b <<")" << endl;
+  Debug("arith::unate") << "ArithUnatePropagator::addImplication"
+                        << "(" << a << ", " << b <<")" << endl;
 
   d_arithOut.lemma(imp);
 }
+
+
+Node ArithUnatePropagator::getImpliedUpperBoundUsingLeq(TNode leq, bool weaker) const {
+  Assert(leq.getKind() == LEQ);
+  Node left = leq[0];
+
+  if(!leftIsSetup(left)) return Node::null();
+
+  const Rational& value = rightHandRational(leq);
+  const BoundValueSet& bvSet = getBoundValueSet(left);
+
+  Node ub = getUpperBound(bvSet, value, false, weaker);
+  return ub;
+}
+
+Node ArithUnatePropagator::getImpliedUpperBoundUsingLT(TNode lt, bool weaker) const {
+  Assert(lt.getKind() == NOT && lt[0].getKind() == GEQ);
+  Node atom = lt[0];
+  Node left = atom[0];
+
+  if(!leftIsSetup(left)) return Node::null();
+
+  const Rational& value = rightHandRational(atom);
+  const BoundValueSet& bvSet = getBoundValueSet(left);
+
+  return getUpperBound(bvSet, value, true, weaker);
+}
+
+Node ArithUnatePropagator::getBestImpliedUpperBound(TNode upperBound) const {
+  Node result = Node::null();
+  if(upperBound.getKind() == LEQ ){
+    result = getImpliedUpperBoundUsingLeq(upperBound, false);
+  }else if(upperBound.getKind() == NOT && upperBound[0].getKind() == GEQ){
+    result = getImpliedUpperBoundUsingLT(upperBound, false);
+  }else if(upperBound.getKind() == LT){
+    Node geq = NodeBuilder<2>(GEQ) << upperBound[0] << upperBound[1];
+    Node lt = NodeBuilder<1>(NOT) << geq;
+    result = getImpliedUpperBoundUsingLT(lt, false);
+  }else{
+    Unreachable();
+  }
+
+  Debug("arith::unate") << upperBound <<" -> " << result << std::endl;
+  return result;
+}
+
+Node ArithUnatePropagator::getWeakerImpliedUpperBound(TNode upperBound) const {
+  Node result = Node::null();
+  if(upperBound.getKind() == LEQ ){
+    result = getImpliedUpperBoundUsingLeq(upperBound, true);
+  }else if(upperBound.getKind() == NOT && upperBound[0].getKind() == GEQ){
+    result = getImpliedUpperBoundUsingLT(upperBound, true);
+  }else if(upperBound.getKind() == LT){
+    Node geq = NodeBuilder<2>(GEQ) << upperBound[0] << upperBound[1];
+    Node lt = NodeBuilder<1>(NOT) << geq;
+    result = getImpliedUpperBoundUsingLT(lt, true);
+  }else{
+    Unreachable();
+  }
+  Assert(upperBound != result);
+  Debug("arith::unate") << upperBound <<" -> " << result << std::endl;
+  return result;
+}
+
+Node ArithUnatePropagator::getImpliedLowerBoundUsingGT(TNode gt, bool weaker) const {
+  Assert(gt.getKind() == NOT && gt[0].getKind() == LEQ);
+  Node atom = gt[0];
+  Node left = atom[0];
+
+  if(!leftIsSetup(left)) return Node::null();
+
+  const Rational& value = rightHandRational(atom);
+  const BoundValueSet& bvSet = getBoundValueSet(left);
+
+  return getLowerBound(bvSet, value, true, weaker);
+}
+
+Node ArithUnatePropagator::getImpliedLowerBoundUsingGeq(TNode geq, bool weaker) const {
+  Assert(geq.getKind() == GEQ);
+  Node left = geq[0];
+
+  if(!leftIsSetup(left)) return Node::null();
+
+  const Rational& value = rightHandRational(geq);
+  const BoundValueSet& bvSet = getBoundValueSet(left);
+
+  return getLowerBound(bvSet, value, false, weaker);
+}
+
+Node ArithUnatePropagator::getBestImpliedLowerBound(TNode lowerBound) const {
+  Node result = Node::null();
+  if(lowerBound.getKind() == GEQ ){
+    result = getImpliedLowerBoundUsingGeq(lowerBound, false);
+  }else if(lowerBound.getKind() == NOT && lowerBound[0].getKind() == LEQ){
+    result = getImpliedLowerBoundUsingGT(lowerBound, false);
+  }else if(lowerBound.getKind() == GT){
+    Node leq = NodeBuilder<2>(LEQ)<<lowerBound[0]<< lowerBound[1];
+    Node gt = NodeBuilder<1>(NOT) << leq;
+    result = getImpliedLowerBoundUsingGT(gt, false);
+  }else{
+    Unreachable();
+  }
+  Debug("arith::unate") << lowerBound <<" -> " << result << std::endl;
+  return result;
+}
+
+Node ArithUnatePropagator::getWeakerImpliedLowerBound(TNode lowerBound) const {
+  Node result = Node::null();
+  if(lowerBound.getKind() == GEQ ){
+    result = getImpliedLowerBoundUsingGeq(lowerBound, true);
+  }else if(lowerBound.getKind() == NOT && lowerBound[0].getKind() == LEQ){
+    result = getImpliedLowerBoundUsingGT(lowerBound, true);
+  }else if(lowerBound.getKind() == GT){
+    Node leq = NodeBuilder<2>(LEQ)<<lowerBound[0]<< lowerBound[1];
+    Node gt = NodeBuilder<1>(NOT) << leq;
+    result = getImpliedLowerBoundUsingGT(gt, true);
+  }else{
+    Unreachable();
+  }
+  Assert(result != lowerBound);
+
+  Debug("arith::unate") << lowerBound <<" -> " << result << std::endl;
+  return result;
+}
diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h
index 383b9f8e8..8c2720aea 100644
--- a/src/theory/arith/unate_propagator.h
+++ b/src/theory/arith/unate_propagator.h
@@ -68,15 +68,14 @@ private:
    */
   OutputChannel& d_arithOut;
 
-  struct OrderedSetTriple {
-    OrderedSet d_leqSet;
-    OrderedSet d_eqSet;
-    OrderedSet d_geqSet;
+  struct VariablesSets {
+    BoundValueSet d_boundValueSet;
+    EqualValueSet d_eqValueSet;
   };
 
   /** TODO: justify making this a TNode. */
-  typedef __gnu_cxx::hash_map<Node, OrderedSetTriple, NodeHashFunction> NodeToOrderedSetMap;
-  NodeToOrderedSetMap d_orderedListMap;
+  typedef __gnu_cxx::hash_map<TNode, VariablesSets, NodeHashFunction> NodeToSetsMap;
+  NodeToSetsMap d_setsMap;
 
 public:
   ArithUnatePropagator(context::Context* cxt, OutputChannel& arith);
@@ -88,20 +87,30 @@ public:
   void addAtom(TNode atom);
 
   /** Returns true if v has been added as a left hand side in an atom */
-  bool hasAnyAtoms(TNode v);
+  bool hasAnyAtoms(TNode v) const;
+
+  bool containsLiteral(TNode lit) const;
+  bool containsAtom(TNode atom) const;
+  bool containsEquality(TNode atom) const;
+  bool containsLeq(TNode atom) const;
+  bool containsGeq(TNode atom) const;
+
+
 
 private:
-  OrderedSetTriple& getOrderedSetTriple(TNode left);
-  OrderedSet& getEqSet(TNode left);
-  OrderedSet& getLeqSet(TNode left);
-  OrderedSet& getGeqSet(TNode left);
+  VariablesSets& getVariablesSets(TNode left);
+  BoundValueSet& getBoundValueSet(TNode left);
+  EqualValueSet& getEqualValueSet(TNode left);
 
+  const VariablesSets& getVariablesSets(TNode left) const;
+  const BoundValueSet& getBoundValueSet(TNode left) const;
+  const EqualValueSet& getEqualValueSet(TNode left) const;
 
   /** Sends an implication (=> a b) to the PropEngine via d_arithOut. */
   void addImplication(TNode a, TNode b);
 
   /** Check to make sure an lhs has been properly set-up. */
-  bool leftIsSetup(TNode left);
+  bool leftIsSetup(TNode left) const;
 
   /** Initializes the lists associated with a unique lhs. */
   void setupLefthand(TNode left);
@@ -123,18 +132,30 @@ private:
    * of all of the special casing and C++ iterator manipulation required.
    */
 
-  void addImplicationsUsingEqualityAndEqualityList(TNode eq, OrderedSet& eqSet);
-  void addImplicationsUsingEqualityAndLeqList(TNode eq, OrderedSet& leqSet);
-  void addImplicationsUsingEqualityAndGeqList(TNode eq, OrderedSet& geqSet);
+  void addImplicationsUsingEqualityAndEqualityValues(TNode eq);
+  void addImplicationsUsingEqualityAndBoundValues(TNode eq);
+
+  void addImplicationsUsingLeqAndEqualityValues(TNode leq);
+  void addImplicationsUsingLeqAndBoundValues(TNode leq);
+
+  void addImplicationsUsingGeqAndEqualityValues(TNode geq);
+  void addImplicationsUsingGeqAndBoundValues(TNode geq);
 
-  void addImplicationsUsingLeqAndEqualityList(TNode leq, OrderedSet& eqSet);
-  void addImplicationsUsingLeqAndLeqList(TNode leq, OrderedSet& leqSet);
-  void addImplicationsUsingLeqAndGeqList(TNode leq, OrderedSet& geqSet);
+  bool hasBoundValueEntry(TNode n);
+
+  Node getImpliedUpperBoundUsingLeq(TNode leq, bool weaker) const;
+  Node getImpliedUpperBoundUsingLT(TNode lt, bool weaker) const;
+
+  Node getImpliedLowerBoundUsingGeq(TNode geq, bool weaker) const;
+  Node getImpliedLowerBoundUsingGT(TNode gt, bool weaker) const;
+
+public:
+  Node getBestImpliedUpperBound(TNode upperBound) const;
+  Node getBestImpliedLowerBound(TNode lowerBound) const;
 
-  void addImplicationsUsingGeqAndEqualityList(TNode geq, OrderedSet& eqSet);
-  void addImplicationsUsingGeqAndLeqList(TNode geq, OrderedSet& leqSet);
-  void addImplicationsUsingGeqAndGeqList(TNode geq, OrderedSet& geqSet);
 
+  Node getWeakerImpliedUpperBound(TNode upperBound) const;
+  Node getWeakerImpliedLowerBound(TNode lowerBound) const;
 };
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 6226406d7..6973a7cad 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -103,6 +103,8 @@ class TheoryEngine {
 
     void propagate(TNode lit, bool)
       throw(theory::Interrupted, AssertionException) {
+      Debug("theory") << "EngineOutputChannel::propagate("
+                      << lit << ")" << std::endl;
       d_propagatedLiterals.push_back(lit);
       ++(d_engine->d_statistics.d_statPropagate);
     }
@@ -117,6 +119,8 @@ class TheoryEngine {
 
     void explanation(TNode explanationNode, bool)
       throw(theory::Interrupted, AssertionException) {
+      Debug("theory") << "EngineOutputChannel::explanation("
+                      << explanationNode << ")" << std::endl;
       d_explanationNode = explanationNode;
       ++(d_engine->d_statistics.d_statExplanation);
     }
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index eb63885a2..aaf9ca03b 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -47,7 +47,9 @@ libutil_la_SOURCES = \
 	language.h \
 	triple.h \
 	trans_closure.h \
-	trans_closure.cpp
+	trans_closure.cpp \
+	boolean_simplification.h
+
 libutil_la_LIBADD = \
 	@builddir@/libutilcudd.la
 libutilcudd_la_SOURCES = \
diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h
new file mode 100644
index 000000000..062bf11b6
--- /dev/null
+++ b/src/util/boolean_simplification.h
@@ -0,0 +1,116 @@
+/*********************                                                        */
+/*! \file bitvector.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BOOLEAN_SIMPLIFICATION_H
+#define __CVC4__BOOLEAN_SIMPLIFICATION_H
+
+#include "expr/node.h"
+#include "util/Assert.h"
+#include <vector>
+
+
+namespace CVC4 {
+
+class BooleanSimplification {
+public:
+
+  static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10;
+
+  static void removeDuplicates(std::vector<Node>& buffer){
+    if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD){
+      std::sort(buffer.begin(), buffer.end());
+      std::vector<Node>::iterator new_end = std::unique(buffer.begin(), buffer.end());
+      buffer.erase(new_end, buffer.end());
+    }
+  }
+
+  static Node simplifyConflict(Node andNode){
+    Assert(andNode.getKind() == kind::AND);
+    std::vector<Node> buffer;
+    push_back_associative_commute(andNode, buffer, kind::AND, kind::OR, false);
+
+    removeDuplicates(buffer);
+
+    NodeBuilder<> nb(kind::AND);
+    nb.append(buffer);
+    return nb;
+  }
+
+  static Node simplifyClause(Node orNode){
+    Assert(orNode.getKind() == kind::OR);
+    std::vector<Node> buffer;
+    push_back_associative_commute(orNode, buffer, kind::OR, kind::AND, false);
+
+    removeDuplicates(buffer);
+
+    NodeBuilder<> nb(kind::OR);
+    nb.append(buffer);
+    return nb;
+  }
+
+  static Node simplifyHornClause(Node implication){
+    Assert(implication.getKind() == kind::IMPLIES);
+    TNode left = implication[0];
+    TNode right = implication[1];
+    Node notLeft = NodeBuilder<1>(kind::NOT)<<left;
+    Node clause = NodeBuilder<2>(kind::OR)<< notLeft << right;
+    return simplifyClause(clause);
+  }
+
+  static void push_back_associative_commute(Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode){
+    Node::iterator i = n.begin(), end = n.end();
+    for(; i != end; ++i){
+      Node child = *i;
+      if(child.getKind() == k){
+        push_back_associative_commute(child, buffer, k, notK, negateNode);
+      }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){
+        push_back_associative_commute(child, buffer, notK, k, !negateNode);
+      }else{
+        if(negateNode){
+          buffer.push_back(negate(child));
+        }else{
+          buffer.push_back(child);
+        }
+      }
+    }
+  }
+
+  static Node negate(TNode n){
+    bool polarity = true;
+    TNode base = n;
+    while(base.getKind() == kind::NOT){
+      base = base[0];
+      polarity = !polarity;
+    }
+    if(polarity){
+      return base.notNode();
+    }else{
+      return base;
+    }
+  }
+
+};/* class BitVector */
+
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__BITVECTOR_H */
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 03dedfe00..6018ce611 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -81,6 +81,7 @@ Options::Options() :
   replayStream(NULL),
   replayLog(NULL),
   rewriteArithEqualities(false),
+  arithPropagation(false),
   satRandomFreq(0.0),
   satRandomSeed(91648253), //Minisat's default value
   pivotRule(MINIMUM)
@@ -120,6 +121,7 @@ static const string optionsDescription = "\
    --random-freq=P        sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\
    --random-seed=S        sets the random seed for the sat solver\n\
    --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic\n\
+   --enable-arithmetic-propagation turns on arithmetic propagation\n \
    --incremental          enable incremental solving\n";
 
 static const string languageDescription = "\
@@ -179,7 +181,8 @@ enum OptionValue {
   PIVOT_RULE,
   RANDOM_FREQUENCY,
   RANDOM_SEED,
-  REWRITE_ARITHMETIC_EQUALITIES
+  REWRITE_ARITHMETIC_EQUALITIES,
+  ARITHMETIC_PROPAGATION
 };/* enum OptionValue */
 
 /**
@@ -247,6 +250,7 @@ static struct option cmdlineOptions[] = {
   { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY  },
   { "random-seed" , required_argument, NULL, RANDOM_SEED  },
   { "rewrite-arithmetic-equalities", no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES },
+  { "enable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -477,6 +481,10 @@ throw(OptionException) {
       rewriteArithEqualities = true;
       break;
 
+    case ARITHMETIC_PROPAGATION:
+      arithPropagation = true;
+      break;
+
     case RANDOM_SEED:
       satRandomSeed = atof(optarg);
       break;
diff --git a/src/util/options.h b/src/util/options.h
index 8273db458..be432e5a7 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -143,6 +143,9 @@ struct CVC4_PUBLIC Options {
   /** Whether to rewrite equalities in arithmetic theory */
   bool rewriteArithEqualities;
 
+  /** Turn on and of arithmetic propagation. */
+  bool arithPropagation;
+
   /**
    * Frequency for the sat solver to make random decisions.
    * Should be between 0 and 1.
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 060c3036d..fb82a7ac9 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -150,6 +150,8 @@ public:
     Node leq1 = d_nm->mkNode(LEQ, x, c1);
     Node geq1 = d_nm->mkNode(GEQ, x, c1);
     Node lt1 = d_nm->mkNode(NOT, geq1);
+    Node gt0 = d_nm->mkNode(NOT, leq0);
+    Node gt1 = d_nm->mkNode(NOT, leq1);
 
     fakeTheoryEnginePreprocess(leq0);
     fakeTheoryEnginePreprocess(leq1);
@@ -161,20 +163,20 @@ public:
     d_arith->check(d_level);
     d_arith->propagate(d_level);
 
-    Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1);
+    Node gt1ThenGt0  = NodeBuilder<2>(IMPLIES) << gt1 << gt0;
+    Node geq1ThenGt0  = NodeBuilder<2>(IMPLIES) << geq1 << gt0;
     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
-    Node leq0ThenLt1  = NodeBuilder<2>(IMPLIES) << leq0 << lt1;
 
     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
 
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0);
 
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0);
 
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1);
   }
 
 
@@ -187,6 +189,8 @@ public:
     Node leq1 = d_nm->mkNode(LEQ, x, c1);
     Node geq1 = d_nm->mkNode(GEQ, x, c1);
     Node lt1 = d_nm->mkNode(NOT, geq1);
+    Node gt0 = d_nm->mkNode(NOT, leq0);
+    Node gt1 = d_nm->mkNode(NOT, leq1);
 
     fakeTheoryEnginePreprocess(leq0);
     fakeTheoryEnginePreprocess(leq1);
@@ -197,20 +201,20 @@ public:
 
     d_arith->check(d_level);
 
-    Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1);
+    Node gt1ThenGt0  = NodeBuilder<2>(IMPLIES) << gt1 << gt0;
+    Node geq1ThenGt0  = NodeBuilder<2>(IMPLIES) << geq1 << gt0;
     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
-    Node leq0ThenLt1  = NodeBuilder<2>(IMPLIES) << leq0 << lt1;
 
     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
 
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0);
 
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0);
 
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1);
   }
   void testTPLeq1() {
     Node x = d_nm->mkVar(*d_realType);
@@ -221,6 +225,8 @@ public:
     Node leq1 = d_nm->mkNode(LEQ, x, c1);
     Node geq1 = d_nm->mkNode(GEQ, x, c1);
     Node lt1 = d_nm->mkNode(NOT, geq1);
+    Node gt0 = d_nm->mkNode(NOT, leq0);
+    Node gt1 = d_nm->mkNode(NOT, leq1);
 
     fakeTheoryEnginePreprocess(leq0);
     fakeTheoryEnginePreprocess(leq1);
@@ -232,19 +238,19 @@ public:
     d_arith->check(d_level);
     d_arith->propagate(d_level);
 
-    Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1);
+    Node gt1ThenGt0  = NodeBuilder<2>(IMPLIES) << gt1 << gt0;
+    Node geq1ThenGt0  = NodeBuilder<2>(IMPLIES) << geq1 << gt0;
     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
-    Node leq0ThenLt1  = NodeBuilder<2>(IMPLIES) << leq0 << lt1;
 
     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
 
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0);
 
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0);
 
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1);
+    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1);
   }
 };