array_records_CVC4,1.5_SP.oracle 8.88 KB
Newer Older
1 2 3 4
Strongest Postcondition
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
5
a, [[@introduced]] = {"type" : "Record" ,
6 7 8
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
9 10 11
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
12 13 14 15 16 17 18 19 20 21 22 23 24 25
"val" : "-1" }
Line 27:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
i, [[@introduced],
[@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
26
a, [[@introduced]] = {"type" : "Record" ,
27 28 29
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
30 31 32
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
33 34 35 36 37 38 39 40 41 42 43 44 45 46
"val" : "-1" }
Line 27:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
i, [[@introduced],
[@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
47
a, [[@introduced]] = {"type" : "Record" ,
48 49 50
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
51 52 53
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
54 55 56 57 58 59 60 61 62 63 64 65
"val" : "-1" }
Line 27:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
i, [[@introduced],
[@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Sylvain Dailler's avatar
Sylvain Dailler committed
66 67 68 69 70 71 72 73
Counter-example model:File array.mlw:
Line 23:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
File array_records.mlw:
74
Line 23:
75
a, [[@introduced],
76 77 78 79 80
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
81 82 83
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
84
"val" : "-1" }
85 86 87 88 89 90
Line 27:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
91
Line 28:
Sylvain Dailler's avatar
Sylvain Dailler committed
92
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
93 94 95 96 97 98 99 100 101
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
i, [[@introduced],
[@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Sylvain Dailler's avatar
Sylvain Dailler committed
102 103 104 105 106 107 108 109
Counter-example model:File array.mlw:
Line 23:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
File array_records.mlw:
110
Line 23:
111
a, [[@introduced],
112 113 114 115 116
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
117 118 119
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
120
"val" : "-1" }
121 122 123 124 125 126
Line 27:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
127
Line 28:
Sylvain Dailler's avatar
Sylvain Dailler committed
128
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
129 130 131 132 133 134 135 136 137 138 139
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
i, [[@introduced],
[@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
140
a, [[@introduced],
141 142 143 144 145
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
146 147 148
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
149
"val" : "-1" }
Sylvain Dailler's avatar
Sylvain Dailler committed
150 151
Line 27:
a, [[@introduced]] = {"type" : "Record" ,
152 153 154
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
Sylvain Dailler's avatar
Sylvain Dailler committed
155 156 157 158
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
Line 28:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
159 160 161 162 163 164 165 166 167 168 169
"val" : {"Field" : [{"field" : "first_value" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"field" : "flag" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"field" : "second_value" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
i, [[@introduced],
[@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
170
i, [[@introduced]] = {"type" : "Integer" ,
171 172 173 174 175 176 177 178
"val" : "-1" }
Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
179
i, [[@introduced]] = {"type" : "Integer" ,
180 181 182 183 184 185 186 187
"val" : "-1" }
Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
188
i, [[@introduced]] = {"type" : "Integer" ,
189 190 191 192 193 194 195 196
"val" : "-1" }
Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
197
i, [[@introduced]] = {"type" : "Integer" ,
198 199 200 201 202 203 204 205
"val" : "-1" }
Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
206
i, [[@introduced]] = {"type" : "Integer" ,
207 208 209 210 211 212 213 214
"val" : "-1" }
Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
215
i, [[@introduced]] = {"type" : "Integer" ,
216 217 218 219 220 221 222 223
"val" : "-1" }
Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
224
i, [[@introduced]] = {"type" : "Integer" ,
225 226 227 228 229 230 231 232
"val" : "0" }
Line 31:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }

bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
233
i, [[@introduced]] = {"type" : "Integer" ,
234 235 236 237 238
"val" : "0" }
Line 25:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }