-
Notifications
You must be signed in to change notification settings - Fork 0
/
dl-vcgen.html
70 lines (69 loc) · 13.4 KB
/
dl-vcgen.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
<h1>Why3 Proof Results for Project "dl-vcgen"</h1>
<h2><span style="color:#008000">Theory "dl-vcgen.FOLformulas": fully verified</span></h2>
<table border="1" style="border-collapse:collapse"><tr><td colspan="1">Obligations</td><td text-rotation="90">CVC4 1.8</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">VC for toFOL</td><td style="background-color:#C0FFC0">0.63</td></tr>
</table>
<h2><span style="color:#008000">Theory "dl-vcgen.VCGenDL": fully verified</span></h2>
<table border="1" style="border-collapse:collapse"><tr><td colspan="3">Obligations</td><td text-rotation="90">Alt-Ergo 2.4.0</td><td text-rotation="90">CVC4 1.8</td><td text-rotation="90">Z3 4.8.6</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">VC for singletonFOL</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.09</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">VC for addFOL</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.14</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">VC for vcgen</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="3">split_vc</td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td></tr>
<tr><td rowspan="57" style="width:1ex"></td><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.09</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.07</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.10</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.12</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.09</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.11</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.11</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.12</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.09</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.15</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.09</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.04</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.12</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.09</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.12</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.11</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.08</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.10</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.03</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.07</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.10</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">variant decrease</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.07</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">precondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.07</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">split_vc</td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td></tr>
<tr><td rowspan="9" style="width:1ex"></td><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.44</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#C0FFC0">0.60</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#C0FFC0">0.85</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#C0FFC0">2.16</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.42</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#C0FFC0">0.98</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#C0FFC0">3.01</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#C0FFC0">0.29</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">postcondition</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#E0E0E0">---</td><td style="background-color:#C0FFC0">0.09</td></tr>
</table>