diff options
author | makaimann <makaim@stanford.edu> | 2019-03-21 18:10:01 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-22 01:10:01 +0000 |
commit | a20702bcbb04422ddfcda5a241fd0cc0ec32edc8 (patch) | |
tree | 5abcba103332741021daad54f3040974bb54bd9b | |
parent | a5466f262e16f3ebcd7c62df266a5ac0cd9c5b9a (diff) |
Use empty vector instead of false in query with null Expr assumption (#2876)
This solution is less confusing than using a `false` assumption.
-rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8305d1d4d..6bca668e0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3594,7 +3594,7 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) Result SmtEngine::query(const Expr& assumption, bool inUnsatCore) { return checkSatisfiability( - assumption.isNull() ? d_exprManager->mkConst<bool>(false) : assumption, + assumption.isNull() ? std::vector<Expr>() : std::vector<Expr>{assumption}, inUnsatCore, true); } @@ -3609,7 +3609,7 @@ Result SmtEngine::checkSatisfiability(const Expr& expr, bool isQuery) { return checkSatisfiability( - expr.isNull() ? vector<Expr>() : vector<Expr>{expr}, + expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr}, inUnsatCore, isQuery); } |