diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-01-04 15:28:24 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-01-04 15:41:05 -0600 |
commit | 5552e43454c3b45ae8c7b35a822ac4b39adca72f (patch) | |
tree | bf7eacb6908c439bde2c8e8052a83f52cdcd46ca /src/printer | |
parent | 0beaa6fbb218328ade97d1f3c5b40fde7aa6d3b5 (diff) |
Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor changes.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 8 |
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; } |