Commit 9d25d06b authored by Sylvain Dailler's avatar Sylvain Dailler

ce: Prefer concrete counterexample projections assignment over defaults

parent 5e7ddfba
......@@ -34,11 +34,11 @@ Line 25:
l, [[@introduced], [@model_trace:l]] = {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "17" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "164" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "162" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "160" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "158" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "156" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "154" },
{"type" : "Apply" , "val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
......
......@@ -23,9 +23,8 @@ a, [[@introduced], [@model_trace:a],
[@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" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
......
......@@ -23,9 +23,8 @@ a, [[@introduced], [@model_trace:a],
[@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" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : [{"others" : {"type" : "Integer" , "val" : "4" } }] } },
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
......
......@@ -10,5 +10,5 @@ r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
Line 8:
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
"val" : "84" } }
......@@ -10,13 +10,13 @@ r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
Line 8:
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
"val" : "84" } }
Line 9:
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
"val" : "42" } }
Line 10:
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "22" } }
"val" : "84" } }
......@@ -6,7 +6,7 @@ Counter-example model:File int32.mlw:
Line 6:
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
"val" : "22" } }
Line 8:
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......
......@@ -6,7 +6,7 @@ Counter-example model:File int32.mlw:
Line 6:
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
"val" : "22" } }
Line 8:
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -14,7 +14,7 @@ r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
Line 9:
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "84" } }
"val" : "42" } }
Line 10:
r, [[@introduced], [@model_trace:r]] = {"proj_name" : "int32qtint" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......
......@@ -7,7 +7,7 @@ two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 18:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -25,7 +25,7 @@ two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 18:
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
......@@ -38,7 +38,7 @@ a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Timeout or Unknown
......@@ -49,7 +49,7 @@ two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 24:
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
......@@ -62,7 +62,7 @@ a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
bench/ce/jlamp_array.mlw Array VC h: Valid
bench/ce/jlamp_array.mlw Array VC h: Timeout or Unknown
......@@ -73,7 +73,7 @@ two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 30:
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
......@@ -86,5 +86,5 @@ a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
......@@ -7,7 +7,7 @@ two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 18:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -25,7 +25,7 @@ two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 18:
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
......@@ -38,7 +38,7 @@ a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
Line 22:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -53,7 +53,7 @@ two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 24:
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
......@@ -66,7 +66,7 @@ a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
Line 28:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -81,7 +81,7 @@ two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
"value" : {"type" : "Integer" , "val" : "3" } }
Line 30:
a, [[@introduced], [@model_trace:a],
[@at:'Old:loc:location],
......@@ -94,7 +94,7 @@ a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "3" } }
Line 34:
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......
......@@ -4,7 +4,7 @@ Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......@@ -17,7 +17,7 @@ Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......@@ -33,7 +33,7 @@ Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......@@ -49,7 +49,7 @@ Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......
......@@ -4,7 +4,7 @@ Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......@@ -17,7 +17,7 @@ Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......@@ -33,7 +33,7 @@ Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......@@ -49,7 +49,7 @@ Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
Line 14:
three, [[@model_trace:three]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......
......@@ -30,7 +30,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "42" } }
"val" : "0" } }
Line 31:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "43" }
......@@ -41,7 +41,7 @@ y at 'Old, [[@introduced],
[@model_trace:y], [@at:'Old],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "42" } }
"val" : "0" } }
bench/ce/record_one_field.mlw M VC incr: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
......@@ -49,12 +49,12 @@ Line 39:
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "1" } }
Line 41:
x23, [[@introduced], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 42:
x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -62,11 +62,11 @@ x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "1" } }
bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
......@@ -74,18 +74,18 @@ Line 39:
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 49:
x, [[@introduced], [@model_trace:x],
[@at:'Old:loc:location],
[@at:L:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 56:
x at L, [[@introduced], [@model_trace:x], [@at:L],
[@at:L:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
x at M, [[@introduced], [@model_trace:x], [@at:M],
[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -102,26 +102,26 @@ Line 39:
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "0" } }
Line 49:
x, [[@introduced], [@model_trace:x],
[@at:'Old:loc:location],
[@at:L:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "0" } }
Line 56:
x at L, [[@introduced], [@model_trace:x], [@at:L],
[@at:L:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "0" } }
x at M, [[@introduced], [@model_trace:x], [@at:M],
[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
x, [[@introduced],
[@model_trace:x]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
......@@ -129,7 +129,7 @@ Line 39:
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "-2" } }
"val" : "0" } }
Line 49:
x, [[@introduced], [@model_trace:x],
[@at:'Old:loc:location],
......@@ -140,7 +140,7 @@ x, [[@introduced], [@model_trace:x],
Line 50:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "-2" } }
"val" : "0" } }
x at 'Old, [[@introduced], [@model_trace:x], [@at:'Old],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......
......@@ -34,7 +34,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "42" } }
"val" : "0" } }
Line 31:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "43" }
......@@ -45,7 +45,7 @@ y at 'Old, [[@introduced],
[@model_trace:y], [@at:'Old],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "42" } }
"val" : "0" } }
Line 33:
y, [[@introduced], [@model_trace:y]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -57,12 +57,12 @@ Line 39:
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "1" } }
Line 41:
x23, [[@introduced], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 42:
x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -70,11 +70,11 @@ x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "1" } }
Line 45:
y, [[@introduced], [@model_trace:y]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -82,7 +82,7 @@ y, [[@introduced], [@model_trace:y]] = {"proj_name" : "contents" ,
Line 46:
x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "1" } }
Line 47:
x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -94,13 +94,13 @@ Line 39:
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 49:
x, [[@introduced], [@model_trace:x],
[@at:'Old:loc:location],
[@at:L:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 53:
x, [[@introduced], [@model_trace:x],
[@at:M:loc:location] = {"proj_name" : "contents" ,
......@@ -109,12 +109,12 @@ x, [[@introduced], [@model_trace:x],
y, [[@introduced],
[@model_trace:y]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 56:
x at L, [[@introduced], [@model_trace:x], [@at:L],
[@at:L:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
x at M, [[@introduced], [@model_trace:x], [@at:M],
[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -131,21 +131,21 @@ Line 39:
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "0" } }
Line 49:
x, [[@introduced], [@model_trace:x],
[@at:'Old:loc:location],
[@at:L:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "0" } }
Line 53:
x, [[@introduced], [@model_trace:x],
[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
y, [[@introduced],
[@model_trace:y]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
"value" : {"type" : "Integer" , "val" : "0" } }
Line 55:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -154,18 +154,18 @@ Line 56:
x at L, [[@introduced], [@model_trace:x], [@at:L],
[@at:L:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "0" } }
x at M, [[@introduced], [@model_trace:x], [@at:M],
[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
x, [[@introduced],
[@model_trace:x]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
"value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "3" } }
"val" : "2" } }
bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
......@@ -173,7 +173,7 @@ Line 39:
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "-2" } }
"val" : "0" } }
Line 49:
x, [[@introduced], [@model_trace:x],
[@at:'Old:loc:location],
......@@ -184,7 +184,7 @@ x, [[@introduced], [@model_trace:x],
Line 50:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "-2" } }
"val" : "0" } }
x at 'Old, [[@introduced], [@model_trace:x], [@at:'Old],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -193,12 +193,12 @@ Line 53:
x, [[@introduced], [@model_trace:x],
[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "-2" } }
"val" : "0" } }
y, [[@introduced],
[@model_trace:y]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "-2" } }
"value" : {"type" : "Integer" , "val" : "0" } }
Line 55:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "-2" } }
"val" : "0" } }
......@@ -36,7 +36,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "43" }
y, [[@introduced],
[@model_trace:y]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "0" } }
"value" : {"type" : "Integer" , "val" : "42" } }
y at 'Old, [[@introduced],
[@model_trace:y], [@at:'Old],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
......@@ -49,7 +49,7 @@ Line 39:
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "1" } }
Line 41:
x23, [[@introduced], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
......@@ -58,7 +58,7 @@ x23, [[@introduced], [@model_trace:x23],
Line 42:
x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -66,7 +66,7 @@ x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "1" } }
bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
......@@ -89,11 +89,11 @@ x at L, [[@introduced], [@model_trace:x], [@at:L],
x at M, [[@introduced], [@model_trace:x], [@at:M],
[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
x, [[@introduced],
[@model_trace:x]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
bench/ce/record_one_field.mlw M VC test_loop: Valid
bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
......@@ -117,11 +117,11 @@ x at L, [[@introduced], [@model_trace:x], [@at:L],
x at M, [[@introduced], [@model_trace:x], [@at:M],
[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
x, [[@introduced],
[@model_trace:x]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
......@@ -136,7 +136,7 @@ x, [[@introduced], [@model_trace:x],
[@at:L:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "-2" } }
Line 50:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -144,5 +144,5 @@ x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
x at 'Old, [[@introduced], [@model_trace:x], [@at:'Old],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "-2" } }
......@@ -40,7 +40,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "43" }
y, [[@introduced],
[@model_trace:y]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "0" } }
"value" : {"type" : "Integer" , "val" : "42" } }
y at 'Old, [[@introduced],
[@model_trace:y], [@at:'Old],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
......@@ -49,7 +49,7 @@ y at 'Old, [[@introduced],
Line 33:
y, [[@introduced], [@model_trace:y]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "42" } }
bench/ce/record_one_field.mlw M VC incr: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
......@@ -57,7 +57,7 @@ Line 39:
y, [[@introduced], [@model_trace:y],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "1" } }
Line 41:
x23, [[@introduced], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
......@@ -66,7 +66,7 @@ x23, [[@introduced], [@model_trace:x23],
Line 42:
x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -74,19 +74,19 @@ x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
y at 'Old, [[@introduced], [@model_trace:y], [@at:'Old],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "1" } }
Line 45:
y, [[@introduced], [@model_trace:y]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
Line 46:
x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "1" } }
Line 47:
x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
......@@ -105,7 +105,7 @@ Line 53:
x, [[@introduced], [@model_trace:x],
[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
Line 56:
x at L, [[@introduced], [@model_trace:x], [@at:L],
[@at:L:loc:location] = {"proj_name" : "contents" ,
......@@ -114,11 +114,11 @@ x at L, [[@introduced], [@model_trace:x], [@at:L],
x at M, [[@introduced], [@model_trace:x], [@at:M],
[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
x, [[@introduced],
[@model_trace:x]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
bench/ce/record_one_field.mlw M VC test_loop: Valid
bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
......@@ -138,11 +138,11 @@ Line 53:
x, [[@introduced], [@model_trace:x],
[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
Line 55:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "3" } }
Line 56:
x at L, [[@introduced], [@model_trace:x], [@at:L],
[@at:L:loc:location] = {"proj_name" : "contents" ,
......@@ -151,14 +151,14 @@ x at L, [[@introduced], [@model_trace:x], [@at:L],
x at M, [[@introduced], [@model_trace:x], [@at:M],
[@at:M:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
x, [[@introduced],
[@model_trace:x]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "0" } }
"value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
bench/ce/record_one_field.mlw M VC test_loop: Timeout or Unknown
Counter-example model:File record_one_field.mlw:
......@@ -173,7 +173,7 @@ x, [[@introduced], [@model_trace:x],
[@at:L:loc:location],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "-2" } }
Line 50:
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -181,7 +181,7 @@ x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
x at 'Old, [[@introduced], [@model_trace:x], [@at:'Old],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }