diff options
Diffstat (limited to 'Test/test21/InterestingExamples3.bpl')
-rw-r--r-- | Test/test21/InterestingExamples3.bpl | 66 |
1 files changed, 33 insertions, 33 deletions
diff --git a/Test/test21/InterestingExamples3.bpl b/Test/test21/InterestingExamples3.bpl index 24e89b2b..4990fb72 100644 --- a/Test/test21/InterestingExamples3.bpl +++ b/Test/test21/InterestingExamples3.bpl @@ -1,33 +1,33 @@ -// 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"
-
-procedure P() returns () {
-
- assume (forall<t> m : [t]bool :: // uses "infinitely many" map types
- (forall x : t :: m[x] == false));
-
-}
-
-
-procedure Q() returns () {
- var h : [int] bool;
-
- assume (forall<t> m : [t]bool, x : t :: m[x] == false);
- assert !h[42];
- assert false; // should really be provable
-}
-
-
-
-procedure R() returns () {
- var h : [int] bool;
-
- assume (forall<t> m : [t]bool, x : t :: m[x] == false);
- assert !h[42];
- assert !h[42 := true][42];
- assert false; // wow
-}
+// 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" + +procedure P() returns () { + + assume (forall<t> m : [t]bool :: // uses "infinitely many" map types + (forall x : t :: m[x] == false)); + +} + + +procedure Q() returns () { + var h : [int] bool; + + assume (forall<t> m : [t]bool, x : t :: m[x] == false); + assert !h[42]; + assert false; // should really be provable +} + + + +procedure R() returns () { + var h : [int] bool; + + assume (forall<t> m : [t]bool, x : t :: m[x] == false); + assert !h[42]; + assert !h[42 := true][42]; + assert false; // wow +} |