1 files changed, 14 insertions, 18 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 801711a13..cfafd63c4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5258,36 +5258,32 @@ Model* SmtEngine::getModel() {
   return m;
 }
 
-Expr SmtEngine::getHeapExpr()
+std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void)
 {
-  NodeManagerScope nms(d_nodeManager);
-  Expr heap;
-  Expr nil;  // we don't actually use this
-  Model* m = getModel();
-  if (m->getHeapModel(heap, nil))
+  if (!d_logic.isTheoryEnabled(THEORY_SEP))
   {
-    return heap;
+    const char* msg =
+        "Cannot obtain separation logic expressions if not using the "
+        "separation logic theory.";
+    throw RecoverableModalException(msg);
   }
-  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 heap;
   Expr nil;
   Model* m = getModel();
   if (m->getHeapModel(heap, nil))
   {
-    return nil;
+    return std::make_pair(heap, nil);
   }
   InternalError(
-      "SmtEngine::getNilExpr(): failed to obtain nil expression from theory "
-      "model.");
+      "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
+      "expressions from theory model.");
 }
 
+Expr SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
+
+Expr SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
+
 void SmtEngine::checkUnsatCore() {
   Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off");