From a20702bcbb04422ddfcda5a241fd0cc0ec32edc8 Mon Sep 17 00:00:00 2001
From: makaimann <makaim@stanford.edu>
Date: Thu, 21 Mar 2019 18:10:01 -0700
Subject: [PATCH] Use empty vector instead of false in query with null Expr
 assumption (#2876)

This solution is less confusing than using a `false` assumption.
---
 src/smt/smt_engine.cpp | 4 ++--
 1 file 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);
 }
-- 
2.30.2