array_mono_Z3,4.6.0_WP.oracle 2.6 KB
Newer Older
1 2 3 4
Weakest Precondition
bench/ce/array_mono.mlw Array VC array: Valid
bench/ce/array_mono.mlw A VC f1: Timeout or Unknown
Counter-example model:File array_mono.mlw:
5 6 7 8
Line 16:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
9
"val" : "0" } }] } }
10 11 12 13 14
Line 35:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
15 16 17 18 19 20 21 22 23 24
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }

bench/ce/array_mono.mlw A VC f2: Valid
bench/ce/array_mono.mlw A VC f2: Timeout or Unknown
Counter-example model:File array_mono.mlw:
25 26
Line 25:
a at 'Old, [[@at:'Old], [@at:'Old:loc:location],
27 28
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
29 30
"val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
31
"val" : "2" } }] } }
32
a, [] = {"type" : "Record" ,
33 34 35
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
36 37 38 39 40 41 42
"value" : {"type" : "Integer" , "val" : "2" } }] } }
Line 38:
a, [[@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
43
"val" : "2" } }] } }
44
Line 40:
45 46 47 48 49 50
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
51 52 53 54 55 56 57
Line 41:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
58