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/test20/TypeSynonyms1.bpl | 98 +++++++++++++++++++++---------------------- 1 file changed, 49 insertions(+), 49 deletions(-) (limited to 'Test/test20/TypeSynonyms1.bpl') diff --git a/Test/test20/TypeSynonyms1.bpl b/Test/test20/TypeSynonyms1.bpl index 98ecedca..9f61335c 100644 --- a/Test/test20/TypeSynonyms1.bpl +++ b/Test/test20/TypeSynonyms1.bpl @@ -1,49 +1,49 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - - - -type C a b; -type C2 b a = C a b; - - -// ordering of map type parameters -function g0([C2 a b]int) returns (int); -function g1([C2 b a]int) returns (int); -function g2([C a b]int) returns (int); -function g3([C b a]int) returns (int); - -const c0 : [C2 a b]int; -const c1 : [C2 b a]int; -const c2 : [C a b]int; -const c3 : [C b a]int; - -axiom g0(c0) == 0; -axiom g1(c0) == 0; -axiom g2(c0) == 0; -axiom g3(c0) == 0; -axiom g0(c1) == 0; -axiom g1(c1) == 0; -axiom g2(c1) == 0; -axiom g3(c1) == 0; -axiom g0(c2) == 0; -axiom g1(c2) == 0; -axiom g2(c2) == 0; -axiom g3(c2) == 0; -axiom g0(c3) == 0; -axiom g1(c3) == 0; -axiom g2(c3) == 0; -axiom g3(c3) == 0; - - -type nested a = [b, b, a]int; -type nested2 = nested (nested int); - - -function h(nested2) returns (bool); -const e : [b, b, [b2, b2, int]int]int; -axiom h(e); - -const e2 : [b, b, [b2, b, int]int]int; // wrong binding -axiom h(e2); - +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + + +type C a b; +type C2 b a = C a b; + + +// ordering of map type parameters +function g0([C2 a b]int) returns (int); +function g1([C2 b a]int) returns (int); +function g2([C a b]int) returns (int); +function g3([C b a]int) returns (int); + +const c0 : [C2 a b]int; +const c1 : [C2 b a]int; +const c2 : [C a b]int; +const c3 : [C b a]int; + +axiom g0(c0) == 0; +axiom g1(c0) == 0; +axiom g2(c0) == 0; +axiom g3(c0) == 0; +axiom g0(c1) == 0; +axiom g1(c1) == 0; +axiom g2(c1) == 0; +axiom g3(c1) == 0; +axiom g0(c2) == 0; +axiom g1(c2) == 0; +axiom g2(c2) == 0; +axiom g3(c2) == 0; +axiom g0(c3) == 0; +axiom g1(c3) == 0; +axiom g2(c3) == 0; +axiom g3(c3) == 0; + + +type nested a = [b, b, a]int; +type nested2 = nested (nested int); + + +function h(nested2) returns (bool); +const e : [b, b, [b2, b2, int]int]int; +axiom h(e); + +const e2 : [b, b, [b2, b, int]int]int; // wrong binding +axiom h(e2); + -- cgit v1.2.3