diff options
Diffstat (limited to 'Test/test21/InterestingExamples5.bpl')
-rw-r--r-- | Test/test21/InterestingExamples5.bpl | 42 |
1 files changed, 21 insertions, 21 deletions
diff --git a/Test/test21/InterestingExamples5.bpl b/Test/test21/InterestingExamples5.bpl index 3f4e4f34..8eadadc9 100644 --- a/Test/test21/InterestingExamples5.bpl +++ b/Test/test21/InterestingExamples5.bpl @@ -1,22 +1,22 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
-// RUN: %diff "%s.n.expect" "%t"
-// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
-// RUN: %diff "%s.p.expect" "%t"
-// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
-// RUN: %diff "%s.a.expect" "%t"
-
-
-type C a;
-
-function f<a>(C a) returns (int);
-
-//axiom (forall<a> x:C a :: {f(x)} (exists y:C a :: f(y) == 42));
-
-function g<a>(C a) returns (C a);
-axiom (forall<a> x:C a :: f(g(x)) == 42);
-
-procedure P() returns () {
- var z : C int;
- assume g(z) == z;
- assert (exists x : C int :: f(x) == 42);
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" + + +type C a; + +function f<a>(C a) returns (int); + +//axiom (forall<a> x:C a :: {f(x)} (exists y:C a :: f(y) == 42)); + +function g<a>(C a) returns (C a); +axiom (forall<a> x:C a :: f(g(x)) == 42); + +procedure P() returns () { + var z : C int; + assume g(z) == z; + assert (exists x : C int :: f(x) == 42); }
\ No newline at end of file |