diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-22 10:37:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-22 10:37:50 -0500 |
commit | c74797f4cbded274e2dca6fee5e0efb439da03f5 (patch) | |
tree | 54b54a1e9e468dec4d97673e03be473632ed1549 /src/theory/quantifiers/fmf | |
parent | ab8d44b83e210ed38623a1440e3ef1d318f7d0d0 (diff) |
Fix invalid iterator comparisons (#2349)
Diffstat (limited to 'src/theory/quantifiers/fmf')
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index f0789a503..8d8bf7f50 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -459,18 +459,18 @@ void BoundedIntegers::checkOwnership(Node f) success = true; //set Attributes on literals for( unsigned b=0; b<2; b++ ){ - if (bound_lit_map[b].find(v) != bound_lit_map[b].end()) + std::map<Node, Node>& blm = bound_lit_map[b]; + if (blm.find(v) != blm.end()) { + std::map<Node, bool>& blmp = bound_lit_pol_map[b]; // WARNING_CANDIDATE: // This assertion may fail. We intentionally do not enable this in // production as it is considered safe for this to fail. We fail // the assertion in debug mode to have this instance raised to // our attention. - Assert(bound_lit_pol_map[b].find(v) - != bound_lit_pol_map[b].end()); + Assert(blmp.find(v) != blmp.end()); BoundIntLitAttribute bila; - bound_lit_map[b][v].setAttribute(bila, - bound_lit_pol_map[b][v] ? 1 : 0); + bound_lit_map[b][v].setAttribute(bila, blmp[v] ? 1 : 0); } else { |