diff options
Diffstat (limited to 'Chalice/tests/regressions/workitem-10223.chalice')
| -rw-r--r-- | Chalice/tests/regressions/workitem-10223.chalice | 8 |
1 files changed, 8 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)) + } +} |