diff options
Diffstat (limited to 'Test/z3api/bar3.bpl')
-rw-r--r-- | Test/z3api/bar3.bpl | 82 |
1 files changed, 41 insertions, 41 deletions
diff --git a/Test/z3api/bar3.bpl b/Test/z3api/bar3.bpl index 7bd91184..17fc79c3 100644 --- a/Test/z3api/bar3.bpl +++ b/Test/z3api/bar3.bpl @@ -1,41 +1,41 @@ -var y: int;
-var x: int;
-
-procedure {:inline 1} bar(b: bool)
-modifies y;
-{
- if (b) {
- y := y + 1;
- } else {
- y := y - 1;
- }
-}
-
-procedure {:inline 1} foo()
-modifies x, y;
-{
- var b: bool;
- if (b) {
- x := x + 1;
- call bar(true);
- call bar(true);
- x := x + 1;
- } else {
- x := x - 1;
- call bar(false);
- call bar(false);
- x := x - 1;
- }
-}
-
-
-procedure main()
-requires x == y;
-ensures x == y;
-modifies x, y;
-modifies y;
-{
- call foo();
- assert x == y;
- call bar(false);
-}
+var y: int; +var x: int; + +procedure {:inline 1} bar(b: bool) +modifies y; +{ + if (b) { + y := y + 1; + } else { + y := y - 1; + } +} + +procedure {:inline 1} foo() +modifies x, y; +{ + var b: bool; + if (b) { + x := x + 1; + call bar(true); + call bar(true); + x := x + 1; + } else { + x := x - 1; + call bar(false); + call bar(false); + x := x - 1; + } +} + + +procedure main() +requires x == y; +ensures x == y; +modifies x, y; +modifies y; +{ + call foo(); + assert x == y; + call bar(false); +} |