From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 20 Oct 2021 22:09:07 +0000 (-0500)
Subject: Throw exception if checking model with separation logic heap (#7422)
X-Git-Tag: cvc5-1.0.0~1032
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=04c1d3b5c6af01c77a6c38e24847d4458a14ef3b;p=cvc5.git

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 36d107429..5d16c12ce 100644
--- 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;