Farkas proof coefficients.

This commit adds tracking of Farkas coefficients to proof enabled builds in the theory of linear
real arithmetic when proofs are enabled. There could be some performance changes due to subtly
different search paths being taken.

Additional bug fixes:
- Polynomial::exactDivide did not satisfy preconditions to the Monomial constructor.
  To prevent future problems, Monomials should now be made via one of the mkMonomial functions.
- Fixes a bug in SumOfInfeasibilitiesSPD::greedyConflictSubsets().
  There was a way to use a row twice in the construction of the conflicts.
  This was violating an assumption in the Tableau when constructing the intermediate rows.

Constraints:
- To enable proofs, all conflicts and propagations are designed to go through the Constraint system
  before they are converted to externally understandable conflicts and propagations in the form
  of Node.
- Constraints must now be given a reason for marking them as true that corresponds to a proof.
- Constraints should now be marked as being true by one of the impliedbyX functions.
- Each impliedByX function has an ArithProofType associated with it.
- Each call to an impliedByX function stores a context dependent ConstraintRule object
  to track the proof.
- After marking the node as true the caller should either try to propagate the constraint or raise
	a conflict.
- There are no more special cases for marking a node as being true when its negation has a proof
  vs. when the negation does not have a proof. One must now explicitly pass in a inConflict flag
	to the impliedByX (and similar functions).
	For example,this is now longer both:
	  void setAssertedToTheTheory(TNode witness);
	  void setAssertedToTheTheoryWithNegationTrue(TNode witness);
  There is just:
    void setAssertedToTheTheory(TNode witness, bool inConflict);

21 files changed, 1907 insertions, 910 deletions

diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp
index 9a7878750..acae61db0 100644
--- a/src/theory/arith/arithvar.cpp
+++ b/src/theory/arith/arithvar.cpp
@@ -18,6 +18,7 @@
 
 #include "theory/arith/arithvar.h"
 #include <limits>
