diff options
| author |  Rustan Leino <unknown> | 2014-07-02 14:09:57 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-07-02 14:09:57 -0700 |
| commit | c5ed80858adb0a19fc1e1014d31ed609f18c3b33 (patch) | |
| tree | 9af0251e11a17f8df1b660212ba80a8cc01da5c9 /Test/dafny0/SmallTests.dfy | |
| parent | 61f46d7b7789290098361c2de7e775fbe487bd7f (diff) | |
Fixed a crash in the translation of fresh(seq<T>).
Diffstat (limited to 'Test/dafny0/SmallTests.dfy')
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index b996e1c5..a4afecff 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -204,7 +204,14 @@ class AllocatedTests { if (*) {
assert !fresh(U); // error: n was not allocated initially
} else {
- assert fresh(U); // correct (note, the assertion does NOT say: everything was unallocated in the initial state)
+ assert fresh(U); // error: k was not allocated initially
+ }
+
+ var Q := [k,n];
+ if (*) {
+ assert !fresh(Q); // error: n was not allocated initially
+ } else {
+ assert fresh(Q); // error: k was not allocated initially
}
}
}
|