blob: 8f309b75acc6149a343fbcaad0a732fd989d3f7a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
// RUN: %boogie -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// 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
}
|
