blob: be09226138a060f92e80b295703cb8d563fb6022 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This once crashed Dafny
method M() {
var s := [1, "2"];
if * {
assert exists n :: n in s && n != 1;
} else {
assert "2" in s;
}
}
|