Merge branch 'master' into fixBiasfixBias

7 files changed, 862 insertions, 338 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 6fa7eadeb..e6ff02f10 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -917,6 +917,7 @@ void CvcPrinter::toStream(
     case kind::STRING_LENGTH:
       out << "LENGTH";
       break;
+    case kind::STRING_SUBSTR: out << "SUBSTR"; break;
 
     default:
       Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl;
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 1d51f99e1..0d2bb5be0 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -19,10 +19,14 @@
 #include <memory>
 #include <stack>
 
+#include "expr/node.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
+#include "theory/arith/constraint_forward.h"
 #include "theory/arith/theory_arith.h"
 
+#define CVC4_ARITH_VAR_TERM_PREFIX "term."
+
 namespace CVC4 {
 
 inline static Node eqNode(TNode n1, TNode n2) {
@@ -674,151 +678,169 @@ void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM
   // !d_realMode <--> term.getType().isInteger()
 
   Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARITH);
-  switch (term.getKind()) {
+  switch (term.getKind())
+  {
+    case kind::CONST_RATIONAL:
+    {
+      Assert(term.getNumChildren() == 0);
+      Assert(term.getType().isInteger() || term.getType().isReal());
 
-  case kind::CONST_RATIONAL: {
-    Assert (term.getNumChildren() == 0);
-    Assert (term.getType().isInteger() || term.getType().isReal());
+      const Rational& r = term.getConst<Rational>();
+      bool neg = (r < 0);
 
-    const Rational& r = term.getConst<Rational>();
-    bool neg = (r < 0);
+      os << (!d_realMode ? "(a_int " : "(a_real ");
 
-    os << (!d_realMode ? "(a_int " : "(a_real ");
+      if (neg)
+      {
+        os << "(~ ";
+      }
 
-    if (neg) {
-      os << "(~ ";
-    }
+      if (!d_realMode)
+      {
+        os << r.abs();
+      }
+      else
+      {
+        printRational(os, r.abs());
+      }
 
-    if (!d_realMode) {
-      os << r.abs();
-    } else {
-      os << r.abs().getNumerator();
-      os << "/";
-      os << r.getDenominator();
+      if (neg)
+      {
+        os << ") ";
+      }
+
+      os << ") ";
+      return;
     }
 
-    if (neg) {
+    case kind::UMINUS:
+    {
+      Assert(term.getNumChildren() == 1);
+      Assert(term.getType().isInteger() || term.getType().isReal());
+      os << (!d_realMode ? "(u-_Int " : "(u-_Real ");
+      d_proofEngine->printBoundTerm(term[0], os, map);
       os << ") ";
+      return;
     }
 
-    os << ") ";
-    return;
-  }
+    case kind::PLUS:
+    {
+      Assert(term.getNumChildren() >= 2);
 
-  case kind::UMINUS: {
-    Assert (term.getNumChildren() == 1);
-    Assert (term.getType().isInteger() || term.getType().isReal());
-    os << (!d_realMode ? "(u-_Int " : "(u-_Real ");
-    d_proofEngine->printBoundTerm(term[0], os, map);
-    os << ") ";
-    return;
-  }
+      std::stringstream paren;
+      for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
+      {
+        os << (!d_realMode ? "(+_Int " : "(+_Real ");
+        d_proofEngine->printBoundTerm(term[i], os, map);
+        os << " ";
+        paren << ") ";
+      }
 
-  case kind::PLUS: {
-    Assert (term.getNumChildren() >= 2);
+      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
+      os << paren.str();
+      return;
+    }
 
-    std::stringstream paren;
-    for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
-      os << (!d_realMode ? "(+_Int " : "(+_Real ");
-      d_proofEngine->printBoundTerm(term[i], os, map);
-      os << " ";
-      paren << ") ";
+    case kind::MINUS:
+    {
+      Assert(term.getNumChildren() >= 2);
+
+      std::stringstream paren;
+      for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
+      {
+        os << (!d_realMode ? "(-_Int " : "(-_Real ");
+        d_proofEngine->printBoundTerm(term[i], os, map);
+        os << " ";
+        paren << ") ";
+      }
+
+      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
+      os << paren.str();
+      return;
     }
 
-    d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
-    os << paren.str();
-    return;
-  }
+    case kind::MULT:
+    {
+      Assert(term.getNumChildren() >= 2);
 
-  case kind::MINUS: {
-    Assert (term.getNumChildren() >= 2);
+      std::stringstream paren;
+      for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
+      {
+        os << (!d_realMode ? "(*_Int " : "(*_Real ");
+        d_proofEngine->printBoundTerm(term[i], os, map);
+        os << " ";
+        paren << ") ";
+      }
 
-    std::stringstream paren;
-    for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
-      os << (!d_realMode ? "(-_Int " : "(-_Real ");
-      d_proofEngine->printBoundTerm(term[i], os, map);
-      os << " ";
-      paren << ") ";
+      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
+      os << paren.str();
+      return;
     }
 
-    d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
-    os << paren.str();
-    return;
-  }
+    case kind::DIVISION:
+    case kind::DIVISION_TOTAL:
+    {
+      Assert(term.getNumChildren() >= 2);
 
-  case kind::MULT: {
-    Assert (term.getNumChildren() >= 2);
+      std::stringstream paren;
+      for (unsigned i = 0; i < term.getNumChildren() - 1; ++i)
+      {
+        os << (!d_realMode ? "(/_Int " : "(/_Real ");
+        d_proofEngine->printBoundTerm(term[i], os, map);
+        os << " ";
+        paren << ") ";
+      }
 
-    std::stringstream paren;
-    for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
-      os << (!d_realMode ? "(*_Int " : "(*_Real ");
-      d_proofEngine->printBoundTerm(term[i], os, map);
-      os << " ";
-      paren << ") ";
+      d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
+      os << paren.str();
+      return;
     }
 
-    d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
-    os << paren.str();
-    return;
-  }
+    case kind::GT:
+      Assert(term.getNumChildren() == 2);
+      os << (!d_realMode ? "(>_Int " : "(>_Real ");
+      d_proofEngine->printBoundTerm(term[0], os, map);
+      os << " ";
+      d_proofEngine->printBoundTerm(term[1], os, map);
+      os << ") ";
+      return;
 
-  case kind::DIVISION:
-  case kind::DIVISION_TOTAL: {
-    Assert (term.getNumChildren() >= 2);
+    case kind::GEQ:
+      Assert(term.getNumChildren() == 2);
+      os << (!d_realMode ? "(>=_Int " : "(>=_Real ");
+      d_proofEngine->printBoundTerm(term[0], os, map);
+      os << " ";
+      d_proofEngine->printBoundTerm(term[1], os, map);
+      os << ") ";
+      return;
 
-    std::stringstream paren;
-    for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
-      os << (!d_realMode ? "(/_Int " : "(/_Real ");
-      d_proofEngine->printBoundTerm(term[i], os, map);
+    case kind::LT:
+      Assert(term.getNumChildren() == 2);
+      os << (!d_realMode ? "(<_Int " : "(<_Real ");
+      d_proofEngine->printBoundTerm(term[0], os, map);
       os << " ";
-      paren << ") ";
-    }
+      d_proofEngine->printBoundTerm(term[1], os, map);
+      os << ") ";
+      return;
 
-    d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
-    os << paren.str();
-    return;
-  }
+    case kind::LEQ:
+      Assert(term.getNumChildren() == 2);
+      os << (!d_realMode ? "(<=_Int " : "(<=_Real ");
+      d_proofEngine->printBoundTerm(term[0], os, map);
+      os << " ";
+      d_proofEngine->printBoundTerm(term[1], os, map);
+      os << ") ";
+      return;
 
-  case kind::GT:
-    Assert (term.getNumChildren() == 2);
-    os << (!d_realMode ? "(>_Int " : "(>_Real ");
-    d_proofEngine->printBoundTerm(term[0], os, map);
-    os << " ";
-    d_proofEngine->printBoundTerm(term[1], os, map);
-    os << ") ";
-    return;
-
-  case kind::GEQ:
-    Assert (term.getNumChildren() == 2);
-    os << (!d_realMode ? "(>=_Int " : "(>=_Real ");
-    d_proofEngine->printBoundTerm(term[0], os, map);
-    os << " ";
-    d_proofEngine->printBoundTerm(term[1], os, map);
-    os << ") ";
-    return;
-
-  case kind::LT:
-    Assert (term.getNumChildren() == 2);
-    os << (!d_realMode ? "(<_Int " : "(<_Real ");
-    d_proofEngine->printBoundTerm(term[0], os, map);
-    os << " ";
-    d_proofEngine->printBoundTerm(term[1], os, map);
-    os << ") ";
-    return;
-
-  case kind::LEQ:
-    Assert (term.getNumChildren() == 2);
-    os << (!d_realMode ? "(<=_Int " : "(<=_Real ");
-    d_proofEngine->printBoundTerm(term[0], os, map);
-    os << " ";
-    d_proofEngine->printBoundTerm(term[1], os, map);
-    os << ") ";
-    return;
+    case kind::VARIABLE:
+    case kind::SKOLEM:
+      os << CVC4_ARITH_VAR_TERM_PREFIX << ProofManager::sanitize(term);
+      return;
 
-  default:
-    Debug("pf::arith") << "Default printing of term: " << term << std::endl;
-    os << term;
-    return;
+    default:
+      Debug("pf::arith") << "Default printing of term: " << term << std::endl;
+      os << term;
+      return;
   }
 }
 
@@ -833,26 +855,327 @@ void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) {
   }
 }
 
-void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
-  os << " ;; Arith Theory Lemma \n;;";
-  for (unsigned i = 0; i < lemma.size(); ++i) {
-    os << lemma[i] <<" ";
+void LFSCArithProof::printRational(std::ostream& o, const Rational& r)
+{
+  if (r.sgn() < 0)
+  {
+    o << "(~ " << r.getNumerator().abs() << "/" << r.getDenominator().abs()
+      << ")";
+  }
+  else
+  {
+    o << r.getNumerator() << "/" << r.getDenominator();
+  }
+}
+
+void LFSCArithProof::printLinearPolynomialNormalizer(std::ostream& o,
+                                                     const Node& n)
+{
+  switch (n.getKind())
+  {
+    case kind::PLUS:
+    {
+      // Since our axioms are binary, but n may be n-ary, we rig up
+      // a right-associative tree.
+      size_t nchildren = n.getNumChildren();
+      for (size_t i = 0; i < nchildren; ++i)
+      {
+        if (i < nchildren - 1)
+        {
+          o << "\n      (pn_+ _ _ _ _ _ ";
+        }
+        printLinearMonomialNormalizer(o, n[i]);
+      }
+      std::fill_n(std::ostream_iterator<char>(o), nchildren - 1, ')');
+      break;
+    }
+    case kind::MULT:
+    case kind::VARIABLE:
+    case kind::CONST_RATIONAL:
+    case kind::SKOLEM:
+    {
+      printLinearMonomialNormalizer(o, n);
+      break;
+    }
+    default:
+#ifdef CVC4_ASSERTIONS
+      std::ostringstream msg;
+      msg << "Invalid operation " << n.getKind() << " in linear polynomial";
+      Unreachable(msg.str().c_str());
+#endif  // CVC4_ASSERTIONS
+      break;
+  }
+}
+
+void LFSCArithProof::printLinearMonomialNormalizer(std::ostream& o,
+                                                   const Node& n)
+{
+  switch (n.getKind())
+  {
+    case kind::MULT: {
+#ifdef CVC4_ASSERTIONS
+      std::ostringstream s;
+      s << "node " << n << " is not a linear monomial";
+      s << " " << n[0].getKind() << " " << n[1].getKind();
+      Assert((n[0].getKind() == kind::CONST_RATIONAL
+              && (n[1].getKind() == kind::VARIABLE
+                  || n[1].getKind() == kind::SKOLEM)),
+             s.str().c_str());
+#endif  // CVC4_ASSERTIONS
+
+      o << "\n        (pn_mul_c_L _ _ _ ";
+      printConstRational(o, n[0]);
+      o << " ";
+      printVariableNormalizer(o, n[1]);
+      o << ")";
+      break;
+    }
+    case kind::CONST_RATIONAL:
+    {
+      o << "\n        (pn_const ";
+      printConstRational(o, n);
+      o << ")";
+      break;
+    }
+    case kind::VARIABLE:
+    case kind::SKOLEM:
+    {
+      o << "\n        ";
+      printVariableNormalizer(o, n);
+      break;
+    }
+    default:
+#ifdef CVC4_ASSERTIONS
+      std::ostringstream msg;
+      msg << "Invalid operation " << n.getKind() << " in linear monomial";
+      Unreachable(msg.str().c_str());
+#endif  // CVC4_ASSERTIONS
+      break;
+  }
+}
+
+void LFSCArithProof::printConstRational(std::ostream& o, const Node& n)
+{
+  Assert(n.getKind() == kind::CONST_RATIONAL);
+  const Rational value = n.getConst<Rational>();
+  printRational(o, value);
+}
+
+void LFSCArithProof::printVariableNormalizer(std::ostream& o, const Node& n)
+{
+  std::ostringstream msg;
+  msg << "Invalid variable kind " << n.getKind() << " in linear monomial";
+  Assert(n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM,
+         msg.str().c_str());
+  o << "(pn_var " << n << ")";
+}
+
+void LFSCArithProof::printLinearPolynomialPredicateNormalizer(std::ostream& o,
+                                                              const Node& n)
+{
+  Assert(n.getKind() == kind::GEQ,
+         "can only print normalization witnesses for (>=) nodes");
+  Assert(n[1].getKind() == kind::CONST_RATIONAL);
+  o << "(poly_formula_norm_>= _ _ _ ";
+  o << "\n    (pn_- _ _ _ _ _ ";
+  printLinearPolynomialNormalizer(o, n[0]);
+  o << "\n      (pn_const ";
+  printConstRational(o, n[1]);
+  o << ")))";
+}
+
+void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
+                                           std::ostream& os,
+                                           std::ostream& paren,
+                                           const ProofLetMap& map)
+{
+  Debug("pf::arith") << "Printing proof for lemma " << lemma << std::endl;
+  // Prefixes for the names of linearity witnesses
+  const char* linearityWitnessPrefix = "lp";
+  const char* linearizedProofPrefix = "pf_lp";
+  std::ostringstream lemmaParen;
+
+  // Construct the set of conflicting literals
+  std::set<Node> conflictSet;
+  std::transform(lemma.begin(),
+                 lemma.end(),
+                 std::inserter(conflictSet, conflictSet.begin()),
+                 [](const Expr& e) {
+                   return NodeManager::currentNM()->fromExpr(e).negate();
+                 });
+
+  // If we have Farkas coefficients stored for this lemma, use them to write a
+  // proof. Otherwise, just `trust` the lemma.
+  if (d_recorder.hasFarkasCoefficients(conflictSet))
+  {
+    // Get farkas coefficients & literal order
+    const auto& farkasInfo = d_recorder.getFarkasCoefficients(conflictSet);
+    const Node& conflict = farkasInfo.first;
+    theory::arith::RationalVectorCP farkasCoefficients = farkasInfo.second;
+    Assert(farkasCoefficients != theory::arith::RationalVectorCPSentinel);
+    Assert(conflict.getNumChildren() == farkasCoefficients->size());
+    const size_t nAntecedents = conflict.getNumChildren();
+
+    // Print proof
+    os << "\n;; Farkas Proof" << std::endl;
+
+    // Construct witness that the literals are linear polynomials
+    os << ";  Linear Polynomial Normalization Witnesses" << std::endl;
+    for (size_t i = 0; i != nAntecedents; ++i)
+    {
+      const Node& antecedent = conflict[i];
+      const Rational farkasC = (*farkasCoefficients)[i];
+      os << "\n; " << antecedent << " w/ farkas c = " << farkasC << std::endl;
+      os << "  (@ "
+         << ProofManager::getLitName(antecedent.negate(),
+                                     linearityWitnessPrefix)
+         << " ";
+      const Node& nonneg =
+          antecedent.getKind() == kind::NOT ? antecedent[0] : antecedent;
+      printLinearPolynomialPredicateNormalizer(os, nonneg);
+      lemmaParen << ")";
+    }
+
+    // Prove linear polynomial constraints
+    os << "\n;  Linear Polynomial Proof Conversions";
+    for (size_t i = 0; i != nAntecedents; ++i)
+    {
+      const Node& antecedent = conflict[i];
+      os << "\n  (@ "
+         << ProofManager::getLitName(antecedent.negate(), linearizedProofPrefix)
+         << " ";
+      lemmaParen << ")";
+      switch (conflict[i].getKind())
+      {
+        case kind::NOT:
+        {
+          Assert(conflict[i][0].getKind() == kind::GEQ);
+          os << "(poly_flip_not_>= _ _ "
+             << "(poly_form_not _ _ "
+             << ProofManager::getLitName(antecedent.negate(),
+                                         linearityWitnessPrefix)
+             << " " << ProofManager::getLitName(antecedent.negate(), "")
+             << "))";
+          break;
+        }
+        case kind::GEQ:
+        {
+          os << "(poly_form _ _ "
+             << ProofManager::getLitName(antecedent.negate(),
+                                         linearityWitnessPrefix)
+             << " " << ProofManager::getLitName(antecedent.negate(), "") << ")";
+          break;
+        }
+        default: Unreachable();
+      }
+    }
+
+    /* Combine linear polynomial constraints to derive a contradiction.
+     *
+     * The linear polynomial constraints are refered to as **antecedents**,
+     * since they are antecedents to the contradiction.
+     *
+     * The structure of the combination is a tree
+     *
+     *   (=> <=)
+     *      |
+     *      +                   0
+     *     / \
+     *    *   +                 1
+     *       / \
+     *      *   +               2
+     *         / \
+     *        *  ...            i
+     *             \
+     *              +           n-1
+     *             / \
+     *            *   (0 >= 0)
+     *
+     * Where each * is a linearized antecedant being scaled by a farkas
+     * coefficient and each + is the sum of inequalities. The tricky bit is that
+     * each antecedent can be strict (>) or relaxed (>=) and the axiom used for
+     * each * and + depends on this... The axiom for * depends on the
+     * strictness of its linear polynomial input, and the axiom for + depends
+     * on the strictness of **both** its inputs. The contradiction axiom is
+     * also a function of the strictness of its input.
+     *
+     * There are n *s and +s and we precompute
+     *    1. The strictness of the ith antecedant  (`ith_antecedent_is_strict`)
+     *    2. The strictness of the right argument of the ith sum
+     * (`ith_acc_is_strict`)
+     *    3. The strictness of the final result (`strict_contradiction`)
+     *
+     * Precomupation is helpful since
+     *    the computation is post-order,
+     *    but printing is pre-order.
+     */
+    std::vector<bool> ith_antecedent_is_strict(nAntecedents, false);
+    std::vector<bool> ith_acc_is_strict(nAntecedents, false);
+    for (int i = nAntecedents - 1; i >= 0; --i)
+    {
+      ith_antecedent_is_strict[i] = conflict[i].getKind() == kind::NOT;
+      if (i == (int)nAntecedents - 1)
+      {
+        ith_acc_is_strict[i] = false;
+      }
+      else
+      {
+        ith_acc_is_strict[i] =
+            ith_acc_is_strict[i + 1] || ith_antecedent_is_strict[i + 1];
+      }
+    }
+    bool strict_contradiction =
+        ith_acc_is_strict[0] || ith_antecedent_is_strict[0];
+
+    // Now, print the proof
+    os << "\n;  Farkas Combination";
+    // Choose the appropriate contradiction axiom
+    os << "\n  (lra_contra_" << (strict_contradiction ? ">" : ">=") << " _ ";
+    for (size_t i = 0; i != nAntecedents; ++i)
+    {
+      const Node& lit = conflict[i];
+      const char* ante_op = ith_antecedent_is_strict[i] ? ">" : ">=";
+      const char* acc_op = ith_acc_is_strict[i] ? ">" : ">=";
+      os << "\n    (lra_add_" << ante_op << "_" << acc_op << " _ _ _ ";
+      os << "\n       (lra_mul_c_" << ante_op << " _ _ ";
+      printRational(os, (*farkasCoefficients)[i].abs());
+      os << " " << ProofManager::getLitName(lit.negate(), linearizedProofPrefix)
+         << ")"
+         << " ; " << lit;
+    }
+
+    // The basis, at least, is always the same...
+    os << "\n    (lra_axiom_>= 0/1)";
+    std::fill_n(std::ostream_iterator<char>(os),
+                nAntecedents,
+                ')');  // close lra_add_*_*
+    os << ")";         // close lra_contra_*
+
+    os << lemmaParen.str();  // close normalizers and proof-normalizers
+  }
+  else
+  {
+    os << "\n; Arithmetic proofs which use reasoning more complex than Farkas "
+          "proofs are currently unsupported\n(clausify_false trust)\n";
   }
-  os <<"\n";
-  //os << " (clausify_false trust)";
-  ArithProof::printTheoryLemmaProof(lemma, os, paren, map);
 }
 
 void LFSCArithProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
+  // Nothing to do here at this point.
 }
 
 void LFSCArithProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
