From 6df0b6f2ac842b0407232fcee72ff68b7e9deee5 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 16 Sep 2011 20:49:58 +0000
Subject: [PATCH] fix an oversight in the language printers

---
 src/printer/cvc/cvc_printer.cpp   | 6 +++++-
 src/printer/smt2/smt2_printer.cpp | 6 +++++-
 2 files changed, 10 insertions(+), 2 deletions(-)

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