diff options
author | Tim King <taking@cs.nyu.edu> | 2018-08-08 16:50:16 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-08 16:50:16 -0700 |
commit | 987df3df987768e2ce0c36d17469929f8e92fdec (patch) | |
tree | 6d85a85966084879e55b8ab04c330662a4cfe7f0 /src/theory | |
parent | ece17ee2c38fa5769ae3ab7fa3607c0e88c0021f (diff) |
Proposal for adding map utility functions to CVC4. (#2232)
* Proposal for adding map utility functions to CVC4.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 7094ad541..cfa50bef8 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -15,6 +15,7 @@ **/ #include "theory/quantifiers/fmf/bounded_integers.h" + #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/first_order_model.h" @@ -451,11 +452,20 @@ 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() ){ - Assert( bound_lit_pol_map[b].find( v )!=bound_lit_pol_map[b].end() ); + if (bound_lit_map[b].find(v) != bound_lit_map[b].end()) + { + // 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 + // in debug mode to have this instances raised to our attention. + Assert(bound_lit_pol_map[b].find(v) + != bound_lit_pol_map[b].end()); BoundIntLitAttribute bila; - bound_lit_map[b][v].setAttribute( bila, bound_lit_pol_map[b][v] ? 1 : 0 ); - }else{ + bound_lit_map[b][v].setAttribute(bila, + bound_lit_pol_map[b][v] ? 1 : 0); + } + else + { Assert( it->second!=BOUND_INT_RANGE ); } } |