Commit 9712712e authored by Benedikt Becker's avatar Benedikt Becker

Update oracle files

parent 17390b39
......@@ -27,9 +27,8 @@ bench/ce/array_mono.mlw A f2'vc: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 25:
old a, [[@introduced], [@at:'Old],
[@at:'Old:loc:location],
[@at:'Old:loc:location] =
old a,
[[@at:'Old], [@at:'Old:loc:bench/ce/array_mono.mlw:25], [@at:'Old:loc:bench/ce/array_mono.mlw:26], [@introduced]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"indice" : {"type" : "Integer" ,
"val" : "0" } , "value" : {"type" : "Integer" , "val" : "42" } },
......@@ -48,8 +47,8 @@ File array_mono.mlw:
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 38:
a, [[@introduced], [@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location] =
a,
[[@at:'Old], [@at:'Old:loc:bench/ce/array_mono.mlw:25], [@at:'Old:loc:bench/ce/array_mono.mlw:26], [@introduced]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"indice" : {"type" : "Integer" ,
"val" : "0" } , "value" : {"type" : "Integer" , "val" : "42" } },
......
......@@ -27,9 +27,8 @@ bench/ce/array_mono.mlw A f2'vc: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 25:
old a, [[@introduced], [@at:'Old],
[@at:'Old:loc:location],
[@at:'Old:loc:location] =
old a,
[[@at:'Old], [@at:'Old:loc:bench/ce/array_mono.mlw:25], [@at:'Old:loc:bench/ce/array_mono.mlw:26], [@introduced]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"indice" : {"type" : "Integer" ,
"val" : "0" } , "value" : {"type" : "Integer" , "val" : "42" } },
......@@ -48,8 +47,8 @@ File array_mono.mlw:
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 38:
a, [[@introduced], [@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location] =
a,
[[@at:'Old], [@at:'Old:loc:bench/ce/array_mono.mlw:25], [@at:'Old:loc:bench/ce/array_mono.mlw:26], [@introduced]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"indice" : {"type" : "Integer" ,
"val" : "0" } , "value" : {"type" : "Integer" , "val" : "42" } },
......
......@@ -18,9 +18,8 @@ bench/ce/array_mono.mlw A f2'vc: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 25:
old a, [[@introduced], [@at:'Old],
[@at:'Old:loc:location],
[@at:'Old:loc:location] =
old a,
[[@at:'Old], [@at:'Old:loc:bench/ce/array_mono.mlw:25], [@at:'Old:loc:bench/ce/array_mono.mlw:26], [@introduced]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }, {"field" : "length" ,
......@@ -33,8 +32,8 @@ File array_mono.mlw:
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 38:
a, [[@introduced], [@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location] =
a,
[[@at:'Old], [@at:'Old:loc:bench/ce/array_mono.mlw:25], [@at:'Old:loc:bench/ce/array_mono.mlw:26], [@introduced]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }, {"field" : "length" ,
......
......@@ -18,9 +18,8 @@ bench/ce/array_mono.mlw A f2'vc: Timeout or Unknown
Counter-example model:
File array_mono.mlw:
Line 25:
old a, [[@introduced], [@at:'Old],
[@at:'Old:loc:location],
[@at:'Old:loc:location] =
old a,
[[@at:'Old], [@at:'Old:loc:bench/ce/array_mono.mlw:25], [@at:'Old:loc:bench/ce/array_mono.mlw:26], [@introduced]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }, {"field" : "length" ,
......@@ -33,8 +32,8 @@ File array_mono.mlw:
{"field" : "length" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 38:
a, [[@introduced], [@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location] =
a,
[[@at:'Old], [@at:'Old:loc:bench/ce/array_mono.mlw:25], [@at:'Old:loc:bench/ce/array_mono.mlw:26], [@introduced]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "elts" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }, {"field" : "length" ,
......
......@@ -3,20 +3,20 @@ bench/ce/bv32.mlw Ce_int32bv dummy_update'vc: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 7:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "34" } }] } }
Line 9:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] =
r,
[[@field:0:contents], [@introduced], [@mlw:reference_var], [@model_trace:r]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
Line 10:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "66" } }] } }
Line 11:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
......@@ -24,20 +24,20 @@ bench/ce/bv32.mlw Ce_int32bv dummy_update_with_int'vc: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 13:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 15:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] =
r,
[[@field:0:contents], [@introduced], [@mlw:reference_var], [@model_trace:r]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
Line 16:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "66" } }] } }
Line 17:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "4294967295" } }] } }
......@@ -3,20 +3,20 @@ bench/ce/bv32.mlw Ce_int32bv dummy_update'vc: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 7:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "34" } }] } }
Line 9:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] =
r,
[[@field:0:contents], [@introduced], [@mlw:reference_var], [@model_trace:r]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
Line 10:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "66" } }] } }
Line 11:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
......@@ -24,20 +24,20 @@ bench/ce/bv32.mlw Ce_int32bv dummy_update_with_int'vc: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 13:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 15:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] =
r,
[[@field:0:contents], [@introduced], [@mlw:reference_var], [@model_trace:r]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
Line 16:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "66" } }] } }
Line 17:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "4294967295" } }] } }
......@@ -3,20 +3,20 @@ bench/ce/bv32.mlw Ce_int32bv dummy_update'vc: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 7:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "34" } }] } }
Line 9:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] =
r,
[[@field:0:contents], [@introduced], [@mlw:reference_var], [@model_trace:r]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
Line 10:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "66" } }] } }
Line 11:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
......@@ -24,20 +24,20 @@ bench/ce/bv32.mlw Ce_int32bv dummy_update_with_int'vc: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 13:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "34" } }] } }
Line 15:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] =
r,
[[@field:0:contents], [@introduced], [@mlw:reference_var], [@model_trace:r]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
Line 16:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "66" } }] } }
Line 17:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
......@@ -3,20 +3,20 @@ bench/ce/bv32.mlw Ce_int32bv dummy_update'vc: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 7:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "34" } }] } }
Line 9:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] =
r,
[[@field:0:contents], [@introduced], [@mlw:reference_var], [@model_trace:r]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
Line 10:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "66" } }] } }
Line 11:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
......@@ -24,20 +24,20 @@ bench/ce/bv32.mlw Ce_int32bv dummy_update_with_int'vc: Timeout or Unknown
Counter-example model:
File bv32.mlw:
Line 13:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "34" } }] } }
Line 15:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
[@model_trace:r]] =
r,
[[@field:0:contents], [@introduced], [@mlw:reference_var], [@model_trace:r]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
Line 16:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "66" } }] } }
Line 17:
r, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
r, [[@field:0:contents], [@introduced], [@mlw:reference_var]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "132" } }] } }
......@@ -3,11 +3,11 @@ bench/ce/if_assign.mlw Test f'vc: Timeout or Unknown
Counter-example model:
File if_assign.mlw:
Line 10:
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
x, [[@field:0:contents], [@introduced], [@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
Line 12:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
......@@ -15,11 +15,11 @@ bench/ce/if_assign.mlw Test f2'vc: Timeout or Unknown
Counter-example model:
File if_assign.mlw:
Line 16:
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
x, [[@field:0:contents], [@introduced], [@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
......@@ -30,30 +30,26 @@ File int.mlw:
a, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
File ref.mlw:
Line 18:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
x,
[[@field:0:contents], [@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
File if_assign.mlw:
Line 21:
a, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
Line 22:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw], [@model_trace:x]] =
x,
[[@field:0:contents], [@introduced], [@model_trace:x], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
Line 25:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw], [@model_trace:x]] =
x,
[[@field:0:contents], [@introduced], [@model_trace:x], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
Line 27:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw], [@model_trace:x]] =
x,
[[@field:0:contents], [@introduced], [@model_trace:x], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
......@@ -64,30 +60,26 @@ File int.mlw:
a, [[@introduced]] = {"type" : "Integer" , "val" : "-1" }
File ref.mlw:
Line 18:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
x,
[[@field:0:contents], [@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
File if_assign.mlw:
Line 21:
a, [[@introduced]] = {"type" : "Integer" , "val" : "-1" }
Line 22:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw], [@model_trace:x]] =
x,
[[@field:0:contents], [@introduced], [@model_trace:x], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
Line 25:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw], [@model_trace:x]] =
x,
[[@field:0:contents], [@introduced], [@model_trace:x], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
Line 27:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw], [@model_trace:x]] =
x,
[[@field:0:contents], [@introduced], [@model_trace:x], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
......@@ -100,7 +92,7 @@ File if_assign.mlw:
Line 30:
a, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
Line 34:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
......@@ -112,7 +104,7 @@ File int.mlw:
a, [[@introduced]] = {"type" : "Integer" , "val" : "-1" }
File ref.mlw:
Line 20:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
File if_assign.mlw:
......@@ -121,11 +113,11 @@ File if_assign.mlw:
Line 31:
the check fails with all inputs
Line 34:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 36:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
......@@ -3,11 +3,11 @@ bench/ce/if_assign.mlw Test f'vc: Timeout or Unknown
Counter-example model:
File if_assign.mlw:
Line 10:
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
x, [[@field:0:contents], [@introduced], [@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
Line 12:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
......@@ -15,11 +15,11 @@ bench/ce/if_assign.mlw Test f2'vc: Timeout or Unknown
Counter-example model:
File if_assign.mlw:
Line 16:
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
x, [[@field:0:contents], [@introduced], [@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
......@@ -30,18 +30,18 @@ File int.mlw:
a, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
File ref.mlw:
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
File if_assign.mlw:
Line 21:
a, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
Line 22:
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
x, [[@field:0:contents], [@introduced], [@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
Line 25:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
......@@ -52,18 +52,18 @@ File int.mlw:
a, [[@introduced]] = {"type" : "Integer" , "val" : "-1" }
File ref.mlw:
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
File if_assign.mlw:
Line 21:
a, [[@introduced]] = {"type" : "Integer" , "val" : "-1" }
Line 22:
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
x, [[@field:0:contents], [@introduced], [@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
Line 27:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
......@@ -76,7 +76,7 @@ File if_assign.mlw:
Line 30:
a, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
Line 34:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
......@@ -89,7 +89,7 @@ File int.mlw:
a, [[@introduced]] = {"type" : "Integer" , "val" : "-1" }
File ref.mlw:
Line 20:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
File if_assign.mlw:
......@@ -98,7 +98,7 @@ File if_assign.mlw:
Line 31:
the check fails with all inputs
Line 36:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
......@@ -3,11 +3,11 @@ bench/ce/if_assign.mlw Test f'vc: Timeout or Unknown
Counter-example model:
File if_assign.mlw:
Line 10:
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
x, [[@field:0:contents], [@introduced], [@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
Line 12:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
......@@ -15,11 +15,11 @@ bench/ce/if_assign.mlw Test f2'vc: Timeout or Unknown
Counter-example model:
File if_assign.mlw:
Line 16:
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
x, [[@field:0:contents], [@introduced], [@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
Line 18:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
x, [[@field:0:contents], [@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
......@@ -30,30 +30,26 @@ File int.mlw:
a, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
File ref.mlw:
Line 18:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
x,
[[@field:0:contents], [@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
File if_assign.mlw:
Line 21:
a, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
Line 22:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw], [@model_trace:x]] =
x,
[[@field:0:contents], [@introduced], [@model_trace:x], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
Line 25:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw], [@model_trace:x]] =
x,
[[@field:0:contents], [@introduced], [@model_trace:x], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
Line 27:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw], [@model_trace:x]] =
x,
[[@field:0:contents], [@introduced], [@model_trace:x], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "42" } }] } }
......@@ -64,30 +60,26 @@ File int.mlw:
a, [[@introduced]] = {"type" : "Integer" , "val" : "2" }
File ref.mlw:
Line 18:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
x,
[[@field:0:contents], [@introduced], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
File if_assign.mlw:
Line 21:
a, [[@introduced]] = {"type" : "Integer" , "val" : "2" }
Line 22:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw], [@model_trace:x]] =
x,
[[@field:0:contents], [@introduced], [@model_trace:x], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
Line 25:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw], [@model_trace:x]] =
x,
[[@field:0:contents], [@introduced], [@model_trace:x], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
Line 27:
x, [[@introduced], [@field:0:contents],
[@vc:written:25:4:20:bench/ce/if_assign.mlw],
[@vc:written:27:4:11:bench/ce/if_assign.mlw], [@model_trace:x]] =
x,
[[@field:0:contents], [@introduced], [@model_trace:x], [@vc:written:25:4:20:bench/ce/if_assign.mlw], [@vc:written:27:4:11:bench/ce/if_assign.mlw]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "18" } }] } }
......@@ -100,7 +92,7 @@ File if_assign.mlw:
Line 30:
a, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
Line 34: