summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGereon Kremer <gkremer@stanford.edu>2021-11-29 13:51:17 -0800
committerGitHub <noreply@github.com>2021-11-29 21:51:17 +0000
commitd6e6421b211917ac1504f58228e29389efce72c9 (patch)
tree15f1f51d2914dd9cd76cabf7a6222b688c884a9f
parent96153f641d3738971b61ed1f5055f19a18bbe158 (diff)
Fix minor issues (#7704)
This fixes a few minor coverity issues.
-rw-r--r--src/theory/arith/theory_arith_private.cpp9
-rw-r--r--src/util/resource_manager.cpp1
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback