diff options
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 { |