From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Apr 2022 12:48:38 +0000 (-0500)
Subject: Minor fix for printing nullary operators in smt2 (#8577)
X-Git-Tag: cvc5-1.0.1~289
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f5452c401c82b84250e498e27c0383b928ef13de;p=cvc5.git

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 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 {