1 files changed, 0 insertions, 191 deletions
diff --git a/Test/test20/Answer b/Test/test20/Answer
deleted file mode 100644
index 7e7af57b..00000000
--- a/Test/test20/Answer
+++ /dev/null
@@ -1,191 +0,0 @@
-TypeDecls0.bpl(22,5): Error: more than one declaration of type name: C
-TypeDecls0.bpl(15,12): Error: more than one declaration of type variable: a
-TypeDecls0.bpl(16,18): Error: more than one declaration of type variable: a
-TypeDecls0.bpl(20,17): Error: type variable must occur in map arguments: b
-TypeDecls0.bpl(24,9): Error: type constructor received wrong number of arguments: C
-TypeDecls0.bpl(26,9): Error: undeclared type: A0
-TypeDecls0.bpl(27,9): Error: undeclared type: F
-TypeDecls0.bpl(30,9): Error: type constructor received wrong number of arguments: E
-TypeDecls0.bpl(32,9): Error: type constructor received wrong number of arguments: E
-TypeDecls0.bpl(34,9): Error: type constructor received wrong number of arguments: E
-TypeDecls0.bpl(40,11): Error: type constructor received wrong number of arguments: E
-TypeDecls0.bpl(40,13): Error: type constructor received wrong number of arguments: E
-12 name resolution errors detected in TypeDecls0.bpl
-TypeDecls1.bpl(9,13): Error: invalid type for argument 0 in map select: int (expected: <b>[b]a)
-TypeDecls1.bpl(15,25): Error: right-hand side in map store with wrong type: int (expected: bool)
-TypeDecls1.bpl(21,36): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
-TypeDecls1.bpl(23,13): Error: invalid type for argument 0 in map select: <a>[<b>[b]a]bool (expected: <b>[b]a)
-4 type checking errors detected in TypeDecls1.bpl
-Prog0.bpl(19,10): Error: type variable must occur in map arguments: a
-Prog0.bpl(31,27): Error: more than one declaration of type variable: beta
-Prog0.bpl(34,22): Error: undeclared type: alpha
-Prog0.bpl(35,35): Error: undeclared type: alpha
-4 name resolution errors detected in Prog0.bpl
-Prog1.bpl(20,11): Error: invalid type for argument 0 in map select: int (expected: ref)
-Prog1.bpl(21,14): Error: invalid type for argument 1 in map select: int (expected: Field a)
-Prog1.bpl(22,17): Error: invalid argument types (bool and int) to binary operator >=
-3 type checking errors detected in Prog1.bpl
-Prog2.bpl(8,14): Error: trigger does not mention alpha, which does not occur in variables types either
-1 type checking errors detected in Prog2.bpl
-PolyFuns0.bpl(25,33): Error: invalid type for argument 1 in application of fieldValue: ref (expected: Field a)
-PolyFuns0.bpl(42,18): Error: invalid type for argument 1 in application of lessThan: bool (expected: a)
-PolyFuns0.bpl(43,43): Error: invalid type for argument 1 in application of lessThan: b (expected: a)
-PolyFuns0.bpl(55,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
-4 type checking errors detected in PolyFuns0.bpl
-PolyFuns1.bpl(12,9): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)
-PolyFuns1.bpl(13,9): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
-PolyFuns1.bpl(14,31): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)
-PolyFuns1.bpl(15,31): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
-PolyFuns1.bpl(19,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
-PolyFuns1.bpl(20,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
-PolyFuns1.bpl(30,11): Error: invalid type for argument 0 in call to Uhu: <dd>[Field dd]dd (expected: <c>[Field c]a)
-PolyFuns1.bpl(31,15): Error: invalid type for argument 1 in call to Uhu: <cc>[Field cc]T (expected: <d>[Field d]d)
-PolyFuns1.bpl(32,12): Error: invalid argument types (<cc>[Field cc]T and <dd>[Field dd]dd) to binary operator ==
-PolyFuns1.bpl(33,12): Error: invalid argument types (<dd>[Field dd]dd and <cc>[Field cc]T) to binary operator ==
-PolyFuns1.bpl(35,15): Error: invalid type for argument 1 in call to Uhu: <ee>[Field T]ee (expected: <d>[Field d]d)
-PolyFuns1.bpl(43,11): Error: invalid argument types (<a>[a,a]int and <b>[b,int]int) to binary operator ==
-PolyFuns1.bpl(44,11): Error: invalid argument types (<b>[b,int]int and <c>[int,c]int) to binary operator ==
-PolyFuns1.bpl(45,11): Error: invalid argument types (<a>[a,a]int and <c>[int,c]int) to binary operator ==
-PolyFuns1.bpl(52,11): Error: invalid argument types (<a,b>[a,a,b]int and <a,b>[a,b,b]int) to binary operator ==
-PolyFuns1.bpl(59,54): Error: invalid argument types (Field b and NagainCtor b) to binary operator ==
-16 type checking errors detected in PolyFuns1.bpl
-PolyProcs0.bpl(13,16): Error: invalid type for argument 0 in map select: Field b (expected: ref)
-PolyProcs0.bpl(13,19): Error: invalid type for argument 1 in map select: ref (expected: Field a)
-PolyProcs0.bpl(23,30): Error: invalid type for argument 1 in call to FieldAccess: Field int (expected: ref)
-PolyProcs0.bpl(23,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)
-PolyProcs0.bpl(27,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int)
-PolyProcs0.bpl(28,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)
-6 type checking errors detected in PolyProcs0.bpl
-TypeSynonyms0.bpl(13,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)
-TypeSynonyms0.bpl(14,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)
-TypeSynonyms0.bpl(16,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)
-TypeSynonyms0.bpl(26,10): Error: type constructor received wrong number of arguments: Field
-TypeSynonyms0.bpl(27,10): Error: type synonym received wrong number of arguments: Set
-TypeSynonyms0.bpl(30,10): Error: type variable must occur in map arguments: a
-6 name resolution errors detected in TypeSynonyms0.bpl
-TypeSynonyms1.bpl(48,8): Error: invalid type for argument 0 in application of h: <b>[b,b,<b2>[b2,b,int]int]int (expected: nested2)
-1 type checking errors detected in TypeSynonyms1.bpl
-
-Boogie program verifier finished with 1 verified, 0 errors
-
-type Set a = [a]bool;
-
-type Field _;
-
-type Heap = <a>[ref,Field a]a;
-
-type notAllParams a b = Field b;
-
-type Cyclic0 = Cyclic1;
-
-type Cyclic1 = Cyclic0;
-
-type AlsoCyclic a = <b>[AlsoCyclic b]int;
-
-type C _ _;
-
-type C2 b a = C a b;
-
-function f(C int bool) : int;
-
-const x: C2 bool int;
-
-const y: Field int bool;
-
-const z: Set int bool;
-
-const d: <a,b>[notAllParams a b]int;
-
-type ref;
-<console>(10,-1): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)
-<console>(12,-1): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)
-<console>(14,-1): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)
-<console>(24,8): Error: type constructor received wrong number of arguments: Field
-<console>(26,8): Error: type synonym received wrong number of arguments: Set
-<console>(28,8): Error: type variable must occur in map arguments: a
-6 name resolution errors detected in TypeSynonyms0.bpl
-
-type Set a = [a]bool;
-
-function union<a>(x: Set a, y: Set a) : Set a;
-
-axiom (forall<a> x: Set a, y: Set a, z: a :: (x[z] || y[z]) == union(x, y)[z]);
-
-const intSet0: Set int;
-
-axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3));
-
-const intSet1: Set int;
-
-axiom (forall x: int :: intSet1[x] == (x == -5 || x == 3));
-
-procedure P();
-
-
-
-implementation P()
-{
-    assert (forall x: int :: union(intSet0, intSet1)[x] == (x == -5 || x == 0 || x == 2 || x == 3));
-}
-
-
-
-type Set a = [a]bool;
-
-function union<a>(x: Set a, y: Set a) : Set a;
-
-axiom (forall<a> x: Set a, y: Set a, z: a :: x[z] || y[z] <==> union(x, y)[z]);
-
-const intSet0: Set int;
-
-axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3);
-
-const intSet1: Set int;
-
-axiom (forall x: int :: intSet1[x] <==> x == -5 || x == 3);
-
-procedure P();
-
-
-
-implementation P()
-{
-    assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == -5 || x == 0 || x == 2 || x == 3);
-}
-
-
-
-Boogie program verifier finished with 0 verified, 0 errors
-PolyPolyPoly.bpl(14,26): Error: invalid argument types ([]? and <a>[]C a) to binary operator ==
-PolyPolyPoly.bpl(17,23): Error: invalid argument types ([]? and <a>[]C a) to binary operator ==
-PolyPolyPoly.bpl(23,57): Error: invalid type for argument 1 in map select: b (expected: a)
-3 type checking errors detected in PolyPolyPoly.bpl
-PolyPolyPoly2.bpl(7,8): Warning: type parameter a is ambiguous, instantiating to int
-PolyPolyPoly2.bpl(9,8): Warning: type parameter a is ambiguous, instantiating to <arg0,res>[arg0]res
-PolyPolyPoly2.bpl(13,8): Warning: type parameter a is ambiguous, instantiating to bv0
-PolyPolyPoly2.bpl(13,15): Warning: type parameter a is ambiguous, instantiating to bv0
-PolyPolyPoly2.bpl(13,27): Warning: type parameter a is ambiguous, instantiating to bv17
-PolyPolyPoly2.bpl(14,8): Warning: type parameter a is ambiguous, instantiating to bv17
-PolyPolyPoly2.bpl(14,15): Warning: type parameter a is ambiguous, instantiating to bv0
-PolyPolyPoly2.bpl(24,7): Warning: type parameter a is ambiguous, instantiating to int
-PolyPolyPoly2.bpl(33,3): Warning: type parameter a is ambiguous, instantiating to int
-PolyPolyPoly2.bpl(34,3): Warning: type parameter a is ambiguous, instantiating to int
-
-Boogie program verifier finished with 0 verified, 0 errors
-ProcParamReordering.bpl(15,15): Error: mismatched type of in-parameter in implementation P: y (named b in implementation)
-ProcParamReordering.bpl(17,15): Error: mismatched number of type parameters in procedure implementation: P
-2 type checking errors detected in ProcParamReordering.bpl
-ParallelAssignment.bpl(19,2): Error: mismatched types in assignment command (cannot assign bool to int)
-ParallelAssignment.bpl(20,4): Error: invalid type for argument 0 in map assignment: bool (expected: int)
-ParallelAssignment.bpl(22,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: z
-3 type checking errors detected in ParallelAssignment.bpl
-ParallelAssignment2.bpl(11,7): Error: number of left-hand sides does not match number of right-hand sides
-ParallelAssignment2.bpl(12,9): Error: variable a is assigned more than once in parallel assignment
-2 name resolution errors detected in ParallelAssignment2.bpl
-Coercions.bpl(13,8): Error: int cannot be coerced to E <a>[a]int
-Coercions.bpl(15,8): Error: C cannot be coerced to D
-Coercions.bpl(17,9): Error: int cannot be coerced to D
-Coercions.bpl(18,9): Error: int cannot be coerced to E int
-4 type checking errors detected in Coercions.bpl
-
-Boogie program verifier finished with 0 verified, 0 errors