From f5452c401c82b84250e498e27c0383b928ef13de Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Apr 2022 07:48:38 -0500
Subject: [PATCH] Minor fix for printing nullary operators in smt2 (#8577)

---
 src/printer/smt2/smt2_printer.cpp | 6 +++++-
 src/smt/listeners.h               | 1 -
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 91c5dc185..c9199c64d 100644
--- 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 e327ddf53..8a5e24002 100644
--- a/src/smt/listeners.h
+++ b/src/smt/listeners.h
@@ -25,7 +25,6 @@
 
 namespace cvc5::internal {
 
-class OutputManager;
 class SolverEngine;
 
 namespace smt {
-- 
2.30.2