Commit 336a4782 authored by Sylvain Dailler's avatar Sylvain Dailler

Update session, ce-bench and coq files for "VC" -> "vc" in goal name

parent c292a2c1
Strongest Postcondition
bench/ce/array_mono.mlw Array array'VC: Valid
bench/ce/array_mono.mlw A f1'VC: Timeout or Unknown
bench/ce/array_mono.mlw Array array'vc: Valid
bench/ce/array_mono.mlw A f1'vc: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 16:
......@@ -22,8 +22,8 @@ File array_mono.mlw:
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
bench/ce/array_mono.mlw A f2'VC: Valid
bench/ce/array_mono.mlw A f2'VC: Timeout or Unknown
bench/ce/array_mono.mlw A f2'vc: Valid
bench/ce/array_mono.mlw A f2'vc: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 25:
......
Weakest Precondition
bench/ce/array_mono.mlw Array array'VC: Valid
bench/ce/array_mono.mlw A f1'VC: Timeout or Unknown
bench/ce/array_mono.mlw Array array'vc: Valid
bench/ce/array_mono.mlw A f1'vc: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 16:
......@@ -22,8 +22,8 @@ File array_mono.mlw:
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
bench/ce/array_mono.mlw A f2'VC: Valid
bench/ce/array_mono.mlw A f2'VC: Timeout or Unknown
bench/ce/array_mono.mlw A f2'vc: Valid
bench/ce/array_mono.mlw A f2'vc: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 25:
......
Strongest Postcondition
bench/ce/array_mono.mlw Array array'VC: Valid
bench/ce/array_mono.mlw A f1'VC: Timeout or Unknown
bench/ce/array_mono.mlw Array array'vc: Valid
bench/ce/array_mono.mlw A f1'vc: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 16:
......@@ -13,8 +13,8 @@ File array_mono.mlw:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "length" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } }
bench/ce/array_mono.mlw A f2'VC: Valid
bench/ce/array_mono.mlw A f2'VC: Timeout or Unknown
bench/ce/array_mono.mlw A f2'vc: Valid
bench/ce/array_mono.mlw A f2'vc: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 25:
......
Weakest Precondition
bench/ce/array_mono.mlw Array array'VC: Valid
bench/ce/array_mono.mlw A f1'VC: Timeout or Unknown
bench/ce/array_mono.mlw Array array'vc: Valid
bench/ce/array_mono.mlw A f1'vc: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 16:
......@@ -13,8 +13,8 @@ File array_mono.mlw:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "length" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } }
bench/ce/array_mono.mlw A f2'VC: Valid
bench/ce/array_mono.mlw A f2'VC: Timeout or Unknown
bench/ce/array_mono.mlw A f2'vc: Valid
bench/ce/array_mono.mlw A f2'vc: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 25:
......
Strongest Postcondition
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -8,7 +8,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -17,7 +17,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -26,7 +26,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -35,7 +35,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -44,7 +44,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -53,7 +53,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -62,7 +62,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -71,7 +71,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -80,7 +80,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -89,7 +89,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -98,7 +98,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -107,7 +107,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -116,7 +116,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......
Weakest Precondition
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -8,7 +8,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -17,7 +17,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -26,7 +26,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -35,7 +35,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -44,7 +44,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -53,7 +53,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -62,7 +62,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -71,7 +71,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -80,7 +80,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -89,7 +89,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -98,7 +98,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -107,7 +107,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -116,7 +116,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......
Strongest Postcondition
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -8,7 +8,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -17,7 +17,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -26,7 +26,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -35,7 +35,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -44,7 +44,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -53,7 +53,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -62,7 +62,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -71,7 +71,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -80,7 +80,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -89,7 +89,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -98,7 +98,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -107,7 +107,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -116,7 +116,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "2" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......
Weakest Precondition
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -8,7 +8,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -17,7 +17,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -26,7 +26,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -35,7 +35,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -44,7 +44,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -53,7 +53,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -62,7 +62,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -71,7 +71,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -80,7 +80,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -89,7 +89,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -98,7 +98,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -107,7 +107,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......@@ -116,7 +116,7 @@ File array_records.mlw:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "2" }
bench/ce/array_records.mlw Array_records var_overwrite'VC: Timeout or Unknown
bench/ce/array_records.mlw Array_records var_overwrite'vc: Timeout or Unknown
Counter-example model:
File array_records.mlw:
Line 23:
......
Strongest Postcondition
bench/ce/arrays.mlw A f1'VC: Timeout or Unknown
bench/ce/arrays.mlw A f2'VC: Valid
bench/ce/arrays.mlw A f2'VC: Timeout or Unknown
bench/ce/arrays.mlw B f1'VC: Timeout or Unknown
bench/ce/arrays.mlw B f2'VC: Timeout or Unknown
bench/ce/arrays.mlw A f1'vc: Timeout or Unknown
bench/ce/arrays.mlw A f2'vc: Valid
bench/ce/arrays.mlw A f2'vc: Timeout or Unknown
bench/ce/arrays.mlw B f1'vc: Timeout or Unknown
bench/ce/arrays.mlw B f2'vc: Timeout or Unknown
Weakest Precondition
bench/ce/arrays.mlw A f1'VC: Timeout or Unknown
bench/ce/arrays.mlw A f2'VC: Valid
bench/ce/arrays.mlw A f2'VC: Timeout or Unknown
bench/ce/arrays.mlw B f1'VC: Timeout or Unknown
bench/ce/arrays.mlw B f2'VC: Timeout or Unknown
bench/ce/arrays.mlw A f1'vc: Timeout or Unknown
bench/ce/arrays.mlw A f2'vc: Valid
bench/ce/arrays.mlw A f2'vc: Timeout or Unknown
bench/ce/arrays.mlw B f1'vc: Timeout or Unknown
bench/ce/arrays.mlw B f2'vc: Timeout or Unknown
Strongest Postcondition
bench/ce/arrays.mlw A f1'VC: Timeout or Unknown
bench/ce/arrays.mlw A f2'VC: Valid