+#include <set>
 
 namespace CVC4 {
 namespace theory {
@@ -25,6 +26,11 @@ namespace arith {
 
 const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
 
+bool debugIsASet(const std::vector<ArithVar>& variables){
+  std::set<ArithVar> asSet(variables.begin(), variables.end());
+  return asSet.size() == variables.size();
+}
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
index 00545fb48..dd049e94f 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.h
@@ -37,6 +37,9 @@ typedef std::vector<ArithVar> ArithVarVec;
 typedef std::pair<ArithVar, Rational> ArithRatPair;
 typedef std::vector< ArithRatPair > ArithRatPairVec;
 
+extern bool debugIsASet(const ArithVarVec& variables);
+
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 68bf3bbae..b6e579465 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -57,29 +57,117 @@ void BasicVarModelUpdateCallBack::operator()(ArithVar x){
   d_ta.signal(x);
 }
 
-RaiseConflict::RaiseConflict(TheoryArithPrivate& ta, ConstraintCPVec& buf )
+RaiseConflict::RaiseConflict(TheoryArithPrivate& ta)
   : d_ta(ta)
-  , d_construction(buf)
 {}
 
+void RaiseConflict::raiseConflict(ConstraintCP c) const{
+  Assert(c->inConflict());
+  d_ta.raiseConflict(c);
+}
+
+FarkasConflictBuilder::FarkasConflictBuilder()
+  : d_farkas()
+  , d_constraints()
+  , d_consequent(NullConstraint)
+  , d_consequentSet(false)
+{
+  reset();
+}
+
+bool FarkasConflictBuilder::underConstruction() const{
+  return d_consequent != NullConstraint;
+}
+
+bool FarkasConflictBuilder::consequentIsSet() const{
+  return d_consequentSet;
+}
+
+void FarkasConflictBuilder::reset(){
+  d_consequent = NullConstraint;
+  d_constraints.clear();
+  d_consequentSet = false;
+  PROOF(d_farkas.clear());
+  Assert(!underConstruction());
+}
+
 /* Adds a constraint to the constraint under construction. */
-void RaiseConflict::addConstraint(ConstraintCP c){
-  d_construction.push_back(c);
+void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){
+  Assert(!PROOF_ON() ||
+         (!underConstruction() && d_constraints.empty() && d_farkas.empty()) ||
+         (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
+  Assert(PROOF_ON() || d_farkas.empty());
+  Assert(c->isTrue());
+
+  
+  if(d_consequent == NullConstraint){
+    d_consequent = c;
+  } else {
+    d_constraints.push_back(c);
+  }
+  PROOF(d_farkas.push_back(fc););
+  Assert(!PROOF_ON() || d_constraints.size() + 1 == d_farkas.size());
+  Assert(PROOF_ON() || d_farkas.empty());
 }
-/* Turns the vector under construction into a conflict */
-void RaiseConflict::commitConflict(){
-  Assert(!d_construction.empty());
-  sendConflict(d_construction);
-  d_construction.clear();
+
+void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult){
+  Assert(!mult.isZero());
+  if(PROOF_ON() && !mult.isOne()){
+    Rational prod = fc * mult;
+    addConstraint(c, prod);
+  }else{
+    addConstraint(c, fc);
+  }
 }
 
-void RaiseConflict::sendConflict(const ConstraintCPVec& vec){
-  d_ta.raiseConflict(vec);
+void FarkasConflictBuilder::makeLastConsequent(){
+  Assert(!d_consequentSet);
+  Assert(underConstruction());
+
+  if(d_constraints.empty()){
+    // no-op
+    d_consequentSet = true;
+  } else {
+    Assert(d_consequent != NullConstraint);
+    ConstraintCP last = d_constraints.back();
+    d_constraints.back() = d_consequent;
+    d_consequent = last;
+    PROOF( std::swap( d_farkas.front(), d_farkas.back() ) );
+    d_consequentSet = true;
+  }
+
+  Assert(! d_consequent->negationHasProof() );
+  Assert(d_consequentSet);
 }
 
+/* Turns the vector under construction into a conflict */
+ConstraintCP FarkasConflictBuilder::commitConflict(){
+  Assert(underConstruction());
+  Assert(!d_constraints.empty());
+  Assert(!PROOF_ON() ||
+         (!underConstruction() && d_constraints.empty() && d_farkas.empty()) ||
+         (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
+  Assert(PROOF_ON() || d_farkas.empty());
+  Assert(d_consequentSet);
+
+  ConstraintP not_c = d_consequent->getNegation();
+  RationalVectorCP coeffs = NULLPROOF(&d_farkas);
+  not_c->impliedByFarkas(d_constraints, coeffs, true );
+
+  reset();
+  Assert(!underConstruction());
+  Assert( not_c->inConflict() );
+  Assert(!d_consequentSet);
+  return not_c;
+}
+
+RaiseEqualityEngineConflict::RaiseEqualityEngineConflict(TheoryArithPrivate& ta)
+  : d_ta(ta)
+{}
+
 /* If you are not an equality engine, don't use this! */
-void RaiseConflict::blackBoxConflict(Node n){
-  d_ta.blackBoxConflict(n);
+void RaiseEqualityEngineConflict::raiseEEConflict(Node n) const{
+  d_ta.raiseBlackBoxConflict(n);
 }
 
 
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index f0e314bfb..ad88aea86 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -100,19 +100,80 @@ public:
 class RaiseConflict {
 private:
   TheoryArithPrivate& d_ta;
-  ConstraintCPVec& d_construction;
 public:
-  RaiseConflict(TheoryArithPrivate& ta, ConstraintCPVec& d_construction);
+  RaiseConflict(TheoryArithPrivate& ta);
+
+  /** Calls d_ta.raiseConflict(c) */
+  void raiseConflict(ConstraintCP c) const;
+};
+
+class FarkasConflictBuilder {
+private:
+  RationalVector d_farkas;
+  ConstraintCPVec d_constraints;
+  ConstraintCP d_consequent;
+  bool d_consequentSet;
+public:
+
+  /**
+   * Constructs a new FarkasConflictBuilder.
+   */
+  FarkasConflictBuilder();
+
+  /**
+   * Adds an antecedent constraint to the conflict under construction
+   * with the farkas coefficient fc * mult.
+   *
+   * The value mult is either 1 or -1.
+   */
+  void addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult);
+
+  /**
+   * Adds an antecedent constraint to the conflict under construction
+   * with the farkas coefficient fc.
+   */
+  void addConstraint(ConstraintCP c, const Rational& fc);
+  
+  /**
+   * Makes the last constraint added the consequent.
+   * Can be done exactly once per reset().
+   */
+  void makeLastConsequent();
+  
+  /**
+   * Turns the antecendents into a proof of the negation of one of the
+   * antecedents.
+   *
+   * The buffer is no longer underConstruction afterwards.
+   *
+   * precondition:
+   * - At least two constraints have been asserted.
+   * - makeLastConsequent() has been called.
+   *
+   * postcondition: The returned constraint is in conflict.
+   */
+  ConstraintCP commitConflict();
+
+  /** Returns true if a conflict has been pushed back since the last reset. */
+  bool underConstruction() const;
+  
+  /** Returns true if the consequent has been set since the last reset. */
+  bool consequentIsSet() const;
+
+  /** Resets the state of the buffer. */
+  void reset();
+};
 
-  /* Adds a constraint to the constraint under construction. */
-  void addConstraint(ConstraintCP c);
-  /* Turns the vector under construction into a conflict */
-  void commitConflict();
 
-  void sendConflict(const ConstraintCPVec& vec);
+class RaiseEqualityEngineConflict {
+private:
+  TheoryArithPrivate& d_ta;
+  
+public:
+  RaiseEqualityEngineConflict(TheoryArithPrivate& ta);
 
   /* If you are not an equality engine, don't use this! */
-  void blackBoxConflict(Node n);
+  void raiseEEConflict(Node n) const;
 };
 
 class BoundCountingLookup {
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 99f6e0836..8a145ffc2 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -23,7 +23,7 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, SetupLiteralCallBack setup, const ArithVariables& avars, RaiseConflict raiseConflict)
+ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, SetupLiteralCallBack setup, const ArithVariables& avars, RaiseEqualityEngineConflict raiseConflict)
   : d_inConflict(c),
     d_raiseConflict(raiseConflict),
     d_notify(*this),
@@ -109,7 +109,7 @@ void ArithCongruenceManager::raiseConflict(Node conflict){
   Assert(!inConflict());
   Debug("arith::conflict") << "difference manager conflict   " << conflict << std::endl;
   d_inConflict.raise();
-  d_raiseConflict.blackBoxConflict(conflict);
+  d_raiseConflict.raiseEEConflict(conflict);
 }
 bool ArithCongruenceManager::inConflict() const{
   return d_inConflict.isRaised();
@@ -172,7 +172,7 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP
   ++(d_statistics.d_watchedVariableIsZero);
 
   ArithVar s = lb->getVariable();
-  Node reason = Constraint_::externalExplainByAssertions(lb,ub);
+  Node reason = Constraint::externalExplainByAssertions(lb,ub);
 
   d_keepAlive.push_back(reason);
   assertionToEqualityEngine(true, s, reason);
@@ -413,7 +413,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
                           << ub << std::endl;
 
   ArithVar x = lb->getVariable();
-  Node reason = Constraint_::externalExplainByAssertions(lb,ub);
+  Node reason = Constraint::externalExplainByAssertions(lb,ub);
 
   Node xAsNode = d_avariables.asNode(x);
   Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart());
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index b0fa8f6f4..7ecfd21cf 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -41,7 +41,7 @@ namespace arith {
 class ArithCongruenceManager {
 private:
   context::CDRaised d_inConflict;
-  RaiseConflict d_raiseConflict;
+  RaiseEqualityEngineConflict d_raiseConflict;
 
   /**
    * The set of ArithVars equivalent to a pair of terms.
@@ -132,7 +132,7 @@ private:
 
 public:
 
-  ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseConflict raiseConflict);
+  ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseEqualityEngineConflict raiseConflict);
 
   Node explain(TNode literal);
   void explain(TNode lit, NodeBuilder<>& out);
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 5e3808fc7..94632e50e 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -20,6 +20,8 @@
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
 
+#include "proof/proof.h"
+
 #include <ostream>
 #include <algorithm>
 
@@ -64,7 +66,7 @@ ConstraintType constraintTypeOfComparison(const Comparison& cmp){
   }
 }
 
-Constraint_::Constraint_(ArithVar x,  ConstraintType t, const DeltaRational& v)
+Constraint::Constraint(ArithVar x,  ConstraintType t, const DeltaRational& v)
   : d_variable(x),
     d_type(t),
     d_value(v),
@@ -74,7 +76,7 @@ Constraint_::Constraint_(ArithVar x,  ConstraintType t, const DeltaRational& v)
     d_canBePropagated(false),
     d_assertionOrder(AssertionOrderSentinel),
     d_witness(TNode::null()),
-    d_proof(ProofIdSentinel),
+    d_crid(ConstraintRuleIdSentinel),
     d_split(false),
     d_variablePosition()
 {
@@ -82,6 +84,28 @@ Constraint_::Constraint_(ArithVar x,  ConstraintType t, const DeltaRational& v)
 }
 
 
+std::ostream& operator<<(std::ostream& o, const ArithProofType apt){
+  switch(apt){
+  case NoAP:  o << "NoAP"; break;
+  case AssumeAP:  o << "AssumeAP"; break;
+  case InternalAssumeAP:  o << "InternalAssumeAP"; break;
+  case FarkasAP:  o << "FarkasAP"; break;
+  case TrichotomyAP:  o << "TrichotomyAP"; break;
+  case EqualityEngineAP:  o << "EqualityEngineAP"; break;
+  case IntHoleAP: o << "IntHoleAP"; break;
+  default: break;
+  }
+  return o;
+}
+
+std::ostream& operator<<(std::ostream& o, const ConstraintCP c){
+  if(c == NullConstraint){
+    return o << "NullConstraint";
+  }else{
+    return o << *c;
+  }
+}
+
 std::ostream& operator<<(std::ostream& o, const ConstraintP c){
   if(c == NullConstraint){
     return o << "NullConstraint";
@@ -105,7 +129,7 @@ std::ostream& operator<<(std::ostream& o, const ConstraintType t){
   }
 }
 
-std::ostream& operator<<(std::ostream& o, const Constraint_& c){
+std::ostream& operator<<(std::ostream& o, const Constraint& c){
   o << c.getVariable() << ' ' << c.getType() << ' ' << c.getValue();
   if(c.hasLiteral()){
     o << "(node " << c.getLiteral() << ')';
@@ -154,7 +178,7 @@ std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v){
   return o;
 }
 
-void Constraint_::debugPrint() const {
+void Constraint::debugPrint() const {
   Message() << *this << endl;
 }
 
@@ -360,19 +384,25 @@ ConstraintP ValueCollection::nonNull() const{
   }
 }
 
-bool Constraint_::initialized() const {
+bool Constraint::initialized() const {
   return d_database != NULL;
 }
 
-void Constraint_::initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation){
+const ConstraintDatabase& Constraint::getDatabase() const{
+  Assert(initialized());
+  return *d_database;
+}
+
+void Constraint::initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation){
   Assert(!initialized());
   d_database = db;
   d_variablePosition = v;
   d_negation = negation;
 }
 
-Constraint_::~Constraint_() {
-  Assert(safeToGarbageCollect());
+Constraint::~Constraint() {
+  // Call this instead of safeToGarbageCollect()
+  Assert(!contextDependentDataIsSet());
 
   if(initialized()){
     ValueCollection& vc =  d_variablePosition->second;
@@ -392,11 +422,17 @@ Constraint_::~Constraint_() {
   }
 }
 
-const ValueCollection& Constraint_::getValueCollection() const{
+const ConstraintRule& Constraint::getConstraintRule() const {
+  Assert(hasProof());
+  return d_database->d_watches->d_constraintProofs[d_crid];
+}
+
+const ValueCollection& Constraint::getValueCollection() const{
   return d_variablePosition->second;
 }
 
-ConstraintP Constraint_::getCeiling() {
+
+ConstraintP Constraint::getCeiling() {
   Debug("getCeiling") << "Constraint_::getCeiling on " << *this << endl;
   Assert(getValue().getInfinitesimalPart().sgn() > 0);
 
@@ -406,7 +442,7 @@ ConstraintP Constraint_::getCeiling() {
   return d_database->getConstraint(getVariable(), getType(), ceiling);
 }
 
-ConstraintP Constraint_::getFloor() {
+ConstraintP Constraint::getFloor() {
   Assert(getValue().getInfinitesimalPart().sgn() < 0);
 
   DeltaRational floor(Rational(getValue().floor()));
@@ -415,26 +451,27 @@ ConstraintP Constraint_::getFloor() {
   return d_database->getConstraint(getVariable(), getType(), floor);
 }
 
-void Constraint_::setCanBePropagated() {
+void Constraint::setCanBePropagated() {
   Assert(!canBePropagated());
   d_database->pushCanBePropagatedWatch(this);
 }
 
-void Constraint_::setAssertedToTheTheoryWithNegationTrue(TNode witness) {
+void Constraint::setAssertedToTheTheory(TNode witness, bool nowInConflict) {
   Assert(hasLiteral());
   Assert(!assertedToTheTheory());
-  Assert(d_negation->hasProof());
+  Assert(negationHasProof() == nowInConflict);
   d_database->pushAssertionOrderWatch(this, witness);
-}
 
-void Constraint_::setAssertedToTheTheory(TNode witness) {
-  Assert(hasLiteral());
-  Assert(!assertedToTheTheory());
-  Assert(!d_negation->assertedToTheTheory());
-  d_database->pushAssertionOrderWatch(this, witness);
+  if(Debug.isOn("constraint::conflictCommit") && nowInConflict ){
+    Debug("constraint::conflictCommit") << "inConflict@setAssertedToTheTheory";
+    Debug("constraint::conflictCommit") << "\t" << this << std::endl;
+    Debug("constraint::conflictCommit") << "\t" << getNegation() << std::endl;
+    Debug("constraint::conflictCommit") << "\t" << getNegation()->externalExplainByAssertions() << std::endl;
+
+  }
 }
 
-bool Constraint_::satisfiedBy(const DeltaRational& dr) const {
+bool Constraint::satisfiedBy(const DeltaRational& dr) const {
   switch(getType()){
   case LowerBound:
     return getValue() <= dr;
@@ -448,19 +485,31 @@ bool Constraint_::satisfiedBy(const DeltaRational& dr) const {
   Unreachable();
 }
 
-bool Constraint_::isInternalDecision() const {
-  return d_proof == d_database->d_internalDecisionProof;
+bool Constraint::isInternalAssumption() const {
+  return getProofType() == InternalAssumeAP;
+}
+
+bool Constraint::isAssumption() const {
+  return getProofType() == AssumeAP;
+}
+
+bool Constraint::hasEqualityEngineProof() const {
+  return getProofType() == EqualityEngineAP;
 }
 
-bool Constraint_::isSelfExplaining() const {
-  return d_proof == d_database->d_selfExplainingProof;
+bool Constraint::hasFarkasProof() const {
+  return getProofType() == FarkasAP;
 }
 
-bool Constraint_::hasEqualityEngineProof() const {
-  return d_proof == d_database->d_equalityEngineProof;
+bool Constraint::hasIntHoleProof() const {
+  return getProofType() == IntHoleAP;
 }
 
-bool Constraint_::sanityChecking(Node n) const {
+bool Constraint::hasTrichotomyProof() const {
+  return getProofType() == TrichotomyAP;
+}
+
+bool Constraint::sanityChecking(Node n) const {
   Comparison cmp = Comparison::parseNormalForm(n);
   Kind k = cmp.comparisonKind();
   Polynomial pleft = cmp.normalizedVariablePart();
@@ -473,15 +522,15 @@ bool Constraint_::sanityChecking(Node n) const {
 
   const ArithVariables& avariables = d_database->getArithVariables();
 
-  Debug("nf::tmp") << cmp.getNode() << endl;
-  Debug("nf::tmp") << k << endl;
-  Debug("nf::tmp") << pleft.getNode() << endl;
-  Debug("nf::tmp") << left << endl;
-  Debug("nf::tmp") << right << endl;
-  Debug("nf::tmp") << getValue() << endl;
-  Debug("nf::tmp") << avariables.hasArithVar(left) << endl;
-  Debug("nf::tmp") << avariables.asArithVar(left) << endl;
-  Debug("nf::tmp") << getVariable() << endl;
+  Debug("Constraint::sanityChecking") << cmp.getNode() << endl;
+  Debug("Constraint::sanityChecking") << k << endl;
+  Debug("Constraint::sanityChecking") << pleft.getNode() << endl;
+  Debug("Constraint::sanityChecking") << left << endl;
+  Debug("Constraint::sanityChecking") << right << endl;
+  Debug("Constraint::sanityChecking") << getValue() << endl;
+  Debug("Constraint::sanityChecking") << avariables.hasArithVar(left) << endl;
+  Debug("Constraint::sanityChecking") << avariables.asArithVar(left) << endl;
+  Debug("Constraint::sanityChecking") << getVariable() << endl;
 
 
   if(avariables.hasArithVar(left) &&
@@ -504,7 +553,176 @@ bool Constraint_::sanityChecking(Node n) const {
   }
 }
 
-ConstraintP Constraint_::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){
+void ConstraintRule::debugPrint() const {
+  print(std::cerr);
+}
+
+ConstraintCP ConstraintDatabase::getAntecedent (AntecedentId p) const {
+  Assert(p < d_antecedents.size());
+  return d_antecedents[p];
+}
+
+
+void ConstraintRule::print(std::ostream& out) const {
+  
+  RationalVectorCP coeffs = NULLPROOF(d_farkasCoefficients);
+  out << "{ConstraintRule, ";
+  out << d_constraint << std::endl;
+  out << "d_proofType= " << d_proofType << ", " << std::endl;
+  out << "d_antecedentEnd= "<< d_antecedentEnd << std::endl;
+  
+  if(d_constraint != NullConstraint){
+    const ConstraintDatabase& database = d_constraint->getDatabase();
+    
+    size_t coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffs->size()-1 : 0;
+    AntecedentId p = d_antecedentEnd;
+    // must have at least one antecedent
+    ConstraintCP antecedent = database.getAntecedent(p);
+    while(antecedent != NullConstraint){
+      if(coeffs != RationalVectorCPSentinel){
+        out << coeffs->at(coeffIterator);
+      } else {
+        out << "_";
+      }
+      out << " * (" << *antecedent << ")" << std::endl;
+      
+      Assert((coeffs == RationalVectorCPSentinel) || coeffIterator > 0);
+      --p;
+      coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffIterator-1 : 0;
+      antecedent = database.getAntecedent(p);
+    }
+    if(coeffs != RationalVectorCPSentinel){
+      out << coeffs->front();
+    } else {
+      out << "_";
+    }
+    out << " * (" << *(d_constraint->getNegation()) << ")";
+    out << " [not d_constraint] " << endl;
+  }
+  out << "}";  
+}
+
+bool Constraint::wellFormedFarkasProof() const {
+  Assert(hasProof());
+  
+  const ConstraintRule& cr = getConstraintRule();
+  if(cr.d_constraint != this){ return false; }
+  if(cr.d_proofType != FarkasAP){ return false; }
+
+  AntecedentId p = cr.d_antecedentEnd;
+
+  // must have at least one antecedent
+  ConstraintCP antecedent = d_database->d_antecedents[p];
+  if(antecedent  == NullConstraint) { return false; }
+
+#ifdef CVC4_PROOF
+  if(!PROOF_ON()){ return cr.d_farkasCoefficients == RationalVectorCPSentinel; }
+  Assert(PROOF_ON());
+  
+  if(cr.d_farkasCoefficients == RationalVectorCPSentinel){ return false; }
+  if(cr.d_farkasCoefficients->size() < 2){ return false; }
+
+  const ArithVariables& vars = d_database->getArithVariables();
+
+  DeltaRational rhs(0);
+  Node lhs = Polynomial::mkZero().getNode();
+
+  RationalVector::const_iterator coeffIterator = cr.d_farkasCoefficients->end()-1;
+  RationalVector::const_iterator coeffBegin = cr.d_farkasCoefficients->begin();
+
+  while(antecedent != NullConstraint){
+    Assert(lhs.isNull() || Polynomial::isMember(lhs));
+
+    const Rational& coeff = *coeffIterator;
+    int coeffSgn = coeff.sgn();
+
+    rhs += antecedent->getValue() * coeff;
+
+    ArithVar antVar = antecedent->getVariable();
+    if(!lhs.isNull() && vars.hasNode(antVar)){
+      Node antAsNode = vars.asNode(antVar);
+      if(Polynomial::isMember(antAsNode)){
+        Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
+        Polynomial antPoly = Polynomial::parsePolynomial(antAsNode);
+        Polynomial sum = lhsPoly + (antPoly * coeff);
+        lhs = sum.getNode();
+      }else{
+        lhs = Node::null();
+      }
+    } else {
+      lhs = Node::null();
+    }
+    Debug("constraints::wffp") << "running sum: " << lhs << " <= " << rhs << endl;
+
+    switch( antecedent->getType() ){
+    case LowerBound:
+      // fc[l] < 0, therefore return false if coeffSgn >= 0
+      if(coeffSgn >= 0){ return false; }
+      break;
+    case UpperBound:
+      // fc[u] > 0, therefore return false if coeffSgn <= 0
+      if(coeffSgn <= 0){ return false; }
+      break;
+    case Equality:
+      if(coeffSgn == 0) { return false; }
+      break;
+    case Disequality:
+    default:
+      return false;
+    }
+    
+    if(coeffIterator == coeffBegin){ return false; }
+    --coeffIterator;
+    --p;
+    antecedent = d_database->d_antecedents[p];
+  }
+  if(coeffIterator != coeffBegin){ return false; }
+
+  const Rational& firstCoeff = (*coeffBegin);
+  int firstCoeffSgn = firstCoeff.sgn();
+  rhs += (getNegation()->getValue()) * firstCoeff;
+  if(!lhs.isNull() && vars.hasNode(getVariable())){
+    Node firstAsNode = vars.asNode(getVariable());
+    if(Polynomial::isMember(firstAsNode)){
+      Polynomial lhsPoly = Polynomial::parsePolynomial(lhs);
+      Polynomial firstPoly = Polynomial::parsePolynomial(firstAsNode);
+      Polynomial sum = lhsPoly + (firstPoly * firstCoeff);
+      lhs = sum.getNode();
+    }else{
+      lhs = Node::null();
+    }
+  }else{
+    lhs = Node::null();
+  }
+
+  switch( getNegation()->getType() ){
+  case LowerBound:
+    // fc[l] < 0, therefore return false if coeffSgn >= 0
+    if(firstCoeffSgn >= 0){ return false; }
+    break;
+  case UpperBound:
+    // fc[u] > 0, therefore return false if coeffSgn <= 0
+    if(firstCoeffSgn <= 0){ return false; }
+    break;
+  case Equality:
+    if(firstCoeffSgn == 0) { return false; }
+    break;
+  case Disequality:
+  default:
+    return false;
+  }
+  Debug("constraints::wffp") << "final sum: " << lhs << " <= " << rhs << endl;
+  // 0 = lhs <= rhs < 0
+  return
+    (lhs.isNull() || Constant::isMember(lhs) && Constant(lhs).isZero() ) &&
+    rhs.sgn() < 0;
+
+#else
+  return true;
+#endif
+}
+
+ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){
   switch(t){
   case LowerBound:
     {
@@ -513,12 +731,12 @@ ConstraintP Constraint_::makeNegation(ArithVar v, ConstraintType t, const DeltaR
         Assert(r.getInfinitesimalPart() == 1);
         // make (not (v > r)), which is (v <= r)
         DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
-        return new Constraint_(v, UpperBound, dropInf);
+        return new Constraint(v, UpperBound, dropInf);
       }else{
         Assert(r.infinitesimalSgn() == 0);
         // make (not (v >= r)), which is (v < r)
         DeltaRational addInf(r.getNoninfinitesimalPart(), -1);
-        return new Constraint_(v, UpperBound, addInf);
+        return new Constraint(v, UpperBound, addInf);
       }
     }
   case UpperBound:
@@ -528,18 +746,18 @@ ConstraintP Constraint_::makeNegation(ArithVar v, ConstraintType t, const DeltaR
         Assert(r.getInfinitesimalPart() == -1);
         // make (not (v < r)), which is (v >= r)
         DeltaRational dropInf(r.getNoninfinitesimalPart(), 0);
-        return new Constraint_(v, LowerBound, dropInf);
+        return new Constraint(v, LowerBound, dropInf);
       }else{
         Assert(r.infinitesimalSgn() == 0);
         // make (not (v <= r)), which is (v > r)
         DeltaRational addInf(r.getNoninfinitesimalPart(), 1);
-        return new Constraint_(v, LowerBound, addInf);
+        return new Constraint(v, LowerBound, addInf);
       }
     }
   case Equality:
-    return new Constraint_(v, Disequality, r);
+    return new Constraint(v, Disequality, r);
   case Disequality:
-    return new Constraint_(v, Equality, r);
+    return new Constraint(v, Equality, r);
   default:
     Unreachable();
     return NullConstraint;
@@ -547,24 +765,18 @@ ConstraintP Constraint_::makeNegation(ArithVar v, ConstraintType t, const DeltaR
 }
 
 ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVariables& avars, ArithCongruenceManager& cm, RaiseConflict raiseConflict)
-  : d_varDatabases(),
-    d_toPropagate(satContext),
-    d_proofs(satContext, false),
-    d_watches(new Watches(satContext, userContext)),
-    d_avariables(avars),
-    d_congruenceManager(cm),
-    d_satContext(satContext),
-    d_satAllocationLevel(d_satContext->getLevel()),
-    d_raiseConflict(raiseConflict)
+  : d_varDatabases()
+  , d_toPropagate(satContext)
+  , d_antecedents(satContext, false)
+  , d_watches(new Watches(satContext, userContext))
+  , d_avariables(avars)
+  , d_congruenceManager(cm)
+  , d_satContext(satContext)
+  , d_raiseConflict(raiseConflict)
+  , d_one(1)
+  , d_negOne(-1)
 {
-  d_selfExplainingProof = d_proofs.size();
-  d_proofs.push_back(NullConstraint);
-
-  d_equalityEngineProof = d_proofs.size();
-  d_proofs.push_back(NullConstraint);
-
-  d_internalDecisionProof = d_proofs.size();
-  d_proofs.push_back(NullConstraint);
+  
 }
 
 SortedConstraintMap& ConstraintDatabase::getVariableSCM(ArithVar v) const{
@@ -592,10 +804,13 @@ void ConstraintDatabase::pushAssertionOrderWatch(ConstraintP c, TNode witness){
   d_watches->d_assertionOrderWatches.push_back(c);
 }
 
-void ConstraintDatabase::pushProofWatch(ConstraintP c, ProofId pid){
-  Assert(c->d_proof == ProofIdSentinel);
-  c->d_proof = pid;
-  d_watches->d_proofWatches.push_back(c);
+
+void ConstraintDatabase::pushConstraintRule(const ConstraintRule& crp){
+  ConstraintP c = crp.d_constraint;
+  Assert(c->d_crid == ConstraintRuleIdSentinel);
+  Assert(!c->hasProof());
+  c->d_crid = d_watches->d_constraintProofs.size();
+  d_watches->d_constraintProofs.push_back(crp);
 }
 
 ConstraintP ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r){
@@ -610,8 +825,8 @@ ConstraintP ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, cons
   if(vc.hasConstraintOfType(t)){
     return vc.getConstraintOfType(t);
   }else{
-    ConstraintP c = new Constraint_(v, t, r);
-    ConstraintP negC = Constraint_::makeNegation(v, t, r);
+    ConstraintP c = new Constraint(v, t, r);
+    ConstraintP negC = Constraint::makeNegation(v, t, r);
 
     SortedConstraintMapIterator negPos;
     if(t == Equality || t == Disequality){
@@ -649,8 +864,6 @@ bool ConstraintDatabase::emptyDatabase(const std::vector<PerVariableDatabase>& v
 }
 
 ConstraintDatabase::~ConstraintDatabase(){
-  Assert(d_satAllocationLevel <= d_satContext->getLevel());
-
   delete d_watches;
 
   std::vector<ConstraintP> constraintList;
@@ -727,14 +940,17 @@ void ConstraintDatabase::removeVariable(ArithVar v){
   d_reclaimable.add(v);
 }
 
-bool Constraint_::safeToGarbageCollect() const{
-  return !isSplit()
-    && !canBePropagated()
-    && !hasProof()
-    && !assertedToTheTheory();
+bool Constraint::safeToGarbageCollect() const{
+  // Do not call during destructor as getNegation() may be Null by this point
+  Assert(getNegation() != NullConstraint);
+  return !contextDependentDataIsSet() && ! getNegation()->contextDependentDataIsSet();
 }
 
-Node Constraint_::split(){
+bool Constraint::contextDependentDataIsSet() const{
+  return hasProof() || isSplit() || canBePropagated() || assertedToTheTheory();
+}
+
+Node Constraint::split(){
   Assert(isEquality() || isDisequality());
 
   bool isEq = isEquality();
@@ -763,25 +979,6 @@ bool ConstraintDatabase::hasLiteral(TNode literal) const {
   return lookup(literal) != NullConstraint;
 }
 
-// ConstraintP ConstraintDatabase::addLiteral(TNode literal){
-//   Assert(!hasLiteral(literal));
-//   bool isNot = (literal.getKind() == NOT);
-//   TNode atom = isNot ? literal[0] : literal;
-
-//   ConstraintP atomC = addAtom(atom);
-
-//   return isNot ? atomC->d_negation : atomC;
-// }
-
-// ConstraintP ConstraintDatabase::allocateConstraintForComparison(ArithVar v, const Comparison cmp){
-//   Debug("arith::constraint") << "allocateConstraintForLiteral(" << v << ", "<< cmp <<")" << endl;
-//   Kind kind = cmp.comparisonKind();
-//   ConstraintType type = constraintTypeOfLiteral(kind);
-  
-//   DeltaRational dr = cmp.getDeltaRational();
-//   return new Constraint_(v, type, dr);
-// }
-
 ConstraintP ConstraintDatabase::addLiteral(TNode literal){
   Assert(!hasLiteral(literal));
   bool isNot = (literal.getKind() == NOT);
@@ -795,12 +992,11 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){
   ConstraintType posType = constraintTypeOfComparison(posCmp);
 
   Polynomial nvp = posCmp.normalizedVariablePart();
-  Debug("nf::tmp") << "here " <<  nvp.getNode() << " " << endl;
   ArithVar v = d_avariables.asArithVar(nvp.getNode());
 
   DeltaRational posDR = posCmp.normalizedDeltaRational();
 
-  ConstraintP posC = new Constraint_(v, posType, posDR);
+  ConstraintP posC = new Constraint(v, posType, posDR);
 
   Debug("arith::constraint") << "addliteral( literal ->" << literal << ")" << endl;
   Debug("arith::constraint") << "addliteral( posC ->" << posC << ")" << endl;
@@ -831,7 +1027,7 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){
     ConstraintType negType = constraintTypeOfComparison(negCmp);
     DeltaRational negDR = negCmp.normalizedDeltaRational();
 
-    ConstraintP negC = new Constraint_(v, negType, negDR);
+    ConstraintP negC = new Constraint(v, negType, negDR);
 
     SortedConstraintMapIterator negI;
 
@@ -866,22 +1062,6 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){
   }
 }
 
-// ConstraintType constraintTypeOfLiteral(Kind k){
-//   switch(k){
-//   case LT:
-//   case LEQ:
-//     return UpperBound;
-//   case GT:
-//   case GEQ:
-//     return LowerBound;
-//   case EQUAL:
-//     return Equality;
-//   case DISTINCT:
-//     return Disequality;
-//   default:
-//     Unreachable();
-//   }
-// }
 
 ConstraintP ConstraintDatabase::lookup(TNode literal) const{
   NodetoConstraintMap::const_iterator iter = d_nodetoConstraintMap.find(literal);
@@ -892,151 +1072,236 @@ ConstraintP ConstraintDatabase::lookup(TNode literal) const{
   }
 }
 
-void Constraint_::selfExplainingWithNegationTrue(){
+void Constraint::setAssumption(bool nowInConflict){
   Assert(!hasProof());
-  Assert(getNegation()->hasProof());
+  Assert(negationHasProof() == nowInConflict);
   Assert(hasLiteral());
   Assert(assertedToTheTheory());
-  d_database->pushProofWatch(this, d_database->d_selfExplainingProof);
+
+  d_database->pushConstraintRule(ConstraintRule(this, AssumeAP));
+  
+  Assert(inConflict() == nowInConflict);
+  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+    Debug("constraint::conflictCommit") << "inConflict@setAssumption " << this << std::endl;
+  }
 }
 
-void Constraint_::selfExplaining(){
-  markAsTrue();
+void Constraint::tryToPropagate(){
+  Assert(hasProof());
+  Assert(!isAssumption());
+  Assert(!isInternalAssumption());
+
+  if(canBePropagated() && !assertedToTheTheory() && !isAssumption() && !isInternalAssumption()){
+    propagate();
+  }
 }
 
-void Constraint_::propagate(){
+void Constraint::propagate(){
   Assert(hasProof());
   Assert(canBePropagated());
   Assert(!assertedToTheTheory());
-  Assert(!isSelfExplaining());
+  Assert(!isAssumption());
+  Assert(!isInternalAssumption());
 
   d_database->d_toPropagate.push(this);
 }
 
-void Constraint_::propagate(ConstraintCP a){
-  Assert(!hasProof());
-  Assert(canBePropagated());
-
-  markAsTrue(a);
-  propagate();
-}
 
-void Constraint_::propagate(ConstraintCP a, ConstraintCP b){
+/*
+ * Example:
+ *    x <= a and a < b
+ * |= x <= b
+ * ---
+ *  1*(x <= a) + (-1)*(x > b) => (0 <= a-b)
+ */
+void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){
   Assert(!hasProof());
-  Assert(canBePropagated());
+  Assert(imp->hasProof());
+  Assert(negationHasProof() == nowInConflict);
 
-  markAsTrue(a, b);
-  propagate();
-}
 
-void Constraint_::propagate(const ConstraintCPVec& b){
-  Assert(!hasProof());
-  Assert(canBePropagated());
+  d_database->d_antecedents.push_back(NullConstraint);
+  d_database->d_antecedents.push_back(imp);
 
-  markAsTrue(b);
-  propagate();
-}
+  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
 
-void Constraint_::impliedBy(ConstraintCP a){
-  Assert(truthIsUnknown());
+  RationalVectorP coeffs;
+  if(PROOF_ON()){
+    std::pair<int, int> sgns = unateFarkasSigns(getNegation(), imp);
 
-  markAsTrue(a);
-  if(canBePropagated()){
-    propagate();
+    Rational first(sgns.first);
+    Rational second(sgns.second);
+
+    coeffs = new RationalVector();
+    coeffs->push_back(first);
+    coeffs->push_back(second);
+  } else {
+    coeffs = RationalVectorPSentinel;
   }
-}
 
-void Constraint_::impliedBy(ConstraintCP a, ConstraintCP b){
-  Assert(truthIsUnknown());
+  // no need to delete coeffs the memory is owned by ConstraintRule
+  d_database->pushConstraintRule(ConstraintRule(this, FarkasAP, antecedentEnd, coeffs));
 
-  markAsTrue(a, b);
-  if(canBePropagated()){
-    propagate();
+  Assert(inConflict() == nowInConflict);
+  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+    Debug("constraint::conflictCommit") << "inConflict@impliedByUnate " << this << std::endl;
+  }
+  
+  if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){
+    getConstraintRule().print(Debug("constraints::wffp"));
   }
+  Assert(wellFormedFarkasProof());
 }
 
-void Constraint_::impliedBy(const ConstraintCPVec& b){
-  Assert(truthIsUnknown());
+void Constraint::impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool nowInConflict){
+  Assert(!hasProof());
+  Assert(negationHasProof() == nowInConflict);
+  Assert(a->hasProof());
+  Assert(b->hasProof());
 
-  markAsTrue(b);
-  if(canBePropagated()){
-    propagate();
-  }
-}
+  d_database->d_antecedents.push_back(NullConstraint);
+  d_database->d_antecedents.push_back(a);
+  d_database->d_antecedents.push_back(b);
 
-void Constraint_::setInternalDecision(){
-  Assert(truthIsUnknown());
-  Assert(!assertedToTheTheory());
+  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
+  d_database->pushConstraintRule(ConstraintRule(this, TrichotomyAP, antecedentEnd));
 
-  d_database->pushProofWatch(this, d_database->d_internalDecisionProof);
+  Assert(inConflict() == nowInConflict);
+  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+    Debug("constraint::conflictCommit") << "inConflict@impliedByTrichotomy " << this << std::endl;
+  }
 }
 
-void Constraint_::setEqualityEngineProof(){
-  Assert(truthIsUnknown());
-  Assert(hasLiteral());
-  d_database->pushProofWatch(this, d_database->d_equalityEngineProof);
-}
 
-void Constraint_::markAsTrue(){
-  Assert(truthIsUnknown());
-  Assert(hasLiteral());
-  Assert(assertedToTheTheory());
-  d_database->pushProofWatch(this, d_database->d_selfExplainingProof);
+bool Constraint::allHaveProof(const ConstraintCPVec& b){
+  for(ConstraintCPVec::const_iterator i=b.begin(), i_end=b.end(); i != i_end; ++i){
+    ConstraintCP cp = *i;
+    if(! (cp->hasProof())){ return false; }
+  }
+  return true;
 }
 
-void Constraint_::markAsTrue(ConstraintCP imp){
-  Assert(truthIsUnknown());
-  Assert(imp->hasProof());
+void Constraint::impliedByIntHole(ConstraintCP a, bool nowInConflict){
+  Assert(!hasProof());
+  Assert(negationHasProof() == nowInConflict);
+  Assert(a->hasProof());
+
+  d_database->d_antecedents.push_back(NullConstraint);
+  d_database->d_antecedents.push_back(a);
+  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
+  d_database->pushConstraintRule(ConstraintRule(this, IntHoleAP, antecedentEnd));
 
-  d_database->d_proofs.push_back(NullConstraint);
-  d_database->d_proofs.push_back(imp);
-  ProofId proof = d_database->d_proofs.size() - 1;
-  d_database->pushProofWatch(this, proof);
+  Assert(inConflict() == nowInConflict);
+  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+    Debug("constraint::conflictCommit") << "inConflict impliedByIntHole" << this << std::endl;
+  }
 }
 
-void Constraint_::markAsTrue(ConstraintCP impA, ConstraintCP impB){
-  Assert(truthIsUnknown());
-  Assert(impA->hasProof());
-  Assert(impB->hasProof());
+void Constraint::impliedByIntHole(const ConstraintCPVec& b, bool nowInConflict){
+  Assert(!hasProof());
+  Assert(negationHasProof() == nowInConflict);
+  Assert(allHaveProof(b));
+
+  CDConstraintList& antecedents = d_database->d_antecedents;
+  antecedents.push_back(NullConstraint);
+  for(ConstraintCPVec::const_iterator i=b.begin(), i_end=b.end(); i != i_end; ++i){
+    antecedents.push_back(*i);
+  }
+  AntecedentId antecedentEnd = antecedents.size() - 1;
 
-  d_database->d_proofs.push_back(NullConstraint);
-  d_database->d_proofs.push_back(impA);
-  d_database->d_proofs.push_back(impB);
-  ProofId proof = d_database->d_proofs.size() - 1;
+  d_database->pushConstraintRule(ConstraintRule(this, IntHoleAP, antecedentEnd));
 
-  d_database->pushProofWatch(this, proof);
+  Assert(inConflict() == nowInConflict);
+  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+    Debug("constraint::conflictCommit") << "inConflict@impliedByIntHole[vec] " << this << std::endl;
+  }
 }
 
-void Constraint_::markAsTrue(const ConstraintCPVec& a){
-  Assert(truthIsUnknown());
+/*
+ * If proofs are off, coeffs == RationalVectorSentinal.
+ * If proofs are on,
+ *   coeffs != RationalVectorSentinal,
+ *   coeffs->size() = a.size() + 1,
+ *   for i in [0,a.size) : coeff[i] corresponds to a[i], and
+ *   coeff.back() corresponds to the current constraint. 
+ */
+void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coeffs, bool nowInConflict){
+  Assert(!hasProof());
+  Assert(negationHasProof() == nowInConflict);
+  Assert(allHaveProof(a));
+
+  Assert( PROOF_ON() == (coeffs != RationalVectorCPSentinel) );
+  // !PROOF_ON() => coeffs == RationalVectorCPSentinel
+  //  PROOF_ON() => coeffs->size() == a.size() + 1
+  Assert(!PROOF_ON() || coeffs->size() == a.size() + 1);
   Assert(a.size() >= 1);
-  d_database->d_proofs.push_back(NullConstraint);
+
+  d_database->d_antecedents.push_back(NullConstraint);
   for(ConstraintCPVec::const_iterator i = a.begin(), end = a.end(); i != end; ++i){
     ConstraintCP c_i = *i;
     Assert(c_i->hasProof());
-    //Assert(!c_i->isPseudoConstraint());
-    d_database->d_proofs.push_back(c_i);
+    d_database->d_antecedents.push_back(c_i);
+  }
+  AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1;
+
+  RationalVectorCP coeffsCopy;
+  if(PROOF_ON()){
+    Assert(coeffs != RationalVectorCPSentinel);
+    coeffsCopy = new RationalVector(*coeffs);
+  } else {
+    coeffsCopy = RationalVectorCPSentinel;
+  }
+  d_database->pushConstraintRule(ConstraintRule(this, FarkasAP, antecedentEnd, coeffsCopy));
+
+  Assert(inConflict() == nowInConflict);
+  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+    Debug("constraint::conflictCommit") << "inConflict@impliedByFarkas " << this << std::endl;
+  }
+  if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){
+    getConstraintRule().print(Debug("constraints::wffp"));
+  }
+  Assert(wellFormedFarkasProof());
+}
+
+
+void Constraint::setInternalAssumption(bool nowInConflict){
+  Assert(!hasProof());
+  Assert(negationHasProof() == nowInConflict);
+  Assert(!assertedToTheTheory());
+
+  d_database->pushConstraintRule(ConstraintRule(this, InternalAssumeAP));
+
+  Assert(inConflict() == nowInConflict);
+  if(Debug.isOn("constraint::conflictCommit") && inConflict()){
+    Debug("constraint::conflictCommit") << "inConflict@setInternalAssumption " << this << std::endl;
   }
+}
 
-  ProofId proof = d_database->d_proofs.size() - 1;
 
-  d_database->pushProofWatch(this, proof);
+void Constraint::setEqualityEngineProof(){
+  Assert(truthIsUnknown());
+  Assert(hasLiteral());
+  d_database->pushConstraintRule(ConstraintRule(this, EqualityEngineAP));
 }
 
-SortedConstraintMap& Constraint_::constraintSet() const{
+
+SortedConstraintMap& Constraint::constraintSet() const{
   Assert(d_database->variableDatabaseIsSetup(d_variable));
   return (d_database->d_varDatabases[d_variable])->d_constraints;
 }
 
-bool Constraint_::proofIsEmpty() const{
+bool Constraint::antecentListIsEmpty() const{
   Assert(hasProof());
-  bool result = d_database->d_proofs[d_proof] == NullConstraint;
-  //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPseudoConstraint());
-  Assert((!result) || isSelfExplaining() || hasEqualityEngineProof());
-  return result;
+  return d_database->d_antecedents[getEndAntecedent()] == NullConstraint;
 }
 
-Node Constraint_::externalImplication(const ConstraintCPVec& b) const{
+bool Constraint::antecedentListLengthIsOne() const {
+  Assert(hasProof());
+  return !antecentListIsEmpty() &&
+    d_database->d_antecedents[getEndAntecedent()-1] == NullConstraint;
+}
+
+Node Constraint::externalImplication(const ConstraintCPVec& b) const{
   Assert(hasLiteral());
   Node antecedent = externalExplainByAssertions(b);
   Node implied = getLiteral();
@@ -1044,10 +1309,19 @@ Node Constraint_::externalImplication(const ConstraintCPVec& b) const{
 }
 
 
-Node Constraint_::externalExplainByAssertions(const ConstraintCPVec& b){
+Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){
   return externalExplain(b, AssertionOrderSentinel);
 }
 
+Node Constraint::externalExplainConflict() const{
+  Assert(inConflict());
+  NodeBuilder<> nb(kind::AND);
+  externalExplainByAssertions(nb);
+  getNegation()->externalExplainByAssertions(nb);
+
+  return safeConstructNary(nb);
+}
+
 struct ConstraintCPHash {
   /* Todo replace with an id */
   size_t operator()(ConstraintCP c) const{
@@ -1056,13 +1330,13 @@ struct ConstraintCPHash {
   }
 };
 
-void Constraint_::assertionFringe(ConstraintCPVec& v){
+void Constraint::assertionFringe(ConstraintCPVec& v){
   hash_set<ConstraintCP, ConstraintCPHash> visited;
   size_t writePos = 0;
 
   if(!v.empty()){
     const ConstraintDatabase* db = v.back()->d_database;
-    const CDConstraintList& proofs = db->d_proofs;
+    const CDConstraintList& antecedents = db->d_antecedents;
     for(size_t i = 0; i < v.size(); ++i){
       ConstraintCP vi = v[i];
       if(visited.find(vi) == visited.end()){
@@ -1072,13 +1346,14 @@ void Constraint_::assertionFringe(ConstraintCPVec& v){
           v[writePos] = vi;
           writePos++;
         }else{
-          Assert(!vi->isSelfExplaining());
-          ProofId p = vi->d_proof;
-          ConstraintCP antecedent = proofs[p];
+          Assert(vi->hasFarkasProof() || vi->hasIntHoleProof() );
+          AntecedentId p = vi->getEndAntecedent();
+
+          ConstraintCP antecedent = antecedents[p];
           while(antecedent != NullConstraint){
             v.push_back(antecedent);
             --p;
-            antecedent = proofs[p];
+            antecedent = antecedents[p];
           }
         }
       }
@@ -1087,12 +1362,12 @@ void Constraint_::assertionFringe(ConstraintCPVec& v){
   }
 }
 
-void Constraint_::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i){
+void Constraint::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i){
   o.insert(o.end(), i.begin(), i.end());
   assertionFringe(o);
 }
 
-Node Constraint_::externalExplain(const ConstraintCPVec& v, AssertionOrder order){
+Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order){
   NodeBuilder<> nb(kind::AND);
   ConstraintCPVec::const_iterator i, end;
   for(i = v.begin(), end = v.end(); i != end; ++i){
@@ -1102,65 +1377,70 @@ Node Constraint_::externalExplain(const ConstraintCPVec& v, AssertionOrder order
   return safeConstructNary(nb);
 }
 
-void Constraint_::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{
+void Constraint::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{
   Assert(hasProof());
-  Assert(!isSelfExplaining() || assertedToTheTheory());
-  Assert(!isInternalDecision());
+  Assert(!isAssumption() || assertedToTheTheory());
+  Assert(!isInternalAssumption());
 
   if(assertedBefore(order)){
     nb << getWitness();
   }else if(hasEqualityEngineProof()){
     d_database->eeExplain(this, nb);
   }else{
-    Assert(!isSelfExplaining());
-    ProofId p = d_proof;
-    ConstraintCP antecedent = d_database->d_proofs[p];
+    Assert(!isAssumption());
+    AntecedentId p = getEndAntecedent();
+    ConstraintCP antecedent = d_database->d_antecedents[p];
 
-    for(; antecedent != NullConstraint; antecedent = d_database->d_proofs[--p] ){
+    while(antecedent != NullConstraint){
       antecedent->externalExplain(nb, order);
+      --p;
+      antecedent = d_database->d_antecedents[p];
     }
   }
 }
 
-Node Constraint_::externalExplain(AssertionOrder order) const{
+Node Constraint::externalExplain(AssertionOrder order) const{
   Assert(hasProof());
-  Assert(!isSelfExplaining() || assertedBefore(order));
-  Assert(!isInternalDecision());
+  Assert(!isAssumption() || assertedBefore(order));
+  Assert(!isInternalAssumption());
   if(assertedBefore(order)){
     return getWitness();
   }else if(hasEqualityEngineProof()){
     return d_database->eeExplain(this);
   }else{
-    Assert(!proofIsEmpty());
+    Assert(hasFarkasProof() || hasIntHoleProof() || hasTrichotomyProof());
+    Assert(!antecentListIsEmpty());
     //Force the selection of the layer above if the node is
     // assertedToTheTheory()!
-    if(d_database->d_proofs[d_proof-1] == NullConstraint){
-      ConstraintCP antecedent = d_database->d_proofs[d_proof];
+
+    AntecedentId listEnd = getEndAntecedent();
+    if(antecedentListLengthIsOne()){
+      ConstraintCP antecedent = d_database->d_antecedents[listEnd];
       return antecedent->externalExplain(order);
     }else{
       NodeBuilder<> nb(kind::AND);
-      Assert(!isSelfExplaining());
+      Assert(!isAssumption());
 
-      ProofId p = d_proof;
-      ConstraintCP antecedent = d_database->d_proofs[p];
+      AntecedentId p = listEnd;
+      ConstraintCP antecedent = d_database->d_antecedents[p];
       while(antecedent != NullConstraint){
         antecedent->externalExplain(nb, order);
         --p;
-        antecedent = d_database->d_proofs[p];
+        antecedent = d_database->d_antecedents[p];
       }
       return nb;
     }
   }
 }
 
-Node Constraint_::externalExplainByAssertions(ConstraintCP a, ConstraintCP b){
+Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b){
   NodeBuilder<> nb(kind::AND);
   a->externalExplainByAssertions(nb);
   b->externalExplainByAssertions(nb);
   return nb;
 }
 
-Node Constraint_::externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c){
+Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c){
   NodeBuilder<> nb(kind::AND);
   a->externalExplainByAssertions(nb);
   b->externalExplainByAssertions(nb);
@@ -1168,7 +1448,7 @@ Node Constraint_::externalExplainByAssertions(ConstraintCP a, ConstraintCP b, Co
   return nb;
 }
 
-ConstraintP Constraint_::getStrictlyWeakerLowerBound(bool hasLiteral, bool asserted) const {
+ConstraintP Constraint::getStrictlyWeakerLowerBound(bool hasLiteral, bool asserted) const {
   Assert(initialized());
   Assert(!asserted || hasLiteral);
 
@@ -1193,7 +1473,7 @@ ConstraintP Constraint_::getStrictlyWeakerLowerBound(bool hasLiteral, bool asser
   return NullConstraint;
 }
 
-ConstraintP Constraint_::getStrictlyWeakerUpperBound(bool hasLiteral, bool asserted) const {
+ConstraintP Constraint::getStrictlyWeakerUpperBound(bool hasLiteral, bool asserted) const {
   SortedConstraintMapConstIterator i = d_variablePosition;
   const SortedConstraintMap& scm = constraintSet();
   SortedConstraintMapConstIterator i_end = scm.end();
@@ -1273,12 +1553,12 @@ ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t
     }
   }
 }
-Node ConstraintDatabase::eeExplain(const Constraint_* const c) const{
+Node ConstraintDatabase::eeExplain(const Constraint* const c) const{
   Assert(c->hasLiteral());
   return d_congruenceManager.explain(c->getLiteral());
 }
 
-void ConstraintDatabase::eeExplain(const Constraint_* const c, NodeBuilder<>& nb) const{
+void ConstraintDatabase::eeExplain(const Constraint* const c, NodeBuilder<>& nb) const{
   Assert(c->hasLiteral());
   d_congruenceManager.explain(c->getLiteral(), nb);
 }
@@ -1289,14 +1569,14 @@ bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const {
 
 
 ConstraintDatabase::Watches::Watches(context::Context* satContext, context::Context* userContext):
-  d_proofWatches(satContext),
+  d_constraintProofs(satContext),
   d_canBePropagatedWatches(satContext),
   d_assertionOrderWatches(satContext),
   d_splitWatches(userContext)
 {}
 
 
-void Constraint_::setLiteral(Node n) {
+void Constraint::setLiteral(Node n) {
   Assert(!hasLiteral());
   Assert(sanityChecking(n));
   d_literal = n;
@@ -1414,17 +1694,21 @@ void ConstraintDatabase::outputUnateInequalityLemmas(std::vector<Node>& lemmas)
   }
 }
 
-void ConstraintDatabase::raiseUnateConflict(ConstraintP ant, ConstraintP cons){
-  Assert(ant->hasProof());
-  ConstraintP negCons = cons->getNegation();
-  Assert(negCons->hasProof());
-
-  Debug("arith::unate::conf") << ant << "implies " << cons << endl;
-  Debug("arith::unate::conf") << negCons << " is true." << endl;
-
-  d_raiseConflict.addConstraint(ant);
-  d_raiseConflict.addConstraint(negCons);
-  d_raiseConflict.commitConflict();
+bool ConstraintDatabase::handleUnateProp(ConstraintP ant, ConstraintP cons){
+  if(cons->negationHasProof()){
+    Debug("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl;
+    cons->impliedByUnate(ant, true);
+    d_raiseConflict.raiseConflict(cons);
+    return true;
+  }else if(!cons->isTrue()){
+    ++d_statistics.d_unatePropagateImplications;
+    Debug("arith::unate") << "handleUnate: " << ant << " implies " << cons << endl;
+    cons->impliedByUnate(ant, false);
+    cons->tryToPropagate();
+    return false;
+  } else {
+    return false;
+  }
 }
 
 void ConstraintDatabase::unatePropLowerBound(ConstraintP curr, ConstraintP prev){
@@ -1460,27 +1744,11 @@ void ConstraintDatabase::unatePropLowerBound(ConstraintP curr, ConstraintP prev)
     //These should all be handled by propagating the LowerBounds!
     if(vc.hasLowerBound()){
       ConstraintP lb = vc.getLowerBound();
-      if(lb->negationHasProof()){
-        raiseUnateConflict(curr, lb);
-        return;
-      }else if(!lb->isTrue()){
-        ++d_statistics.d_unatePropagateImplications;
-        Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << lb << endl;
-
-        lb->impliedBy(curr);
-      }
+      if(handleUnateProp(curr, lb)){ return; }
     }
     if(vc.hasDisequality()){
       ConstraintP dis = vc.getDisequality();
-      if(dis->negationHasProof()){
-        raiseUnateConflict(curr, dis);
-        return;
-      }else if(!dis->isTrue()){
-        ++d_statistics.d_unatePropagateImplications;
-        Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << dis << endl;
-
-        dis->impliedBy(curr);
-      }
+      if(handleUnateProp(curr, dis)){ return; }
     }
   }
 }
@@ -1511,26 +1779,11 @@ void ConstraintDatabase::unatePropUpperBound(ConstraintP curr, ConstraintP prev)
     //These should all be handled by propagating the UpperBounds!
     if(vc.hasUpperBound()){
       ConstraintP ub = vc.getUpperBound();
-      if(ub->negationHasProof()){
-        raiseUnateConflict(curr, ub);
-        return;
-      }else if(!ub->isTrue()){
-        ++d_statistics.d_unatePropagateImplications;
-        Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << ub << endl;
-        ub->impliedBy(curr);
-      }
+      if(handleUnateProp(curr, ub)){ return; }
     }
     if(vc.hasDisequality()){
       ConstraintP dis = vc.getDisequality();
-      if(dis->negationHasProof()){
-        raiseUnateConflict(curr, dis);
-        return;
-      }else if(!dis->isTrue()){
-        Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl;
-        ++d_statistics.d_unatePropagateImplications;
-
-        dis->impliedBy(curr);
-      }
+      if(handleUnateProp(curr, dis)){ return; }
     }
   }
 }
@@ -1568,26 +1821,11 @@ void ConstraintDatabase::unatePropEquality(ConstraintP curr, ConstraintP prevLB,
     //These should all be handled by propagating the LowerBounds!
     if(vc.hasLowerBound()){
       ConstraintP lb = vc.getLowerBound();
-      if(lb->negationHasProof()){
-        raiseUnateConflict(curr, lb);
-        return;
-      }else if(!lb->isTrue()){
-        ++d_statistics.d_unatePropagateImplications;
-        Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << lb << endl;
-        lb->impliedBy(curr);
-      }
+      if(handleUnateProp(curr, lb)){ return; }
     }
     if(vc.hasDisequality()){
       ConstraintP dis = vc.getDisequality();
-      if(dis->negationHasProof()){
-        raiseUnateConflict(curr, dis);
-        return;
-      }else if(!dis->isTrue()){
-        ++d_statistics.d_unatePropagateImplications;
-        Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl;
-
-        dis->impliedBy(curr);
-      }
+      if(handleUnateProp(curr, dis)){ return; }
     }
   }
   Assert(scm_i == scm_curr);
@@ -1603,28 +1841,51 @@ void ConstraintDatabase::unatePropEquality(ConstraintP curr, ConstraintP prevLB,
     //These should all be handled by propagating the UpperBounds!
     if(vc.hasUpperBound()){
       ConstraintP ub = vc.getUpperBound();
-      if(ub->negationHasProof()){
-        raiseUnateConflict(curr, ub);
-        return;
-      }else if(!ub->isTrue()){
-        ++d_statistics.d_unatePropagateImplications;
-        Debug("arith::unate") << "unateProp " << curr << " implies " << ub << endl;
-
-        ub->impliedBy(curr);
-      }
+      if(handleUnateProp(curr, ub)){ return; }
     }
     if(vc.hasDisequality()){
       ConstraintP dis = vc.getDisequality();
-      if(dis->negationHasProof()){
-        raiseUnateConflict(curr, dis);
-        return;
-      }else if(!dis->isTrue()){
-        ++d_statistics.d_unatePropagateImplications;
-        Debug("arith::unate") << "unateProp " << curr << " implies " << dis << endl;
-        dis->impliedBy(curr);
-      }
+      if(handleUnateProp(curr, dis)){ return; }
+    }
+  }
+}
+
+std::pair<int, int> Constraint::unateFarkasSigns(ConstraintCP ca, ConstraintCP cb){
+  ConstraintType a = ca->getType();
+  ConstraintType b = cb->getType();
+
+  Assert(a != Disequality);
+  Assert(b != Disequality);
+
+  int a_sgn = (a == LowerBound) ? -1 : ((a == UpperBound) ? 1 : 0);
+  int b_sgn = (b == LowerBound) ? -1 : ((b == UpperBound) ? 1 : 0);
+
+  if(a_sgn == 0 && b_sgn == 0){
+    Assert(a == Equality);
+    Assert(b == Equality);
+    Assert(ca->getValue() != cb->getValue());
+    if(ca->getValue() < cb->getValue()){
+      a_sgn = 1;
+      b_sgn = -1;
+    }else{
+      a_sgn = -1;
+      b_sgn = 1;
     }
+  }else if(a_sgn == 0){
+    Assert(b_sgn != 0);
+    Assert(a == Equality);
+    a_sgn = -b_sgn;
+  }else if(b_sgn == 0){
+    Assert(a_sgn != 0);
+    Assert(b == Equality);
+    b_sgn = -a_sgn;
   }
+  Assert(a_sgn != 0);
+  Assert(b_sgn != 0);
+
+  Debug("arith::unateFarkasSigns") << "Constraint::unateFarkasSigns("<<a <<", " << b << ") -> "
+                                   << "("<<a_sgn<<", "<< b_sgn <<")"<< endl;
+  return make_pair(a_sgn, b_sgn);
 }
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index badb97bdd..795798450 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -26,7 +26,7 @@
  **   the TheoryEngine.
  **
  ** In addition, Constraints keep track of the following:
- **  - A Constrain that is the negation of the Constraint.
+ **  - A Constraint that is the negation of the Constraint.
  **  - An iterator into a set of Constraints for the ArithVar sorted by
  **    DeltaRational value.
  **  - A context dependent internal proof of the node that can be used for
@@ -58,6 +58,16 @@
  ** Internals:
  **  - Constraints are pointers to ConstraintValues.
  **  - Undefined Constraints are NullConstraint.
+
+ **
+ ** Assumption vs. Assertion:
+ ** - An assertion is anything on the theory d_fact queue.
+ **   This includes any thing propagated and returned to the fact queue.
+ **   These can be used in external conflicts and propagations of earlier proofs.
+ ** - An assumption is anything on the theory d_fact queue that has no further
+ **   explanation i.e. this theory did not propagate it.
+ ** - To set something an assumption, first set it as being as assertion.
+ ** - Internal assumptions have no explanations and must be regressed out of the proof.
  **/
 
 #include "cvc4_private.h"
@@ -66,6 +76,7 @@
 #define __CVC4__THEORY__ARITH__CONSTRAINT_H
 
 #include "expr/node.h"
+#include "proof/proof.h"
 
 #include "context/context.h"
 #include "context/cdlist.h"
@@ -87,6 +98,38 @@ namespace theory {
 namespace arith {
 
 /**
+ * Logs the types of different proofs. 
+ * Current, proof types:
+ * - NoAP             : This constraint is not known to be true.
+ * - AssumeAP         : This is an input assertion. There is no proof.
+ *                    : Something can be both asserted and have a proof.
+ * - InternalAssumeAP : An internal assumption. This has no guarantee of having an external proof.
+ *                    : This must be removed by regression.
+ * - FarkasAP         : A proof with Farka's coefficients, i.e.
+ *                    :  \sum lambda_i ( asNode(x_i) <= c_i  ) |= 0 < 0
+ *                    : If proofs are on, coefficients will be logged.
+ *                    : If proofs are off, coefficients will not be logged.
+ *                    : A unate implication is a FarkasAP.
+ * - TrichotomyAP     : This is any entailment using (x<= a and x >=a) => x = a
+ *                    : Equivalently, (x > a or x < a or x = a)
+ *                    : There are 3 candidate ways this can propagate:
+ *                    :   !(x > a) and !(x = a) => x < a
+ *                    :   !(x < a) and !(x = a) => x > a
+ *                    :   !(x > a) and !(x < a) => x = a
+ * - EqualityEngineAP : This is propagated by the equality engine.
+ *                    : Consult this for the proof.
+ * - IntHoleAP        : This is currently a catch-all for all integer specific reason.
+ */
+enum ArithProofType
+  { NoAP,
+    AssumeAP,
+    InternalAssumeAP,
+    FarkasAP,
+    TrichotomyAP,
+    EqualityEngineAP,
+    IntHoleAP};
+
+/**
  * The types of constraints.
  * The convex constraints are the constraints are LowerBound, Equality,
  * and UpperBound.
@@ -98,11 +141,16 @@ typedef context::CDList<ConstraintCP> CDConstraintList;
 
 typedef __gnu_cxx::hash_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap;
 
-typedef size_t ProofId;
-static ProofId ProofIdSentinel = std::numeric_limits<ProofId>::max();
+typedef size_t ConstraintRuleID;
+static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits<ConstraintRuleID>::max();
+
+typedef size_t AntecedentId;
+static const AntecedentId AntecedentIdSentinel = std::numeric_limits<AntecedentId>::max();
+
 
 typedef size_t AssertionOrder;
-static AssertionOrder AssertionOrderSentinel = std::numeric_limits<AssertionOrder>::max();
+static const AssertionOrder AssertionOrderSentinel = std::numeric_limits<AssertionOrder>::max();
+
 
 /**
  * A ValueCollection binds together convex constraints that have the same
@@ -195,7 +243,103 @@ struct PerVariableDatabase{
   }
 };
 
-class Constraint_ {
+
+/**
+ * If proofs are on, there is a vector of rationals for farkas coefficients.
+ * This is the owner of the memory for the vector, and calls delete upon cleanup.
+ * 
+ */
+struct ConstraintRule {
+  ConstraintP d_constraint;
+  ArithProofType d_proofType;
+  AntecedentId d_antecedentEnd;    
+
+  /**
+   * In this comment, we abbreviate ConstraintDatabase::d_antecedents
+   * and d_farkasCoefficients as ans and fc.
+   *
+   * This list is always empty if proofs are not enabled.
+   *
+   * If proofs are enabled, the proof of constraint c at p in ans[p] of length n is
+   *  (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p])
+   * 
+   * Farkas' proofs show a contradiction with the negation of c, c_not = c->getNegation().
+   *
+   * We treat the position for NullConstraint (p-n) as the position for the farkas
+   * coefficient for so we pretend c_not is ans[p-n].
+   * So this correlation for the constraints we are going to use:
+   *   (c_not, ans[p-(n-1)], ... , ans[p-1], ans[p])
+   * With the coefficients at positions:
+   *   (fc[0], fc[1)], ... fc[n])
+   *
+   * The index of the constraints in the proof are {i | i <= 0 <= n] } (with c_not being p-n).
+   * Partition the indices into L, U, and E, the lower bounds, the upper bounds and equalities.
+   *
+   * We standardize the proofs to be upper bound oriented following the convention:
+   *   A x <= b
+   * with the proof witness of the form
+   *  (lambda) Ax <= (lambda) b and lambda >= 0.
+   *
+   * To accomplish this cleanly, the fc coefficients must be negative for lower bounds.
+   * The signs of equalities can be either positive or negative.
+   *
+   * Thus the proof corresponds to (with multiplication over inequalities):
+   *    \sum_{u in U} fc[u] ans[p-n+u] + \sum_{e in E} fc[e] ans[p-n+e]
+   *  + \sum_{l in L} fc[l] ans[p-n+l]
+   * |= 0 < 0
+   * where fc[u] > 0, fc[l] < 0, and fc[e] != 0 (i.e. it can be either +/-).
+   * 
+   * There is no requirement that the proof is minimal.
+   * We do however use all of the constraints by requiring non-zero coefficients.
+   */
+#ifdef CVC4_PROOF
+  RationalVectorCP d_farkasCoefficients;
+#endif
+  ConstraintRule()
+    : d_constraint(NullConstraint)
+    , d_proofType(NoAP)
+    , d_antecedentEnd(AntecedentIdSentinel)
+  {
+#ifdef CVC4_PROOF
+    d_farkasCoefficients = RationalVectorCPSentinel;
+#endif
+  }
+
+  ConstraintRule(ConstraintP con, ArithProofType pt)
+    : d_constraint(con)
+    , d_proofType(pt)
+    , d_antecedentEnd(AntecedentIdSentinel)
+  {
+#ifdef CVC4_PROOF
+    d_farkasCoefficients = RationalVectorCPSentinel;
+#endif
+  }
+  ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd)
+    : d_constraint(con)
+    , d_proofType(pt)
+    , d_antecedentEnd(antecedentEnd)
+  {
+#ifdef CVC4_PROOF
+    d_farkasCoefficients = RationalVectorCPSentinel;
+#endif
+  }
+
+  ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd, RationalVectorCP coeffs)
+    : d_constraint(con)
+    , d_proofType(pt)
+    , d_antecedentEnd(antecedentEnd)
+  {
+    Assert(PROOF_ON() || coeffs == RationalVectorCPSentinel);
+#ifdef CVC4_PROOF
+    d_farkasCoefficients = coeffs;
+#endif
+  }
+  
+  void print(std::ostream& out) const;
+  void debugPrint() const;
+}; /* class ConstraintRule */
+
+class Constraint {
 private:
   /** The ArithVar associated with the constraint. */
   const ArithVar d_variable;
@@ -207,7 +351,7 @@ private:
   const DeltaRational d_value;
 
   /** A pointer to the associated database for the Constraint. */
-  ConstraintDatabase * d_database;
+  ConstraintDatabase* d_database;
 
   /**
    * The node to be communicated with the TheoryEngine.
@@ -253,12 +397,13 @@ private:
   TNode d_witness;
 
   /**
-   * This points at the proof for the constraint in the current context.
+   * The position of the constraint in the constraint rule id.
    *
    * Sat Context Dependent.
-   * This is initially ProofIdSentinel.
+   * This is initially 
    */
-  ProofId d_proof;
+  ConstraintRuleID d_crid;
+  
 
   /**
    * True if the equality has been split.
@@ -285,14 +430,15 @@ private:
    * Because of circular dependencies a Constraint is not fully valid until
    * initialize has been called on it.
    */
-  Constraint_(ArithVar x,  ConstraintType t, const DeltaRational& v);
+  Constraint(ArithVar x,  ConstraintType t, const DeltaRational& v);
 
   /**
    * Destructor for a constraint.
    * This should only be called if safeToGarbageCollect() is true.
    */
-  ~Constraint_();
+  ~Constraint();
 
+  /**  Returns true if the constraint has been initialized. */
   bool initialized() const;
 
   /**
@@ -301,12 +447,18 @@ private:
    */
   void initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation);
 
-  class ProofCleanup {
+
+  class ConstraintRuleCleanup {
   public:
-    inline void operator()(ConstraintP* p){
-      ConstraintP constraint = *p;
-      Assert(constraint->d_proof != ProofIdSentinel);
-      constraint->d_proof = ProofIdSentinel;
+    inline void operator()(ConstraintRule* crp){
+      Assert(crp != NULL);
+      ConstraintP constraint = crp->d_constraint;
+      Assert(constraint->d_crid != ConstraintRuleIdSentinel);
+      constraint->d_crid = ConstraintRuleIdSentinel;
+      
+      PROOF(if(crp->d_farkasCoefficients != RationalVectorCPSentinel){
+              delete crp->d_farkasCoefficients;
+            });
     }
   };
 
@@ -339,10 +491,18 @@ private:
     }
   };
 
-  /** Returns true if the node is safe to garbage collect. */
+  /**
+   * Returns true if the node is safe to garbage collect.
+   * Both it and its negation must have no context dependent data set.
+   */
   bool safeToGarbageCollect() const;
 
   /**
+   * Returns true if the constraint has no context dependent data set.
+   */
+  bool contextDependentDataIsSet() const;
+
+  /**
    * Returns true if the node correctly corresponds to the constraint that is
    * being set.
    */
@@ -351,13 +511,17 @@ private:
   /** Returns a reference to the map for d_variable. */
   SortedConstraintMap& constraintSet() const;
 
+  /** Returns coefficients for the proofs for farkas cancellation. */
+  static std::pair<int, int> unateFarkasSigns(ConstraintCP a, ConstraintCP b);
+
+
 public:
 
-  ConstraintType getType() const {
+  inline ConstraintType getType() const {
     return d_type;
   }
 
-  ArithVar getVariable() const {
+  inline ArithVar getVariable() const {
     return d_variable;
   }
 
@@ -365,7 +529,7 @@ public:
     return d_value;
   }
 
-  ConstraintP getNegation() const {
+  inline ConstraintP getNegation() const {
     return d_negation;
   }
 
@@ -429,14 +593,18 @@ public:
     return d_assertionOrder < time;
   }
 
-  /** Sets the witness literal for a node being on the assertion stack.
-   * The negation of the node cannot be true. */
-  void setAssertedToTheTheory(TNode witness);
-
-  /** Sets the witness literal for a node being on the assertion stack.
-   * The negation of the node must be true!
-   * This is for conflict generation specificially! */
-  void setAssertedToTheTheoryWithNegationTrue(TNode witness);
+  /**
+   * Sets the witness literal for a node being on the assertion stack.
+   *
+   * If the negation of the node is true, inConflict must be true.
+   * If the negation of the node is false, inConflict must be false.
+   * Hence, negationHasProof() == inConflict.
+   *
+   * This replaces:
+   *   void setAssertedToTheTheory(TNode witness);
+   *   void setAssertedToTheTheoryWithNegationTrue(TNode witness);
+   */
+  void setAssertedToTheTheory(TNode witness, bool inConflict);
 
   bool hasLiteral() const {
     return !d_literal.isNull();
@@ -450,25 +618,35 @@ public:
   }
 
   /**
-   * Set the node as selfExplaining().
+   * Set the node as having a proof and being an assumption.
    * The node must be assertedToTheTheory().
+   *
+   * Precondition: negationHasProof() == inConflict.
+   *
+   * Replaces:
+   *  selfExplaining().
+   *  selfExplainingWithNegationTrue().
    */
-  void selfExplaining();
-
-  void selfExplainingWithNegationTrue();
+  void setAssumption(bool inConflict);
 
-  /** Returns true if the node is selfExplaining.*/
-  bool isSelfExplaining() const;
+  /** Returns true if the node is an assumption.*/
+  bool isAssumption() const;
 
-  /**
-   * Set the constraint to be a EqualityEngine proof.
-   */
+  /** Set the constraint to have an EqualityEngine proof. */
   void setEqualityEngineProof();
   bool hasEqualityEngineProof() const;
 
+  /** Returns true if the node has a Farkas' proof. */
+  bool hasFarkasProof() const;
+
+  /** Returns true if the node has a int hole proof. */
+  bool hasIntHoleProof() const;
+
+  /** Returns true if the node has a trichotomy proof. */
+  bool hasTrichotomyProof() const;
 
   /**
-   * A sets the constraint to be an internal decision.
+   * A sets the constraint to be an internal assumption.
    *
    * This does not need to have a witness or an associated literal.
    * This is always itself in the explanation fringe for both conflicts
@@ -476,9 +654,10 @@ public:
    * This cannot be converted back into a Node conflict or explanation.
    *
    * This cannot have a proof or be asserted to the theory!
+   *
    */
-  void setInternalDecision();
-  bool isInternalDecision() const;
+  void setInternalAssumption(bool inConflict);
+  bool isInternalAssumption() const;
 
   /**
    * Returns a explanation of the constraint that is appropriate for conflicts.
@@ -509,10 +688,8 @@ public:
 
   /* Equivalent to calling externalExplainByAssertions on all constraints in b */
   static Node externalExplainByAssertions(const ConstraintCPVec& b);
-  /* utilities for calling externalExplainByAssertions on 2 constraints */
   static Node externalExplainByAssertions(ConstraintCP a, ConstraintCP b);
   static Node externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c);
-  //static Node externalExplainByAssertions(ConstraintCP a);
 
   /**
    * This is the minimum fringe of the implication tree s.t. every constraint is
@@ -523,38 +700,31 @@ public:
   static void assertionFringe(ConstraintCPVec& v);
   static void assertionFringe(ConstraintCPVec& out, const ConstraintCPVec& in);
 
-  /** Utility function built from explainForConflict. */
-  //static Node explainConflict(ConstraintP a, ConstraintP b);
-  //static Node explainConflict(ConstraintP a, ConstraintP b, Constraint c);
-
-  //static Node explainConflictForEE(ConstraintCP a, ConstraintCP b);
-  //static Node explainConflictForEE(ConstraintCP a);
-  //static Node explainConflictForDio(ConstraintCP a);
-  //static Node explainConflictForDio(ConstraintCP a, ConstraintCP b);
-
+  /** The fringe of a farkas' proof. */
   bool onFringe() const {
-    return assertedToTheTheory() || isInternalDecision() || hasEqualityEngineProof();
+    return assertedToTheTheory() || isInternalAssumption() || hasEqualityEngineProof();
   }
 
   /**
    * Returns an explanation of a propagation by the ConstraintDatabase.
    * The constraint must have a proof.
-   * The constraint cannot be selfExplaining().
+   * The constraint cannot be an assumption.
    *
    * This is the minimum fringe of the implication tree (excluding the constraint itself)
    * s.t. every constraint is assertedToTheTheory() or hasEqualityEngineProof().
    */
   Node externalExplainForPropagation() const {
     Assert(hasProof());
-    Assert(!isSelfExplaining());
+    Assert(!isAssumption());
+    Assert(!isInternalAssumption());
     return externalExplain(d_assertionOrder);
   }
 
-  // void externalExplainForPropagation(NodeBuilder<>& nb) const{
-  //   Assert(hasProof());
-  //   Assert(!isSelfExplaining());
-  //   externalExplain(nb, d_assertionOrder);
-  // }
+  /**
+   * Explain the constraint and its negation in terms of assertions.
+   * The constraint must be in conflict.
+   */
+  Node externalExplainConflict() const;
 
 private:
   Node externalExplain(AssertionOrder order) const;
@@ -572,23 +742,32 @@ private:
   static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order);
 
 public:
-  bool hasProof() const {
-    return d_proof != ProofIdSentinel;
+
+  /** The constraint is known to be true. */
+  inline bool hasProof() const {
+    return d_crid != ConstraintRuleIdSentinel;
   }
-  bool negationHasProof() const {
+
+  /** The negation of the constraint is known to hold. */
+  inline bool negationHasProof() const {
     return d_negation->hasProof();
   }
 
-  /* Neither the contraint has a proof nor the negation has a proof.*/
+  /** Neither the contraint has a proof nor the negation has a proof.*/
   bool truthIsUnknown() const {
     return !hasProof() && !negationHasProof();
   }
 
-  /* This is a synonym for hasProof(). */
-  bool isTrue() const {
+  /** This is a synonym for hasProof(). */
+  inline bool isTrue() const {
     return hasProof();
   }
 
+  /** Both the constraint and its negation are true. */
+  inline bool inConflict() const {
+    return hasProof() && negationHasProof();
+  }
+
   /**
    * Returns the constraint that corresponds to taking
    *    x r ceiling(getValue()) where r is the node's getType().
@@ -613,53 +792,118 @@ public:
   ConstraintP getStrictlyWeakerLowerBound(bool hasLiteral, bool mustBeAsserted) const;
 
   /**
-   * Marks the node as having a proof a.
-   * Adds the node the database's propagation queue.
+   * Marks a the constraint c as being entailed by a.
+   * The Farkas proof 1*(a) + -1 (c) |= 0<0
+   *
+   * After calling impliedByUnate(), the caller should either raise a conflict
+   * or try call tryToPropagate().
+   */
+  void impliedByUnate(ConstraintCP a, bool inConflict);
+
+  /**
+   * Marks a the constraint c as being entailed by a.
+   * The reason has to do with integer rounding.
+   *
+   * After calling impliedByIntHole(), the caller should either raise a conflict
+   * or try call tryToPropagate().
+   */
+  void impliedByIntHole(ConstraintCP a, bool inConflict);
+
+  /**
+   * Marks a the constraint c as being entailed by a.
+   * The reason has to do with integer rounding.
+   *
+   * After calling impliedByIntHole(), the caller should either raise a conflict
+   * or try call tryToPropagate().
+   */
+  void impliedByIntHole(const ConstraintCPVec& b, bool inConflict);
+
+  /**
+   * This is a lemma of the form:
+   *   x < d or x = d or x > d
+   * The current constraint c is one of the above constraints and {a,b}
+   * are the negation of the other two constraints.
    *
    * Preconditions:
-   * canBePropagated()
-   * !assertedToTheTheory()
+   * - negationHasProof() == inConflict.
+   *
+   * After calling impliedByTrichotomy(), the caller should either raise a conflict
+   * or try call tryToPropagate().
    */
-  void propagate(ConstraintCP a);
-  void propagate(ConstraintCP a, ConstraintCP b);
-  //void propagate(const std::vector<Constraint>& b);
-  void propagate(const ConstraintCPVec& b);
+  void impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool inConflict);
 
   /**
-   * The only restriction is that this is not known be true.
-   * This propagates if there is a node.
+   * Marks the node as having a Farkas proof.
+   *
+   * Preconditions:
+   * - coeffs == NULL if proofs are off.
+   * - See the comments for ConstraintRule for the form of coeffs when
+   *   proofs are on.
+   * - negationHasProof() == inConflict.
+   *
+   * After calling impliedByFarkas(), the caller should either raise a conflict
+   * or try call tryToPropagate().
    */
-  void impliedBy(ConstraintCP a);
-  void impliedBy(ConstraintCP a, ConstraintCP b);
-  //void impliedBy(const std::vector<Constraint>& b);
-  void impliedBy(const ConstraintCPVec& b);
+  void impliedByFarkas(const ConstraintCPVec& b, RationalVectorCP coeffs, bool inConflict);
 
+  /**
+   * Generates an implication node, B => getLiteral(),
+   * where B is the result of externalExplainByAssertions(b).
+   * Does not guarantee b is the explanation of the constraint.
+   */
   Node externalImplication(const ConstraintCPVec& b) const;
-  static Node externalConjunction(const ConstraintCPVec& b);
-  //static Node makeConflictNode(const ConstraintCPVec& b);
-
-  /** The node must have a proof already and be eligible for propagation! */
-  void propagate();
 
+  /**
+   * Returns true if the variable is assigned the value dr,
+   * the constraint would be satisfied.
+   */
   bool satisfiedBy(const DeltaRational& dr) const;
 
-private:
   /**
-   * Marks the node as having a proof and being selfExplaining.
-   * Neither the node nor its negation can have a proof.
-   * This is internal!
+   * The node must have a proof already and be eligible for propagation!
+   * You probably want to call tryToPropagate() instead.
+   *
+   * Preconditions:
+   * - hasProof()
+   * - canBePropagated()
+   * - !assertedToTheTheory()
    */
-  void markAsTrue();
+  void propagate();
+
   /**
-   * Marks the node as having a proof a.
-   * This is safe if the node does not have
+   * If the constraint
+   *   canBePropagated() and 
+   *   !assertedToTheTheory(),
+   * the constraint is added to the database's propagation queue.
+   *
+   * Precondition:
+   * - hasProof()
    */
-  void markAsTrue(ConstraintCP a);
+  void tryToPropagate();
+
+  /**
+   * Returns a reference to the containing database.
+   * Precondition: the constraint must be initialized.
+   */
+  const ConstraintDatabase& getDatabase() const;
+
+private:
+
+  /** Returns the constraint rule at the position. */
+  const ConstraintRule& getConstraintRule() const;
+  
+  inline ArithProofType getProofType() const {
+    return getConstraintRule().d_proofType;
+  }
 
-  void markAsTrue(ConstraintCP a, ConstraintCP b);
-  //void markAsTrue(const std::vector<Constraint>& b);
-  void markAsTrue(const ConstraintCPVec& b);
+  inline AntecedentId getEndAntecedent() const {
+    return getConstraintRule().d_antecedentEnd;
+  }
 
+  inline RationalVectorCP getFarkasCoefficients() const {
+    return NULLPROOF(getConstraintRule().d_farkasCoefficients);
+  }
+  
   void debugPrint() const;
 
   /**
@@ -668,15 +912,25 @@ private:
    *   isSelfExplaining() or
    *    hasEqualityEngineProof()
    */
-  bool proofIsEmpty() const;
+  bool antecentListIsEmpty() const;
+
+  bool antecedentListLengthIsOne() const;
+
+  /** Return true if every element in b has a proof. */
+  static bool allHaveProof(const ConstraintCPVec& b);
 
+  /** Precondition: hasFarkasProof() */
+  bool wellFormedFarkasProof() const;
+  
 }; /* class ConstraintValue */
 
-std::ostream& operator<<(std::ostream& o, const Constraint_& c);
+std::ostream& operator<<(std::ostream& o, const Constraint& c);
 std::ostream& operator<<(std::ostream& o, const ConstraintP c);
+std::ostream& operator<<(std::ostream& o, const ConstraintCP c);
 std::ostream& operator<<(std::ostream& o, const ConstraintType t);
 std::ostream& operator<<(std::ostream& o, const ValueCollection& c);
 std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v);
+std::ostream& operator<<(std::ostream& o, const ArithProofType);
 
 
 class ConstraintDatabase {
@@ -701,62 +955,46 @@ private:
   context::CDQueue<ConstraintCP> d_toPropagate;
 
   /**
-   * Proof Lists.
-   * Proofs are lists of valid constraints terminated by the first smaller
+   * Proofs are lists of valid constraints terminated by the first null
    * sentinel value in the proof list.
-   * The proof at p in d_proofs[p] of length n is
-   *  (NullConstraint, d_proofs[p-(n-1)], ... , d_proofs[p-1], d_proofs[p])
+   * We abbreviate d_antecedents as ans in the comment.
+   *
+   * The proof at p in ans[p] of length n is
+   *  (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p])
+   *
    * The proof at p corresponds to the conjunction:
    *  (and x_i)
    *
    * So the proof of a Constraint c corresponds to the horn clause:
    *  (implies (and x_i) c)
-   * where (and x_i) is the proof at c.d_proofs.
+   * where (and x_i) is the proof at c.d_crid d_antecedentEnd.
    *
-   * Constraints are pointers so this list is designed not to require any
-   * destruction.
+   * Constraints are pointers so this list is designed not to require any destruction.
    */
-  CDConstraintList d_proofs;
+  CDConstraintList d_antecedents;
 
-  /**
-   * This is a special proof for marking that nodes are their own explanation
-   * from the perspective of the theory.
-   * These must always be asserted to the theory.
-   *
-   * This proof is always a member of the list.
-   */
-  ProofId d_selfExplainingProof;
-
-  /**
-   * Marks a node as being proved by the equality engine.
-   * The equality engine will be asked for the explanation of such nodes.
-   *
-   * This is a special proof that is always a member of the list.
-   */
-  ProofId d_equalityEngineProof;
+  typedef context::CDList<ConstraintRule, Constraint::ConstraintRuleCleanup> ConstraintRuleList;
+  typedef context::CDList<ConstraintP, Constraint::CanBePropagatedCleanup> CBPList;
+  typedef context::CDList<ConstraintP, Constraint::AssertionOrderCleanup> AOList;
+  typedef context::CDList<ConstraintP, Constraint::SplitCleanup> SplitList;
 
-  /**
-   * Marks a constraint as being proved by making an internal
-   * decision. Such nodes cannot be used in external explanations
-   * but can be used internally.
-   */
-  ProofId d_internalDecisionProof;
 
-  typedef context::CDList<ConstraintP, Constraint_::ProofCleanup> ProofCleanupList;
-  typedef context::CDList<ConstraintP, Constraint_::CanBePropagatedCleanup> CBPList;
-  typedef context::CDList<ConstraintP, Constraint_::AssertionOrderCleanup> AOList;
-  typedef context::CDList<ConstraintP, Constraint_::SplitCleanup> SplitList;
 
   /**
    * The watch lists are collected together as they need to be garbage collected
    * carefully.
    */
   struct Watches{
+
     /**
-     * Contains the exact list of atoms that have a proof.
+     * Contains the exact list of constraints that have a proof.
+     * Upon pop, this unsets d_crid to NoAP.
+     *
+     * The index in this list is the proper ordering of the proofs.
      */
-    ProofCleanupList d_proofWatches;
-
+    ConstraintRuleList d_constraintProofs;
+    
+    
     /**
      * Contains the exact list of constraints that can be used for propagation.
      */
@@ -781,7 +1019,9 @@ private:
   void pushSplitWatch(ConstraintP c);
   void pushCanBePropagatedWatch(ConstraintP c);
   void pushAssertionOrderWatch(ConstraintP c, TNode witness);
-  void pushProofWatch(ConstraintP c, ProofId pid);
+
+  /** Assumes that antecedents have already been pushed. */
+  void pushConstraintRule(const ConstraintRule& crp);
 
   /** Returns true if all of the entries of the vector are empty. */
   static bool emptyDatabase(const std::vector<PerVariableDatabase>& vec);
@@ -796,12 +1036,15 @@ private:
   ArithCongruenceManager& d_congruenceManager;
 
   const context::Context * const d_satContext;
-  const int d_satAllocationLevel;
 
   RaiseConflict d_raiseConflict;
 
-  friend class Constraint_;
 
+  const Rational d_one;
+  const Rational d_negOne;
+  
+  friend class Constraint;
+  
 public:
 
   ConstraintDatabase( context::Context* satContext,
@@ -906,8 +1149,12 @@ public:
   void unatePropUpperBound(ConstraintP curr, ConstraintP prev);
   void unatePropEquality(ConstraintP curr, ConstraintP prevLB, ConstraintP prevUB);
 
+  /** AntecendentID must be in range. */
+  ConstraintCP getAntecedent(AntecedentId p) const;
+  
 private:
-  void raiseUnateConflict(ConstraintP ant, ConstraintP cons);
+  /** returns true if cons is now in conflict. */
+  bool handleUnateProp(ConstraintP ant, ConstraintP cons);
 
   DenseSet d_reclaimable;
 
diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h
index c9a630984..bfa42af46 100644
--- a/src/theory/arith/constraint_forward.h
+++ b/src/theory/arith/constraint_forward.h
@@ -26,16 +26,22 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-class Constraint_;
-typedef Constraint_* ConstraintP;
-typedef const Constraint_* ConstraintCP;
+class Constraint;
+typedef Constraint* ConstraintP;
+typedef const Constraint* ConstraintCP;
 
-const ConstraintP NullConstraint = NULL;
+static const ConstraintP NullConstraint = NULL;
 
 class ConstraintDatabase;
 
 typedef std::vector<ConstraintCP> ConstraintCPVec;
 
+typedef std::vector<Rational> RationalVector;
+typedef RationalVector* RationalVectorP;
+typedef const RationalVector* RationalVectorCP;
+static const RationalVectorCP RationalVectorCPSentinel = NULL;
+static const RationalVectorP RationalVectorPSentinel = NULL;
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 36208ff8d..7e50dad87 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -145,6 +145,8 @@ void DioSolver::pushInputConstraint(const Comparison& eq, Node reason){
     return;
   }
 
+
+
   uint32_t length = sp.maxLength();
   if(length > d_maxInputCoefficientLength){
     d_maxInputCoefficientLength = length;
@@ -155,7 +157,10 @@ void DioSolver::pushInputConstraint(const Comparison& eq, Node reason){
   //Variable proofVariable(makeIntegerVariable());
 
   TrailIndex posInTrail = d_trail.size();
-  d_trail.push_back(Constraint(sp,Polynomial(Monomial(VarList(proofVariable)))));
+  Debug("dio::pushInputConstraint") << "pushInputConstraint @ " << posInTrail
+                                    << " " << eq.getNode()
+                                    << " " << reason << endl;
+  d_trail.push_back(Constraint(sp,Polynomial::mkPolynomial(proofVariable)));
 
   size_t posInConstraintList = d_inputConstraints.size();
   d_inputConstraints.push_back(InputConstraint(reason, posInTrail));
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 2aeee696e..bd252bf49 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -55,6 +55,10 @@ LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, Bou
   d_basicVariableUpdates(f),
   d_increasing(1),
   d_decreasing(-1),
+  d_upperBoundDifference(),
+  d_lowerBoundDifference(),
+  d_one(1),
+  d_negOne(-1),
   d_btracking(boundsTracking),
   d_areTracking(false),
   d_trackCallback(this)
@@ -505,40 +509,117 @@ void LinearEqualityModule::propagateBasicFromRow(ConstraintP c){
   RowIndex ridx = d_tableau.basicToRowIndex(basic);
 
   ConstraintCPVec bounds;
-  propagateRow(bounds, ridx, upperBound, c);
-  c->impliedBy(bounds);
+  RationalVectorP coeffs = NULLPROOF(new RationalVector());
+  propagateRow(bounds, ridx, upperBound, c, coeffs);
+  c->impliedByFarkas(bounds, coeffs, false);
+  c->tryToPropagate();
+  
+  if(coeffs != RationalVectorPSentinel) { delete coeffs; }
 }
 
-void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bool rowUp, ConstraintP c){
+/* An explanation of the farkas coefficients.
+ *
+ * We are proving c using the other variables on the row.
+ * The proof is in terms of the other constraints and the negation of c, ~c.
+ *
+ * A row has the form:
+ *   sum a_i * x_i  = 0 
+ * or
+ *   sx + sum r y + sum q z = 0 
+ * where r > 0 and q < 0.
+ *
+ * If rowUp, we are proving c
+ *   g = sum r u_y + sum q l_z
+ *   and c is entailed by -sx <= g
+ * If !rowUp, we are proving c
+ *   g = sum r l_y + sum q u_z
+ *   and c is entailed by -sx >= g
+ *
+ *             | s     | c         | ~c       | u_i     | l_i
+ *   if  rowUp | s > 0 | x >= -g/s | x < -g/s | a_i > 0 | a_i < 0
+ *   if  rowUp | s < 0 | x <= -g/s | x > -g/s | a_i > 0 | a_i < 0
+ *   if !rowUp | s > 0 | x <= -g/s | x > -g/s | a_i < 0 | a_i > 0
+ *   if !rowUp | s < 0 | x >= -g/s | x < -g/s | a_i < 0 | a_i > 0
+ *
+ *
+ * Thus we treat !rowUp as multiplying the row by -1 and rowUp as 1
+ * for the entire row.
+ */
+void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bool rowUp, ConstraintP c, RationalVectorP farkas){
   Assert(!c->assertedToTheTheory());
   Assert(c->canBePropagated());
   Assert(!c->hasProof());
 
+  if(farkas != RationalVectorPSentinel){
+    Assert(farkas->empty());
+    farkas->push_back(Rational(0));
+  }
+  
   ArithVar v = c->getVariable();
-  Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
-                                   << v <<") start" << endl;
+  Debug("arith::propagateRow") << "LinearEqualityModule::propagateRow("
+                                   << ridx << ", " << rowUp << ", " << v << ") start" << endl;
+
+  const Rational& multiple = rowUp ? d_one : d_negOne;
 
+  Debug("arith::propagateRow") << "multiple: " << multiple << endl;
+  
   Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
   for(; !iter.atEnd(); ++iter){
     const Tableau::Entry& entry = *iter;
     ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == v){ continue; }
-
     const Rational& a_ij = entry.getCoefficient();
-
     int sgn = a_ij.sgn();
     Assert(sgn != 0);
     bool selectUb = rowUp ? (sgn > 0) : (sgn < 0);
-    ConstraintCP bound = selectUb
-      ? d_variables.getUpperBoundConstraint(nonbasic)
-      : d_variables.getLowerBoundConstraint(nonbasic);
 
-    Assert(bound != NullConstraint);
-    Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl;
-    into.push_back(bound);
+    Assert( nonbasic != v ||
+            ( rowUp && a_ij.sgn() > 0 && c->isLowerBound()) ||
+            ( rowUp && a_ij.sgn() < 0 && c->isUpperBound()) ||
+            (!rowUp && a_ij.sgn() > 0 && c->isUpperBound()) ||
+            (!rowUp && a_ij.sgn() < 0 && c->isLowerBound())
+            );
+
+    if(Debug.isOn("arith::propagateRow")){
+      if(nonbasic == v){
+        Debug("arith::propagateRow") << "(target) "
+                                     << rowUp << " "
+                                     << a_ij.sgn() << " "
+                                     << c->isLowerBound() << " "
+                                     << c->isUpperBound() << endl;
+
+        Debug("arith::propagateRow") << "(target) ";
+      }
+      Debug("arith::propagateRow") << "propagateRow " << a_ij << " * " << nonbasic ;
+    }
+
+    if(nonbasic == v){
+      if(farkas != RationalVectorPSentinel){
+        Assert(farkas->front().isZero());
+        Rational multAij = multiple * a_ij;
+        Debug("arith::propagateRow") << "("<<multAij<<") ";        
+        farkas->front() = multAij;      
+      }
+
+      Debug("arith::propagateRow") << c << endl;
+    }else{
+
+      ConstraintCP bound = selectUb
+        ? d_variables.getUpperBoundConstraint(nonbasic)
+        : d_variables.getLowerBoundConstraint(nonbasic);
+      
+      if(farkas != RationalVectorPSentinel){
+        Rational multAij = multiple * a_ij;
+        Debug("arith::propagateRow") << "("<<multAij<<") ";        
+        farkas->push_back(multAij);
+      }
+      Assert(bound != NullConstraint);
+      Debug("arith::propagateRow") << bound << endl;
+      into.push_back(bound);
+    }
   }
-  Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
-                                   << v << ") done" << endl;
+  Debug("arith::propagateRow") << "LinearEqualityModule::propagateRow("
+                                   << ridx << ", " << rowUp << ", " << v << ") done" << endl;
+
 }
 
 ConstraintP LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic) const {
@@ -574,13 +655,13 @@ ConstraintP LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRatio
         anyWeakening = true;
         surplus = surplus - diff;
 
-        Debug("weak") << "found:" << endl;
+        Debug("arith::weak") << "found:" << endl;
         if(v == basic){
-          Debug("weak") << "  basic: ";
+          Debug("arith::weak") << "  basic: ";
         }
-        Debug("weak") << "  " << surplus << " "<< diff  << endl
-                      << "  " << bound << c << endl
-                      << "  " << weakerBound << weaker << endl;
+        Debug("arith::weak") << "  " << surplus << " "<< diff  << endl
+                             << "  " << bound << c << endl
+                             << "  " << weakerBound << weaker << endl;
 
         Assert(diff.sgn() > 0);
         c = weaker;
@@ -591,9 +672,48 @@ ConstraintP LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRatio
   return c;
 }
 
-void LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, RaiseConflict& rc) const {
+/* An explanation of the farkas coefficients.
+ *
+ * We are proving a conflict on the basic variable x_b.
+ * If aboveUpper, then the conflict is with the constraint c : x_b <= u_b.
+ * If !aboveUpper, then the conflict is with the constraint c : x_b >= l_b.
+ *
+ * A row has the form:
+ *   -x_b sum a_i * x_i  = 0 
+ * or
+ *   -x_b + sum r y + sum q z = 0,
+ *    x_b = sum r y + sum q z
+ * where r > 0 and q < 0.
+ *
+ *
+ * If !aboveUp, we are proving ~c: x_b < l_b
+ *   g = sum r u_y + sum q l_z
+ *   x_b <= g < l_b
+ *   and ~c is entailed by x_b <= g
+ *
+ * If aboveUp, we are proving ~c : x_b > u_b
+ *   g = sum r l_y + sum q u_z
+ *   x_b >= g > u_b
+ *   and ~c is entailed by x_b >= g
+ *
+ *
+ *               | s     | c         | ~c       | u_i     | l_i
+ *   if !aboveUp | s > 0 | x >= -g/s | x < -g/s | a_i > 0 | a_i < 0
+ *   if !aboveUp | s < 0 | x <= -g/s | x > -g/s | a_i > 0 | a_i < 0
+ *   if  aboveUp | s > 0 | x <= -g/s | x > -g/s | a_i < 0 | a_i > 0
+ *   if  aboveUp | s < 0 | x >= -g/s | x < -g/s | a_i < 0 | a_i > 0
+ *
+ * Thus we treat aboveUp as multiplying the row by -1 and !aboveUp as 1
+ * for the entire row.
+ */
+ConstraintCP LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, FarkasConflictBuilder& fcs) const {
+  Assert(!fcs.underConstruction());
   TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime);
 
+  Debug("arith::weak") << "LinearEqualityModule::minimallyWeakConflict("
+                       << aboveUpper <<", "<< basicVar << ", ...) start" << endl;
+
+  const Rational& adjustSgn = aboveUpper ? d_negOne : d_one;
   const DeltaRational& assignment = d_variables.getAssignment(basicVar);
   DeltaRational surplus;
   if(aboveUpper){
@@ -605,7 +725,7 @@ void LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basic
     Assert(assignment < d_variables.getLowerBound(basicVar));
     surplus = d_variables.getLowerBound(basicVar) - assignment;
   }
-
+  
   bool anyWeakenings = false;
   for(Tableau::RowIterator i = d_tableau.basicRowIterator(basicVar); !i.atEnd(); ++i){
     const Tableau::Entry& entry = *i;
@@ -613,18 +733,29 @@ void LinearEqualityModule::minimallyWeakConflict(bool aboveUpper, ArithVar basic
     const Rational& coeff = entry.getCoefficient();
     bool weakening = false;
     ConstraintP c = weakestExplanation(aboveUpper, surplus, v, coeff, weakening, basicVar);
-    Debug("weak") << "weak : " << weakening << " "
-                  << c->assertedToTheTheory() << " "
-                  << d_variables.getAssignment(v) << " "
-                  << c << endl;
+    Debug("arith::weak") << "weak : " << weakening << " "
+                         << c->assertedToTheTheory() << " "
+                         << d_variables.getAssignment(v) << " "
+                         << c << endl;
     anyWeakenings = anyWeakenings || weakening;
 
-    rc.addConstraint(c);
+    fcs.addConstraint(c, coeff, adjustSgn);
+    if(basicVar == v){
+      Assert(! c->negationHasProof() );
+      fcs.makeLastConsequent();
+    }
   }
+  Assert(fcs.consequentIsSet());
+
+  ConstraintCP conflicted = fcs.commitConflict();
+
   ++d_statistics.d_weakeningAttempts;
   if(anyWeakenings){
     ++d_statistics.d_weakeningSuccesses;
   }
+  Debug("arith::weak") << "LinearEqualityModule::minimallyWeakConflict("
+                       << aboveUpper <<", "<< basicVar << ", ...) done" << endl;
+  return conflicted;
 }
 
 ArithVar LinearEqualityModule::minVarOrder(ArithVar x, ArithVar y) const {
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 5e325d799..f6717d141 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -199,6 +199,7 @@ public:
 
   typedef bool (LinearEqualityModule::*UpdatePreferenceFunction)(const UpdateInfo&, const UpdateInfo&) const;
 
+  
 private:
   /**
    * Manages information about the assignment and upper and lower bounds on the
@@ -217,6 +218,8 @@ private:
   Maybe<DeltaRational> d_upperBoundDifference;
   Maybe<DeltaRational> d_lowerBoundDifference;
 
+  Rational d_one;
+  Rational d_negOne;
 public:
 
   /**
@@ -417,10 +420,20 @@ public:
   void propagateBasicFromRow(ConstraintP c);
 
   /**
+   * Let v be the variable for the constraint c.
    * Exports either the explanation of an upperbound or a lower bound
-   * of the basic variable basic, using the non-basic variables in the row.
+   * of v using the other variables in the row.
+   *
+   * If farkas != RationalVectorPSentinel, this function additionally
+   * stores the farkas coefficients of the constraints stored in into.
+   * Position 0 is the coefficient of v.
+   * Position i > 0, corresponds to the order of the other constraints.
    */
-  void propagateRow(ConstraintCPVec& into, RowIndex ridx, bool rowUp, ConstraintP c);
+  void propagateRow(ConstraintCPVec& into
+                    , RowIndex ridx
+                    , bool rowUp
+                    , ConstraintP c
+                    , RationalVectorP farkas);
 
   /**
    * Computes the value of a basic variable using the assignments
@@ -598,20 +611,22 @@ private:
 public:
   /**
    * Constructs a minimally weak conflict for the basic variable basicVar.
+   *
+   * Returns a constraint that is now in conflict.
    */
-  void minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, RaiseConflict& rc) const;
+  ConstraintCP minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, FarkasConflictBuilder& rc) const;
 
   /**
-   * Given a non-basic variable that is know to have a conflict on it,
+   * Given a basic variable that is know to have a conflict on it,
    * construct and return a conflict.
    * Follows section 4.2 in the CAV06 paper.
    */
-  inline void generateConflictAboveUpperBound(ArithVar conflictVar, RaiseConflict& rc) const {
-    minimallyWeakConflict(true, conflictVar, rc);
+  inline ConstraintCP generateConflictAboveUpperBound(ArithVar conflictVar, FarkasConflictBuilder& rc) const {
+    return minimallyWeakConflict(true, conflictVar, rc);
   }
 
-  inline void generateConflictBelowLowerBound(ArithVar conflictVar, RaiseConflict& rc) const {
-    minimallyWeakConflict(false, conflictVar, rc);
+  inline ConstraintCP generateConflictBelowLowerBound(ArithVar conflictVar, FarkasConflictBuilder& rc) const {
+    return minimallyWeakConflict(false, conflictVar, rc);
   }
 
   /**
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index c5ad46dfc..fda34960a 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -211,6 +211,16 @@ Monomial Monomial::mkMonomial(const Constant& c, const VarList& vl) {
     return Monomial(c, vl);
   }
 }
+
+Monomial Monomial::mkMonomial(const VarList& vl) {
+  // acts like Monomial::mkMonomial( 1, vl)
+  if( vl.empty() ) {
+    return Monomial::mkOne();
+  } else if(true){
+    return Monomial(vl);
+  }
+}
+
 Monomial Monomial::parseMonomial(Node n) {
   if(n.getKind() == kind::CONST_RATIONAL) {
     return Monomial(Constant(n));
@@ -340,6 +350,17 @@ Polynomial Polynomial::operator+(const Polynomial& vl) const {
   return result;
 }
 
+Polynomial Polynomial::exactDivide(const Integer& z) const {
+  Assert(isIntegral());
+  if(z.isOne()){
+    return (*this);
+  }else {
+    Constant invz = Constant::mkConstant(Rational(1,z));
+    Polynomial prod = (*this) * Monomial::mkMonomial(invz);
+    Assert(prod.isIntegral());
+    return prod;
+  }
+}
 
 Polynomial Polynomial::sumPolynomials(const std::vector<Polynomial>& ps){
   if(ps.empty()){
@@ -368,11 +389,7 @@ Polynomial Polynomial::sumPolynomials(const std::vector<Polynomial>& ps){
         Constant c = Constant::mkConstant((*ci).second);
         Node n = (*ci).first;
         VarList vl = VarList::parseVarList(n);
-        if(vl.empty()){
-          monos.push_back(Monomial(c));
-        }else{
-          monos.push_back(Monomial(c, vl));
-        }
+        monos.push_back(Monomial::mkMonomial(c, vl));
       }
     }
     Monomial::sort(monos);
@@ -1085,7 +1102,7 @@ Node Comparison::mkRatEquality(const Polynomial& p){
   Constant coeffInv = -(minimalVList.getConstant().inverse());
 
   Polynomial newRight = (p - minimalVList) * coeffInv;
-  Polynomial newLeft(minimalVList.getVarList());
+  Polynomial newLeft(Monomial::mkMonomial(minimalVList.getVarList()));
 
   return toNode(kind::EQUAL, newLeft, newRight);
 }
@@ -1191,7 +1208,7 @@ Node Comparison::mkIntEquality(const Polynomial& p){
     Monomial m = varPartMult.selectAbsMinimum();
     bool mIsPositive =  m.getConstant().isPositive();
 
-    Polynomial noM = (varPartMult + (- m)) + Polynomial(constMult);
+    Polynomial noM = (varPartMult + (- m)) + Polynomial::mkPolynomial(constMult);
 
     // m + noM = 0
     Polynomial newRight = mIsPositive ? -noM : noM;
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index ac5ce10e5..97813338f 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -625,6 +625,7 @@ private:
 };/* class VarList */
 
 
+/** Constructors have side conditions. Use the static mkMonomial functions instead. */ 
 class Monomial : public NodeWrapper {
 private:
   Constant constant;
@@ -651,12 +652,10 @@ private:
       n.getNumChildren() == 2;
   }
 
-public:
-
   Monomial(const Constant& c):
     NodeWrapper(c.getNode()), constant(c), varList(VarList::mkEmptyVarList())
   { }
-
+  
   Monomial(const VarList& vl):
     NodeWrapper(vl.getNode()), constant(Constant::mkConstant(1)), varList(vl)
   {
@@ -672,12 +671,19 @@ public:
 
     Assert(multStructured(getNode()));
   }
-
+public:
   static bool isMember(TNode n);
 
   /** Makes a monomial with no restrictions on c and vl. */
   static Monomial mkMonomial(const Constant& c, const VarList& vl);
 
+  /** If vl is empty, this make one. */
+  static Monomial mkMonomial(const VarList& vl);
+
+  static Monomial mkMonomial(const Constant& c){
+    return Monomial(c);
+  }
+  
   static Monomial mkMonomial(const Variable& v){
     return Monomial(VarList(v));
   }
@@ -692,7 +698,7 @@ public:
   }
   const Constant& getConstant() const { return constant; }
   const VarList& getVarList() const { return varList; }
-
+  
   bool isConstant() const {
     return varList.empty();
   }
@@ -881,8 +887,12 @@ public:
     Assert( Monomial::isStrictlySorted(m) );
   }
 
+  static Polynomial mkPolynomial(const Constant& c){
+    return Polynomial(Monomial::mkMonomial(c));
+  }
+
   static Polynomial mkPolynomial(const Variable& v){
-    return Monomial::mkMonomial(v);
+    return Polynomial(Monomial::mkMonomial(v));
   }
 
   static Polynomial mkPolynomial(const std::vector<Monomial>& m) {
@@ -1016,13 +1026,8 @@ public:
    */
   Integer gcd() const;
 
-  Polynomial exactDivide(const Integer& z) const {
-    Assert(isIntegral());
-    Constant invz = Constant::mkConstant(Rational(1,z));
-    Polynomial prod = (*this) * Monomial(invz);
-    Assert(prod.isIntegral());
-    return prod;
-  }
+  /** z must divide all of the coefficients of the polynomial. */
+  Polynomial exactDivide(const Integer& z) const;
 
   Polynomial operator+(const Polynomial& vl) const;
   Polynomial operator-(const Polynomial& vl) const;
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index b37f24d14..49664e0ea 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -20,12 +20,14 @@
 #include "theory/arith/options.h"
 #include "theory/arith/constraint.h"
 
+
 using namespace std;
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
+
 SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
   : d_conflictVariables()
   , d_linEq(linEq)
@@ -34,14 +36,23 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq,
   , d_errorSet(errors)
   , d_numVariables(0)
   , d_conflictChannel(conflictChannel)
+  , d_conflictBuilder(NULL)
   , d_arithVarMalloc(tvmalloc)
   , d_errorSize(0)
   , d_zero(0)
+  , d_posOne(1)
+  , d_negOne(-1)
 {
   d_heuristicRule = options::arithErrorSelectionRule();
   d_errorSet.setSelectionRule(d_heuristicRule);
+  d_conflictBuilder = new FarkasConflictBuilder();
 }
 
+SimplexDecisionProcedure::~SimplexDecisionProcedure(){
+  delete d_conflictBuilder;
+}
+
+
 bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat& conflicts) {
   TimerStat::CodeTimer codeTimer(timer);
   Assert( d_conflictVariables.empty() );
@@ -77,37 +88,34 @@ bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat&
 void SimplexDecisionProcedure::reportConflict(ArithVar basic){
   Assert(!d_conflictVariables.isMember(basic));
   Assert(checkBasicForConflict(basic));
-  RaiseConflict rc( d_conflictChannel);
 
-  generateConflictForBasic(basic, rc);
+  ConstraintCP conflicted = generateConflictForBasic(basic);
+  Assert(conflicted != NullConstraint);
+  d_conflictChannel.raiseConflict(conflicted);
 
-  // static bool verbose = false;
-  // if(verbose) { Message() << "conflict " << basic << " " << conflict << endl; }
-  // Assert(!conflict.isNull());
-  //d_conflictChannel(conflict);
-  rc.commitConflict();
   d_conflictVariables.add(basic);
 }
 
-void SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic, RaiseConflict& rc) const {
+ConstraintCP SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic) const {
 
   Assert(d_tableau.isBasic(basic));
   Assert(checkBasicForConflict(basic));
 
   if(d_variables.cmpAssignmentLowerBound(basic) < 0){
     Assert(d_linEq.nonbasicsAtUpperBounds(basic));
-    return d_linEq.generateConflictBelowLowerBound(basic, rc);
+    return d_linEq.generateConflictBelowLowerBound(basic, *d_conflictBuilder);
   }else if(d_variables.cmpAssignmentUpperBound(basic) > 0){
     Assert(d_linEq.nonbasicsAtLowerBounds(basic));
-    return d_linEq.generateConflictAboveUpperBound(basic, rc);
+    return d_linEq.generateConflictAboveUpperBound(basic, *d_conflictBuilder);
   }else{
     Unreachable();
+    return NullConstraint;
   }
 }
 bool SimplexDecisionProcedure::maybeGenerateConflictForBasic(ArithVar basic) const {
   if(checkBasicForConflict(basic)){
-    RaiseConflict rc(d_conflictChannel);
-    generateConflictForBasic(basic, rc);
+    ConstraintCP conflicted = generateConflictForBasic(basic);
+    d_conflictChannel.raiseConflict(conflicted);
     return true;
   }else{
     return false;
@@ -183,9 +191,12 @@ void SimplexDecisionProcedure::removeFromInfeasFunc(TimerStat& timer, ArithVar i
 }
 
 ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set){
+  Debug("constructInfeasiblityFunction") << "constructInfeasiblityFunction start" << endl;
+
   TimerStat::CodeTimer codeTimer(timer);
   Assert(!d_errorSet.focusEmpty());
-
+  Assert(debugIsASet(set));
+  
   ArithVar inf = requestVariable();
   Assert(inf != ARITHVAR_SENTINEL);
 
@@ -199,8 +210,13 @@ ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& time
     Assert(!d_variables.assignmentIsConsistent(e));
 
     int sgn = d_errorSet.getSgn(e);
-    coeffs.push_back(Rational(sgn));
+    Assert(sgn == -1 || sgn == 1);
+    const Rational& violatedCoeff = sgn < 0 ? d_negOne : d_posOne;
+    coeffs.push_back(violatedCoeff);
     variables.push_back(e);
+
+    Debug("constructInfeasiblityFunction") << violatedCoeff << " " << e << endl;
+
   }
   d_tableau.addRow(inf, coeffs, variables);
   DeltaRational newAssignment = d_linEq.computeRowValue(inf, false);
@@ -210,7 +226,7 @@ ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& time
   d_linEq.trackRowIndex(d_tableau.basicToRowIndex(inf));
 
   Debug("constructInfeasiblityFunction") << inf << " " << newAssignment << endl;
-
+  Debug("constructInfeasiblityFunction") << "constructInfeasiblityFunction done" << endl;
   return inf;
 }
 
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 91e6e4244..ada9b5efd 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -105,6 +105,9 @@ protected:
   /** This is the call back channel for Simplex to report conflicts. */
   RaiseConflict d_conflictChannel;
 
+  /** This is the call back channel for Simplex to report conflicts. */
+  FarkasConflictBuilder* d_conflictBuilder;
+
   /** Used for requesting d_opt, bound and error variables for primal.*/
   TempVarMalloc d_arithVarMalloc;
 
@@ -114,6 +117,12 @@ protected:
   /** A local copy of 0. */
   const Rational d_zero;
 
+  /** A local copy of 1. */
+  const Rational d_posOne;
+
+  /** A local copy of -1. */
+  const Rational d_negOne;
+
   ArithVar constructInfeasiblityFunction(TimerStat& timer);
   ArithVar constructInfeasiblityFunction(TimerStat& timer, ArithVar e);
   ArithVar constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set);
@@ -126,6 +135,7 @@ protected:
 
 public:
   SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
+  ~SimplexDecisionProcedure();
 
   /**
    * Tries to update the assignments of variables such that all of the
@@ -166,7 +176,7 @@ protected:
    * If a basic variable has a conflict on its row,
    * this produces a minimized row on the conflict channel.
    */
-  void generateConflictForBasic(ArithVar basic, RaiseConflict& rc) const;
+  ConstraintCP generateConflictForBasic(ArithVar basic) const;
 
 
   /** Gets a fresh variable from TheoryArith. */
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 34f911b81..0d07c5ffc 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -634,12 +634,16 @@ unsigned SumOfInfeasibilitiesSPD::trySet(const ArithVarVec& set){
 }
 
 std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
+  Debug("arith::greedyConflictSubsets") << "greedyConflictSubsets start" << endl;
+
   std::vector< ArithVarVec > subsets;
   Assert(d_soiVar == ARITHVAR_SENTINEL);
 
   if(d_errorSize <= 2){
     ArithVarVec inError;
     d_errorSet.pushFocusInto(inError);
+    
+    Assert(debugIsASet(inError));
     subsets.push_back(inError);
     return subsets;
   }
@@ -653,9 +657,11 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
     ArithVar e = *iter;
     addRowSgns(sgns, e, d_errorSet.getSgn(e));
 
-    //cout << "basic error var: " << e << endl;
-    //d_tableau.debugPrintIsBasic(e);
-    //d_tableau.printBasicRow(e, cout);
+    Debug("arith::greedyConflictSubsets") << "basic error var: " << e << endl;
+    if(Debug.isOn("arith::greedyConflictSubsets")){
+      d_tableau.debugPrintIsBasic(e);
+      d_tableau.printBasicRow(e, Debug("arith::greedyConflictSubsets"));
+    }
   }
 
   // Phase 1: Try to find at least 1 pair for every element
@@ -683,9 +689,10 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
       tmp[0] = e;
       tmp[1] = b;
       if(trySet(tmp) == 2){
-        //cout << "found a pair" << endl;
+        Debug("arith::greedyConflictSubsets")  << "found a pair " << b << " " << e << endl;
         hasParticipated.softAdd(b);
         hasParticipated.softAdd(e);
+        Assert(debugIsASet(tmp));
         subsets.push_back(tmp);
         ++(d_statistics.d_soiConflicts);
         ++(d_statistics.d_hasToBeMinimal);
@@ -704,13 +711,15 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
     possibleStarts.pop_back();
     if(hasParticipated.isMember(v)){ continue; }
 
+    hasParticipated.add(v);
+    
     Assert(d_soiVar == ARITHVAR_SENTINEL);
     //d_soiVar's row =  \sumofinfeasibilites underConstruction
     ArithVarVec underConstruction;
     underConstruction.push_back(v);
     d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, v);
 
-    //cout << "trying " << v << endl;
+    Debug("arith::greedyConflictSubsets") << "trying " << v << endl;
 
     const Tableau::Entry* spoiler = NULL;
     while( (spoiler = d_linEq.selectSlackEntry(d_soiVar, false)) != NULL){
@@ -718,16 +727,16 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
       int oppositeSgn = -(spoiler->getCoefficient().sgn());
       Assert(oppositeSgn != 0);
 
-      //cout << "looking for " << nb << " " << oppositeSgn << endl;
+      Debug("arith::greedyConflictSubsets") << "looking for " << nb << " " << oppositeSgn << endl;
 
       ArithVar basicWithOp = find_basic_in_sgns(sgns, nb, oppositeSgn, hasParticipated, false);
 
       if(basicWithOp == ARITHVAR_SENTINEL){
-        //cout << "search did not work  for " << nb << endl;
+        Debug("arith::greedyConflictSubsets") << "search did not work  for " << nb << endl;
         // greedy construction has failed
         break;
       }else{
-        //cout << "found  " << basicWithOp << endl;
+        Debug("arith::greedyConflictSubsets") << "found  " << basicWithOp << endl;
 
         addToInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, basicWithOp);
         hasParticipated.softAdd(basicWithOp);
@@ -735,8 +744,9 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
       }
     }
     if(spoiler == NULL){
-      //cout << "success" << endl;
+      Debug("arith::greedyConflictSubsets") << "success" << endl;
       //then underConstruction contains a conflicting subset
+      Assert(debugIsASet(underConstruction));
       subsets.push_back(underConstruction);
       ++d_statistics.d_soiConflicts;
       if(underConstruction.size() == 3){
@@ -745,7 +755,7 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
         ++d_statistics.d_maybeNotMinimal;
       }
     }else{
-      //cout << "failure" << endl;
+      Debug("arith::greedyConflictSubsets") << "failure" << endl;
     }
     tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
     d_soiVar = ARITHVAR_SENTINEL;
@@ -762,52 +772,89 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
 
 
   Assert(d_soiVar == ARITHVAR_SENTINEL);
+  Debug("arith::greedyConflictSubsets") << "greedyConflictSubsets done" << endl;
   return subsets;
 }
 
-void SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){
+bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){
   Assert(d_soiVar == ARITHVAR_SENTINEL);
   d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, subset);
+  Assert(!subset.empty());
+  Assert(!d_conflictBuilder->underConstruction());
+    
+  Debug("arith::generateSOIConflict") << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) start" << endl;
 
-  //NodeBuilder<> conflict(kind::AND);
+  bool success = false;
+    
   for(ArithVarVec::const_iterator iter = subset.begin(), end = subset.end(); iter != end; ++iter){
     ArithVar e = *iter;
     ConstraintP violated = d_errorSet.getViolated(e);
-    //cout << "basic error var: " << violated << endl;
-    d_conflictChannel.addConstraint(violated);
-    //violated->explainForConflict(conflict);
+    Assert(violated != NullConstraint);
 
-    //d_tableau.debugPrintIsBasic(e);
-    //d_tableau.printBasicRow(e, cout);
-  }
-  for(Tableau::RowIterator i = d_tableau.basicRowIterator(d_soiVar); !i.atEnd(); ++i){
-    const Tableau::Entry& entry = *i;
-    ArithVar v = entry.getColVar();
-    if(v == d_soiVar){ continue; }
-    const Rational& coeff = entry.getCoefficient();
 
-    ConstraintP c = (coeff.sgn() > 0) ?
-      d_variables.getUpperBoundConstraint(v) :
-      d_variables.getLowerBoundConstraint(v);
+    int sgn = d_errorSet.getSgn(e);
+    const Rational& violatedCoeff = sgn > 0 ? d_negOne : d_posOne;
+    Debug("arith::generateSOIConflict") << "basic error var: "
+                                        << "(" <<  violatedCoeff << ")"
+                                        << " " << violated
+                                        << endl;
 
-    //cout << "nb : " << c << endl;
-    d_conflictChannel.addConstraint(c);
+
+    d_conflictBuilder->addConstraint(violated, violatedCoeff);
+    Assert(violated->hasProof());
+    if(!success && !violated->negationHasProof()){
+      success = true;
+      d_conflictBuilder->makeLastConsequent();
+    }
+  }
+  
+  if(!success){
+    // failure
+    d_conflictBuilder->reset();
+  } else {
+    // pick a violated constraint arbitrarily. any of them may be selected for the conflict
+    Assert(d_conflictBuilder->underConstruction());
+    Assert(d_conflictBuilder->consequentIsSet());
+    
+    for(Tableau::RowIterator i = d_tableau.basicRowIterator(d_soiVar); !i.atEnd(); ++i){
+      const Tableau::Entry& entry = *i;
+      ArithVar v = entry.getColVar();
+      if(v == d_soiVar){ continue; }
+      const Rational& coeff = entry.getCoefficient();
+
+      ConstraintP c = (coeff.sgn() > 0) ?
+        d_variables.getUpperBoundConstraint(v) :
+        d_variables.getLowerBoundConstraint(v);
+      
+      Debug("arith::generateSOIConflict") << "non-basic var: "
+                                          << "(" <<  coeff << ")"
+                                          << " " << c
+                                          << endl;
+      d_conflictBuilder->addConstraint(c, coeff);
+    }
+    ConstraintCP conflicted = d_conflictBuilder->commitConflict();
+    d_conflictChannel.raiseConflict(conflicted);
   }
 
-  //Node conf = conflict;
   tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
   d_soiVar = ARITHVAR_SENTINEL;
-  d_conflictChannel.commitConflict();
-  //return conf;
+  Debug("arith::generateSOIConflict") << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) done" << endl;
+  Assert(d_soiVar == ARITHVAR_SENTINEL);
+  Assert(!d_conflictBuilder->underConstruction());
+  return success;
 }
 
 
 WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
   static int instance = 0;
   instance++;
-  //cout << "SOI conflict " << instance << ": |E| = " << d_errorSize << endl;
-  //d_errorSet.debugPrint(cout);
-  //cout << endl;
+  
+  Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() start "
+                              << instance << ": |E| = " << d_errorSize << endl;
+  if(Debug.isOn("arith::SOIConflict")){
+    d_errorSet.debugPrint(cout);
+  }
+  Debug("arith::SOIConflict") << endl;
 
   tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
   d_soiVar = ARITHVAR_SENTINEL;
@@ -815,24 +862,22 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
   if(options::soiQuickExplain()){
     quickExplain();
     generateSOIConflict(d_qeConflict);
-    //Node conflict = generateSOIConflict(d_qeConflict);
-    //cout << conflict << endl;
-    //d_conflictChannel(conflict);
   }else{
-
     vector<ArithVarVec> subsets = greedyConflictSubsets();
     Assert(  d_soiVar == ARITHVAR_SENTINEL);
-
+    bool anySuccess = false;
     Assert(!subsets.empty());
     for(vector<ArithVarVec>::const_iterator i = subsets.begin(), end = subsets.end(); i != end; ++i){
       const ArithVarVec& subset = *i;
-      generateSOIConflict(subset);
+      Assert(debugIsASet(subset));
+      anySuccess = generateSOIConflict(subset) || anySuccess;
       //Node conflict = generateSOIConflict(subset);
       //cout << conflict << endl;
 
       //reportConflict(conf); do not do this. We need a custom explanations!
       //d_conflictChannel(conflict);
     }
+    Assert(anySuccess);
   }
   Assert(  d_soiVar == ARITHVAR_SENTINEL);
   d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization);
@@ -840,7 +885,8 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
   //reportConflict(conf); do not do this. We need a custom explanations!
   d_conflictVariables.add(d_soiVar);
 
-  //cout << "SOI conflict " << instance << "end" << endl;
+  Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() done "
+                              << instance << "end" << endl;
   return ConflictFound;
 }
 
@@ -877,7 +923,6 @@ WitnessImprovement SumOfInfeasibilitiesSPD::soiRound() {
 }
 
 bool SumOfInfeasibilitiesSPD::debugSOI(WitnessImprovement w, ostream& out, int instance) const{
-//#warning "Redo SOI"
   return true;
   // out << "DLV("<<instance<<") ";
   // switch(w){
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index d9f6e9707..6dd6373d4 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -171,7 +171,7 @@ private:
   WitnessImprovement soiRound();
   WitnessImprovement SOIConflict();
   std::vector< ArithVarVec > greedyConflictSubsets();
-  void generateSOIConflict(const ArithVarVec& subset);
+  bool generateSOIConflict(const ArithVarVec& subset);
 
   // WitnessImprovement focusUsingSignDisagreements(ArithVar basic);
   // WitnessImprovement focusDownToLastHalf();
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index ea0bec095..231eb1562 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -95,14 +95,12 @@ void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCa
   cb.multiplyRow(rid, -a_rs_sgn);
 }
 
-
-
 void Tableau::addRow(ArithVar basic,
                      const std::vector<Rational>& coefficients,
                      const std::vector<ArithVar>& variables)
 {
   Assert(basic < getNumColumns());
-
+  Assert(debugIsASet(variables));
   Assert(coefficients.size() == variables.size() );
   Assert(!isBasic(basic));
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c8e7991a5..2cf313fc2 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -99,8 +99,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_containing(containing),
   d_nlIncomplete( false),
   d_rowTracking(),
-  d_conflictBuffer(),
-  d_constraintDatabase(c, u, d_partialModel, d_congruenceManager, RaiseConflict(*this, d_conflictBuffer)),
+  d_constraintDatabase(c, u, d_partialModel, d_congruenceManager, RaiseConflict(*this)),
   d_qflraStatus(Result::SAT_UNKNOWN),
   d_unknownsInARow(0),
   d_hasDoneWorkSinceCut(false),
@@ -122,15 +121,14 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_tableauResetDensity(1.6),
   d_tableauResetPeriod(10),
   d_conflicts(c),
-
   d_blackBoxConflict(c, Node::null()),
-  d_congruenceManager(c, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseConflict(*this, d_conflictBuffer)),
+  d_congruenceManager(c, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseEqualityEngineConflict(*this)),
   d_cmEnabled(c, true),
 
-  d_dualSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
-  d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
-  d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
-  d_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)),
+  d_dualSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
+  d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
+  d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
+  d_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
 
   d_pass1SDP(NULL),
   d_otherSDP(NULL),
@@ -540,6 +538,17 @@ bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap){
   return true;
 }
 
+void TheoryArithPrivate::raiseConflict(ConstraintCP a){
+  Assert(a->inConflict());
+  d_conflicts.push_back(a);
+}
+
+void TheoryArithPrivate::raiseBlackBoxConflict(Node bb){
+  if(d_blackBoxConflict.get().isNull()){
+    d_blackBoxConflict = bb;
+  }
+}
+
 void TheoryArithPrivate::revertOutOfConflict(){
   d_partialModel.revertAssignmentChanges();
   clearUpdates();
@@ -550,20 +559,20 @@ void TheoryArithPrivate::clearUpdates(){
   d_updatedBounds.purge();
 }
 
-void TheoryArithPrivate::raiseConflict(ConstraintCP a, ConstraintCP b){
-  ConstraintCPVec v;
-  v.push_back(a);
-  v.push_back(b);
-  d_conflicts.push_back(v);
-}
+// void TheoryArithPrivate::raiseConflict(ConstraintCP a, ConstraintCP b){
+//   ConstraintCPVec v;
+//   v.push_back(a);
+//   v.push_back(b);
+//   d_conflicts.push_back(v);
+// }
 
-void TheoryArithPrivate::raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c){
-  ConstraintCPVec v;
-  v.push_back(a);
-  v.push_back(b);
-  v.push_back(c);
-  d_conflicts.push_back(v);
-}
+// void TheoryArithPrivate::raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c){
+//   ConstraintCPVec v;
+//   v.push_back(a);
+//   v.push_back(b);
+//   v.push_back(c);
+//   d_conflicts.push_back(v);
+// }
 
 void TheoryArithPrivate::zeroDifferenceDetected(ArithVar x){
   if(d_cmEnabled){
@@ -613,6 +622,9 @@ bool TheoryArithPrivate::getDioCuttingResource(){
 bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
   Assert(constraint != NullConstraint);
   Assert(constraint->isLowerBound());
+  Assert(constraint->isTrue());
+  Assert(!constraint->negationHasProof());
+  
 
   ArithVar x_i = constraint->getVariable();
   const DeltaRational& c_i = constraint->getValue();
@@ -629,17 +641,17 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
   int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i);
   if(cmpToUB > 0){ //  c_i < \lowerbound(x_i)
     ConstraintP ubc = d_partialModel.getUpperBoundConstraint(x_i);
-    raiseConflict(ubc, constraint);
+    ConstraintP negation = constraint->getNegation();
+    negation->impliedByUnate(ubc, true);
+    
+    raiseConflict(constraint);
 
-    // Node conflict = ConstraintValue::explainConflict(ubc, constraint);
-    // Debug("arith") << "AssertLower conflict " << conflict << endl;
-    // raiseConflict(conflict);
     ++(d_statistics.d_statAssertLowerConflicts);
     return true;
   }else if(cmpToUB == 0){
     if(isInteger(x_i)){
       d_constantIntegerVariables.push_back(x_i);
-      Debug("dio::push") << x_i << endl;
+      Debug("dio::push") << "dio::push " << x_i << endl;
     }
     ConstraintP ub = d_partialModel.getUpperBoundConstraint(x_i);
 
@@ -653,26 +665,28 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
     }
 
     const ValueCollection& vc = constraint->getValueCollection();
-    if(vc.hasDisequality()){
-      Assert(vc.hasEquality());
+    if(vc.hasEquality()){
+      
+      Assert(vc.hasDisequality());
       ConstraintP eq = vc.getEquality();
       ConstraintP diseq = vc.getDisequality();
-      if(diseq->isTrue()){
-        //const ConstraintP ub = vc.getUpperBound();
-        raiseConflict(diseq, ub, constraint);
-        //Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint);
-
+      // x <= b, x >= b |= x = b
+      // (x > b or x < b or x = b)
+      Debug("arith::eq") << "lb == ub, propagate eq" << eq << endl;
+      bool triConflict = diseq->isTrue();
+
+      if(!eq->isTrue()){
+        eq->impliedByTrichotomy(constraint, ub, triConflict);
+        eq->tryToPropagate();
+      }
+      if(triConflict){
         ++(d_statistics.d_statDisequalityConflicts);
-        //Debug("eq") << " assert lower conflict " << conflict << endl;
-        //raiseConflict(conflict);
+        raiseConflict(eq);
         return true;
-      }else if(!eq->isTrue()){
-        Debug("eq") << "lb == ub, propagate eq" << eq << endl;
-        eq->impliedBy(constraint, d_partialModel.getUpperBoundConstraint(x_i));
-        // do not need to add to d_learnedBounds
       }
     }
   }else{
+    // l <= x <= u and l < u
     Assert(cmpToUB < 0);
     const ValueCollection& vc = constraint->getValueCollection();
 
@@ -680,17 +694,20 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
       const ConstraintP diseq = vc.getDisequality();
       if(diseq->isTrue()){
         const ConstraintP ub = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), UpperBound);
-
-        if(ub->hasProof()){
-          raiseConflict(diseq, ub, constraint);
+        ConstraintP negUb = ub->getNegation();
+
+        // l <= x, l != x |= l < x
+        // |= not (l >= x)
+        bool ubInConflict = ub->hasProof();
+        bool learnNegUb = !(negUb->hasProof());
+        if(learnNegUb){
+          negUb->impliedByTrichotomy(constraint, diseq, ubInConflict);
+          negUb->tryToPropagate();
+        }
+        if(ubInConflict){
+          raiseConflict(ub);
           return true;
-          // Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint);
-          // Debug("eq") << " assert upper conflict " << conflict << endl;
-          // raiseConflict(conflict);
-          // return true;
-        }else if(!ub->negationHasProof()){
-          ConstraintP negUb = ub->getNegation();
-          negUb->impliedBy(constraint, diseq);
+        }else if(learnNegUb){
           d_learnedBounds.push_back(negUb);
         }
       }
@@ -740,13 +757,16 @@ bool TheoryArithPrivate::AssertLower(ConstraintP constraint){
 
 /* procedure AssertUpper( x_i <= c_i) */
 bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
+  Assert(constraint != NullConstraint);
+  Assert(constraint->isUpperBound());
+  Assert(constraint->isTrue());
+  Assert(!constraint->negationHasProof());
+  
   ArithVar x_i = constraint->getVariable();
   const DeltaRational& c_i = constraint->getValue();
 
   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
-  AssertArgument(constraint != NullConstraint,
-                 "AssertUpper() called on a NullConstraint.");
-  Assert(constraint->isUpperBound());
+
 
   //Too strong because of rounding with integers
   //Assert(!constraint->hasLiteral() || original == constraint->getLiteral());
@@ -757,22 +777,25 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
   if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
     return false; //sat
   }
-
+  
   // cmpToLb =  \lowerbound(x_i).cmp(c_i)
   int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i);
   if( cmpToLB < 0 ){ //  \upperbound(x_i) < \lowerbound(x_i)
+    // l_i <= x_i and c_i < l_i |= c_i < x_i
+    // or ... |= not (x_i <= c_i)
     ConstraintP lbc = d_partialModel.getLowerBoundConstraint(x_i);
-    raiseConflict(lbc, constraint);
-    //Node conflict =  ConstraintValue::explainConflict(lbc, constraint);
-    //Debug("arith") << "AssertUpper conflict " << conflict << endl;
+    ConstraintP negConstraint = constraint->getNegation();
+    negConstraint->impliedByUnate(lbc, true);
+    raiseConflict(constraint);
     ++(d_statistics.d_statAssertUpperConflicts);
-    //raiseConflict(conflict);
     return true;
   }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i)
     if(isInteger(x_i)){
       d_constantIntegerVariables.push_back(x_i);
-      Debug("dio::push") << x_i << endl;
+      Debug("dio::push") << "dio::push " << x_i << endl;
     }
+
+    const ValueCollection& vc = constraint->getValueCollection();
     ConstraintP lb = d_partialModel.getLowerBoundConstraint(x_i);
     if(d_cmEnabled){
       if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){
@@ -783,39 +806,47 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
       }
     }
 
-    const ValueCollection& vc = constraint->getValueCollection();
     if(vc.hasDisequality()){
-      Assert(vc.hasEquality());
-      const ConstraintP diseq = vc.getDisequality();
-      const ConstraintP eq = vc.getEquality();
-      if(diseq->isTrue()){
-        raiseConflict(diseq, lb, constraint);
-        //Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
-        //Debug("eq") << " assert upper conflict " << conflict << endl;
-        //raiseConflict(conflict);
-        return true;
-      }else if(!eq->isTrue()){
-        Debug("eq") << "lb == ub, propagate eq" << eq << endl;
-        eq->impliedBy(constraint, d_partialModel.getLowerBoundConstraint(x_i));
-        //do not bother to add to d_learnedBounds
+      Assert(vc.hasDisequality());
+      ConstraintP eq = vc.getEquality();
+      ConstraintP diseq = vc.getDisequality();
+      // x <= b, x >= b |= x = b
+      // (x > b or x < b or x = b)
+      Debug("arith::eq") << "lb == ub, propagate eq" << eq << endl;
+      bool triConflict = diseq->isTrue();
+      if(!eq->isTrue()){
+        eq->impliedByTrichotomy(constraint, lb, triConflict);
+        eq->tryToPropagate();
       }
+      if(triConflict){
+        ++(d_statistics.d_statDisequalityConflicts);
+        raiseConflict(eq);
+        return true;
+      }      
     }
   }else if(cmpToLB > 0){
+    // l <= x <= u and l < u
+    Assert(cmpToLB > 0);
     const ValueCollection& vc = constraint->getValueCollection();
+
     if(vc.hasDisequality()){
       const ConstraintP diseq = vc.getDisequality();
       if(diseq->isTrue()){
-        const ConstraintP lb =
-          d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
-        if(lb->hasProof()){
-          raiseConflict(diseq, lb, constraint);
-          //Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
-          //Debug("eq") << " assert upper conflict " << conflict << endl;
-          //raiseConflict(conflict);
+        const ConstraintP lb = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
+        ConstraintP negLb = lb->getNegation();
+
+        // x <= u, u != x |= u < x
+        // |= not (u >= x)
+        bool lbInConflict = lb->hasProof();
+        bool learnNegLb = !(negLb->hasProof());
+        if(learnNegLb){
+          negLb->impliedByTrichotomy(constraint, diseq, lbInConflict);
+          negLb->tryToPropagate();
+        }
+        if(lbInConflict){
+          raiseConflict(lb);
           return true;
-        }else if(!lb->negationHasProof()){
-          ConstraintP negLb = lb->getNegation();
-          negLb->impliedBy(constraint, diseq);
+        }else if(learnNegLb){
           d_learnedBounds.push_back(negLb);
         }
       }
@@ -867,8 +898,10 @@ bool TheoryArithPrivate::AssertUpper(ConstraintP constraint){
 
 /* procedure AssertEquality( x_i == c_i ) */
 bool TheoryArithPrivate::AssertEquality(ConstraintP constraint){
-  AssertArgument(constraint != NullConstraint,
-                 "AssertUpper() called on a NullConstraint.");
+  Assert(constraint != NullConstraint);
+  Assert(constraint->isEquality());
+  Assert(constraint->isTrue());
+  Assert(!constraint->negationHasProof());
 
   ArithVar x_i = constraint->getVariable();
   const DeltaRational& c_i = constraint->getValue();
@@ -887,22 +920,13 @@ bool TheoryArithPrivate::AssertEquality(ConstraintP constraint){
     return false; //sat
   }
 
-  if(cmpToUB > 0){
-    ConstraintP ubc = d_partialModel.getUpperBoundConstraint(x_i);
-    raiseConflict(ubc, constraint);
-    //Node conflict = ConstraintValue::explainConflict(ubc, constraint);
-    //Debug("arith") << "AssertEquality conflicts with upper bound " << conflict << endl;
-    //raiseConflict(conflict);
-    return true;
-  }
-
-  if(cmpToLB < 0){
-    ConstraintP lbc = d_partialModel.getLowerBoundConstraint(x_i);
-    raiseConflict(lbc, constraint);
-
-    // Node conflict = ConstraintValue::explainConflict(lbc, constraint);
-    // Debug("arith") << "AssertEquality conflicts with lower bound" << conflict << endl;
-    // raiseConflict(conflict);
+  if(cmpToUB > 0 || cmpToLB < 0){
+    ConstraintP cb = (cmpToUB > 0) ?  d_partialModel.getUpperBoundConstraint(x_i) :
+      d_partialModel.getLowerBoundConstraint(x_i);
+    ConstraintP diseq = constraint->getNegation();
+    Assert(!diseq->isTrue());
+    diseq->impliedByUnate(cb, true);
+    raiseConflict(constraint);
     return true;
   }
 
@@ -913,7 +937,7 @@ bool TheoryArithPrivate::AssertEquality(ConstraintP constraint){
 
   if(isInteger(x_i)){
     d_constantIntegerVariables.push_back(x_i);
-    Debug("dio::push") << x_i << endl;
+    Debug("dio::push") << "dio::push " << x_i << endl;
   }
 
   // Don't bother to check whether x_i != c_i is in d_diseq
@@ -967,12 +991,13 @@ bool TheoryArithPrivate::AssertEquality(ConstraintP constraint){
 
 /* procedure AssertDisequality( x_i != c_i ) */
 bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
+  Assert(constraint != NullConstraint);
+  Assert(constraint->isDisequality());
+  Assert(constraint->isTrue());
+  Assert(!constraint->negationHasProof());
 
-  AssertArgument(constraint != NullConstraint,
-                 "AssertUpper() called on a NullConstraint.");
   ArithVar x_i = constraint->getVariable();
   const DeltaRational& c_i = constraint->getValue();
-
   Debug("arith") << "AssertDisequality(" << x_i << " " << c_i << ")"<< std::endl;
 
   //Should be fine in integers
@@ -992,12 +1017,11 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
     const ConstraintP lb = vc.getLowerBound();
     const ConstraintP ub = vc.getUpperBound();
     if(lb->isTrue() && ub->isTrue()){
+      ConstraintP eq = constraint->getNegation();
+      eq->impliedByTrichotomy(lb, ub, true);
+      raiseConflict(constraint);
       //in conflict
-      Debug("eq") << "explaining" << endl;
       ++(d_statistics.d_statDisequalityConflicts);
-      raiseConflict(constraint, lb, ub);
-      //Node conflict = ConstraintValue::explainConflict(constraint, lb, ub);
-      //raiseConflict(conflict);
       return true;
     }
   }
@@ -1005,10 +1029,12 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
     const ConstraintP lb = vc.getLowerBound();
     if(lb->isTrue()){
       const ConstraintP ub = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), UpperBound);
-      Debug("eq") << "propagate UpperBound " << constraint << lb << ub << endl;
+      Assert(!ub->isTrue());
+      Debug("arith::eq") << "propagate UpperBound " << constraint << lb << ub << endl;
       const ConstraintP negUb = ub->getNegation();
       if(!negUb->isTrue()){
-        negUb->impliedBy(constraint, lb);
+        negUb->impliedByTrichotomy(constraint, lb, false);
+        negUb->tryToPropagate();
         d_learnedBounds.push_back(negUb);
       }
     }
@@ -1017,11 +1043,13 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
     const ConstraintP ub = vc.getUpperBound();
     if(ub->isTrue()){
       const ConstraintP lb = d_constraintDatabase.ensureConstraint(const_cast<ValueCollection&>(vc), LowerBound);
+      Assert(!lb->isTrue());
 
-      Debug("eq") << "propagate LowerBound " << constraint << lb << ub << endl;
+      Debug("arith::eq") << "propagate LowerBound " << constraint << lb << ub << endl;
       const ConstraintP negLb = lb->getNegation();
       if(!negLb->isTrue()){
-        negLb->impliedBy(constraint, ub);
+        negLb->impliedByTrichotomy(constraint, ub, false);
+        negLb->tryToPropagate();
         d_learnedBounds.push_back(negLb);
       }
     }
@@ -1030,19 +1058,19 @@ bool TheoryArithPrivate::AssertDisequality(ConstraintP constraint){
   bool split = constraint->isSplit();
 
   if(!split && c_i == d_partialModel.getAssignment(x_i)){
-    Debug("eq") << "lemma now! " << constraint << endl;
+    Debug("arith::eq") << "lemma now! " << constraint << endl;
     outputLemma(constraint->split());
     return false;
   }else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){
-    Debug("eq") << "can drop as less than lb" << constraint << endl;
+    Debug("arith::eq") << "can drop as less than lb" << constraint << endl;
   }else if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i)){
-    Debug("eq") << "can drop as less than ub" << constraint << endl;
+    Debug("arith::eq") << "can drop as less than ub" << constraint << endl;
   }else if(!split){
-    Debug("eq") << "push back" << constraint << endl;
+    Debug("arith::eq") << "push back" << constraint << endl;
     d_diseqQueue.push(constraint);
     d_partialModel.invalidateDelta();
   }else{
-    Debug("eq") << "skipping already split " << constraint << endl;
+    Debug("arith::eq") << "skipping already split " << constraint << endl;
   }
   return false;
 }
@@ -1748,7 +1776,7 @@ Comparison TheoryArithPrivate::mkIntegerEqualityFromAssignment(ArithVar v){
   const DeltaRational& beta = d_partialModel.getAssignment(v);
 
   Assert(beta.isIntegral());
-  Polynomial betaAsPolynomial( Constant::mkConstant(beta.floor()) );
+  Polynomial betaAsPolynomial = Polynomial::mkPolynomial( Constant::mkConstant(beta.floor()) );
 
   TNode var = d_partialModel.asNode(v);
   Polynomial varAsPolynomial = Polynomial::parsePolynomial(var);
@@ -1768,7 +1796,7 @@ Node TheoryArithPrivate::dioCutting(){
           // If the bounds are equal this is already in the dioSolver
           //Add v = dr as a speculation.
           Comparison eq = mkIntegerEqualityFromAssignment(v);
-          Debug("dio::push") <<v << " " <<  eq.getNode() << endl;
+          Debug("dio::push") << "dio::push " << v << " " <<  eq.getNode() << endl;
           Assert(!eq.isBoolean());
           d_diosolver.pushInputConstraint(eq, eq.getNode());
           // It does not matter what the explanation of eq is.
@@ -1783,7 +1811,7 @@ Node TheoryArithPrivate::dioCutting(){
     return Node::null();
   }else{
     Polynomial p = plane.getPolynomial();
-    Polynomial c(plane.getConstant() * Constant::mkConstant(-1));
+    Polynomial c = Polynomial::mkPolynomial(plane.getConstant() * Constant::mkConstant(-1));
     Integer gcd = p.gcd();
     Assert(p.isIntegral());
     Assert(c.isIntegral());
@@ -1808,7 +1836,7 @@ Node TheoryArithPrivate::callDioSolver(){
     ArithVar v = d_constantIntegerVariables.front();
     d_constantIntegerVariables.pop();
 
-    Debug("arith::dio")  << v << endl;
+    Debug("arith::dio")  << "callDioSolver " << v << endl;
 
     Assert(isInteger(v));
     Assert(d_partialModel.boundsAreEqual(v));
@@ -1823,7 +1851,7 @@ Node TheoryArithPrivate::callDioSolver(){
     }else if(ub->isEquality()){
       orig = ub->externalExplainByAssertions();
     }else {
-      orig = Constraint_::externalExplainByAssertions(ub, lb);
+      orig = Constraint::externalExplainByAssertions(ub, lb);
     }
 
     Assert(d_partialModel.assignmentIsConsistent(v));
@@ -1838,7 +1866,7 @@ Node TheoryArithPrivate::callDioSolver(){
       Assert(orig.getKind() != EQUAL);
       return orig;
     }else{
-      Debug("dio::push") << v << " " << eq.getNode() << " with reason " << orig << endl;
+      Debug("dio::push") << "dio::push " << v << " " << eq.getNode() << " with reason " << orig << endl;
       d_diosolver.pushInputConstraint(eq, orig);
     }
   }
@@ -1863,7 +1891,7 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(){
         // if is (not true), or false
         Assert((reEq.getConst<bool>() && isDistinct) ||
                (!reEq.getConst<bool>() && !isDistinct));
-        blackBoxConflict(assertion);
+        raiseBlackBoxConflict(assertion);
       }
       return NullConstraint;
     }
@@ -1883,49 +1911,43 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(){
 
   Assert(constraint != NullConstraint);
 
-  if(constraint->negationHasProof()){
+  if(constraint->assertedToTheTheory()){
+    //Do nothing
+    return NullConstraint;
+  }
+  Assert(!constraint->assertedToTheTheory());
+  bool inConflict = constraint->negationHasProof();
+  constraint->setAssertedToTheTheory(assertion, inConflict);
+
+  if(!constraint->hasProof()){
+    Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
+    constraint->setAssumption(inConflict);
+  } else {
+    Debug("arith::constraint") << "already has proof: " << constraint->externalExplainByAssertions() << endl;
+  }
+  
+
+  if(Debug.isOn("arith::negatedassumption") && inConflict){
     ConstraintP negation = constraint->getNegation();
-    if(negation->isSelfExplaining()){
-      if(Debug.isOn("whytheoryenginewhy")){
-        debugPrintFacts();
-      }
+    if(Debug.isOn("arith::negatedassumption") && negation->isAssumption()){
+      debugPrintFacts();
     }
+    Debug("arith::eq") << "negation has proof" << endl;
     Debug("arith::eq") << constraint << endl;
     Debug("arith::eq") << negation << endl;
-
-    constraint->setAssertedToTheTheoryWithNegationTrue(assertion);
-    if(!constraint->hasProof()){
-      Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
-      constraint->selfExplainingWithNegationTrue();
-    }else{
-      Debug("arith::constraint") << "already has proof: " << constraint->externalExplainByAssertions() << endl;
-    }
-
-    raiseConflict(constraint, negation);
-    // NodeBuilder<> nb(kind::AND);
-    // nb << assertion;
-    // negation->explainForConflict(nb);
-    // Node conflict = nb;
-    // Debug("arith::eq") << "conflict" << conflict << endl;
-    // raiseConflict(conflict);
-    return NullConstraint;
   }
-  Assert(!constraint->negationHasProof());
 
-  if(constraint->assertedToTheTheory()){
-    //Do nothing
+  if(inConflict){
+    ConstraintP negation = constraint->getNegation();
+    if(Debug.isOn("arith::negatedassumption") && negation->isAssumption()){
+      debugPrintFacts();
+    }
+    Debug("arith::eq") << "negation has proof" << endl;
+    Debug("arith::eq") << constraint << endl;
+    Debug("arith::eq") << negation << endl;
+    raiseConflict(negation);
     return NullConstraint;
   }else{
-    Debug("arith::constraint") << "arith constraint " << constraint << std::endl;
-    constraint->setAssertedToTheTheory(assertion);
-
-    if(!constraint->hasProof()){
-      Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
-      constraint->selfExplaining();
-    }else{
-      Debug("arith::constraint") << "already has proof: " << constraint->externalExplainByAssertions() << endl;
-    }
-
     return constraint;
   }
 }
@@ -1941,14 +1963,12 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){
     if(isInteger(x_i) && constraint->isStrictUpperBound()){
       ConstraintP floorConstraint = constraint->getFloor();
       if(!floorConstraint->isTrue()){
-        if(floorConstraint->negationHasProof()){
-          raiseConflict(constraint, floorConstraint->getNegation());
-          //Node conf = Constraint_::explainConflict(constraint, floorConstraint->getNegation());
-          //raiseConflict(conf);
+        bool inConflict = floorConstraint->negationHasProof();
+        floorConstraint->impliedByIntHole(constraint, inConflict);
+        floorConstraint->tryToPropagate();
+        if(inConflict){
+          raiseConflict(floorConstraint);
           return true;
-        }else{
-          floorConstraint->impliedBy(constraint);
-          // Do not need to add to d_learnedBounds
         }
       }
       return AssertUpper(floorConstraint);
@@ -1959,14 +1979,13 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){
     if(isInteger(x_i) && constraint->isStrictLowerBound()){
       ConstraintP ceilingConstraint = constraint->getCeiling();
       if(!ceilingConstraint->isTrue()){
-        if(ceilingConstraint->negationHasProof()){
-          raiseConflict(constraint, ceilingConstraint->getNegation());
-          //Node conf = Constraint_::explainConflict(constraint, ceilingConstraint->getNegation());
-          //raiseConflict(conf);
+        bool inConflict = ceilingConstraint->negationHasProof();
+        ceilingConstraint->impliedByIntHole(constraint, inConflict);
+        ceilingConstraint->tryToPropagate();
+        if(inConflict){
+          raiseConflict(ceilingConstraint);
           return true;
         }
-        ceilingConstraint->impliedBy(constraint);
-        // Do not need to add to learnedBounds
       }
       return AssertLower(ceilingConstraint);
     }else{
@@ -2027,21 +2046,75 @@ bool TheoryArithPrivate::hasIntegerModel(){
   }
 }
 
+
+Node flattenAndSort(Node n){
+  Kind k = n.getKind();
+  switch(k){
+  case kind::OR:
+  case kind::AND:
+  case kind::PLUS:
+  case kind::MULT:
+    break;
+  default:
+    return n;
+  }
+
+  std::vector<Node> out;
+  std::vector<Node> process;
+  process.push_back(n);
+  while(!process.empty()){
+    Node b = process.back();
+    process.pop_back();
+    if(b.getKind() == k){
+      for(Node::iterator i=b.begin(), end=b.end(); i!=end; ++i){
+        process.push_back(*i);
+      }
+    } else {
+      out.push_back(b);
+    }
+  }
+  Assert(out.size() >= 2);
+  std::sort(out.begin(), out.end());
+  return NodeManager::currentNM()->mkNode(k, out);
+}
+
+
+
 /** Outputs conflicts to the output channel. */
 void TheoryArithPrivate::outputConflicts(){
   Assert(anyConflict());
+  static unsigned int conflicts = 0;
+  
   if(!conflictQueueEmpty()){
     Assert(!d_conflicts.empty());
     for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){
-      const ConstraintCPVec& vec = d_conflicts[i];
-      Node conflict = Constraint_::externalExplainByAssertions(vec);
-      Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict << endl;
+      ConstraintCP confConstraint = d_conflicts[i];
+      Assert(confConstraint->inConflict());
+      Node conflict = confConstraint->externalExplainConflict();
+
+      ++conflicts;
+      Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict
+        //                               << "("<<conflicts<<")"
+                               << endl;
+      if(Debug.isOn("arith::normalize::external")){
+        conflict = flattenAndSort(conflict);
+        Debug("arith::conflict") << "(normalized to) " << conflict << endl;
+      }
+
       (d_containing.d_out)->conflict(conflict);
     }
   }
   if(!d_blackBoxConflict.get().isNull()){
     Node bb = d_blackBoxConflict.get();
-    Debug("arith::conflict") << "black box conflict" << bb << endl;
+    ++conflicts;
+    Debug("arith::conflict") << "black box conflict" << bb
+      //<< "("<<conflicts<<")"
+                             << endl;
+    if(Debug.isOn("arith::normalize::external")){
+      bb = flattenAndSort(bb);
+      Debug("arith::conflict") << "(normalized to) " << bb << endl;
+    }
+
     (d_containing.d_out)->conflict(bb);
   }
 }
@@ -2134,13 +2207,36 @@ bool TheoryArithPrivate::replayLog(ApproximateSimplex* approx){
     turnOffApproxFor(options::replayNumericFailurePenalty());
   }
 
-  for(size_t i =0, N = res.size(); i < N; ++i){
-    raiseConflict(res[i]);
-  }
+
+  
   if(res.empty()){
     ++d_statistics.d_replayAttemptFailed;
   }else{
-    ++d_statistics.d_mipProofsSuccessful;
+    unsigned successes = 0;
+    for(size_t i =0, N = res.size(); i < N; ++i){
+      ConstraintCPVec& vec = res[i];
+      Assert(vec.size() >= 2);
+      for(size_t j=0, M = vec.size(); j < M; ++j){
+        ConstraintCP at_j = vec[j];
+        Assert(at_j->isTrue());
+        if(!at_j->negationHasProof()){
+          successes++;
+          vec[j] = vec.back();
+          vec.pop_back();
+          ConstraintP neg_at_j = at_j->getNegation();
+
+          Debug("approx::replayLog") << "Setting the proof for the replayLog conflict on:" << endl
+                                     << "  (" << neg_at_j->isTrue() <<") " << neg_at_j << endl
+                                     << "  (" << at_j->isTrue() <<") " << at_j << endl;
+          neg_at_j->impliedByIntHole(vec, true);
+          raiseConflict(at_j);
+          break;
+        }
+      }
+    }
+    if(successes > 0){
+      ++d_statistics.d_mipProofsSuccessful;
+    }
   }
 
   if(d_currentPropagationList.size() > enteringPropN){
@@ -2260,6 +2356,25 @@ Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum){
   return safeConstructNary(nb);
 }
 
+ConstraintCP TheoryArithPrivate::vectorToIntHoleConflict(const ConstraintCPVec& conflict){
+  Assert(conflict.size() >= 2);
+  ConstraintCPVec exp(conflict.begin(), conflict.end()-1);
+  ConstraintCP back = conflict.back();
+  ConstraintP negBack = back->getNegation();
+  negBack->impliedByIntHole(exp, true);
+  return back;
+}
+
+void TheoryArithPrivate::intHoleConflictToVector(ConstraintCP conflicting, ConstraintCPVec& conflict){
+  ConstraintCP negConflicting = conflicting->getNegation();
+  Assert(conflicting->hasProof());
+  Assert(negConflicting->hasProof());
+
+  conflict.push_back(conflicting);
+  conflict.push_back(negConflicting);
+
+  Constraint::assertionFringe(conflict);
+}
 
 void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, BranchCutInfo& bci){
   Assert(conflictQueueEmpty());
@@ -2298,9 +2413,23 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc
       d_partialModel.startQueueingBoundCounts();
     }
     for(size_t i = 0, N = d_conflicts.size(); i < N; ++i){
-      conflicts.push_back(d_conflicts[i]);
-      // remove the floor/ceiling contraint implied by bcneg
-      Constraint_::assertionFringe(conflicts.back());
+
+      conflicts.push_back(ConstraintCPVec());
+      intHoleConflictToVector(d_conflicts[i], conflicts.back());
+      Constraint::assertionFringe(conflicts.back());
+        
+      // ConstraintCP conflicting = d_conflicts[i];
+      // ConstraintCP negConflicting = conflicting->getNegation();
+      // Assert(conflicting->hasProof());
+      // Assert(negConflicting->hasProof());
+
+      // conflicts.push_back(ConstraintCPVec());
+      // ConstraintCPVec& back = conflicts.back();
+      // back.push_back(conflicting);
+      // back.push_back(negConflicting);
+      
+      // // remove the floor/ceiling contraint implied by bcneg
+      // Constraint::assertionFringe(back);
     }
 
     if(Debug.isOn("approx::branch")){
@@ -2317,7 +2446,8 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc
     // make sure to be working on the assertion fringe!
     if(!contains(conf, bcneg)){
       Debug("approx::branch") << "reraise " << conf  << endl;
-      raiseConflict(conf);
+      ConstraintCP conflicting = vectorToIntHoleConflict(conf);
+      raiseConflict(conflicting);
     }else if(!bci.proven()){
       drop(conf, bcneg);
       bci.setExplanation(conf);
@@ -2328,87 +2458,24 @@ void TheoryArithPrivate::tryBranchCut(ApproximateSimplex* approx, int nid, Branc
 
 void TheoryArithPrivate::replayAssert(ConstraintP c) {
   if(!c->assertedToTheTheory()){
-    if(c->negationHasProof()){
-      ConstraintP neg = c->getNegation();
-      raiseConflict(c, neg);
-      Debug("approx::replayAssert") << "replayAssertion conflict " << neg << " : " << c << endl;
-    }else if(!c->hasProof()){
-      c->setInternalDecision();
-      assertionCases(c);
+    bool inConflict = c->negationHasProof();
+    if(!c->hasProof()){
+      c->setInternalAssumption(inConflict);
       Debug("approx::replayAssert") << "replayAssert " << c << " set internal" << endl;
     }else{
-      assertionCases(c);
       Debug("approx::replayAssert") << "replayAssert " << c << " has explanation" << endl;
     }
+    Debug("approx::replayAssert") << "replayAssertion " << c << endl;    
+    if(inConflict){
+      raiseConflict(c);
+    }else{
+      assertionCases(c);
+    }
   }else{
-    Debug("approx::replayAssert") << "replayAssert " << c << " already asserted" << endl;
+    Debug("approx::replayAssert") << "replayAssert " << c << " already asserted" << endl;    
   }
 }
 
-// ConstraintCPVec TheoryArithPrivate::toExplanation(Node n) const {
-//   ConstraintCPVec res;
-//   cout << "toExplanation" << endl;
-//   if(n.getKind() == kind::AND){
-//     for(unsigned i = 0; i < n.getNumChildren(); ++i){
-//       ConstraintP c = d_constraintDatabase.lookup(n[i]);
-//       if(c == NullConstraint){ return std::vector<Constraint>(); }
-//       res.push_back(c);
-//       cout << "\t"<<c << endl;
-//     }
-//   }else{
-//     ConstraintP c = d_constraintDatabase.lookup(n);
-//     if(c == NullConstraint){ return std::vector<Constraint>(); }
-//     res.push_back(c);
-//   }
-//   return res;
-// }
-
-// void TheoryArithPrivate::enqueueConstraints(std::vector<Constraint>& out, Node n) const{
-//   if(n.getKind() == kind::AND){
-//     for(unsigned i = 0, N = n.getNumChildren(); i < N; ++i){
-//       enqueueConstraints(out, n[i]);
-//     }
-//   }else{
-//     ConstraintP c = d_constraintDatabase.lookup(n);
-//     if(c == NullConstraint){
-//       cout << "failing on " << n << endl;
-//     }
-//     Assert(c != NullConstraint);
-//     out.push_back(c);
-//   }
-// }
-
-// ConstraintCPVec TheoryArithPrivate::resolveOutPropagated(const ConstraintCPVec& v, const std::set<ConstraintCP>& propagated) const {
-//   cout << "resolveOutPropagated()" << conf << endl;
-//   std::set<ConstraintCP> final;
-//   std::set<ConstraintCP> processed;
-//   std::vector<ConstraintCP> to_process;
-//   enqueueConstraints(to_process, conf);
-//   while(!to_process.empty()){
-//     ConstraintP c = to_process.back(); to_process.pop_back();
-//     if(processed.find(c) != processed.end()){
-//       continue;
-//     }else{
-//       if(propagated.find(c) == propagated.end()){
-//         final.insert(c);
-//       }else{
-//         Node exp = c->explainForPropagation();
-//         enqueueConstraints(to_process, exp);
-//       }
-//       processed.insert(c);
-//     }
-//   }
-//   cout << "final size: " << final.size() << std::endl;
-//   NodeBuilder<> nb(kind::AND);
-//   std::set<Constraint>::const_iterator iter = final.begin(), end = final.end();
-//   for(; iter != end; ++iter){
-//     ConstraintP c = *iter;
-//     c->explainForConflict(nb);
-//   }
-//   Node newConf = safeConstructNary(nb);
-//   cout << "resolveOutPropagated("<<conf<<", ...) ->" << newConf << endl;
-//   return newConf;
-// }
 
 void TheoryArithPrivate::resolveOutPropagated(std::vector<ConstraintCPVec>& confs, const std::set<ConstraintCP>& propagated) const {
   Debug("arith::resolveOutPropagated")
@@ -2416,7 +2483,7 @@ void TheoryArithPrivate::resolveOutPropagated(std::vector<ConstraintCPVec>& conf
   for(size_t i =0, N = confs.size(); i < N; ++i){
     ConstraintCPVec& conf = confs[i];
     size_t orig = conf.size();
-    Constraint_::assertionFringe(conf);
+    Constraint::assertionFringe(conf);
     Debug("arith::resolveOutPropagated")
       << "  conf["<<i<<"] " << orig << " to " << conf.size() << endl;
   }
@@ -2541,7 +2608,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
             if(con->isTrue()){
               Debug("approx::replayLogRec") << "not asserted?" << endl;
             }else{
-              con->impliedBy(exp);
+              con->impliedByIntHole(exp, false);
               replayAssert(con);
               Debug("approx::replayLogRec") << "cut prop" << endl;
             }
@@ -2580,7 +2647,8 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
     if(!conflictQueueEmpty()){
       /* if a conflict has been found stop */
       for(size_t i = 0, N = d_conflicts.size(); i < N; ++i){
-        res.push_back(d_conflicts[i]);
+        res.push_back(ConstraintCPVec());
+        intHoleConflictToVector(d_conflicts[i], res.back());
       }
       ++d_statistics.d_replayLogRecEarlyExit;
     }else if(nl.isBranch()){
@@ -2818,7 +2886,7 @@ bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){
       Node cutConstraint = cutToLiteral(approx, *cut);
       if(!cutConstraint.isNull()){
         const ConstraintCPVec& exp = cut->getExplanation();
-        Node asLemma = Constraint_::externalExplainByAssertions(exp);
+        Node asLemma = Constraint::externalExplainByAssertions(exp);
 
         Node implied = Rewriter::rewrite(cutConstraint);
         anythingnew = anythingnew || !isSatLiteral(implied);
@@ -3113,9 +3181,20 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
 
   bool useApprox = options::useApprox() && ApproximateSimplex::enabled() && getSolveIntegerResource();
 
+  Debug("TheoryArithPrivate::solveRealRelaxation")
+    << "solveRealRelaxation() approx"
+    << " " <<  options::useApprox()
+    << " " << ApproximateSimplex::enabled()
+    << " " << useApprox
+    << " " << safeToCallApprox()
+    << endl;
+  
   bool noPivotLimitPass1 = noPivotLimit && !useApprox;
   d_qflraStatus = simplex.findModel(noPivotLimitPass1);
 
+  Debug("TheoryArithPrivate::solveRealRelaxation")
+    << "solveRealRelaxation()" << " pass1 " << d_qflraStatus << endl;
+  
   if(d_qflraStatus == Result::SAT_UNKNOWN && useApprox && safeToCallApprox()){
     // pass2: fancy-final
     static const int32_t relaxationLimit = 10000;
@@ -3484,21 +3563,15 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
     break;
   case Result::UNSAT:
     d_unknownsInARow = 0;
-    if(false && previous == Result::SAT){
-      ++d_statistics.d_revertsOnConflicts;
-      Debug("arith::bt") << "clearing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
-      revertOutOfConflict();
-      d_errorSet.clear();
-    }else{
-      ++d_statistics.d_commitsOnConflicts;
 
-      Debug("arith::bt") << "committing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
-      d_partialModel.commitAssignmentChanges();
-      revertOutOfConflict();
+    ++d_statistics.d_commitsOnConflicts;
 
-      if(Debug.isOn("arith::consistency::comitonconflict")){
-        entireStateIsConsistent("commit on conflict");
-      }
+    Debug("arith::bt") << "committing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus  << endl;
+    d_partialModel.commitAssignmentChanges();
+    revertOutOfConflict();
+
+    if(Debug.isOn("arith::consistency::comitonconflict")){
+      entireStateIsConsistent("commit on conflict");
     }
     outputConflicts();
     emmittedConflictOrSplit = true;
@@ -3623,7 +3696,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
       if(possibleConflict != Node::null()){
         revertOutOfConflict();
         Debug("arith::conflict") << "dio conflict   " << possibleConflict << endl;
-        blackBoxConflict(possibleConflict);
+        raiseBlackBoxConflict(possibleConflict);
         outputConflicts();
         emmittedConflictOrSplit = true;
       }
@@ -3768,9 +3841,9 @@ bool TheoryArithPrivate::splitDisequalities(){
     d_diseqQueue.pop();
 
     if(front->isSplit()){
-      Debug("eq") << "split already" << endl;
+      Debug("arith::eq") << "split already" << endl;
     }else{
-      Debug("eq") << "not split already" << endl;
+      Debug("arith::eq") << "not split already" << endl;
 
       ArithVar lhsVar = front->getVariable();
 
@@ -3788,11 +3861,11 @@ bool TheoryArithPrivate::splitDisequalities(){
         //cout << "Now " << Rewriter::rewrite(lemma) << endl;
         splitSomething = true;
       }else if(d_partialModel.strictlyLessThanLowerBound(lhsVar, rhsValue)){
-        Debug("eq") << "can drop as less than lb" << front << endl;
+        Debug("arith::eq") << "can drop as less than lb" << front << endl;
       }else if(d_partialModel.strictlyGreaterThanUpperBound(lhsVar, rhsValue)){
-        Debug("eq") << "can drop as greater than ub" << front << endl;
+        Debug("arith::eq") << "can drop as greater than ub" << front << endl;
       }else{
-        Debug("eq") << "save" << front << ": " <<lhsValue << " != " << rhsValue << endl;
+        Debug("arith::eq") << "save" << front << ": " <<lhsValue << " != " << rhsValue << endl;
         save.push_back(front);
       }
     }
@@ -3852,13 +3925,13 @@ Node TheoryArithPrivate::explain(TNode n) {
 
   ConstraintP c = d_constraintDatabase.lookup(n);
   if(c != NullConstraint){
-    Assert(!c->isSelfExplaining());
+    Assert(!c->isAssumption());
     Node exp = c->externalExplainForPropagation();
     Debug("arith::explain") << "constraint explanation" << n << ":" << exp << endl;
     return exp;
   }else if(d_assertionsThatDoNotMatchTheirLiterals.find(n) != d_assertionsThatDoNotMatchTheirLiterals.end()){
     c = d_assertionsThatDoNotMatchTheirLiterals[n];
-    if(!c->isSelfExplaining()){
+    if(!c->isAssumption()){
       Node exp = c->externalExplainForPropagation();
       Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl;
       return exp;
@@ -3930,7 +4003,7 @@ void TheoryArithPrivate::propagate(Theory::Effort e) {
         normalized[0] : normalized.notNode();
       Node lp = flattenAnd(exp.andNode(notNormalized));
       Debug("arith::prop") << "propagate conflict" <<  lp << endl;
-      blackBoxConflict(lp);
+      raiseBlackBoxConflict(lp);
       outputConflicts();
       return;
     }else{
@@ -4562,6 +4635,7 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b
 
     ConstraintP implied = d_constraintDatabase.getBestImpliedBound(v, t, bound);
     if(implied != NullConstraint){
+      
       return rowImplicationCanBeApplied(ridx, rowUp, implied);
     }
   }
@@ -4606,21 +4680,22 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
                        << " " << hasProof
                        << endl;
 
-  if(implied->negationHasProof()){
-    Warning() << "the negation of " <<  implied << " : " << endl
-              << "has proof " << implied->getNegation() << endl
-              << implied->getNegation()->externalExplainByAssertions() << endl;
-  }
 
-  if(!assertedToTheTheory && canBePropagated && !hasProof ){
+  if( !assertedToTheTheory && canBePropagated && !hasProof ){
     ConstraintCPVec explain;
-    d_linEq.propagateRow(explain, ridx, rowUp, implied);
+
+    PROOF(d_farkasBuffer.clear());
+    RationalVectorP coeffs = NULLPROOF(&d_farkasBuffer);
+ 
+    d_linEq.propagateRow(explain, ridx, rowUp, implied, coeffs);
     if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){
       Node implication = implied->externalImplication(explain);
       Node clause = flattenImplication(implication);
       outputLemma(clause);
     }else{
-      implied->impliedBy(explain);
+      Assert(!implied->negationHasProof());
+      implied->impliedByFarkas(explain, coeffs, false);
+      implied->tryToPropagate();
     }
     return true;
   }
@@ -4636,8 +4711,8 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
 
 double fRand(double fMin, double fMax)
 {
-    double f = (double)rand() / RAND_MAX;
-    return fMin + f * (fMax - fMin);
+  double f = (double)rand() / RAND_MAX;
+  return fMin + f * (fMax - fMin);
 }
 
 bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index ff89945b8..4c539c60d 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -119,8 +119,6 @@ private:
 
   BoundInfoMap d_rowTracking;
 
-  ConstraintCPVec d_conflictBuffer;
-
   /**
    * The constraint database associated with the theory.
    * This must be declared before ArithPartialModel.
@@ -327,21 +325,27 @@ private:
 
 
   /** This is only used by simplex at the moment. */
-  context::CDList<ConstraintCPVec> d_conflicts;
+  context::CDList<ConstraintCP> d_conflicts;
+
+  /** This is only used by simplex at the moment. */
   context::CDO<Node> d_blackBoxConflict;
 public:
-  inline void raiseConflict(const ConstraintCPVec& cv){
-    d_conflicts.push_back(cv);
-  }
 
-  void raiseConflict(ConstraintCP a, ConstraintCP b);
-  void raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c);
+  /**
+   * This adds the constraint a to the queue of conflicts in d_conflicts.
+   * Both a and ~a must have a proof.
+   */
+  void raiseConflict(ConstraintCP a);
 
-  inline void blackBoxConflict(Node bb){
-    if(d_blackBoxConflict.get().isNull()){
-      d_blackBoxConflict = bb;
-    }
-  }
+  // inline void raiseConflict(const ConstraintCPVec& cv){
+  //   d_conflicts.push_back(cv);
+  // }
+  
+  // void raiseConflict(ConstraintCP a, ConstraintCP b);
+  // void raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c);
+
+  /** This is a conflict that is magically known to hold. */
+  void raiseBlackBoxConflict(Node bb);
 
 private:
 
@@ -356,7 +360,7 @@ private:
 
   /**
    * Outputs the contents of d_conflicts onto d_out.
-   * Must be inConflict().
+   * The conditions of anyConflict() must hold.
    */
   void outputConflicts();
 
@@ -717,8 +721,10 @@ private:
   std::pair<ConstraintP, ArithVar> replayGetConstraint(const DenseMap<Rational>& lhs, Kind k, const Rational& rhs, bool branch);
 
   void replayAssert(ConstraintP c);
-  //ConstConstraintVec toExplanation(Node n) const;
 
+  static ConstraintCP vectorToIntHoleConflict(const ConstraintCPVec& conflict);
+  static void intHoleConflictToVector(ConstraintCP conflicting, ConstraintCPVec& conflict);
+  
   // Returns true if the node contains a literal
   // that is an arithmetic literal and is not a sat literal
   // No caching is done so this should likely only
@@ -730,6 +736,8 @@ private:
 
   uint32_t d_solveIntMaybeHelp, d_solveIntAttempts;
 
+  RationalVector d_farkasBuffer;
+
   /** These fields are designed to be accessible to TheoryArith methods. */
   class Statistics {
   public: