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/Maps2.bpl | 62 +++++++++++++++++++++++++-------------------------- 1 file changed, 31 insertions(+), 31 deletions(-) (limited to 'Test/test21/Maps2.bpl') diff --git a/Test/test21/Maps2.bpl b/Test/test21/Maps2.bpl index 0b7980c7..9713875f 100644 --- a/Test/test21/Maps2.bpl +++ b/Test/test21/Maps2.bpl @@ -1,31 +1,31 @@ -// 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" -// XFAIL: * - -type T; - -function f(x : [T][int]int) returns (int); - -axiom (forall x:[T][int]int :: {f(x)} - (exists t:T :: x[t][13] == 42) ==> f(x) == 5); - -procedure P() returns () { - var x : [T][int]int, t : T; - - x[t] := x[t][13 := 42]; - - assert f(x) == 5; -} - - -type name; - -function Field(int) returns (name); -function Unified([name][int]int) returns ([int]int); - -axiom(forall M:[name][int]int, x:int, y:int :: {Unified(M[Field(x) := M[Field(x)][x := y]])} - Unified(M[Field(x) := M[Field(x)][x := y]]) == Unified(M)[x := y]); +// 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" +// XFAIL: * + +type T; + +function f(x : [T][int]int) returns (int); + +axiom (forall x:[T][int]int :: {f(x)} + (exists t:T :: x[t][13] == 42) ==> f(x) == 5); + +procedure P() returns () { + var x : [T][int]int, t : T; + + x[t] := x[t][13 := 42]; + + assert f(x) == 5; +} + + +type name; + +function Field(int) returns (name); +function Unified([name][int]int) returns ([int]int); + +axiom(forall M:[name][int]int, x:int, y:int :: {Unified(M[Field(x) := M[Field(x)][x := y]])} + Unified(M[Field(x) := M[Field(x)][x := y]]) == Unified(M)[x := y]); -- cgit v1.2.3