diff options
author | Tim King <taking@google.com> | 2016-09-25 15:49:52 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-09-25 15:49:52 -0700 |
commit | 061c6941ae2595333987897f73bb6cf32b053c4b (patch) | |
tree | 4388a6484d9d55777e8ddd242cdab4a10747f23b /src/theory | |
parent | 197462bef8b5d19ca34dfeca00a76df837f27de2 (diff) |
Fixing a potential use after free coming from a pop_back() call invalidating strictly earlier entries.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index e47231128..069d3530c 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2520,34 +2520,37 @@ struct SizeOrd { return a.size() < b.size(); } }; -void TheoryArithPrivate::subsumption(std::vector<ConstraintCPVec>& confs) const { + +void TheoryArithPrivate::subsumption( + std::vector<ConstraintCPVec> &confs) const { int checks CVC4_UNUSED = 0; int subsumed CVC4_UNUSED = 0; - for(size_t i =0, N= confs.size(); i < N; ++i){ - ConstraintCPVec& conf = confs[i]; + for (size_t i = 0, N = confs.size(); i < N; ++i) { + ConstraintCPVec &conf = confs[i]; std::sort(conf.begin(), conf.end()); } std::sort(confs.begin(), confs.end(), SizeOrd()); - for(size_t i = 0; i < confs.size(); i++){ - ConstraintCPVec& a = confs[i]; + for (size_t i = 0; i < confs.size(); i++) { // i is not subsumed - for(size_t j = i+1; j < confs.size();){ + for (size_t j = i + 1; j < confs.size();) { + ConstraintCPVec& a = confs[i]; ConstraintCPVec& b = confs[j]; checks++; bool subsumes = std::includes(a.begin(), a.end(), b.begin(), b.end()); - if(subsumes){ + if (subsumes) { ConstraintCPVec& back = confs.back(); b.swap(back); confs.pop_back(); subsumed++; - }else{ + } else { j++; } } } - Debug("arith::subsumption") << "subsumed " << subsumed << "/" << checks << endl; + Debug("arith::subsumption") << "subsumed " << subsumed << "/" << checks + << endl; } std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth){ |