5 files changed, 33 insertions, 13 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index abfaca954..6a04e70d1 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -506,18 +506,8 @@ bool Constraint::hasSimpleFarkasProof() const
   for (ConstraintCP a = d_database->getAntecedent(i); a != NullConstraint;
        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())
-
+    // ... that antecdent must be an assumption OR a tightened assumption ...
+    if (a->isPossiblyTightenedAssumption())
     {
       continue;
     }
@@ -536,6 +526,17 @@ bool Constraint::hasSimpleFarkasProof() const
   return true;
 }
 
+bool Constraint::isPossiblyTightenedAssumption() const
+{
+  // ... that antecdent must be an assumption ...
+
+  if (isAssumption()) return true;
+  if (!hasIntTightenProof()) return false;
+  if (getConstraintRule().d_antecedentEnd == AntecedentIdSentinel) return false;
+  return d_database->getAntecedent(getConstraintRule().d_antecedentEnd)
+      ->isAssumption();
+}
+
 bool Constraint::hasIntTightenProof() const {
   return getProofType() == IntTightenAP;
 }
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 873b33ced..b32616a04 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -514,6 +514,11 @@ class Constraint {
    *
    */
   bool hasSimpleFarkasProof() const;
+  /**
+   * Returns whether this constraint is an assumption or a tightened
+   * assumption.
+   */
+  bool isPossiblyTightenedAssumption() const;
 
   /** Returns true if the node has a int bound tightening proof. */
   bool hasIntTightenProof() const;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 39a3a6558..cdf3c16c7 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1933,7 +1933,8 @@ void TheoryArithPrivate::outputConflicts(){
         }
 
         Assert(conflict.getNumChildren() == pf.d_farkasCoefficients->size());
-        if (confConstraint->hasSimpleFarkasProof())
+        if (confConstraint->hasSimpleFarkasProof()
+            && confConstraint->getNegation()->isPossiblyTightenedAssumption())
         {
           d_containing.d_proofRecorder->saveFarkasCoefficients(
               conflictInFarkasCoefficientOrder, pf.d_farkasCoefficients);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8118d8d79..a3dbd847a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2167,6 +2167,7 @@ set(regress_3_tests
   regress3/incorrect1.smtv1.smt2
   regress3/issue2429.smt2
   regress3/issue4170.smt2
+  regress3/issue4714.smt2
   regress3/pp-regfile.smtv1.smt2
   regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
   regress3/siegel-nl-bases.smt2
diff --git a/test/regress/regress3/issue4714.smt2 b/test/regress/regress3/issue4714.smt2
new file mode 100644
index 000000000..ee3e59a32
--- /dev/null
+++ b/test/regress/regress3/issue4714.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --check-models
+; EXPECT: unknown
+(set-logic UFNIRA)
+(declare-fun c (Int) Int)
+(define-fun d ((k Int)) Int (- (c k) 10))
+(define-fun j ((k Int) (e Int)) Bool (<= 0 e (d k)))
+(define-fun f ((k Int) (a Int) (b Int)) Int (ite (= b 1) a (mod a b)))
+(define-fun g ((k Int) (a Int) (b Int)) Int (f k (* a (c b)) (c k)))
+(define-fun h ((k Int) (a Int) (b Int)) Int (f k (+ a b) (c k)))
+(assert (= (c 0) 1))
+(assert (exists ((l Int) (k Int)) (and (j k l) (distinct (g k (h k l (g k l l)) l) (g k (h k l 0) l)))))
+(check-sat)