diff options
Diffstat (limited to 'Test/stratifiedinline/bar6.bpl')
-rw-r--r-- | Test/stratifiedinline/bar6.bpl | 76 |
1 files changed, 38 insertions, 38 deletions
diff --git a/Test/stratifiedinline/bar6.bpl b/Test/stratifiedinline/bar6.bpl index d763a82c..68c1faac 100644 --- a/Test/stratifiedinline/bar6.bpl +++ b/Test/stratifiedinline/bar6.bpl @@ -1,38 +1,38 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var M: [int]int;
-
-procedure bar(y: int) returns (b: bool)
-modifies M;
-{
- if (b) {
- M[y] := M[y] + 1;
- } else {
- M[y] := M[y] - 1;
- }
-}
-
-procedure foo(x: int, y: int)
-modifies M;
-{
- var b: bool;
-
- call b := bar(y);
- if (b) {
- M[x] := M[x] + 1;
- } else {
- M[x] := M[x] - 1;
- }
-}
-
-procedure {:entrypoint} main(x: int, y: int) returns (b: bool)
-modifies M;
-{
- assume x != y;
- assume M[x] == M[y];
- call foo(x, y);
- if (M[x] == M[y]) {
- call b := bar(y);
- assume (if b then M[x]+1 != M[y] else M[x] != M[y]+1);
- }
-}
+// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var M: [int]int; + +procedure bar(y: int) returns (b: bool) +modifies M; +{ + if (b) { + M[y] := M[y] + 1; + } else { + M[y] := M[y] - 1; + } +} + +procedure foo(x: int, y: int) +modifies M; +{ + var b: bool; + + call b := bar(y); + if (b) { + M[x] := M[x] + 1; + } else { + M[x] := M[x] - 1; + } +} + +procedure {:entrypoint} main(x: int, y: int) returns (b: bool) +modifies M; +{ + assume x != y; + assume M[x] == M[y]; + call foo(x, y); + if (M[x] == M[y]) { + call b := bar(y); + assume (if b then M[x]+1 != M[y] else M[x] != M[y]+1); + } +} |