Infrastructure for storing and printing heap models for separation logic. Ensure value of sep.nil is correct in models. Print instantiations as sexprs.

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);