Change default option to --inst-when=full-last-call (interleave instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs.

1 files changed, 8 insertions, 1 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 86b0faaf6..74cdee0b7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1319,7 +1319,6 @@ void SmtEngine::setDefaults() {
     if( !options::quantConflictFind.wasSetByUser() ){
       options::quantConflictFind.set( false );
     }
-    //for finite model finding
     if( ! options::instWhenMode.wasSetByUser()){
       //instantiate only on last call
       if( options::eMatching() ){
@@ -1327,6 +1326,14 @@ void SmtEngine::setDefaults() {
         options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
       }
     }
+    if( options::mbqiMode()==quantifiers::MBQI_ABS ){
+      if( !options::preSkolemQuant.wasSetByUser() ){
+        options::preSkolemQuant.set( true );
+      }
+      if( !options::fmfOneInstPerRound.wasSetByUser() ){
+        options::fmfOneInstPerRound.set( true );
+      }
+    }
   }
   
   //implied options...