Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.

1 files changed, 1 insertions, 4 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 192485dcc..8fdec25c2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1375,9 +1375,6 @@ void SmtEngine::setDefaults() {
     if( !options::eMatching.wasSetByUser() ){
       options::eMatching.set( options::fmfInstEngine() );
     }
-    if( !options::quantConflictFind.wasSetByUser() ){
-      options::quantConflictFind.set( false );
-    }
     if( ! options::instWhenMode.wasSetByUser()){
       //instantiate only on last call
       if( options::eMatching() ){
@@ -1440,7 +1437,7 @@ void SmtEngine::setDefaults() {
       options::cbqi2.set( true );
     }
   }
-  if( options::recurseCbqi() || options::cbqi2() ){
+  if( options::cbqi2() ){
     options::cbqi.set( true );
   }
   if( options::cbqi2() ){