array_mono_CVC4,1.5_SP.oracle 3.07 KB
Newer Older
1 2 3 4
Strongest Postcondition
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 29 30 31 32 33
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Sylvain Dailler's avatar
Sylvain Dailler committed
34 35 36 37 38
a, [] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
39 40 41 42 43 44 45 46
"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" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
Sylvain Dailler's avatar
Sylvain Dailler committed
47 48
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
49
Line 40:
Sylvain Dailler's avatar
Sylvain Dailler committed
50
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
51 52 53 54 55 56
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
57 58 59 60 61 62 63 64
Line 41:
a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
65