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

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index c77c4ed02fc6187dd5056b6f81936752e618cc50..8472219794f434dfe148fb71744d68498449eaeb 100644 (file)
--- 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 70dc046690aceb8a8182309e9dcdb574b60bed81..dd8a2e50264a2338e94658b6e62833aa78810499 100644 (file)
--- 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,