diff options
Diffstat (limited to 'Test/inline/expansion2.bpl')
-rw-r--r-- | Test/inline/expansion2.bpl | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/Test/inline/expansion2.bpl b/Test/inline/expansion2.bpl index 9883ce83..18eaef33 100644 --- a/Test/inline/expansion2.bpl +++ b/Test/inline/expansion2.bpl @@ -1,19 +1,19 @@ -// RUN: %boogie "-proverLog:%T/expand2.sx" "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// RUN: %OutputCheck "--file-to-check=%T/expand2.sx" "%s"
-function {:inline true} xxgz(x:int) returns(bool)
- { x > 0 }
-function {:inline true} xxf1(x:int,y:bool) returns(int)
- { x + 1 }
-
-axiom (forall z:int :: z>12 ==> xxgz(z));
-axiom (forall y:int, x:bool :: xxf1(y, x) > 1 ==> y > 0);
-
-procedure foo()
-{
- // CHECK-NOT-L: xxgz
- assert xxgz(12);
- // CHECK-NOT-L: xxf1
- assert xxf1(3,true) == 4;
-}
-
+// RUN: %boogie "-proverLog:%T/expand2.sx" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// RUN: %OutputCheck "--file-to-check=%T/expand2.sx" "%s" +function {:inline true} xxgz(x:int) returns(bool) + { x > 0 } +function {:inline true} xxf1(x:int,y:bool) returns(int) + { x + 1 } + +axiom (forall z:int :: z>12 ==> xxgz(z)); +axiom (forall y:int, x:bool :: xxf1(y, x) > 1 ==> y > 0); + +procedure foo() +{ + // CHECK-NOT-L: xxgz + assert xxgz(12); + // CHECK-NOT-L: xxf1 + assert xxf1(3,true) == 4; +} + |