Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor changes.

1 files changed, 4 insertions, 4 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index aa5849960..d75ec2126 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1076,6 +1076,10 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
   while( std::getline( c, ln ) ){
     out << "; " << ln << std::endl;
   }
+  //print the model
+  out << "(model" << endl;
+  this->Printer::toStream(out, m);
+  out << ")" << endl;
   //print the heap model, if it exists
   Expr h, neq;
   if( m.getHeapModel( h, neq ) ){
@@ -1085,10 +1089,6 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
     out << neq << endl;
     out << ")" << std::endl;
   }
-  //print the model
-  out << "(model" << endl;
-  this->Printer::toStream(out, m);
-  out << ")" << endl;
 }