From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Test/stratifiedinline/bar4.bpl | 78 +++++++++++++++++++++--------------------- 1 file changed, 39 insertions(+), 39 deletions(-) (limited to 'Test/stratifiedinline/bar4.bpl') diff --git a/Test/stratifiedinline/bar4.bpl b/Test/stratifiedinline/bar4.bpl index 948683f8..4cf52946 100644 --- a/Test/stratifiedinline/bar4.bpl +++ b/Test/stratifiedinline/bar4.bpl @@ -1,39 +1,39 @@ -// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var y: int; -var x: int; - -procedure bar() returns (b: bool) -modifies y; -{ - if (b) { - y := y + 1; - } else { - y := y - 1; - } -} - -procedure foo() -modifies x, y; -{ - var b: bool; - - call b := bar(); - if (b) { - x := x + 1; - } else { - x := x - 1; - } -} - - -procedure {:entrypoint} main() returns (b: bool) -modifies x, y; -{ - assume x == y; - call foo(); - if (x == y) { - call b := bar(); - assume (if b then x+1 != y else x != y+1); - } -} +// RUN: %boogie -stratifiedInline:1 -vc:i "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var y: int; +var x: int; + +procedure bar() returns (b: bool) +modifies y; +{ + if (b) { + y := y + 1; + } else { + y := y - 1; + } +} + +procedure foo() +modifies x, y; +{ + var b: bool; + + call b := bar(); + if (b) { + x := x + 1; + } else { + x := x - 1; + } +} + + +procedure {:entrypoint} main() returns (b: bool) +modifies x, y; +{ + assume x == y; + call foo(); + if (x == y) { + call b := bar(); + assume (if b then x+1 != y else x != y+1); + } +} -- cgit v1.2.3