diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-24 18:34:25 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-24 18:34:25 +0200 |
commit | d7dc7c2b3038b862af5ea55e7cf6b1fc4e1fe684 (patch) | |
tree | d6c229a2659bfcb3cdf7c7c786414ecc1e59e61c /src/smt | |
parent | 1ec95c559074ed7575a0165deb16fcee45920e9f (diff) |
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.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 5 |
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() ){ |