2 files changed, 32 insertions, 13 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 56703c12a..98ce07fbc 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -500,21 +500,39 @@ bool Constraint::hasSimpleFarkasProof() const
                                << std::endl;
     return false;
   }
-  const ConstraintRule& rule = getConstraintRule();
-  AntecedentId antId = rule.d_antecedentEnd;
-  ConstraintCP antecdent = d_database->getAntecedent(antId);
-  while (antecdent != NullConstraint)
+
+  // For each antecdent ...
+  for (AntecedentId i = getConstraintRule().d_antecedentEnd;
+       i != AntecedentIdSentinel;
+       --i)
   {
-    if (antecdent->getProofType() != AssumeAP)
+    ConstraintCP a = d_database->getAntecedent(i);
+    // ... that antecdent must be an assumption ...
+    if (a->isAssumption())
+    {
+      continue;
+    }
+
+    // ... OR a tightened assumption ...
+    if (a->hasIntTightenProof()
+        && a->getConstraintRule().d_antecedentEnd != AntecedentIdSentinel
+        && d_database->getAntecedent(a->getConstraintRule().d_antecedentEnd)
+               ->isAssumption())
+
+    {
+      continue;
+    }
+
+    // ... otherwise, we do not have a simple Farkas proof.
+    if (Debug.isOn("constraints::hsfp"))
     {
       Debug("constraints::hsfp") << "There is no simple Farkas proof b/c there "
                                     "is an antecdent w/ rule ";
-      antecdent->getConstraintRule().print(Debug("constraints::hsfp"));
+      a->getConstraintRule().print(Debug("constraints::hsfp"));
       Debug("constraints::hsfp") << std::endl;
-      return false;
     }
-    --antId;
-    antecdent = d_database->getAntecedent(antId);
+
+    return false;
   }
   return true;
 }
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 225bf555e..17b4fa4e3 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -496,15 +496,16 @@ class Constraint {
 
   /**
    * @brief Returns whether this constraint is provable using a Farkas
-   * proof that has input assertions as its antecedents.
+   * proof applied to (possibly tightened) input assertions.
    *
    * 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:
+   * An example of another constraint that has 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
+   *       (integer bound-tightening is applied first!).
+   *
+   * An example of a constraint that might be proven **without** a simple
    * Farkas proof:
    *    x < 0 proven from not(x == 0) and not(x > 0).
    *