array_records_CVC4,1.5_SP.oracle 8.47 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 66 67
"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:
68
a, [[@introduced],
69 70 71 72 73
[@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" ,
74 75 76
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
77 78
"val" : "-1" }
Line 28:
79 80 81 82 83 84 85 86
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@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" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Record" ,
87 88 89 90 91 92 93 94 95 96 97
"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:
98
a, [[@introduced],
99 100 101 102 103
[@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" ,
104 105 106
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
107 108
"val" : "-1" }
Line 28:
109 110 111 112 113 114 115 116
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@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" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Record" ,
117 118 119 120 121 122 123 124 125 126 127
"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:
128
a, [[@introduced],
129 130 131 132 133
[@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" ,
134 135 136
"value" : {"type" : "Integer" ,
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
137 138
"val" : "-1" }
Line 28:
139 140 141 142 143 144 145 146
a at 'Old, [[@introduced], [@at:'Old], [@model_trace:a],
[@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" ,
"value" : {"type" : "Integer" , "val" : "5" } }] } }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Record" ,
147 148 149 150 151 152 153 154 155 156 157
"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:
158
i, [[@introduced]] = {"type" : "Integer" ,
159 160 161 162 163 164 165 166
"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:
167
i, [[@introduced]] = {"type" : "Integer" ,
168 169 170 171 172 173 174 175
"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:
176
i, [[@introduced]] = {"type" : "Integer" ,
177 178 179 180 181 182 183 184
"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:
185
i, [[@introduced]] = {"type" : "Integer" ,
186 187 188 189 190 191 192 193
"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:
194
i, [[@introduced]] = {"type" : "Integer" ,
195 196 197 198 199 200 201 202
"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:
203
i, [[@introduced]] = {"type" : "Integer" ,
204 205 206 207 208 209 210 211
"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:
212
i, [[@introduced]] = {"type" : "Integer" ,
213 214 215 216 217 218 219 220
"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:
221
i, [[@introduced]] = {"type" : "Integer" ,
222 223 224 225 226
"val" : "0" }
Line 25:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }