diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0276684d6..cb1445b93 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1212,21 +1212,18 @@ void SmtEngine::setDefaults() { } // set options about ackermannization - if (options::produceModels()) + if (options::ackermann() && options::produceModels() + && (d_logic.isTheoryEnabled(THEORY_ARRAYS) + || d_logic.isTheoryEnabled(THEORY_UF))) { - if (options::ackermann() - && (d_logic.isTheoryEnabled(THEORY_ARRAYS) - || d_logic.isTheoryEnabled(THEORY_UF))) + if (options::produceModels.wasSetByUser()) { - if (options::produceModels.wasSetByUser()) - { - throw OptionException(std::string( - "Ackermannization currently does not support model generation.")); - } - Notice() << "SmtEngine: turn off ackermannization to support model" - << "generation" << endl; - options::ackermann.set(false); + throw OptionException(std::string( + "Ackermannization currently does not support model generation.")); } + Notice() << "SmtEngine: turn off ackermannization to support model" + << "generation" << endl; + options::ackermann.set(false); } if (options::ackermann()) @@ -1237,6 +1234,11 @@ void SmtEngine::setDefaults() { "Incremental Ackermannization is currently not supported."); } + if (d_logic.isQuantified()) + { + throw LogicException("Cannot use Ackermannization on quantified formula"); + } + if (d_logic.isTheoryEnabled(THEORY_UF)) { d_logic = d_logic.getUnlockedCopy(); |