Removed old test infrastructure files except for

./AbsHoudini/
./doomed/
./z3api/
./test17/

because their conversion to lit incomplete.

2 files changed, 0 insertions, 217 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

diff --git a/Test/test20/runtest.bat b/Test/test20/runtest.bat
deleted file mode 100644
index 0e607a1f..00000000
--- a/Test/test20/runtest.bat
+++ /dev/null
@@ -1,26 +0,0 @@
-@echo off

-setlocal

-

-set BGEXE=..\..\Binaries\Boogie.exe

-rem set BGEXE=mono ..\..\Binaries\Boogie.exe

-

-%BGEXE% %* /noVerify TypeDecls0.bpl

-%BGEXE% %* /noVerify TypeDecls1.bpl

-%BGEXE% %* /noVerify Prog0.bpl

-%BGEXE% %* /noVerify Prog1.bpl

-%BGEXE% %* /noVerify Prog2.bpl

-%BGEXE% %* /noVerify PolyFuns0.bpl

-%BGEXE% %* /noVerify PolyFuns1.bpl

-%BGEXE% %* /noVerify PolyProcs0.bpl

-%BGEXE% %* /noVerify TypeSynonyms0.bpl

-%BGEXE% %* /noVerify TypeSynonyms1.bpl

-%BGEXE% %* TypeSynonyms2.bpl

-%BGEXE% %* /noVerify /print:- /env:0 TypeSynonyms0.bpl

-%BGEXE% %* /noVerify /print:- /env:0 /printDesugared TypeSynonyms2.bpl

-%BGEXE% %* /noVerify PolyPolyPoly.bpl

-%BGEXE% %* /noVerify PolyPolyPoly2.bpl

-%BGEXE% %* /noVerify ProcParamReordering.bpl

-%BGEXE% %* /noVerify ParallelAssignment.bpl

-%BGEXE% %* /noVerify ParallelAssignment2.bpl

-%BGEXE% %* /noVerify Coercions.bpl

-%BGEXE% %* /noVerify EmptySeq.bpl