From: makaimann <makaim@stanford.edu>
Date: Fri, 22 Mar 2019 01:10:01 +0000 (-0700)
Subject: Use empty vector instead of false in query with null Expr assumption (#2876)
X-Git-Tag: cvc5-1.0.0~4226
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a20702bcbb04422ddfcda5a241fd0cc0ec32edc8;p=cvc5.git

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 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);
 }