fix function signatures

2 files changed, 6 insertions, 8 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index c8c4bfc20..5aff8ebba 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -28,12 +28,12 @@ namespace smt2 {
 
 void printBvParameterizedOp(std::ostream& out, TNode n);
 
-std::ostream& Smt2Printer::toStream(std::ostream& out, TNode n,
-                                    int toDepth, bool types) const {
+void Smt2Printer::toStream(std::ostream& out, TNode n,
+                           int toDepth, bool types) const {
   // null
   if(n.getKind() == kind::NULL_EXPR) {
     out << "null";
-    return out;
+    return;
   }
 
   // variable
@@ -55,7 +55,7 @@ std::ostream& Smt2Printer::toStream(std::ostream& out, TNode n,
       n.getType().toStream(out, -1, false, language::output::LANG_SMTLIB_V2);
     }
 
-    return out;
+    return;
   }
 
   // constant
@@ -80,7 +80,7 @@ std::ostream& Smt2Printer::toStream(std::ostream& out, TNode n,
       kind::metakind::NodeValueConstPrinter::toStream(out, n);
     }
 
-    return out;
+    return;
   }
 
   bool stillNeedToPrintParams = true;
@@ -191,8 +191,6 @@ std::ostream& Smt2Printer::toStream(std::ostream& out, TNode n,
     }
   }
   out << ')';
-
-  return out;
 }/* Smt2Printer::toStream() */
 
 void printBvParameterizedOp(std::ostream& out, TNode n) {
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 7cd88f0ff..6fce2dfff 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -31,7 +31,7 @@ namespace smt2 {
 
 class Smt2Printer : public CVC4::Printer {
 public:
-  std::ostream& toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
+  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
 };/* class Smt2Printer */
 
 }/* CVC4::printer::smt2 namespace */