1 files changed, 17 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 4006a9e08..c9dc814f2 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1069,6 +1069,23 @@ 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 heap model, if it exists
+  Expr h, neq;
+  if( m.getHeapModel( h, neq ) ){
+    // description of the heap+what nil is equal to fully describes model
+    out << "(heap" << endl;
+    out << h << endl;
+    out << neq << endl;
+    out << ")" << std::endl;
+  }
+  //print the model
   out << "(model" << endl;
   this->Printer::toStream(out, m);
   out << ")" << endl;