1 files changed, 4 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 85a245a09..be6acd09c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1031,6 +1031,10 @@ void SmtEngine::setLogicInternal() throw() {
       options::fmfInstGen.set( false );
     }
   }
+  if ( options::fmfBoundInt() ){
+    //if bounded integers are set, must use full model check for MBQI
+    options::fmfFullModelCheck.set( true );
+  }
   if( options::ufssSymBreak() ){
     options::sortInference.set( true );
   }