Commit 5f7c2dc7 authored by Sylvain Dailler's avatar Sylvain Dailler

ce: Add elements correconding to an internal_loc. Remove duplicates.

parent e3d45ea7
Pipeline #54714 passed with stages
in 47 minutes and 24 seconds
......@@ -7,6 +7,11 @@ a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
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" } }] } }
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
......@@ -31,6 +36,14 @@ a, [] = {"type" : "Record" ,
"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" } }] } }
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" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 40:
......@@ -41,4 +54,12 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
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" } }] } }
......@@ -7,6 +7,11 @@ a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
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" } }] } }
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
......@@ -31,6 +36,14 @@ a, [] = {"type" : "Record" ,
"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" } }] } }
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" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 40:
......@@ -41,4 +54,12 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
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" } }] } }
......@@ -7,6 +7,11 @@ a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
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" } }] } }
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
......@@ -28,7 +33,13 @@ 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" ,
"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" ,
"val" : "2" } }] } }
Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
......@@ -37,4 +48,11 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
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" } }] } }
......@@ -7,6 +7,11 @@ a, [] = {"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }, {"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
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" } }] } }
Line 36:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
......@@ -28,7 +33,13 @@ 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" ,
"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" ,
"val" : "2" } }] } }
Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
......@@ -37,4 +48,11 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
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" } }] } }
......@@ -82,6 +82,12 @@ a, [[@introduced],
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
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" } }] } }
Line 28:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
......@@ -112,6 +118,12 @@ a, [[@introduced],
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
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" } }] } }
Line 28:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
......
......@@ -82,6 +82,12 @@ a, [[@introduced],
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
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" } }] } }
Line 28:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
......@@ -112,6 +118,12 @@ a, [[@introduced],
"val" : "5" } }] } }
i, [[@introduced]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
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" } }] } }
Line 28:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "first_value" ,
......
......@@ -27,6 +27,8 @@ Line 18:
x, [] = {"type" : "Integer" ,
"val" : "42" }
File if_assign.mlw:
Line 21:
a, [] = {"type" : "Integer" , "val" : "0" }
Line 22:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
......@@ -53,6 +55,8 @@ Line 18:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 21:
a, [] = {"type" : "Integer" , "val" : "-1" }
Line 22:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
......@@ -75,6 +79,9 @@ Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 30:
a, [] = {"type" : "Integer" ,
"val" : "0" }
Line 34:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
......@@ -90,9 +97,15 @@ Line 20:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 30:
a, [] = {"type" : "Integer" ,
"val" : "-1" }
Line 31:
the check fails with all inputs
Line 34:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
Line 36:
x, [] = {"type" : "Integer" ,
"val" : "18" }
......@@ -27,9 +27,14 @@ Line 18:
x, [] = {"type" : "Integer" ,
"val" : "42" }
File if_assign.mlw:
Line 21:
a, [] = {"type" : "Integer" , "val" : "0" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 25:
x, [] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File int.mlw:
......@@ -41,9 +46,14 @@ Line 18:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 21:
a, [] = {"type" : "Integer" , "val" : "-1" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
Line 27:
x, [] = {"type" : "Integer" ,
"val" : "18" }
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File int.mlw:
......@@ -51,6 +61,9 @@ Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 30:
a, [] = {"type" : "Integer" ,
"val" : "0" }
Line 34:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
......@@ -67,6 +80,12 @@ Line 20:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 30:
a, [] = {"type" : "Integer" ,
"val" : "-1" }
Line 31:
the check fails with all inputs
Line 36:
x, [] = {"type" : "Integer" ,
"val" : "18" }
......@@ -27,6 +27,8 @@ Line 18:
x, [] = {"type" : "Integer" ,
"val" : "42" }
File if_assign.mlw:
Line 21:
a, [] = {"type" : "Integer" , "val" : "0" }
Line 22:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
......@@ -53,6 +55,8 @@ Line 18:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 21:
a, [] = {"type" : "Integer" , "val" : "2" }
Line 22:
x, [[@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw],
......@@ -75,6 +79,9 @@ Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 30:
a, [] = {"type" : "Integer" ,
"val" : "0" }
Line 34:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
......@@ -90,6 +97,12 @@ Line 20:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 30:
a, [] = {"type" : "Integer" ,
"val" : "2" }
Line 31:
the check fails with all inputs
Line 36:
x, [] = {"type" : "Integer" ,
"val" : "18" }
......@@ -27,9 +27,14 @@ Line 18:
x, [] = {"type" : "Integer" ,
"val" : "42" }
File if_assign.mlw:
Line 21:
a, [] = {"type" : "Integer" , "val" : "0" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "42" }
Line 25:
x, [] = {"type" : "Integer" ,
"val" : "42" }
bench/ce/if_assign.mlw Test VC f3: Timeout or Unknown
Counter-example model:File int.mlw:
......@@ -41,9 +46,14 @@ Line 18:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 21:
a, [] = {"type" : "Integer" , "val" : "2" }
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "18" }
Line 27:
x, [] = {"type" : "Integer" ,
"val" : "18" }
bench/ce/if_assign.mlw Test VC f4: Timeout or Unknown
Counter-example model:File int.mlw:
......@@ -51,6 +61,9 @@ Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_assign.mlw:
Line 30:
a, [] = {"type" : "Integer" ,
"val" : "0" }
Line 34:
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "42" }
......@@ -67,6 +80,12 @@ Line 20:
x, [] = {"type" : "Integer" ,
"val" : "18" }
File if_assign.mlw:
Line 30:
a, [] = {"type" : "Integer" ,
"val" : "2" }
Line 31:
the check fails with all inputs
Line 36:
x, [] = {"type" : "Integer" ,
"val" : "18" }
......@@ -6,6 +6,9 @@ Line 16:
a, [] = {"type" : "Integer" ,
"val" : "5" }
File if_decision_branch.mlw:
Line 18:
a, [] = {"type" : "Integer" ,
"val" : "5" }
Line 19:
result, [[@introduced]] = {"type" : "Integer" ,
"val" : "15" }
......
......@@ -6,6 +6,9 @@ Line 16:
a, [] = {"type" : "Integer" ,
"val" : "5" }
File if_decision_branch.mlw:
Line 18:
a, [] = {"type" : "Integer" ,
"val" : "5" }
Line 19:
result, [[@introduced]] = {"type" : "Integer" ,
"val" : "15" }
......
......@@ -6,6 +6,9 @@ Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_decision_branch.mlw:
Line 18:
a, [] = {"type" : "Integer" ,
"val" : "0" }
Line 19:
result, [[@introduced]] = {"type" : "Integer" ,
"val" : "22" }
......
......@@ -6,6 +6,9 @@ Line 16:
a, [] = {"type" : "Integer" ,
"val" : "0" }
File if_decision_branch.mlw:
Line 18:
a, [] = {"type" : "Integer" ,
"val" : "0" }
Line 19:
result, [[@introduced]] = {"type" : "Integer" ,
"val" : "22" }
......
......@@ -18,4 +18,8 @@ Line 9:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } }
Line 10:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } }
......@@ -18,4 +18,8 @@ Line 9:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } }
Line 10:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } }
......@@ -18,4 +18,8 @@ Line 9:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } }
Line 10:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } }
......@@ -18,4 +18,8 @@ Line 9:
r, [[@introduced]] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "42" } }
Line 10:
r, [] = {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "84" } }
......@@ -30,6 +30,9 @@ a, [[@introduced],
Line 11:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "10" }
Line 13:
a, [] = {"type" : "Integer" ,
"val" : "9" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File jlamp0.mlw:
......@@ -57,6 +60,9 @@ Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, [] = {"type" : "Integer" , "val" : "3" }
c, [] = {"type" : "Integer" ,
"val" : "2" }
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "4" }
Line 23:
......@@ -68,6 +74,9 @@ c, [] = {"type" : "Integer" ,
Line 25:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "5" }
Line 26:
c, [] = {"type" : "Integer" ,
"val" : "4" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File ref.mlw:
......@@ -81,6 +90,10 @@ a, [[@introduced]] = {"type" : "Integer" ,
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, [] = {"type" : "Integer" , "val" : "3" }
c, [] = {"type" : "Integer" ,
"val" : "10" }
Line 22:
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "12" }
......@@ -106,6 +119,10 @@ a, [[@introduced]] = {"type" : "Integer" ,
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, [] = {"type" : "Integer" , "val" : "9" }
c, [] = {"type" : "Integer" ,
"val" : "2" }
Line 23:
a, [] = {"type" : "Integer" , "val" : "9" }
a, [[@introduced],
......@@ -135,4 +152,8 @@ a, [[@introduced],
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, [] = {"type" : "Integer" , "val" : "3" }
c, [] = {"type" : "Integer" ,
"val" : "11" }
......@@ -30,6 +30,9 @@ a, [[@introduced],
Line 11:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "10" }
Line 13:
a, [] = {"type" : "Integer" ,
"val" : "9" }
bench/ce/jlamp0.mlw M VC p1: Timeout or Unknown
Counter-example model:File jlamp0.mlw:
......@@ -44,6 +47,9 @@ a, [] = {"type" : "Integer" , "val" : "5" }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Integer" ,
"val" : "5" }
Line 11:
a, [] = {"type" : "Integer" ,
"val" : "5" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File jlamp0.mlw:
......@@ -71,7 +77,9 @@ Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, [[@introduced]] = {"type" : "Integer" , "val" : "3" }
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "3" }
c, [] = {"type" : "Integer" , "val" : "2" }
c, [[@introduced],
[@model_trace:c]] = {"type" : "Integer" ,
"val" : "4" }
......@@ -81,6 +89,9 @@ c, [] = {"type" : "Integer" ,
Line 25:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "5" }
Line 26:
c, [] = {"type" : "Integer" ,
"val" : "4" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File ref.mlw:
......@@ -97,6 +108,8 @@ c, [[@introduced]] = {"type" : "Integer" ,
Line 21:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "3" }
c, [] = {"type" : "Integer" ,
"val" : "10" }
Line 22:
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "12" }
......@@ -122,6 +135,8 @@ c, [[@introduced]] = {"type" : "Integer" ,
Line 21:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "9" }
c, [] = {"type" : "Integer" ,
"val" : "2" }
Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "11" }
......@@ -149,4 +164,8 @@ a, [[@introduced],
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, [] = {"type" : "Integer" , "val" : "3" }
c, [] = {"type" : "Integer" ,
"val" : "11" }
......@@ -30,6 +30,9 @@ a, [[@introduced],
Line 11:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "10" }
Line 13:
a, [] = {"type" : "Integer" ,
"val" : "9" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File jlamp0.mlw:
......@@ -57,6 +60,9 @@ Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, [] = {"type" : "Integer" , "val" : "3" }
c, [] = {"type" : "Integer" ,
"val" : "2" }
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "4" }
Line 23:
......@@ -68,6 +74,9 @@ c, [] = {"type" : "Integer" ,
Line 25:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "5" }
Line 26:
c, [] = {"type" : "Integer" ,
"val" : "4" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File ref.mlw:
......@@ -81,6 +90,10 @@ a, [[@introduced]] = {"type" : "Integer" ,
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, [] = {"type" : "Integer" , "val" : "3" }
c, [] = {"type" : "Integer" ,
"val" : "10" }
Line 22:
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "12" }
......@@ -106,6 +119,10 @@ a, [[@introduced]] = {"type" : "Integer" ,
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, [] = {"type" : "Integer" , "val" : "9" }
c, [] = {"type" : "Integer" ,
"val" : "2" }
Line 23:
a, [] = {"type" : "Integer" , "val" : "9" }
a, [[@introduced],
......@@ -135,4 +152,8 @@ a, [[@introduced],
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, [] = {"type" : "Integer" , "val" : "3" }
c, [] = {"type" : "Integer" ,
"val" : "11" }
......@@ -30,6 +30,9 @@ a, [[@introduced],
Line 11:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "10" }
Line 13:
a, [] = {"type" : "Integer" ,
"val" : "9" }
bench/ce/jlamp0.mlw M VC p1: Timeout or Unknown
Counter-example model:File jlamp0.mlw:
......@@ -44,6 +47,9 @@ a, [] = {"type" : "Integer" , "val" : "5" }
a, [[@introduced],
[@model_trace:a]] = {"type" : "Integer" ,
"val" : "5" }
Line 11:
a, [] = {"type" : "Integer" ,
"val" : "5" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File jlamp0.mlw:
......@@ -71,7 +77,9 @@ Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, [[@introduced]] = {"type" : "Integer" , "val" : "3" }
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "3" }
c, [] = {"type" : "Integer" , "val" : "2" }
c, [[@introduced],
[@model_trace:c]] = {"type" : "Integer" ,
"val" : "4" }
......@@ -81,6 +89,9 @@ c, [] = {"type" : "Integer" ,
Line 25:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "5" }
Line 26:
c, [] = {"type" : "Integer" ,
"val" : "4" }
bench/ce/jlamp0.mlw M VC p2: Timeout or Unknown
Counter-example model:File ref.mlw:
......@@ -97,6 +108,8 @@ c, [[@introduced]] = {"type" : "Integer" ,
Line 21:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "3" }
c, [] = {"type" : "Integer" ,
"val" : "10" }
Line 22:
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "12" }
......@@ -122,6 +135,8 @@ c, [[@introduced]] = {"type" : "Integer" ,
Line 21:
a, [[@introduced]] = {"type" : "Integer" ,
"val" : "9" }
c, [] = {"type" : "Integer" ,
"val" : "2" }
Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "11" }
......@@ -149,4 +164,8 @@ a, [[@introduced],
Line 20:
c, [[@introduced]] = {"type" : "Integer" ,
"val" : "1" }
Line 21:
a, [] = {"type" : "Integer" , "val" : "3" }
c, [] = {"type" : "Integer" ,
"val" : "11" }
......@@ -42,6 +42,10 @@ a, [[@introduced],
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
Line 22:
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
......@@ -69,6 +73,10 @@ a, [[@introduced],
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
Line 28:
a, [] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,