1 files changed, 11 insertions, 3 deletions
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];