diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-16 12:19:06 -0700 |
|---|---|---|
| committer | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-16 16:52:50 -0700 |
| commit | cbce537b4ebc22bc929b52115a5686ea1deeff26 (patch) | |
| tree | 9caaae084d93749dc123b1a6171a7d7e635615ab /src/theory/arith/constraint.cpp | |
| parent | 905d77664cdedb5d1f3fec91c32c5033a0618e67 (diff) | |
Fix antecedent loop. Whoops
Diffstat (limited to 'src/theory/arith/constraint.cpp')
| -rw-r--r-- | src/theory/arith/constraint.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
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()) { |