projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 57f8d6c) | patch
Throw exception if checking model with separation logic heap (#7422)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 Oct 2021 22:09:07 +0000 (17:09 -0500)
committerGitHub <noreply@github.com>
Wed, 20 Oct 2021 22:09:07 +0000 (22:09 +0000)
commit04c1d3b5c6af01c77a6c38e24847d4458a14ef3b
tree2f311ffd7fb44f2e2defe2801b832326d1318e11tree
parent57f8d6c04430277abdb98916b8ac407930abd215commit | 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.
src/smt/check_models.cpp diff | blob | history