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

ce: Remove duplicates of counterexamples

parent 4a7da0b8
......@@ -2,9 +2,6 @@ Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
......
......@@ -2,9 +2,6 @@ Weakest Precondition
bench/ce/algebraic_type.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
......
......@@ -2,9 +2,6 @@ Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
......@@ -33,12 +30,12 @@ Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "17" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "156" },
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "165" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "154" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "152" },
"list" : [{"type" : "Integer" , "val" : "163" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "161" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "150" }, {"type" : "Apply" ,
"list" : [{"type" : "Integer" , "val" : "159" }, {"type" : "Apply" ,
"val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
......
......@@ -2,9 +2,6 @@ Weakest Precondition
bench/ce/algebraic_type.mlw M G: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
x, [[@introduced]] = {"type" : "Integer" ,
"val" : "0" }
......@@ -33,12 +30,12 @@ Counter-example model:File algebraic_type.mlw:
Line 25:
l, [[@introduced]] = {"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "17" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "156" },
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "164" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "154" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "152" },
"list" : [{"type" : "Integer" , "val" : "162" }, {"type" : "Apply" ,
"val" : {"apply" : "Cons" , "list" : [{"type" : "Integer" , "val" : "160" },
{"type" : "Apply" , "val" : {"apply" : "Cons" ,
"list" : [{"type" : "Integer" , "val" : "150" }, {"type" : "Apply" ,
"list" : [{"type" : "Integer" , "val" : "158" }, {"type" : "Apply" ,
"val" : {"apply" : "Nil" ,
"list" : [] } }] } }] } }] } }] } }] } }
......
......@@ -49,11 +49,6 @@ x, [[@introduced], [@field:0:contents],
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]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
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]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -61,11 +56,6 @@ x, [[@introduced], [@field:0:contents],
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]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
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]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -97,11 +87,6 @@ x, [[@introduced], [@field:0:contents],
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]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "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],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -109,11 +94,6 @@ x, [[@introduced], [@field:0:contents],
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]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "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],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......
......@@ -49,11 +49,6 @@ x, [[@introduced], [@field:0:contents],
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]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
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]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -61,11 +56,6 @@ x, [[@introduced], [@field:0:contents],
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]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "42" } }] } }
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]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -97,11 +87,6 @@ x, [[@introduced], [@field:0:contents],
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]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "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],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -109,11 +94,6 @@ x, [[@introduced], [@field:0:contents],
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]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "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],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......
......@@ -10,12 +10,8 @@ r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"value" : {"type" : "Integer" ,
"val" : "22" } } }] } }
Line 8:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "84" } } }] } }
r, [[@introduced],
[@field:0:contents], [@model_trace:r]] = {"type" : "Record" ,
r, [[@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......
......@@ -10,12 +10,8 @@ r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"value" : {"type" : "Integer" ,
"val" : "22" } } }] } }
Line 8:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "84" } } }] } }
r, [[@introduced],
[@field:0:contents], [@model_trace:r]] = {"type" : "Record" ,
r, [[@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......
......@@ -10,12 +10,8 @@ r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"value" : {"type" : "Integer" ,
"val" : "22" } } }] } }
Line 8:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "84" } } }] } }
r, [[@introduced],
[@field:0:contents], [@model_trace:r]] = {"type" : "Record" ,
r, [[@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......
......@@ -10,12 +10,8 @@ r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"value" : {"type" : "Integer" ,
"val" : "22" } } }] } }
Line 8:
r, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "84" } } }] } }
r, [[@introduced],
[@field:0:contents], [@model_trace:r]] = {"type" : "Record" ,
r, [[@introduced], [@field:0:contents],
[@model_trace:r]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"proj_name" : "int32qtint" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
......
......@@ -30,9 +30,6 @@ b, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
Line 10:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "9" } }] } }
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -82,10 +79,6 @@ Line 21:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
c, [[@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
c, [[@introduced], [@field:0:contents],
[@model_trace:c]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -172,9 +165,6 @@ c, [[@introduced],
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 23:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "9" } }] } }
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -200,9 +190,6 @@ a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 19:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......
......@@ -30,9 +30,6 @@ b, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
Line 10:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "9" } }] } }
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -57,9 +54,6 @@ b, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
Line 10:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "5" } }] } }
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -105,10 +99,6 @@ Line 21:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
c, [[@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
c, [[@introduced], [@field:0:contents],
[@model_trace:c]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -212,9 +202,6 @@ a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 19:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......
......@@ -30,9 +30,6 @@ b, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
Line 10:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "9" } }] } }
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -82,10 +79,6 @@ Line 21:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
c, [[@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
c, [[@introduced], [@field:0:contents],
[@model_trace:c]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -172,9 +165,6 @@ c, [[@introduced],
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 23:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "9" } }] } }
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -200,9 +190,6 @@ a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 19:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......
......@@ -30,9 +30,6 @@ b, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
Line 10:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "9" } }] } }
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -57,9 +54,6 @@ b, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
Line 10:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "5" } }] } }
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -105,10 +99,6 @@ Line 21:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
c, [[@introduced],
[@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "2" } }] } }
c, [[@introduced], [@field:0:contents],
[@model_trace:c]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......@@ -212,9 +202,6 @@ a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "0" } }] } }
Line 19:
a, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
"val" : "3" } }] } }
a, [[@introduced], [@field:0:contents],
[@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Integer" ,
......
......@@ -33,11 +33,8 @@ a, [[@introduced],
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 21:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
a, [[@introduced],
[@model_trace:a]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -64,11 +61,8 @@ a, [[@introduced],
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 27:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
a, [[@introduced],
[@model_trace:a]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......
......@@ -33,11 +33,8 @@ a, [[@introduced],
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 21:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
a, [[@introduced],
[@model_trace:a]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......@@ -64,11 +61,8 @@ a, [[@introduced],
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
Line 27:
a, [[@introduced]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
a, [[@introduced],
[@model_trace:a]] = {"proj_name" : "to_int1" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
a, [[@introduced], [@model_trace:a]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
three, [[@model_trace:three]] = {"proj_name" : "to_int1" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
......
......@@ -18,12 +18,6 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
Line 17:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......
......@@ -18,12 +18,6 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
Line 17:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] } }
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......
......@@ -18,12 +18,6 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
Line 17:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......
......@@ -18,12 +18,6 @@ x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
Line 17:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "3" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] } }] } }
x, [[@introduced], [@field:0:contents],
[@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Array" ,
......
......@@ -17,18 +17,8 @@ Line 14:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "1" }
y, [[@introduced], [@field:0:cont_four_attr],
[@field:1:contents], [@field:2:cont_two],
[@field:3:cont_one_attr]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "cont_four_attr" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "cont_two" ,
"value" : {"type" : "Record" ,
"val" : {"Field" : [{"field" : "cont_one_attr" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }] } } }] } } }] } } }] } }
y, [[@introduced],
[@field:0:cont_four_attr], [@field:1:contents], [@field:2:cont_two],
[@field:3:cont_one_attr], [@model_trace:y]] = {"type" : "Record" ,
[@field:1:contents], [@field:2:cont_two], [@field:3:cont_one_attr],
[@model_trace:y]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "cont_four_attr" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "cont_two" ,
......
......@@ -17,18 +17,8 @@ Line 14:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "1" }
y, [[@introduced], [@field:0:cont_four_attr],
[@field:1:contents], [@field:2:cont_two],
[@field:3:cont_one_attr]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "cont_four_attr" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "cont_two" ,
"value" : {"type" : "Record" ,
"val" : {"Field" : [{"field" : "cont_one_attr" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }] } } }] } } }] } } }] } }
y, [[@introduced],
[@field:0:cont_four_attr], [@field:1:contents], [@field:2:cont_two],
[@field:3:cont_one_attr], [@model_trace:y]] = {"type" : "Record" ,
[@field:1:contents], [@field:2:cont_two], [@field:3:cont_one_attr],
[@model_trace:y]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "cont_four_attr" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "cont_two" ,
......
......@@ -18,18 +18,8 @@ Line 14:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "6030" }
y, [[@introduced], [@field:0:cont_four_attr],
[@field:1:contents], [@field:2:cont_two],
[@field:3:cont_one_attr]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "cont_four_attr" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "cont_two" ,
"value" : {"type" : "Record" ,
"val" : {"Field" : [{"field" : "cont_one_attr" ,
"value" : {"type" : "Integer" ,
"val" : "-53" } }] } } }] } } }] } } }] } }
y, [[@introduced],
[@field:0:cont_four_attr], [@field:1:contents], [@field:2:cont_two],
[@field:3:cont_one_attr], [@model_trace:y]] = {"type" : "Record" ,
[@field:1:contents], [@field:2:cont_two], [@field:3:cont_one_attr],
[@model_trace:y]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "cont_four_attr" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "cont_two" ,
......
......@@ -18,18 +18,8 @@ Line 14:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "6030" }
y, [[@introduced], [@field:0:cont_four_attr],
[@field:1:contents], [@field:2:cont_two],
[@field:3:cont_one_attr]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "cont_four_attr" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "cont_two" ,
"value" : {"type" : "Record" ,
"val" : {"Field" : [{"field" : "cont_one_attr" ,
"value" : {"type" : "Integer" ,
"val" : "-53" } }] } } }] } } }] } } }] } }
y, [[@introduced],
[@field:0:cont_four_attr], [@field:1:contents], [@field:2:cont_two],
[@field:3:cont_one_attr], [@model_trace:y]] = {"type" : "Record" ,
[@field:1:contents], [@field:2:cont_two], [@field:3:cont_one_attr],
[@model_trace:y]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "cont_four_attr" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Record" , "val" : {"Field" : [{"field" : "cont_two" ,
......
......@@ -88,13 +88,10 @@ x23, [[@introduced],
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
Line 42:
x23, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x23, [[@introduced],
[@model_trace:x23]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x23 at 'Old, [[@introduced],
[@at:'Old], [@model_trace:x23],
x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
......
......@@ -88,13 +88,10 @@ x23, [[@introduced],
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
Line 42:
x23, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x23, [[@introduced],
[@model_trace:x23]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x23 at 'Old, [[@introduced],
[@at:'Old], [@model_trace:x23],
x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
......
......@@ -88,13 +88,10 @@ x23, [[@introduced],
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
Line 42:
x23, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x23, [[@introduced],
[@model_trace:x23]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x23 at 'Old, [[@introduced],
[@at:'Old], [@model_trace:x23],
x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
......
......@@ -88,13 +88,10 @@ x23, [[@introduced],
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
Line 42:
x23, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x23, [[@introduced],
[@model_trace:x23]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x23 at 'Old, [[@introduced],
[@at:'Old], [@model_trace:x23],
x23, [[@introduced], [@model_trace:x23]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "2" } }
x23 at 'Old, [[@introduced], [@at:'Old], [@model_trace:x23],
[@at:'Old:loc:location] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" ,
"val" : "0" } }
......
......@@ -214,12 +214,7 @@ x, [[@introduced]] = {"type" : "Record" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 78:
x, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" , "val" : false } }] } }
x, [[@introduced],
[@model_trace:x]] = {"type" : "Record" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
......
......@@ -214,12 +214,7 @@ x, [[@introduced]] = {"type" : "Record" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 78:
x, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" , "val" : false } }] } }
x, [[@introduced],
[@model_trace:x]] = {"type" : "Record" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
......
......@@ -189,12 +189,7 @@ x, [[@introduced]] = {"type" : "Record" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 78:
x, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" , "val" : false } }] } }
x, [[@introduced],
[@model_trace:x]] = {"type" : "Record" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
......
......@@ -189,12 +189,7 @@ x, [[@introduced]] = {"type" : "Record" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
Line 78:
x, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" , "val" : false } }] } }
x, [[@introduced],
[@model_trace:x]] = {"type" : "Record" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : ".my_field_f" ,
"value" : {"type" : "Integer" , "val" : "6" } }, {"field" : "g" ,
"value" : {"type" : "Boolean" ,
......
......@@ -117,12 +117,7 @@ x, [[@introduced]] = {"type" : "Record" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }