From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Test/test21/Maps1.bpl | 84 +++++++++++++++++++++++++-------------------------- 1 file changed, 42 insertions(+), 42 deletions(-) (limited to 'Test/test21/Maps1.bpl') diff --git a/Test/test21/Maps1.bpl b/Test/test21/Maps1.bpl index 024cd50f..bcb5a9b9 100644 --- a/Test/test21/Maps1.bpl +++ b/Test/test21/Maps1.bpl @@ -1,42 +1,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" - - -// different map type classes with the same arity - -const c : [int] bool; -const d : [ref] bool; -const e : [a] bool; -const f : [a] a; - -axiom (c[17] ==> c[19]); -axiom (forall x:t :: e[x]); -axiom (!d[null]); -axiom (forall x:t :: f[x] == x); - -procedure P() returns () { - - var x : [a] bool; - - assume !c[19]; - assert !c[17]; - - x := e; - x[true] := false; - x[17] := true; - - assert !x[true]; - assert !(forall y:t :: x[y]); - assert x != e; - - assert f[x] == x; - assert f[17] > 17; // should not be provable - -} - -type ref; -const null : ref; +// 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" + + +// different map type classes with the same arity + +const c : [int] bool; +const d : [ref] bool; +const e : [a] bool; +const f : [a] a; + +axiom (c[17] ==> c[19]); +axiom (forall x:t :: e[x]); +axiom (!d[null]); +axiom (forall x:t :: f[x] == x); + +procedure P() returns () { + + var x : [a] bool; + + assume !c[19]; + assert !c[17]; + + x := e; + x[true] := false; + x[17] := true; + + assert !x[true]; + assert !(forall y:t :: x[y]); + assert x != e; + + assert f[x] == x; + assert f[17] > 17; // should not be provable + +} + +type ref; +const null : ref; -- cgit v1.2.3