jlamp0_Z3,4.6.0_WP.oracle 3.89 KB
Newer Older
1
Weakest Precondition
2
bench/ce/jlamp0.mlw M VC p1: Timeout or Unknown
3 4
Counter-example model:File jlamp0.mlw:
Line 6:
5
a, [[@introduced]] = {"type" : "Integer" ,
6
"val" : "0" }
7
Line 8:
8
b, [[@introduced]] = {"type" : "Integer" ,
Sylvain Dailler's avatar
Sylvain Dailler committed
9
"val" : "3" }
10
Line 11:
11
a, [[@introduced]] = {"type" : "Integer" ,
12
"val" : "3" }
13
Line 12:
14
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
15
"val" : "3" }
16

17
bench/ce/jlamp0.mlw M VC p1: Timeout or Unknown
18 19
Counter-example model:File jlamp0.mlw:
Line 6:
20
a, [[@introduced]] = {"type" : "Integer" ,
21 22
"val" : "7" }
Line 8:
23
b, [[@introduced]] = {"type" : "Integer" ,
24 25
"val" : "3" }
Line 10:
26 27 28
a, [] = {"type" : "Integer" , "val" : "9" }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Integer" ,
29 30
"val" : "9" }
Line 11:
31
a, [[@introduced]] = {"type" : "Integer" ,
32
"val" : "10" }
33 34 35
Line 13:
a, [] = {"type" : "Integer" ,
"val" : "9" }
36

37
bench/ce/jlamp0.mlw M VC p1: Timeout or Unknown
38 39
Counter-example model:File jlamp0.mlw:
Line 6:
40
a, [[@introduced]] = {"type" : "Integer" ,
41 42
"val" : "2" }
Line 8:
43
b, [[@introduced]] = {"type" : "Integer" ,
44 45
"val" : "3" }
Line 10:
46 47 48
a, [] = {"type" : "Integer" , "val" : "5" }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Integer" ,
49
"val" : "5" }
50 51 52
Line 11:
a, [] = {"type" : "Integer" ,
"val" : "5" }
53

54
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
55 56
Counter-example model:File jlamp0.mlw:
Line 6:
57
a, [[@introduced]] = {"type" : "Integer" ,
58
"val" : "0" }
59
Line 20:
60
c, [[@introduced]] = {"type" : "Integer" ,
61
"val" : "1" }
62
Line 22:
63
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
64 65
"val" : "1" }

66
bench/ce/jlamp0.mlw M VC p2: Valid
67
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
68 69 70 71 72
Counter-example model:File ref.mlw:
Line 18:
c, [] = {"type" : "Integer" ,
"val" : "2" }
File jlamp0.mlw:
73
Line 6:
74
a, [[@introduced]] = {"type" : "Integer" ,
75
"val" : "0" }
76
Line 20:
77
c, [[@introduced]] = {"type" : "Integer" ,
78
"val" : "1" }
79
Line 21:
80 81 82
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "3" }
c, [] = {"type" : "Integer" , "val" : "2" }
83 84 85 86 87
c, [[@introduced],
[@model_trace:c]] = {"type" : "Integer" ,
"val" : "4" }
Line 24:
c, [] = {"type" : "Integer" ,
88
"val" : "4" }
89
Line 25:
90
a, [[@introduced]] = {"type" : "Integer" ,
91
"val" : "5" }
92 93 94
Line 26:
c, [] = {"type" : "Integer" ,
"val" : "4" }
95

96
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
97 98 99 100 101
Counter-example model:File ref.mlw:
Line 18:
c, [] = {"type" : "Integer" ,
"val" : "10" }
File jlamp0.mlw:
102
Line 6:
103
a, [[@introduced]] = {"type" : "Integer" ,
104
"val" : "0" }
105
Line 20:
106
c, [[@introduced]] = {"type" : "Integer" ,
107
"val" : "1" }
108
Line 21:
109
a, [[@introduced]] = {"type" : "Integer" ,
110
"val" : "3" }
111 112
c, [] = {"type" : "Integer" ,
"val" : "10" }
113
Line 22:
114
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
115
"val" : "12" }
116
Line 25:
117
a, [[@introduced]] = {"type" : "Integer" ,
118
"val" : "13" }
119
Line 26:
120
c, [[@introduced]] = {"type" : "Integer" ,
121 122
"val" : "12" }

123
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
124 125 126 127 128
Counter-example model:File ref.mlw:
Line 18:
c, [] = {"type" : "Integer" ,
"val" : "2" }
File jlamp0.mlw:
129
Line 6:
130
a, [[@introduced]] = {"type" : "Integer" ,
131
"val" : "0" }
132
Line 20:
133
c, [[@introduced]] = {"type" : "Integer" ,
134
"val" : "1" }
135
Line 21:
136
a, [[@introduced]] = {"type" : "Integer" ,
137
"val" : "9" }
138 139
c, [] = {"type" : "Integer" ,
"val" : "2" }
140
Line 23:
141
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
142
"val" : "11" }
143
Line 25:
144
a, [[@introduced]] = {"type" : "Integer" ,
145
"val" : "11" }
146
Line 26:
147
c, [[@introduced]] = {"type" : "Integer" ,
148 149
"val" : "4" }

150
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
151 152 153 154 155
Counter-example model:File ref.mlw:
Line 18:
c, [] = {"type" : "Integer" ,
"val" : "11" }
File jlamp0.mlw:
156
Line 6:
157
a, [[@introduced]] = {"type" : "Integer" ,
158
"val" : "0" }
159
Line 19:
160 161 162
a, [] = {"type" : "Integer" , "val" : "3" }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Integer" ,
163
"val" : "3" }
164
Line 20:
165
c, [[@introduced]] = {"type" : "Integer" ,
166
"val" : "1" }
167 168 169 170
Line 21:
a, [] = {"type" : "Integer" , "val" : "3" }
c, [] = {"type" : "Integer" ,
"val" : "11" }
171