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, 3 insertions, 3 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b4c6c97cd..0ec55a5e6 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -798,11 +798,11 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
   }
 }
 
-void TheoryEngine::collectModelComments( theory::TheoryModel* m ){
+void TheoryEngine::postProcessModel( theory::TheoryModel* m ){
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
     if(d_logicInfo.isTheoryEnabled(theoryId)) {
-      Trace("model-builder-debug") << "  CollectModelComments on theory: " << theoryId << endl;
-      d_theoryTable[theoryId]->collectModelComments( m );
+      Trace("model-builder-debug") << "  PostProcessModel on theory: " << theoryId << endl;
+      d_theoryTable[theoryId]->postProcessModel( m );
     }
   }
 }