blob: 666d957504950c0028ea55f85aca173f316a1a24 (
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"]; // error: all elements must have the same type
if * {
assert exists n :: n in s && n != 1; // the type of n is inferred to be int
} else {
assert "2" in s; // error: since the type of s wasn't determined
}
}
|
