diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 099980653..5c3786108 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1762,6 +1762,12 @@ void SmtEngine::setDefaults() { options::prenexQuant.set( quantifiers::PRENEX_QUANT_NONE ); } } + if( options::ufHo() ){ + //if higher-order, then current variants of model-based instantiation cannot be used + if( options::mbqiMode()!=quantifiers::MBQI_NONE ){ + 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 |