From 04c1d3b5c6af01c77a6c38e24847d4458a14ef3b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 17:09:07 -0500 Subject: [PATCH] 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. --- src/smt/check_models.cpp | 6 ++++++ 1 file changed, 6 insertions(+) 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; -- 2.30.2