Throw exception if checking model with separation logic heap (#7422)

Fixes #5515.

It is currently not possible to check-model with separation logic. Checking models requires either additional bookkeeping (heap per formula position) or otherwise is expensive to check.

This makes us give a recoverable exception.

diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index 36d1074299c42680313f8cb8ace571770d0be567..5d16c12ce1e4dfe62f94a4d08b181dcdb3f89149 100644 (file)
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -49,6 +49,12 @@ void CheckModels::checkModel(TheoryModel* m,
     throw RecoverableModalException(
         "Cannot run check-model on a model with approximate values.");
   }
+  Node sepHeap, sepNeq;
+  if (m->getHeapModel(sepHeap, sepNeq))
+  {
+    throw RecoverableModalException(
+        "Cannot run check-model on a model with a separation logic heap.");
+  }
 
   theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
   Trace("check-model") << "checkModel: Check assertions..." << std::endl;