diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-20 17:09:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-20 22:09:07 +0000 |
| commit | 04c1d3b5c6af01c77a6c38e24847d4458a14ef3b (patch) | |
| tree | 2f311ffd7fb44f2e2defe2801b832326d1318e11 | |
| parent | 57f8d6c04430277abdb98916b8ac407930abd215 (diff) | |
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.
| -rw-r--r-- | src/smt/check_models.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
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; |