diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-11-20 13:55:42 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-20 15:55:42 -0600 |
| commit | 13a107e13f52c6418328eb798da315ca2fa1a1ca (patch) | |
| tree | 57dd223bef7a6aa76ae6cbfaa520be3aea1f1a1c | |
| parent | 6beb76055b81510ec38a8b50f5ed35d2f5010139 (diff) | |
Fix #5493. (#5495)
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 109ffe63c..153b8e379 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -3478,7 +3478,9 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) } d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow); - for (std::size_t i = 0; i < d_fcSimplex.getPivots(); ++i) + size_t nPivots = + options::useFC() ? d_fcSimplex.getPivots() : d_dualSimplex.getPivots(); + for (std::size_t i = 0; i < nPivots; ++i) { d_containing.d_out->spendResource( ResourceManager::Resource::ArithPivotStep); |