diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
commit | d652155ae013f36a1ee17653a8e458baad2d9c2c (patch) | |
tree | 067d600fe3cd1723afc11682935f0123a1eab653 /Test/z3api/bar6.bpl | |
parent | d7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff) |
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Test/z3api/bar6.bpl')
-rw-r--r-- | Test/z3api/bar6.bpl | 72 |
1 files changed, 36 insertions, 36 deletions
diff --git a/Test/z3api/bar6.bpl b/Test/z3api/bar6.bpl index e133aef7..b0f72767 100644 --- a/Test/z3api/bar6.bpl +++ b/Test/z3api/bar6.bpl @@ -1,36 +1,36 @@ -var M: [int]int;
-
-procedure {:inline 1} bar(y: int) returns (b: bool)
-modifies M;
-{
- if (b) {
- M[y] := M[y] + 1;
- } else {
- M[y] := M[y] - 1;
- }
-}
-
-procedure {:inline 1} 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 main(x: int, y: int) returns (b: bool)
-requires x != y;
-requires M[x] == M[y];
-ensures !b ==> M[x] == M[y]+1;
-ensures b ==> M[x]+1 == M[y];
-modifies M;
-{
- call foo(x, y);
- assert M[x] == M[y];
- call b := bar(y);
-}
+var M: [int]int; + +procedure {:inline 1} bar(y: int) returns (b: bool) +modifies M; +{ + if (b) { + M[y] := M[y] + 1; + } else { + M[y] := M[y] - 1; + } +} + +procedure {:inline 1} 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 main(x: int, y: int) returns (b: bool) +requires x != y; +requires M[x] == M[y]; +ensures !b ==> M[x] == M[y]+1; +ensures b ==> M[x]+1 == M[y]; +modifies M; +{ + call foo(x, y); + assert M[x] == M[y]; + call b := bar(y); +} |