Fix get-unsat-assumptions output (#2301)

Fixes #2298. The `get-unsat-assumptions` command was printing the result
with square brackets and commas instead of parentheses and spaces
between the assumptions.

2 files changed, 10 insertions, 5 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 65d4396a9..2805d8793 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -35,6 +35,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "util/sexpr.h"
+#include "util/utility.h"
 
 using namespace std;
 
@@ -1873,7 +1874,7 @@ void GetUnsatAssumptionsCommand::printResult(std::ostream& out,
   }
   else
   {
-    out << d_result << endl;
+    container_to_stream(out, d_result, "(", ")\n", " ");
   }
 }
 
diff --git a/src/util/utility.h b/src/util/utility.h
index a9a9a29c3..56a68ca40 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -69,16 +69,20 @@ inline InputIterator find_if_unique(InputIterator first, InputIterator last, Pre
 }
 
 template <typename T>
-void container_to_stream(std::ostream& out, const T& container)
+void container_to_stream(std::ostream& out,
+                         const T& container,
+                         const char* prefix = "[",
+                         const char* postfix = "]",
+                         const char* sep = ", ")
 {
-  out << "[";
+  out << prefix;
   bool is_first = true;
   for (const auto& item : container)
   {
-    out << (!is_first ? ", " : "") << item;
+    out << (!is_first ? sep : "") << item;
     is_first = false;
   }
-  out << "]";
+  out << postfix;
 }
 
 }/* CVC4 namespace */