2 files changed, 12 insertions, 0 deletions
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index eb4254560..ee05709b7 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -197,6 +197,8 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         vector[Term] getUnsatCore() except +
         Term getValue(Term term) except +
         vector[Term] getValue(const vector[Term]& terms) except +
+        Term getSeparationHeap() except +
+        Term getSeparationNilTerm() except +
         void pop(uint32_t nscopes) except +
         void printModel(ostream& out)
         void push(uint32_t nscopes) except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 5abbfb113..ab174ef0d 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -917,6 +917,16 @@ cdef class Solver:
         term.cterm = self.csolver.getValue(t.cterm)
         return term
 
+    def getSeparationHeap(self):
+        cdef Term term = Term()
+        term.cterm = self.csolver.getSeparationHeap()
+        return term
+
+    def getSeparationNilTerm(self):
+        cdef Term term = Term()
+        term.cterm = self.csolver.getSeparationNilTerm()
+        return term
+
     def pop(self, nscopes=1):
         self.csolver.pop(nscopes)