diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0bfc6e634..37ab9cd48 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1018,11 +1018,18 @@ void SmtEngine::setLogicInternal() throw() { //for finite model finding if( ! options::instWhenMode.wasSetByUser()){ + //instantiate only on last call if( options::fmfInstEngine() ){ Trace("smt") << "setting inst when mode to LAST_CALL" << endl; options::instWhenMode.set( INST_WHEN_LAST_CALL ); } } + if ( ! options::fmfInstGen.wasSetByUser()) { + //if full model checking is on, disable inst-gen techniques + if( options::fmfFullModelCheck() ){ + options::fmfInstGen.set( false ); + } + } //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ |