Minor fix for printing nullary operators in smt2 (#8577)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 91c5dc185ab53028720170f7d9e5bfe4fdaf6af8..c9199c64d92351a4268fd26994930ca45b40d11f 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -943,7 +943,11 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::INST_PATTERN_LIST: break;
   default:
     // by default, print the kind using the smtKindString utility
-    out << smtKindString(k, d_variant) << " ";
+    out << smtKindString(k, d_variant);
+    if (n.getNumChildren() > 0)
+    {
+      out << " ";
+    }
     break;
   }
   if( n.getMetaKind() == kind::metakind::PARAMETERIZED &&

diff --git a/src/smt/listeners.h b/src/smt/listeners.h
index e327ddf53ec96f8f7d6cd3db1d193cbe2dc8ec67..8a5e24002aa8940ca6bfbd94b99cb83b8703391b 100644 (file)
--- a/src/smt/listeners.h
+++ b/src/smt/listeners.h
@@ -25,7 +25,6 @@
 
 namespace cvc5::internal {
 
-class OutputManager;
 class SolverEngine;
 
 namespace smt {