diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-28 16:32:14 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-28 16:32:14 +0100 |
| commit | 08e1dc93d185e221b65bd59ccc167526937ee4d4 (patch) | |
| tree | 5af0f9ea8cc49a34adc45e63f5b1ba4326fc2a13 /Test/prover | |
| parent | 68bb2d0882069c9468e7e36c78a0eef710b7c677 (diff) | |
Removed old test infrastructure files except for
./AbsHoudini/
./doomed/
./z3api/
./test17/
because their conversion to lit incomplete.
Diffstat (limited to 'Test/prover')
| -rw-r--r-- | Test/prover/Answer | 50 | ||||
| -rw-r--r-- | Test/prover/runtest.bat | 13 |
2 files changed, 0 insertions, 63 deletions
diff --git a/Test/prover/Answer b/Test/prover/Answer deleted file mode 100644 index 9d972092..00000000 --- a/Test/prover/Answer +++ /dev/null @@ -1,50 +0,0 @@ -==================== -z3multipleErrors ========================
-
--------------------- z3mutl.bpl --------------------
-z3mutl.bpl(22,5): Error BP5001: This assertion might not hold.
-Execution trace:
- z3mutl.bpl(7,1): start
- z3mutl.bpl(10,1): L1
- z3mutl.bpl(22,1): L5
-z3mutl.bpl(22,5): Error BP5001: This assertion might not hold.
-Execution trace:
- z3mutl.bpl(7,1): start
- z3mutl.bpl(13,1): L2
- z3mutl.bpl(22,1): L5
-z3mutl.bpl(22,5): Error BP5001: This assertion might not hold.
-Execution trace:
- z3mutl.bpl(7,1): start
- z3mutl.bpl(16,1): L3
- z3mutl.bpl(22,1): L5
-
-Boogie program verifier finished with 0 verified, 3 errors
-
--------------------- EQ_v2.Eval__v4.Eval_out.bpl --------------------
-EQ_v2.Eval__v4.Eval_out.bpl(2103,5): Error BP5003: A postcondition might not hold on this return path.
-EQ_v2.Eval__v4.Eval_out.bpl(1717,3): Related location: This is the postcondition that might not hold.
-Execution trace:
- EQ_v2.Eval__v4.Eval_out.bpl(1788,3): AA_INSTR_EQ_BODY
- EQ_v2.Eval__v4.Eval_out.bpl(1864,3): inline$v2.Eval$0$label_11_case_2#2
- EQ_v2.Eval__v4.Eval_out.bpl(1896,3): inline$v2.Eval$0$label_12#2
- EQ_v2.Eval__v4.Eval_out.bpl(1991,3): inline$v4.Eval$0$label_11_case_2#2
- EQ_v2.Eval__v4.Eval_out.bpl(2013,3): inline$v4.Eval$0$label_14_true#2
- EQ_v2.Eval__v4.Eval_out.bpl(2083,3): inline$v4.Eval$0$label_12#2
-EQ_v2.Eval__v4.Eval_out.bpl(2103,5): Error BP5003: A postcondition might not hold on this return path.
-EQ_v2.Eval__v4.Eval_out.bpl(1717,3): Related location: This is the postcondition that might not hold.
-Execution trace:
- EQ_v2.Eval__v4.Eval_out.bpl(1788,3): AA_INSTR_EQ_BODY
- EQ_v2.Eval__v4.Eval_out.bpl(1877,3): inline$v2.Eval$0$label_11_case_1#2
- EQ_v2.Eval__v4.Eval_out.bpl(1896,3): inline$v2.Eval$0$label_12#2
- EQ_v2.Eval__v4.Eval_out.bpl(2034,3): inline$v4.Eval$0$label_11_case_1#2
- EQ_v2.Eval__v4.Eval_out.bpl(2056,3): inline$v4.Eval$0$label_13_true#2
- EQ_v2.Eval__v4.Eval_out.bpl(2083,3): inline$v4.Eval$0$label_12#2
-EQ_v2.Eval__v4.Eval_out.bpl(2154,5): Error BP5003: A postcondition might not hold on this return path.
-EQ_v2.Eval__v4.Eval_out.bpl(2122,3): Related location: This is the postcondition that might not hold.
-Execution trace:
- EQ_v2.Eval__v4.Eval_out.bpl(2135,3): AA_INSTR_EQ_BODY
-EQ_v2.Eval__v4.Eval_out.bpl(2194,5): Error BP5003: A postcondition might not hold on this return path.
-EQ_v2.Eval__v4.Eval_out.bpl(2169,3): Related location: This is the postcondition that might not hold.
-Execution trace:
- EQ_v2.Eval__v4.Eval_out.bpl(2180,3): AA_INSTR_EQ_BODY
-
-Boogie program verifier finished with 6 verified, 4 errors
diff --git a/Test/prover/runtest.bat b/Test/prover/runtest.bat deleted file mode 100644 index b9b64190..00000000 --- a/Test/prover/runtest.bat +++ /dev/null @@ -1,13 +0,0 @@ -@echo off
-setlocal
-
-set BGEXE=..\..\Binaries\Boogie.exe
-rem set BGEXE=mono ..\..\Binaries\Boogie.exe
-
-echo ==================== -z3multipleErrors ========================
-for %%f in (z3mutl.bpl EQ_v2.Eval__v4.Eval_out.bpl) do (
- echo.
- echo -------------------- %%f --------------------
- %BGEXE% -typeEncoding:m -z3multipleErrors %* %%f
-)
-
|