diff options
author | guykatzz <katz911@gmail.com> | 2016-12-07 11:11:29 -0800 |
---|---|---|
committer | guykatzz <katz911@gmail.com> | 2016-12-07 11:11:29 -0800 |
commit | 1ce3fb16b0e0e3a51713d643e792499775a7f11b (patch) | |
tree | 38a4e135e1f096678b430571c7744232fe37d25b /src/smt | |
parent | 5f7edbf5d1cf67789dba889220fb2efbd73ad2bd (diff) | |
parent | e8c09abb9165278b13491c83bdcbe17ae535126e (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 4 |
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() ); } |