diff options
Diffstat (limited to 'Test/aitest1/Bound.bpl')
-rw-r--r-- | Test/aitest1/Bound.bpl | 60 |
1 files changed, 30 insertions, 30 deletions
diff --git a/Test/aitest1/Bound.bpl b/Test/aitest1/Bound.bpl index 81b3635f..f2dd2547 100644 --- a/Test/aitest1/Bound.bpl +++ b/Test/aitest1/Bound.bpl @@ -1,30 +1,30 @@ -// RUN: %boogie -infer:j "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const TEST: name;
-
-procedure P()
-{
-var i: int;
-var N: int;
-
-start:
- assume N >= 0;
- i := 0;
- assert i <= N;
- goto LoopHead;
-
-LoopHead:
- goto LoopBody, AfterLoop;
-
-LoopBody:
- assume i < N;
- i := i + 1;
- goto LoopHead;
-
-AfterLoop:
- assume !(i < N);
- assert i == N;
- return;
-}
-
-type name;
+// RUN: %boogie -infer:j "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +const TEST: name; + +procedure P() +{ +var i: int; +var N: int; + +start: + assume N >= 0; + i := 0; + assert i <= N; + goto LoopHead; + +LoopHead: + goto LoopBody, AfterLoop; + +LoopBody: + assume i < N; + i := i + 1; + goto LoopHead; + +AfterLoop: + assume !(i < N); + assert i == N; + return; +} + +type name; |