summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/smt2/smt2_printer.cpp9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 4cdf5a9fb..7b7d569b7 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1068,6 +1068,15 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback