blob: 12aec5f41c39185662f1a50afc3d0458fc201d89 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
// RUN: %dafny /compile:3 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
method F() returns(x:int)
ensures x == 6;
{
x := 5;
x := (var y := 1; y + x);
}
method Main()
{
var x := F();
print x;
}
|