-  for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) {
+  for (ExprSet::const_iterator it = d_declarations.begin();
+       it != d_declarations.end();
+       ++it)
+  {
     Expr term = *it;
     Assert(term.isVariable());
-    os << "(% " << ProofManager::sanitize(term) << " ";
-    os << "(term ";
-    os << term.getType() << ")\n";
+    os << "(% " << ProofManager::sanitize(term) << " var_real\n";
+    os << "(@ " << CVC4_ARITH_VAR_TERM_PREFIX << ProofManager::sanitize(term)
+       << " ";
+    os << "(a_var_real " << ProofManager::sanitize(term) << ")\n";
+    paren << ")";
     paren << ")";
   }
 }
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index a58294998..640d2db8d 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -64,7 +64,7 @@ protected:
   ExprSet d_declarations; // all the variable/function declarations
 
   /**
-   * @brief Where farkas proofs of lemmas are stored.
+   * Where farkas proofs of lemmas are stored.
    */
   proof::ArithProofRecorder d_recorder;
 
@@ -86,6 +86,76 @@ public:
                       std::ostream& os,
                       const ProofLetMap& map) override;
   void printOwnedSort(Type type, std::ostream& os) override;
+
+  /**
+   * Print a rational number in LFSC format.
+   *        e.g. 5/8 or (~ 1/1)
+   *
+   * @param o ostream to print to.
+   * @param r the rational to print
+   */
+  static void printRational(std::ostream& o, const Rational& r);
+
+  /**
+   * Print a value of type poly_formula_norm
+   *
+   * @param o ostream to print to
+   * @param n node (asserted to be of the form [linear polynomial >= constant])
+   */
+  static void printLinearPolynomialPredicateNormalizer(std::ostream& o,
+                                                       const Node& n);
+
+  /**
+   * Print a value of type poly_norm
+   *
+   * @param o ostream to print to
+   * @param n node (asserted to be a linear polynomial)
+   */
+  static void printLinearPolynomialNormalizer(std::ostream& o, const Node& n);
+
+  /**
+   * Print a value of type poly_norm
+   *
+   * @param o ostream to print to
+   * @param n node (asserted to be a linear monomial)
+   */
+  static void printLinearMonomialNormalizer(std::ostream& o, const Node& n);
+
+  /**
+   * Print a LFSC rational
+   *
+   * @param o ostream to print to
+   * @param n node (asserted to be a const rational)
+   */
+  static void printConstRational(std::ostream& o, const Node& n);
+
+  /**
+   * print the pn_var normalizer for n (type poly_norm)
+   *
+   * @param o the ostream to print to
+   * @param n the node to print (asserted to be a variable)
+   */
+  static void printVariableNormalizer(std::ostream& o, const Node& n);
+  /**
+   * print a proof of the lemma
+   *
+   * First, we print linearity witnesses, i.e. witnesses  that each literal has
+   * the form:
+   *   [linear polynomial] >= 0 OR
+   *   [linear polynomial] >  0
+   *
+   * Then we use those witnesses to prove that the above linearized constraints
+   * hold.
+   *
+   * Then we use the farkas coefficients to combine the literals into a
+   * variable-free contradiction. The literals may be a mix of strict and
+   * relaxed inequalities.
+   *
+   * @param lemma the set of literals disjoined in the lemma
+   * @param os stream to print the proof to
+   * @param paren global closing stream (unused)
+   * @param map let map (unused)
+   */
   void printTheoryLemmaProof(std::vector<Expr>& lemma,
                              std::ostream& os,
                              std::ostream& paren,
diff --git a/src/proof/arith_proof_recorder.cpp b/src/proof/arith_proof_recorder.cpp
index d654ea073..097fdb51e 100644
--- a/src/proof/arith_proof_recorder.cpp
+++ b/src/proof/arith_proof_recorder.cpp
@@ -30,17 +30,25 @@ ArithProofRecorder::ArithProofRecorder() : d_lemmasToFarkasCoefficients()
 void ArithProofRecorder::saveFarkasCoefficients(
     Node conflict, theory::arith::RationalVectorCP farkasCoefficients)
 {
+  // Verify that the conflict is a conjuction of (possibly negated) real bounds
+  // Verify that the conflict is a conjunciton ...
   Assert(conflict.getKind() == kind::AND);
   Assert(conflict.getNumChildren() == farkasCoefficients->size());
-  for (size_t i = 0; i < conflict.getNumChildren(); ++i)
+  for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren; ++i)
   {
     const Node& child = conflict[i];
-    Assert(child.getType().isBoolean() && child[0].getType().isReal());
+    // ... of possibly negated ...
+    const Node& nonNegativeChild =
+        child.getKind() == kind::NOT ? child[0] : child;
+    // ... real bounds
+    Assert(nonNegativeChild.getType().isBoolean()
+           && nonNegativeChild[0].getType().isReal());
   }
   Debug("pf::arith") << "Saved Farkas Coefficients:" << std::endl;
   if (Debug.isOn("pf::arith"))
   {
-    for (size_t i = 0; i < conflict.getNumChildren(); ++i)
+    for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren;
+         ++i)
     {
       const Node& child = conflict[i];
       const Rational& r = (*farkasCoefficients)[i];
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 352ba0f36..297e3de37 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -499,6 +499,35 @@ bool Constraint::hasFarkasProof() const {
   return getProofType() == FarkasAP;
 }
 
+bool Constraint::hasSimpleFarkasProof() const
+{
+  Debug("constraints::hsfp") << "hasSimpleFarkasProof " << this << std::endl;
+  if (!hasFarkasProof())
+  {
+    Debug("constraints::hsfp") << "There is no simple Farkas proof because "
+                                  "there is no farkas proof."
+                               << std::endl;
+    return false;
+  }
+  const ConstraintRule& rule = getConstraintRule();
+  AntecedentId antId = rule.d_antecedentEnd;
+  ConstraintCP antecdent = d_database->getAntecedent(antId);
+  while (antecdent != NullConstraint)
+  {
+    if (antecdent->getProofType() != AssumeAP)
+    {
+      Debug("constraints::hsfp") << "There is no simple Farkas proof b/c there "
+                                    "is an antecdent w/ rule ";
+      antecdent->getConstraintRule().print(Debug("constraints::hsfp"));
+      Debug("constraints::hsfp") << std::endl;
+      return false;
+    }
+    --antId;
+    antecdent = d_database->getAntecedent(antId);
+  }
+  return true;
+}
+
 bool Constraint::hasIntHoleProof() const {
   return getProofType() == IntHoleAP;
 }
@@ -568,8 +597,9 @@ void ConstraintRule::print(std::ostream& out) const {
   out << d_constraint << std::endl;
   out << "d_proofType= " << d_proofType << ", " << std::endl;
   out << "d_antecedentEnd= "<< d_antecedentEnd << std::endl;
-  
-  if(d_constraint != NullConstraint){
+
+  if (d_constraint != NullConstraint && d_antecedentEnd != AntecedentIdSentinel)
+  {
     const ConstraintDatabase& database = d_constraint->getDatabase();
     
     size_t coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffs->size()-1 : 0;
@@ -597,7 +627,7 @@ void ConstraintRule::print(std::ostream& out) const {
     out << " * (" << *(d_constraint->getNegation()) << ")";
     out << " [not d_constraint] " << endl;
   }
-  out << "}";  
+  out << "}";
 }
 
 bool Constraint::wellFormedFarkasProof() const {
@@ -1188,6 +1218,8 @@ void Constraint::impliedByIntHole(ConstraintCP a, bool nowInConflict){
   Assert(!hasProof());
   Assert(negationHasProof() == nowInConflict);
   Assert(a->hasProof());
+  Debug("pf::arith") << "impliedByIntHole(" << this << ", " << a << ")"
+                     << std::endl;
 
   d_database->d_antecedents.push_back(NullConstraint);
   d_database->d_antecedents.push_back(a);
@@ -1339,6 +1371,7 @@ Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){
 }
 
 Node Constraint::externalExplainConflict() const{
+  Debug("pf::arith") << this << std::endl;
   Assert(inConflict());
   NodeBuilder<> nb(kind::AND);
   externalExplainByAssertions(nb);
@@ -1407,6 +1440,13 @@ void Constraint::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{
   Assert(!isAssumption() || assertedToTheTheory());
   Assert(!isInternalAssumption());
 
+  if (Debug.isOn("pf::arith"))
+  {
+    Debug("pf::arith") << "Explaining: " << this << " with rule ";
+    getConstraintRule().print(Debug("pf::arith"));
+    Debug("pf::arith") << std::endl;
+  }
+
   if(assertedBefore(order)){
     nb << getWitness();
   }else if(hasEqualityEngineProof()){
@@ -1417,6 +1457,7 @@ void Constraint::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{
     ConstraintCP antecedent = d_database->d_antecedents[p];
 
     while(antecedent != NullConstraint){
+      Debug("pf::arith") << "Explain " << antecedent << std::endl;
       antecedent->externalExplain(nb, order);
       --p;
       antecedent = d_database->d_antecedents[p];
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index d411f2d34..51575bb2f 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -258,7 +258,7 @@ struct PerVariableDatabase{
 struct ConstraintRule {
   ConstraintP d_constraint;
   ArithProofType d_proofType;
-  AntecedentId d_antecedentEnd;    
+  AntecedentId d_antecedentEnd;
 
   /**
    * In this comment, we abbreviate ConstraintDatabase::d_antecedents
@@ -266,37 +266,38 @@ struct ConstraintRule {
    *
    * 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().
+   * 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])
+   * 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-n+(n-1)], ans[p-n+(n)]) 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.
+   * 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.
+   * 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.
+   * 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.
+   * We do however use all of the constraints by requiring non-zero
+   * coefficients.
    */
 #if IS_PROOFS_BUILD
   RationalVectorCP d_farkasCoefficients;
@@ -346,88 +347,10 @@ struct ConstraintRule {
 }; /* class ConstraintRule */
 
 class Constraint {
-private:
-  /** The ArithVar associated with the constraint. */
-  const ArithVar d_variable;
-
-  /** The type of the Constraint. */
-  const ConstraintType d_type;
-
-  /** The DeltaRational value with the constraint. */
-  const DeltaRational d_value;
-
-  /** A pointer to the associated database for the Constraint. */
-  ConstraintDatabase* d_database;
-
-  /**
-   * The node to be communicated with the TheoryEngine.
-   *
-   * This is not context dependent, but may be set once.
-   *
-   * This must be set if the constraint canBePropagated().
-   * This must be set if the constraint assertedToTheTheory().
-   * Otherwise, this may be null().
-   */
-  Node d_literal;
-
-  /** Pointer to the negation of the Constraint. */
-  ConstraintP d_negation;
-
-  /**
-   * This is true if the associated node can be propagated.
-   *
-   * This should be enabled if the node has been preregistered.
-   *
-   * Sat Context Dependent.
-   * This is initially false.
-   */
-  bool d_canBePropagated;
-
-  /**
-   * This is the order the constraint was asserted to the theory.
-   * If this has been set, the node can be used in conflicts.
-   * If this is c.d_assertedOrder < d.d_assertedOrder, then c can be used in the
-   * explanation of d.
-   *
-   * This should be set after the literal is dequeued by Theory::get().
-   *
-   * Sat Context Dependent.
-   * This is initially AssertionOrderSentinel.
-   */
-  AssertionOrder d_assertionOrder;
-
-  /**
-   * This is guaranteed to be on the fact queue.
-   * For example if x + y = x + 1 is on the fact queue, then use this
-   */
-  TNode d_witness;
-
-  /**
-   * The position of the constraint in the constraint rule id.
-   *
-   * Sat Context Dependent.
-   * This is initially 
-   */
-  ConstraintRuleID d_crid;
-  
-
-  /**
-   * True if the equality has been split.
-   * Only meaningful if ConstraintType == Equality.
-   *
-   * User Context Dependent.
-   * This is initially false.
-   */
-  bool d_split;
-
-  /**
-   * Position in sorted constraint set for the variable.
-   * Unset if d_type is Disequality.
-   */
-  SortedConstraintMapIterator d_variablePosition;
 
   friend class ConstraintDatabase;
 
+ public:
   /**
    * This begins construction of a minimal constraint.
    *
@@ -444,86 +367,6 @@ private:
    */
   ~Constraint();
 
-  /**  Returns true if the constraint has been initialized. */
-  bool initialized() const;
-
-  /**
-   * This initializes the fields that cannot be set in the constructor due to
-   * circular dependencies.
-   */
-  void initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation);
-
-
-
-  class ConstraintRuleCleanup {
-  public:
-    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;
-            });
-    }
-  };
-
-  class CanBePropagatedCleanup {
-  public:
-    inline void operator()(ConstraintP* p){
-      ConstraintP constraint = *p;
-      Assert(constraint->d_canBePropagated);
-      constraint->d_canBePropagated = false;
-    }
-  };
-
-  class AssertionOrderCleanup {
-  public:
-    inline void operator()(ConstraintP* p){
-      ConstraintP constraint = *p;
-      Assert(constraint->assertedToTheTheory());
-      constraint->d_assertionOrder = AssertionOrderSentinel;
-      constraint->d_witness = TNode::null();
-      Assert(!constraint->assertedToTheTheory());
-    }
-  };
-
-  class SplitCleanup {
-  public:
-    inline void operator()(ConstraintP* p){
-      ConstraintP constraint = *p;
-      Assert(constraint->d_split);
-      constraint->d_split = false;
-    }
-  };
-
-  /**
-   * 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.
-   */
-  bool sanityChecking(Node n) const;
-
-  /** 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:
-
   static ConstraintType constraintTypeOfComparison(const Comparison& cmp);
 
   inline ConstraintType getType() const {
@@ -648,6 +491,26 @@ public:
   /** Returns true if the node has a Farkas' proof. */
   bool hasFarkasProof() const;
 
+  /**
+   * @brief Returns whether this constraint is provable using a Farkas
+   * proof that has input assertions as its antecedents.
+   *
+   * An example of a constraint that has a simple Farkas proof:
+   *    x <= 0 proven from x + y <= 0 and x - y <= 0.
+   *
+   * An example of a constraint that does not have a simple Farkas proof:
+   *    x <= 0 proven from x + y <= 0 and x - y <= 0.5 for integers x, y
+   *       (since integer reasoning is also required!).
+   * Another example of a constraint that might be proven without a simple
+   * Farkas proof:
+   *    x < 0 proven from not(x == 0) and not(x > 0).
+   *
+   * This could be proven internally by the arithmetic theory using
+   * `TrichotomyAP` as the proof type.
+   *
+   */
+  bool hasSimpleFarkasProof() const;
+
   /** Returns true if the node has a int hole proof. */
   bool hasIntHoleProof() const;
 
@@ -735,22 +598,6 @@ public:
    */
   Node externalExplainConflict() const;
 
-private:
-  Node externalExplain(AssertionOrder order) const;
-
-  /**
-   * Returns an explanation of that was assertedBefore(order).
-   * The constraint must have a proof.
-   * The constraint cannot be selfExplaining().
-   *
-   * This is the minimum fringe of the implication tree
-   * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof().
-   */
-  void externalExplain(NodeBuilder<>& nb, AssertionOrder order) const;
-
-  static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order);
-
-public:
 
   /** The constraint is known to be true. */
   inline bool hasProof() const {
@@ -791,7 +638,6 @@ public:
    */
   ConstraintP getFloor();
 
-
   static ConstraintP makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r);
 
   const ValueCollection& getValueCollection() const;
@@ -896,11 +742,109 @@ public:
    */
   const ConstraintDatabase& getDatabase() const;
 
-private:
-
   /** Returns the constraint rule at the position. */
   const ConstraintRule& getConstraintRule() const;
-  
+
+ private:
+  /**  Returns true if the constraint has been initialized. */
+  bool initialized() const;
+
+  /**
+   * This initializes the fields that cannot be set in the constructor due to
+   * circular dependencies.
+   */
+  void initialize(ConstraintDatabase* db,
+                  SortedConstraintMapIterator v,
+                  ConstraintP negation);
+
+  class ConstraintRuleCleanup
+  {
+   public:
+    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;
+      });
+    }
+  };
+
+  class CanBePropagatedCleanup
+  {
+   public:
+    inline void operator()(ConstraintP* p)
+    {
+      ConstraintP constraint = *p;
+      Assert(constraint->d_canBePropagated);
+      constraint->d_canBePropagated = false;
+    }
+  };
+
+  class AssertionOrderCleanup
+  {
+   public:
+    inline void operator()(ConstraintP* p)
+    {
+      ConstraintP constraint = *p;
+      Assert(constraint->assertedToTheTheory());
+      constraint->d_assertionOrder = AssertionOrderSentinel;
+      constraint->d_witness = TNode::null();
+      Assert(!constraint->assertedToTheTheory());
+    }
+  };
+
+  class SplitCleanup
+  {
+   public:
+    inline void operator()(ConstraintP* p)
+    {
+      ConstraintP constraint = *p;
+      Assert(constraint->d_split);
+      constraint->d_split = false;
+    }
+  };
+
+  /**
+   * 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.
+   */
+  bool sanityChecking(Node n) const;
+
+  /** 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);
+
+  Node externalExplain(AssertionOrder order) const;
+
+  /**
+   * Returns an explanation of that was assertedBefore(order).
+   * The constraint must have a proof.
+   * The constraint cannot be selfExplaining().
+   *
+   * This is the minimum fringe of the implication tree
+   * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof().
+   */
+  void externalExplain(NodeBuilder<>& nb, AssertionOrder order) const;
+
+  static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order);
+
   inline ArithProofType getProofType() const {
     return getConstraintRule().d_proofType;
   }
@@ -934,7 +878,85 @@ private:
    */
 
   bool wellFormedFarkasProof() const;
-  
+
+  /** The ArithVar associated with the constraint. */
+  const ArithVar d_variable;
+
+  /** The type of the Constraint. */
+  const ConstraintType d_type;
+
+  /** The DeltaRational value with the constraint. */
+  const DeltaRational d_value;
+
+  /** A pointer to the associated database for the Constraint. */
+  ConstraintDatabase* d_database;
+
+  /**
+   * The node to be communicated with the TheoryEngine.
+   *
+   * This is not context dependent, but may be set once.
+   *
+   * This must be set if the constraint canBePropagated().
+   * This must be set if the constraint assertedToTheTheory().
+   * Otherwise, this may be null().
+   */
+  Node d_literal;
+
+  /** Pointer to the negation of the Constraint. */
+  ConstraintP d_negation;
+
+  /**
+   * This is true if the associated node can be propagated.
+   *
+   * This should be enabled if the node has been preregistered.
+   *
+   * Sat Context Dependent.
+   * This is initially false.
+   */
+  bool d_canBePropagated;
+
+  /**
+   * This is the order the constraint was asserted to the theory.
+   * If this has been set, the node can be used in conflicts.
+   * If this is c.d_assertedOrder < d.d_assertedOrder, then c can be used in the
+   * explanation of d.
+   *
+   * This should be set after the literal is dequeued by Theory::get().
+   *
+   * Sat Context Dependent.
+   * This is initially AssertionOrderSentinel.
+   */
+  AssertionOrder d_assertionOrder;
+
+  /**
+   * This is guaranteed to be on the fact queue.
+   * For example if x + y = x + 1 is on the fact queue, then use this
+   */
+  TNode d_witness;
+
+  /**
+   * The position of the constraint in the constraint rule id.
+   *
+   * Sat Context Dependent.
+   * This is initially
+   */
+  ConstraintRuleID d_crid;
+
+  /**
+   * True if the equality has been split.
+   * Only meaningful if ConstraintType == Equality.
+   *
+   * User Context Dependent.
+   * This is initially false.
+   */
+  bool d_split;
+
+  /**
+   * Position in sorted constraint set for the variable.
+   * Unset if d_type is Disequality.
+   */
+  SortedConstraintMapIterator d_variablePosition;
+
 }; /* class ConstraintValue */
 
 std::ostream& operator<<(std::ostream& o, const Constraint& c);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 89550295a..48d1b0188 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2138,6 +2138,7 @@ Node flattenAndSort(Node n){
 
 /** Outputs conflicts to the output channel. */
 void TheoryArithPrivate::outputConflicts(){
+  Debug("arith::conflict") << "outputting conflicts" << std::endl;
   Assert(anyConflict());
   static unsigned int conflicts = 0;
   
@@ -2145,13 +2146,39 @@ void TheoryArithPrivate::outputConflicts(){
     Assert(!d_conflicts.empty());
     for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){
       ConstraintCP confConstraint = d_conflicts[i];
+      bool hasProof = confConstraint->hasProof();
       Assert(confConstraint->inConflict());
+      const ConstraintRule& pf = confConstraint->getConstraintRule();
+      if (Debug.isOn("arith::conflict"))
+      {
+        pf.print(std::cout);
+        std::cout << std::endl;
+      }
       Node conflict = confConstraint->externalExplainConflict();
 
       ++conflicts;
       Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict
-        //                               << "("<<conflicts<<")"
-                               << endl;
+                               << " has proof: " << hasProof << endl;
+      PROOF(if (d_containing.d_proofRecorder && confConstraint->hasFarkasProof()
+                && pf.d_farkasCoefficients->size()
+                       == conflict.getNumChildren()) {
+        // The Farkas coefficients and the children of `conflict` seem to be in
+        // opposite orders... There is some relevant documentation in the
+        // comment for the d_farkasCoefficients field  in "constraint.h"
+        //
+        // Anyways, we reverse the children in `conflict` here.
+        NodeBuilder<> conflictInFarkasCoefficientOrder(kind::AND);
+        for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren;
+             ++i)
+        {
+          conflictInFarkasCoefficientOrder
+              << conflict[conflict.getNumChildren() - i - 1];
+        }
+
+        Assert(conflict.getNumChildren() == pf.d_farkasCoefficients->size());
+        d_containing.d_proofRecorder->saveFarkasCoefficients(
+            conflictInFarkasCoefficientOrder, pf.d_farkasCoefficients);
+      })
       if(Debug.isOn("arith::normalize::external")){
         conflict = flattenAndSort(conflict);
         Debug("arith::conflict") << "(normalized to) " << conflict << endl;
@@ -2174,7 +2201,9 @@ void TheoryArithPrivate::outputConflicts(){
     (d_containing.d_out)->conflict(bb);
   }
 }
+
 void TheoryArithPrivate::outputLemma(TNode lem) {
+  Debug("arith::lemma") << "Arith Lemma: " << lem << std::endl;
   (d_containing.d_out)->lemma(lem);
 }
 
@@ -4809,11 +4838,41 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
 
     PROOF(d_farkasBuffer.clear());
     RationalVectorP coeffs = NULLPROOF(&d_farkasBuffer);
- 
+
+    // After invoking `propegateRow`:
+    //   * coeffs[0] is for implied
+    //   * coeffs[i+1] is for explain[i]
     d_linEq.propagateRow(explain, ridx, rowUp, implied, coeffs);
     if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){
       Node implication = implied->externalImplication(explain);
       Node clause = flattenImplication(implication);
+      PROOF(if (d_containing.d_proofRecorder
+                && coeffs != RationalVectorCPSentinel
+                && coeffs->size() == clause.getNumChildren()) {
+        Debug("arith::prop") << "implied    : " << implied << std::endl;
+        Debug("arith::prop") << "implication: " << implication << std::endl;
+        Debug("arith::prop") << "coeff len: " << coeffs->size() << std::endl;
+        Debug("arith::prop") << "exp    : " << explain << std::endl;
+        Debug("arith::prop") << "clause : " << clause << std::endl;
+        Debug("arith::prop")
+            << "clause len: " << clause.getNumChildren() << std::endl;
+        Debug("arith::prop") << "exp len: " << explain.size() << std::endl;
+        // Using the information from the above comment we assemble a conflict
+        // AND in coefficient order
+        NodeBuilder<> conflictInFarkasCoefficientOrder(kind::AND);
+        conflictInFarkasCoefficientOrder << implication[1].negate();
+        for (const Node& antecedent : implication[0])
+        {
+          Debug("arith::prop") << "  ante: " << antecedent << std::endl;
+          conflictInFarkasCoefficientOrder << antecedent;
+        }
+
+        Assert(coeffs != RationalVectorPSentinel);
+        Assert(conflictInFarkasCoefficientOrder.getNumChildren()
+               == coeffs->size());
+        d_containing.d_proofRecorder->saveFarkasCoefficients(
+            conflictInFarkasCoefficientOrder, coeffs);
+      })
       outputLemma(clause);
     }else{
       Assert(!implied->negationHasProof());