diff options
author | Tim King <taking@cs.nyu.edu> | 2018-08-15 18:09:45 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-15 18:09:45 -0700 |
commit | b92e8623c695e10f812e7cc213df9f871924ea8b (patch) | |
tree | 60ac84ab87b00eb8ec7341bc400848bb10314ef3 /src | |
parent | bca6b323721b24805c375f682e05d5463c38a8d2 (diff) |
Switching an Assert to a CVC4_CHECK to test if it resolves CID 1459595. (#2315)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/fmf/ambqi_builder.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/fmf/ambqi_builder.cpp b/src/theory/quantifiers/fmf/ambqi_builder.cpp index 5def5fc95..f2b131f21 100644 --- a/src/theory/quantifiers/fmf/ambqi_builder.cpp +++ b/src/theory/quantifiers/fmf/ambqi_builder.cpp @@ -13,6 +13,8 @@ **/ #include "theory/quantifiers/fmf/ambqi_builder.h" + +#include "base/cvc4_check.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" @@ -367,8 +369,8 @@ void AbsDef::construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int cur }else{ TypeNode tn = m->getVariable( q, depth ).getType(); if( v==depth ){ - unsigned numReps = m->getRepSet()->getNumRepresentatives(tn); - Assert( numReps>0 && numReps < 32 ); + const unsigned numReps = m->getRepSet()->getNumRepresentatives(tn); + CVC4_CHECK(numReps > 0 && numReps < 32); for( unsigned i=0; i<numReps; i++ ){ d_def[ 1 << i ].construct_var( m, q, v, i, depth+1 ); } |