diff options
Diffstat (limited to 'Test/AbsHoudini/int1.bpl')
-rw-r--r-- | Test/AbsHoudini/int1.bpl | 52 |
1 files changed, 26 insertions, 26 deletions
diff --git a/Test/AbsHoudini/int1.bpl b/Test/AbsHoudini/int1.bpl index 0ee0f1b9..eb4e6b51 100644 --- a/Test/AbsHoudini/int1.bpl +++ b/Test/AbsHoudini/int1.bpl @@ -1,26 +1,26 @@ -function {:existential true} b0(x:int): bool;
-function {:existential true} b1(x:int): bool;
-
-var g: int;
-
-procedure foo()
-modifies g;
-requires b0(g);
-ensures b1(g);
-{
- if(*) {
- g := g + 1;
- call foo();
- }
-}
-
-procedure main()
-modifies g;
-{
- g := 0;
- if(*) { g := 5; }
- call foo();
-}
-
-
-// Expected: b0(x) = [0,\infty], b1(x) = [0, \infty]
+function {:existential true} b0(x:int): bool; +function {:existential true} b1(x:int): bool; + +var g: int; + +procedure foo() +modifies g; +requires b0(g); +ensures b1(g); +{ + if(*) { + g := g + 1; + call foo(); + } +} + +procedure main() +modifies g; +{ + g := 0; + if(*) { g := 5; } + call foo(); +} + + +// Expected: b0(x) = [0,\infty], b1(x) = [0, \infty] |