summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authormakaimann <makaim@stanford.edu>2019-03-21 18:10:01 -0700
committerAndres Noetzli <andres.noetzli@gmail.com>2019-03-22 01:10:01 +0000
commita20702bcbb04422ddfcda5a241fd0cc0ec32edc8 (patch)
tree5abcba103332741021daad54f3040974bb54bd9b
parenta5466f262e16f3ebcd7c62df266a5ac0cd9c5b9a (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.cpp4
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback