From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Mon, 16 Mar 2020 19:19:06 +0000 (-0700)
Subject: Fix antecedent loop. Whoops
X-Git-Tag: cvc5-1.0.0~3485
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cbce537b4ebc22bc929b52115a5686ea1deeff26;p=cvc5.git

Fix antecedent loop. Whoops
---

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 98ce07fbc..cdab772f8 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -502,11 +502,11 @@ bool Constraint::hasSimpleFarkasProof() const
   }
 
   // For each antecdent ...
-  for (AntecedentId i = getConstraintRule().d_antecedentEnd;
-       i != AntecedentIdSentinel;
-       --i)
+  AntecedentId i = getConstraintRule().d_antecedentEnd;
+  for (ConstraintCP a = d_database->getAntecedent(i);
+       a != NullConstraint;
+       a = d_database->getAntecedent(--i))
   {
-    ConstraintCP a = d_database->getAntecedent(i);
     // ... that antecdent must be an assumption ...
     if (a->isAssumption())
     {