diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-12-01 23:44:21 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-01 23:44:21 -0800 |
| commit | 6b92c671980054cd30f72715d6081bff59c1e03a (patch) | |
| tree | 901954e7cef1b4ee86026af25bd7efb63abd5494 /src/smt/smt_engine.cpp | |
| parent | 4b311b17906994186a6c58ee1cb3aaeb590231f5 (diff) | |
| parent | 901cea314c4dc3be411c345e42c858063fe5aa1b (diff) | |
Merge branch 'master' into fixClangWarningsfixClangWarnings
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 14 |
1 files changed, 3 insertions, 11 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0f40db530..2faad7961 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -332,6 +332,7 @@ SmtEngine::~SmtEngine() d_absValues.reset(nullptr); d_asserts.reset(nullptr); d_dumpm.reset(nullptr); + d_model.reset(nullptr); d_sygusSolver.reset(nullptr); @@ -468,11 +469,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) value.getValue() == "2.6" ) { ilang = language::input::LANG_SMTLIB_V2_6; } - else - { - Warning() << "Warning: unsupported smt-lib-version: " << value << endl; - throw UnrecognizedOptionException(); - } options::inputLanguage.set(ilang); // also update the output language if (!options::outputLanguage.wasSetByUser()) @@ -497,7 +493,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) d_state->notifyExpectedStatus(s); return; } - throw UnrecognizedOptionException(); } bool SmtEngine::isValidGetInfoFlag(const std::string& key) const @@ -517,10 +512,6 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const SmtScope smts(this); Trace("smt") << "SMT getInfo(" << key << ")" << endl; - if (!isValidGetInfoFlag(key)) - { - throw UnrecognizedOptionException(); - } if (key == "all-statistics") { vector<SExpr> stats; @@ -1508,7 +1499,8 @@ Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) if(!d_logic.isPure(THEORY_ARITH) && strict){ Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; } - return d_quantElimSolver->getQuantifierElimination(*d_asserts, q, doFull); + return d_quantElimSolver->getQuantifierElimination( + *d_asserts, q, doFull, d_isInternalSubsolver); } bool SmtEngine::getInterpol(const Node& conj, |