diff options
| author |  stefanheule <unknown> | 2012-06-03 21:27:22 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-06-03 21:27:22 +0200 |
| commit | 3c394ddda72509a6d1fcd315dea3804a3cf579ce (patch) | |
| tree | 5f35a10c4287d8b1e24a1c2cf6f09e85ab03e136 /Chalice | |
| parent | 4e1e7628c0bf8dfcb1e7bb5d5df37996f8662a04 (diff) | |
Chalice: Add regression test for unfolding expressions in predicates.
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/tests/regressions/workitem-10223.chalice | 8 | ||||
| -rw-r--r-- | Chalice/tests/regressions/workitem-10223.output.txt | 4 |
2 files changed, 12 insertions, 0 deletions
diff --git a/Chalice/tests/regressions/workitem-10223.chalice b/Chalice/tests/regressions/workitem-10223.chalice new file mode 100644 index 00000000..eb4bd00b --- /dev/null +++ b/Chalice/tests/regressions/workitem-10223.chalice @@ -0,0 +1,8 @@ +class Lala { + var next: Lala; + var x: int; + predicate inv { + acc(next) && acc(x) && + (next != null ==> (next.inv && unfolding next.inv in this.x > next.x)) + } +} diff --git a/Chalice/tests/regressions/workitem-10223.output.txt b/Chalice/tests/regressions/workitem-10223.output.txt new file mode 100644 index 00000000..f4bfd78d --- /dev/null +++ b/Chalice/tests/regressions/workitem-10223.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10223.chalice using parameters=""
+
+ +Boogie program verifier finished with 0 errors and 0 smoke test warnings.
|