diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3343abc29..910855505 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3678,15 +3678,17 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) Result SmtEngine::query(const Expr& assumption, bool inUnsatCore) { - return checkSatisfiability( - assumption.isNull() ? std::vector<Expr>() : std::vector<Expr>{assumption}, - inUnsatCore, - true); + return checkSatisfiability(assumption.isNull() + ? std::vector<Expr>() + : std::vector<Expr>{assumption}, + inUnsatCore, + true) + .asValidityResult(); } Result SmtEngine::query(const vector<Expr>& assumptions, bool inUnsatCore) { - return checkSatisfiability(assumptions, inUnsatCore, true); + return checkSatisfiability(assumptions, inUnsatCore, true).asValidityResult(); } Result SmtEngine::checkSatisfiability(const Expr& expr, @@ -3771,7 +3773,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, d_private->addFormula(e.getNode(), inUnsatCore, true, true); } - r = isQuery ? check().asValidityResult() : check().asSatisfiabilityResult(); + r = check(); if ((options::solveRealAsInt() || options::solveIntAsBV() > 0) && r.asSatisfiabilityResult().isSat() == Result::UNSAT) |