diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-11-29 13:51:17 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-29 21:51:17 +0000 |
commit | d6e6421b211917ac1504f58228e29389efce72c9 (patch) | |
tree | 15f1f51d2914dd9cd76cabf7a6222b688c884a9f | |
parent | 96153f641d3738971b61ed1f5055f19a18bbe158 (diff) |
Fix minor issues (#7704)
This fixes a few minor coverity issues.
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 9 | ||||
-rw-r--r-- | src/util/resource_manager.cpp | 1 |
2 files changed, 4 insertions, 6 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index d4b84be01..643ba9a28 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2530,12 +2530,9 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex Assert(d_partialModel.canBeReleased(v)); if(!d_tableau.isBasic(v)){ /* if it is not basic make it basic. */ - ArithVar b = ARITHVAR_SENTINEL; - for(Tableau::ColIterator ci = d_tableau.colIterator(v); !ci.atEnd(); ++ci){ - const Tableau::Entry& e = *ci; - b = d_tableau.rowIndexToBasic(e.getRowIndex()); - break; - } + auto ci = d_tableau.colIterator(v); + Assert(!ci.atEnd()); + ArithVar b = d_tableau.rowIndexToBasic((*ci).getRowIndex()); Assert(b != ARITHVAR_SENTINEL); DeltaRational cp = d_partialModel.getAssignment(b); if(d_partialModel.cmpAssignmentLowerBound(b) < 0){ diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index c4a94dfa2..4a5be537c 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -158,6 +158,7 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, d_cumulativeTimeUsed(0), d_cumulativeResourceUsed(0), d_thisCallResourceUsed(0), + d_thisCallResourceBudget(0), d_statistics(new ResourceManager::Statistics(stats)) { d_statistics->d_resourceUnitsUsed.set(d_cumulativeResourceUsed); |