Multiple fixes for datatypes theory solver: add support for parametric datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup.

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