jlamp_array_CVC4,1.5_SP.oracle 3.57 KB
Newer Older
1 2 3 4
Strongest Postcondition
bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
5
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
6 7 8
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
9 10
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
11
"val" : "3" } }
12 13 14
Line 18:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
15 16 17 18 19 20 21 22
Line 22:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }

bench/ce/jlamp_array.mlw Array VC f: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
23
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
24 25 26
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
27
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
28
"value" : {"type" : "Integer" , "val" : "3" } }
29
Line 18:
30
a, [[@introduced],
31 32 33 34 35
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 21:
Sylvain Dailler's avatar
Sylvain Dailler committed
36 37 38 39 40
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
a, [[@introduced],
[@model_trace:a]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
41 42 43
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
44
"val" : "3" } }
45 46 47 48
Line 22:
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
49 50 51 52 53

bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
Counter-example model:File jlamp_array.mlw:
Line 11:
54
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
55 56 57
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
58
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
59
"value" : {"type" : "Integer" , "val" : "3" } }
60
Line 24:
61
a, [[@introduced],
62 63 64 65 66
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 27:
Sylvain Dailler's avatar
Sylvain Dailler committed
67 68 69 70 71
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
a, [[@introduced],
[@model_trace:a]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
72 73 74
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
75
"val" : "3" } }
76 77 78 79
Line 28:
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
80 81 82

bench/ce/jlamp_array.mlw Array VC h: Valid
bench/ce/jlamp_array.mlw Array VC h: Timeout or Unknown
Sylvain Dailler's avatar
Sylvain Dailler committed
83 84 85 86 87 88
Counter-example model:File array.mlw:
Line 32:
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
File jlamp_array.mlw:
89
Line 11:
90
two, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
91 92 93
"value" : {"type" : "Integer" ,
"val" : "2" } }
Line 14:
94
three, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
95
"value" : {"type" : "Integer" , "val" : "3" } }
96
Line 30:
97
a, [[@introduced],
98 99 100 101 102
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 33:
Sylvain Dailler's avatar
Sylvain Dailler committed
103
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
104 105 106 107
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
108
"val" : "3" } }
109 110 111 112
Line 34:
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
113