1 files changed, 8 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 35e6f1a73..4cdf5a9fb 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1061,6 +1061,14 @@ void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core, const std::
 
 
 void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
+  //print the model comments
+  std::stringstream c;
+  m.getComments( c );
+  std::string ln;
+  while( std::getline( c, ln ) ){
+    out << "; " << ln << std::endl;
+  }
+  //print the model
   out << "(model" << endl;
   this->Printer::toStream(out, m);
   out << ")" << endl;