Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by default in EPR mode.

1 files changed, 7 insertions, 3 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b7997a204..19bc85e3e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1748,6 +1748,12 @@ void SmtEngine::setDefaults() {
       options::finiteModelFind.set( true );
     }
   }
+  //EPR
+  if( options::quantEpr() ){
+    if( !options::preSkolemQuant.wasSetByUser() ){
+      options::preSkolemQuant.set( true );
+    }
+  }
 
   //now, have determined whether finite model find is on/off
   //apply finite model finding options
@@ -1840,9 +1846,7 @@ void SmtEngine::setDefaults() {
       }
       if( !options::instWhenMode.wasSetByUser() && options::cbqiModel() ){
         //only instantiation should happen at last call when model is avaiable
-        if( !options::instWhenMode.wasSetByUser() ){
-          options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
-        }
+        options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
       }
     }
   }