diff options
Diffstat (limited to 'src/smt/set_defaults.cpp')
-rw-r--r-- | src/smt/set_defaults.cpp | 31 |
1 files changed, 14 insertions, 17 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index e06363883..bae7fbe68 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -538,18 +538,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) smte.setOption("produce-models", SExpr("true")); } - // Set the options for the theoryOf - if (!options::theoryOfMode.wasSetByUser()) - { - if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV) - && !logic.isTheoryEnabled(THEORY_STRINGS) - && !logic.isTheoryEnabled(THEORY_SETS)) - { - Trace("smt") << "setting theoryof-mode to term-based" << std::endl; - options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED); - } - } - ///////////////////////////////////////////////////////////////////////////// // Theory widening // @@ -609,6 +597,18 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } ///////////////////////////////////////////////////////////////////////////// + // Set the options for the theoryOf + if (!options::theoryOfMode.wasSetByUser()) + { + if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV) + && !logic.isTheoryEnabled(THEORY_STRINGS) + && !logic.isTheoryEnabled(THEORY_SETS)) + { + Trace("smt") << "setting theoryof-mode to term-based" << std::endl; + options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED); + } + } + // by default, symmetry breaker is on only for non-incremental QF_UF if (!options::ufSymmetryBreaker.wasSetByUser()) { @@ -1161,11 +1161,8 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) // prenexing if (options::cegqiNestedQE()) { - // only complete with prenex = disj_normal or normal - if (options::prenexQuant() <= options::PrenexQuantMode::DISJ_NORMAL) - { - options::prenexQuant.set(options::PrenexQuantMode::DISJ_NORMAL); - } + // only complete with prenex = normal + options::prenexQuant.set(options::PrenexQuantMode::NORMAL); } else if (options::globalNegate()) { |