blob: 7d1f0dafdc9c63b688bc16b38714e62ddaa91ecd (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
// Examples from the Boogie2 language report
// (examples where already resolution fails)
var x : int;
var y : int;
var a : [int]int;
procedure P(i:int, j:int) returns () modifies x, y, a; {
x, y := 1; // wrong number of rhss
a[i], a[j] := a[j], a[i]; // variable assigned more than once
}
|
