diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bac2f2f50..9914992ef 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3559,8 +3559,10 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) Result SmtEngine::query(const Expr& assumption, bool inUnsatCore) { - Assert(!assumption.isNull()); - return checkSatisfiability(assumption, inUnsatCore, true); + return checkSatisfiability( + assumption.isNull() ? d_exprManager->mkConst<bool>(false) : assumption, + inUnsatCore, + true); } Result SmtEngine::query(const vector<Expr>& assumptions, bool inUnsatCore) |