diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7abfd8273..ae20fa156 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1809,12 +1809,6 @@ void SmtEngine::setDefaults() { options::mbqiMode.set( quantifiers::MBQI_NONE ); } } - if( options::mbqiMode()==quantifiers::MBQI_ABS ){ - if( !d_logic.isPure(THEORY_UF) ){ - //MBQI_ABS is only supported in pure quantified UF - options::mbqiMode.set( quantifiers::MBQI_FMC ); - } - } if( options::fmfFunWellDefinedRelevant() ){ if( !options::fmfFunWellDefined.wasSetByUser() ){ options::fmfFunWellDefined.set( true ); @@ -1852,17 +1846,6 @@ void SmtEngine::setDefaults() { options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } - if( options::mbqiMode()==quantifiers::MBQI_ABS ){ - if( !options::preSkolemQuant.wasSetByUser() ){ - options::preSkolemQuant.set( true ); - } - if( !options::preSkolemQuantNested.wasSetByUser() ){ - options::preSkolemQuantNested.set( true ); - } - if( !options::fmfOneInstPerRound.wasSetByUser() ){ - options::fmfOneInstPerRound.set( true ); - } - } } //apply counterexample guided instantiation options |