Proposal for adding map utility functions to CVC4. (#2232)

* Proposal for adding map utility functions to CVC4.

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 );
             }
           }