2 files changed, 9 insertions, 4 deletions
diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp
index ed7f8febf..2ac514988 100644
--- a/src/printer/smt/smt_printer.cpp
+++ b/src/printer/smt/smt_printer.cpp
@@ -34,15 +34,19 @@ namespace printer {
 namespace smt {
 
 void SmtPrinter::toStream(std::ostream& out, TNode n,
-                          int toDepth, bool types) const {
+                          int toDepth, bool types) const throw() {
   n.toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2);
 }/* SmtPrinter::toStream() */
 
 void SmtPrinter::toStream(std::ostream& out, const Command* c,
-                          int toDepth, bool types) const {
+                          int toDepth, bool types) const throw() {
   c->toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2);
 }/* SmtPrinter::toStream() */
 
+void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+  s->toStream(out, language::output::LANG_SMTLIB_V2);
+}
+
 }/* CVC4::printer::smt namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h
index 14d6c09e1..370e0908c 100644
--- a/src/printer/smt/smt_printer.h
+++ b/src/printer/smt/smt_printer.h
@@ -31,8 +31,9 @@ namespace smt {
 
 class SmtPrinter : public CVC4::Printer {
 public:
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const;
+  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, const CommandStatus* s) const throw();
 };/* class SmtPrinter */
 
 }/* CVC4::printer::smt namespace */