From: Tim King <taking@cs.nyu.edu>
Date: Thu, 16 Aug 2018 01:09:45 +0000 (-0700)
Subject: Switching an Assert to a CVC4_CHECK to test if it resolves CID 1459595. (#2315)
X-Git-Tag: cvc5-1.0.0~4778
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b92e8623c695e10f812e7cc213df9f871924ea8b;p=cvc5.git

Switching an Assert to a CVC4_CHECK to test if it resolves CID 1459595. (#2315)
---

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