From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 16 Sep 2011 20:49:58 +0000 (+0000)
Subject: fix an oversight in the language printers
X-Git-Tag: cvc5-1.0.0~8475
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6df0b6f2ac842b0407232fcee72ff68b7e9deee5;p=cvc5.git

fix an oversight in the language printers
---

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 0f3d635bd..fa1855ebe 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -393,7 +393,8 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<SetOptionCommand>(out, c) ||
      tryToStream<GetOptionCommand>(out, c) ||
      tryToStream<DatatypeDeclarationCommand>(out, c) ||
-     tryToStream<CommentCommand>(out, c)) {
+     tryToStream<CommentCommand>(out, c) ||
+     tryToStream<EmptyCommand>(out, c)) {
     return;
   }
 
@@ -550,6 +551,9 @@ static void toStream(std::ostream& out, const CommentCommand* c) {
   out << "% " << c->getComment();
 }
 
+static void toStream(std::ostream& out, const EmptyCommand* c) {
+}
+
 template <class T>
 static bool tryToStream(std::ostream& out, const Command* c) {
   if(typeid(*c) == typeid(T)) {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5758b1101..e926c350f 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -291,7 +291,8 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<SetOptionCommand>(out, c) ||
      tryToStream<GetOptionCommand>(out, c) ||
      tryToStream<DatatypeDeclarationCommand>(out, c) ||
-     tryToStream<CommentCommand>(out, c)) {
+     tryToStream<CommentCommand>(out, c) ||
+     tryToStream<EmptyCommand>(out, c)) {
     return;
   }
 
@@ -462,6 +463,9 @@ static void toStream(std::ostream& out, const CommentCommand* c) {
   out << "(set-info :notes \"" << c->getComment() << "\")";
 }
 
+static void toStream(std::ostream& out, const EmptyCommand* c) {
+}
+
 template <class T>
 static bool tryToStream(std::ostream& out, const Command* c) {
   if(typeid(*c) == typeid(T)) {