1 files changed, 23 insertions, 17 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index a903b2576..15101b0e4 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -767,9 +767,9 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
 
 
 void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
-  out << "(model" << std::endl;
+  out << "(model" << endl;
   this->Printer::toStream(out, m);
-  out << ")" << std::endl;
+  out << ")" << endl;
 }
 
 
@@ -783,23 +783,23 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
       for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
         out << "(" << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << ")";
       }
-      out << ")))" << std::endl;
+      out << ")))" << endl;
     } else {
       if( tn.isSort() ){
         //print the cardinality
         if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
-          out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
+          out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << endl;
         }
       }
-      out << c << std::endl;
+      out << c << endl;
       if( tn.isSort() ){
         //print the representatives
         if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
           for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
             if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
-              out << "(declare-fun " << quoteSymbol((*tm.d_rep_set.d_type_reps.find(tn)).second[i]) << " () " << tn << ")" << std::endl;
+              out << "(declare-fun " << quoteSymbol((*tm.d_rep_set.d_type_reps.find(tn)).second[i]) << " () " << tn << ")" << endl;
             }else{
-              out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
+              out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << endl;
             }
           }
         }
@@ -820,7 +820,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
     if(val.getKind() == kind::LAMBDA) {
       out << "(define-fun " << n << " " << val[0]
           << " " << n.getType().getRangeType()
-          << " " << val[1] << ")" << std::endl;
+          << " " << val[1] << ")" << endl;
     } else {
       if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) {
         TypeNode tn = val[1].getType();
@@ -830,7 +830,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
         }
       }
       out << "(define-fun " << n << " () "
-          << n.getType() << " " << val << ")" << std::endl;
+          << n.getType() << " " << val << ")" << endl;
     }
 /*
     //for table format (work in progress)
@@ -856,7 +856,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
     }
 */
   }else{
-    out << c << std::endl;
+    out << c << endl;
   }
 }
 
@@ -886,7 +886,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
     out << PushCommand() << endl
         << AssertCommand(e) << endl
         << CheckSatCommand() << endl
-        << PopCommand() << endl;
+        << PopCommand();
   } else {
     out << "(check-sat)";
   }
@@ -898,7 +898,7 @@ static void toStream(std::ostream& out, const QueryCommand* c) throw() {
     out << PushCommand() << endl
         << AssertCommand(BooleanSimplification::negate(e)) << endl
         << CheckSatCommand() << endl
-        << PopCommand() << endl;
+        << PopCommand();
   } else {
     out << "(check-sat)";
   }
@@ -909,10 +909,16 @@ static void toStream(std::ostream& out, const QuitCommand* c) throw() {
 }
 
 static void toStream(std::ostream& out, const CommandSequence* c) throw() {
-  for(CommandSequence::const_iterator i = c->begin();
-      i != c->end();
-      ++i) {
-    out << *i << endl;
+  CommandSequence::const_iterator i = c->begin();
+  if(i != c->end()) {
+    for(;;) {
+      out << *i;
+      if(++i != c->end()) {
+        out << endl;
+      } else {
+        break;
+      }
+    }
   }
 }
 
@@ -996,7 +1002,7 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
   out << "(get-value ( ";
   const vector<Expr>& terms = c->getTerms();
   copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
-  out << " ))";
+  out << "))";
 }
 
 static void toStream(std::ostream& out, const GetModelCommand* c) throw() {