Use empty vector instead of false in query with null Expr assumption (#2876)

This solution is less confusing than using a `false` assumption.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8305d1d4dc8440c8fc2bb79a34a01aa362bef413..6bca668e0a57c5c6b03e6e40f63a205596636667 100644 (file)
--- 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);
 }