Removed old test infrastructure files except for

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

because their conversion to lit incomplete.

2 files changed, 0 insertions, 175 deletions

diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
deleted file mode 100644
index 1d19f568..00000000
--- a/Test/aitest0/Answer
+++ /dev/null
@@ -1,168 +0,0 @@
-var GlobalFlag: bool;

-

-const A: int;

-

-const B: int;

-

-const C: int;

-

-procedure Join(b: bool);

-  modifies GlobalFlag;

-

-

-

-implementation Join(b: bool)

-{

-  var x: int;

-  var y: int;

-  var z: int;

-

-  start:

-    assume {:inferred} true;

-    GlobalFlag := true;

-    x := 3;

-    y := 4;

-    z := x + y;

-    assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7;

-    goto Then, Else;

-

-  Else:

-    assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7;

-    assume b <==> false;

-    y := 4;

-    assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7 && !b;

-    goto join;

-

-  join:

-    assume {:inferred} GlobalFlag && 3 <= x && x < 5 && y == 4 && z == 7;

-    assert y == 4;

-    assert z == 7;

-    assert GlobalFlag <==> true;

-    assume {:inferred} GlobalFlag && 3 <= x && x < 5 && y == 4 && z == 7;

-    return;

-

-  Then:

-    assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7;

-    assume b <==> true;

-    x := x + 1;

-    assume {:inferred} GlobalFlag && x == 4 && y == 4 && z == 7 && b;

-    goto join;

-}

-

-

-

-procedure Loop();

-

-

-

-implementation Loop()

-{

-  var c: int;

-  var i: int;

-

-  start:

-    assume {:inferred} true;

-    c := 0;

-    i := 0;

-    assume {:inferred} c == 0 && i == 0;

-    goto test;

-

-  test:  // cut point

-    assume {:inferred} c == 0 && 0 <= i && i < 11;

-    assume {:inferred} c == 0 && 0 <= i && i < 11;

-    goto Then, Else;

-

-  Else:

-    assume {:inferred} c == 0 && 0 <= i && i < 11;

-    assume {:inferred} c == 0 && 0 <= i && i < 11;

-    return;

-

-  Then:

-    assume {:inferred} c == 0 && 0 <= i && i < 11;

-    assume i < 10;

-    i := i + 1;

-    assume {:inferred} c == 0 && 1 <= i && i < 11;

-    goto test;

-}

-

-

-

-procedure Evaluate();

-

-

-

-implementation Evaluate()

-{

-  var i: int;

-

-  start:

-    assume {:inferred} true;

-    i := 5;

-    i := 3 * i + 1;

-    i := 3 * (i + 1);

-    i := 1 + 3 * i;

-    i := (i + 1) * 3;

-    assume {:inferred} i == 465;

-    return;

-}

-

-

-

-Boogie program verifier finished with 0 verified, 0 errors

-Intervals.bpl(64,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Intervals.bpl(59,5): anon0

-    Intervals.bpl(60,3): anon3_LoopHead

-    Intervals.bpl(60,3): anon3_LoopDone

-Intervals.bpl(75,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Intervals.bpl(70,5): anon0

-    Intervals.bpl(71,3): anon3_LoopHead

-    Intervals.bpl(71,3): anon3_LoopDone

-Intervals.bpl(94,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Intervals.bpl(89,5): anon0

-    Intervals.bpl(90,3): loop_head

-    Intervals.bpl(93,3): after_loop

-Intervals.bpl(140,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Intervals.bpl(135,5): anon0

-    Intervals.bpl(136,3): anon3_LoopHead

-    Intervals.bpl(136,3): anon3_LoopDone

-Intervals.bpl(151,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Intervals.bpl(146,5): anon0

-    Intervals.bpl(147,3): anon3_LoopHead

-    Intervals.bpl(147,3): anon3_LoopDone

-Intervals.bpl(202,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Intervals.bpl(192,8): anon0

-    Intervals.bpl(193,3): anon4_LoopHead

-    Intervals.bpl(193,3): anon4_LoopDone

-Intervals.bpl(240,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Intervals.bpl(235,5): anon0

-    Intervals.bpl(236,3): anon3_LoopHead

-    Intervals.bpl(236,3): anon3_LoopDone

-Intervals.bpl(252,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Intervals.bpl(246,8): anon0

-    Intervals.bpl(247,3): anon3_LoopHead

-    Intervals.bpl(247,3): anon3_LoopDone

-Intervals.bpl(263,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Intervals.bpl(258,5): anon0

-    Intervals.bpl(259,3): anon3_LoopHead

-    Intervals.bpl(259,3): anon3_LoopDone

-Intervals.bpl(285,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Intervals.bpl(280,5): anon0

-    Intervals.bpl(281,3): anon3_LoopHead

-    Intervals.bpl(281,3): anon3_LoopDone

-Intervals.bpl(307,3): Error BP5001: This assertion might not hold.

-Execution trace:

-    Intervals.bpl(302,5): anon0

-    Intervals.bpl(303,3): anon3_LoopHead

-    Intervals.bpl(303,3): anon3_LoopDone

-

-Boogie program verifier finished with 16 verified, 11 errors

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

-setlocal

-

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

-

-%BGEXE% %* -infer:j -instrumentInfer:e -printInstrumented -noVerify constants.bpl

-%BGEXE% %* -infer:j Intervals.bpl