Add regressions for finite model finding

2 files changed, 4 insertions, 3 deletions

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 060f6dbba..dd5e404c6 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1376,7 +1376,7 @@ Constraint TheoryArithPrivate::constraintFromFactQueue(){
   Assert(!done());
   TNode assertion = get();
 
-  if( options::finiteModelFind() ){
+  if( options::finiteModelFind() && d_quantEngine && d_quantEngine->getBoundedIntegers() ){
     d_quantEngine->getBoundedIntegers()->assertNode(assertion);
   }
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ef8169433..e01d83853 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -62,8 +62,9 @@ d_lemmas_produced_c(u){
     d_model_engine = new quantifiers::ModelEngine( c, this );
     d_modules.push_back( d_model_engine );
 
-    d_bint = new quantifiers::BoundedIntegers( c, this );
-    d_modules.push_back( d_bint );
+    //d_bint = new quantifiers::BoundedIntegers( c, this );
+    //d_modules.push_back( d_bint );
+    d_bint = NULL;
   }else{
     d_model_engine = NULL;
     d_bint = NULL;