From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 10 Apr 2018 01:50:39 +0000 (-0700)
Subject: Fix dumping of benchmark in SmtEngine::checkSatisfiability(). (#1764)
X-Git-Tag: cvc5-1.0.0~5164
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=80792d1026600d162f293839615fecdf19665e17;p=cvc5.git

Fix dumping of benchmark in SmtEngine::checkSatisfiability(). (#1764)
---

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index c77c4ed02..847221979 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -449,8 +449,6 @@ CheckSatAssumingCommand::CheckSatAssumingCommand(const std::vector<Expr>& terms,
                                                  bool inUnsatCore)
     : d_terms(terms), d_inUnsatCore(inUnsatCore)
 {
-  PrettyCheckArgument(
-      terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
 }
 
 const std::vector<Expr>& CheckSatAssumingCommand::getTerms() const
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 70dc04669..dd8a2e502 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4646,11 +4646,16 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
     // Dump the query if requested
     if (Dump.isOn("benchmark"))
     {
+      size_t size = assumptions.size();
       // the expr already got dumped out if assertion-dumping is on
-      if (isQuery && assumptions.size() == 1)
+      if (isQuery && size == 1)
       {
         Dump("benchmark") << QueryCommand(assumptions[0]);
       }
+      else if (size == 0)
+      {
+        Dump("benchmark") << CheckSatCommand();
+      }
       else
       {
         Dump("benchmark") << CheckSatAssumingCommand(d_assumptions,