diff options
Diffstat (limited to 'Chalice/tests/regressions/internal-bug-2.chalice')
| -rw-r--r-- | Chalice/tests/regressions/internal-bug-2.chalice | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Chalice/tests/regressions/internal-bug-2.chalice b/Chalice/tests/regressions/internal-bug-2.chalice new file mode 100644 index 00000000..ac6b5a09 --- /dev/null +++ b/Chalice/tests/regressions/internal-bug-2.chalice @@ -0,0 +1,13 @@ +class Lala {
+ var x;
+
+ predicate inv { acc(x) }
+
+ method koko()
+ requires inv
+ {
+ x := x + 1;
+ assert (unfolding inv in x) == old(unfolding inv in x)
+ }
+}
+
|