2 files changed, 9 insertions, 4 deletions
diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp
index 553692dc5..6424e377e 100644
--- a/src/printer/smt1/smt1_printer.cpp
+++ b/src/printer/smt1/smt1_printer.cpp
@@ -51,8 +51,13 @@ void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw()
   Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
 }/* Smt1Printer::toStream() */
 
-void Smt1Printer::toStream(std::ostream& out, Model* m, const Command* c) const throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c);
+void Smt1Printer::toStream(std::ostream& out, Model& m) const throw() {
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m);
+}
+
+void Smt1Printer::toStream(std::ostream& out, Model& m, const Command* c) const throw() {
+  // shouldn't be called; only the non-Command* version above should be
+  Unreachable();
 }
 
 }/* CVC4::printer::smt1 namespace */
diff --git a/src/printer/smt1/smt1_printer.h b/src/printer/smt1/smt1_printer.h
index d1b36208c..39f69e8ff 100644
--- a/src/printer/smt1/smt1_printer.h
+++ b/src/printer/smt1/smt1_printer.h
@@ -30,13 +30,13 @@ namespace printer {
 namespace smt1 {
 
 class Smt1Printer : public CVC4::Printer {
+  void toStream(std::ostream& out, Model& m, const Command* c) const throw();
 public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   void toStream(std::ostream& out, const SExpr& sexpr) const throw();
-  //for models
-  void toStream(std::ostream& out, Model* m, const Command* c) const throw();
+  void toStream(std::ostream& out, Model& m) const throw();
 };/* class Smt1Printer */
 
 }/* CVC4::printer::smt1 namespace */