Merge branch 'master' of https://github.com/CVC4/CVC4

1 files changed, 4 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 84384ba04..a79416b76 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1774,6 +1774,10 @@ void SmtEngine::setDefaults() {
   //now, have determined whether finite model find is on/off
   //apply finite model finding options
   if( options::finiteModelFind() ){
+    //apply conservative quantifiers splitting
+    if( !options::quantDynamicSplit.wasSetByUser() ){
+      options::quantDynamicSplit.set( quantifiers::QUANT_DSPLIT_MODE_DEFAULT );
+    }
     if( !options::eMatching.wasSetByUser() ){
       options::eMatching.set( options::fmfInstEngine() );
     }