From d6e6421b211917ac1504f58228e29389efce72c9 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 29 Nov 2021 13:51:17 -0800 Subject: [PATCH] Fix minor issues (#7704) This fixes a few minor coverity issues. --- src/theory/arith/theory_arith_private.cpp | 9 +++------ 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 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); -- 2.30.2