1 files changed, 24 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 71256e3d8..a275c7d63 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5251,6 +5251,30 @@ Model* SmtEngine::getModel() {
   return m;
 }
 
+Expr SmtEngine::getHeapExpr() {
+  NodeManagerScope nms(d_nodeManager);
+  Expr heap;
+  Expr nil; // we don't actually use this
+  Model* m = getModel();
+  if (m->getHeapModel( heap, nil ))
+  {
+    return heap;
+  }
+  InternalError("SmtEngine::getHeapExpr(): failed to obtain heap expression from theory model.");
+}
+
+Expr SmtEngine::getNilExpr() {
+  NodeManagerScope nms(d_nodeManager);
+  Expr heap; // we don't actually use this
+  Expr nil;
+  Model* m = getModel();
+  if (m->getHeapModel( heap, nil ))
+  {
+    return nil;
+  }
+  InternalError("SmtEngine::getNilExpr(): failed to obtain nil expression from theory model.");
+}
+
 void SmtEngine::checkUnsatCore() {
   Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off");