fix #161 Avoid duplication of model_trace and get the priority of the

model_trace from the model_context when defining a new variable

bench/ce/arrays_CVC4,1.5.oracle

@@ -16,19 +16,19 @@ a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
 "val" : "2" }
 a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
 "val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
-{"others" : {"type" : "Integer" , "val" : "0" } }] }
-a, ["model_trace:a",
-"model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "0" ,
-"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
-"value" : {"type" : "Integer" , "val" : "42" } },
 {"others" : {"type" : "Integer" ,
 "val" : "0" } }] }
-Line 12:
-a, ["model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
+a, ["model_trace:a@call"] = {"type" : "Array" ,
 "val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
 {"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
 {"others" : {"type" : "Integer" ,
 "val" : "0" } }] }
+Line 12:
+a, ["model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "0" ,
+"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
+"value" : {"type" : "Integer" , "val" : "42" } },
+{"others" : {"type" : "Integer" ,
+"val" : "0" } }] }
 
 bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
 Counter-example model:File arrays.mlw:

bench/ce/arrays_Z3,4.6.0.oracle

@@ -16,65 +16,59 @@ a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
 "val" : "2" }
 a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
 "val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
-{"others" : {"type" : "Integer" , "val" : "6" } }] }
-a, ["model_trace:a",
-"model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "0" ,
-"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
-"value" : {"type" : "Integer" , "val" : "42" } },
 {"others" : {"type" : "Integer" ,
 "val" : "6" } }] }
-Line 12:
-a, ["model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
+a, ["model_trace:a@call"] = {"type" : "Array" ,
 "val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
 {"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
 {"others" : {"type" : "Integer" ,
 "val" : "6" } }] }
+Line 12:
+a, ["model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "0" ,
+"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
+"value" : {"type" : "Integer" , "val" : "42" } },
+{"others" : {"type" : "Integer" ,
+"val" : "6" } }] }
 
 bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
 Counter-example model:File arrays.mlw:
 Line 26:
 a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
-"val" : "5874" }
+"val" : "7211" }
 a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
-"val" : [{"indice" : "-1744" , "value" : {"type" : "Integer" ,
-"val" : "-3798" } }, {"indice" : "-309" , "value" : {"type" : "Integer" ,
-"val" : "-13696" } }, {"indice" : "5864" , "value" : {"type" : "Integer" ,
-"val" : "8257" } }, {"indice" : "2" , "value" : {"type" : "Integer" ,
-"val" : "-13696" } }, {"indice" : "5338" , "value" : {"type" : "Integer" ,
-"val" : "-7249" } }, {"indice" : "0" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"indice" : "5466" , "value" : {"type" : "Integer" ,
-"val" : "5876" } }, {"indice" : "-298" , "value" : {"type" : "Integer" ,
-"val" : "1424" } }, {"indice" : "1" , "value" : {"type" : "Integer" ,
-"val" : "-5876" } }, {"indice" : "-1547" , "value" : {"type" : "Integer" ,
-"val" : "-2419" } }, {"indice" : "-1" , "value" : {"type" : "Integer" ,
-"val" : "-5875" } }, {"indice" : "5875" , "value" : {"type" : "Integer" ,
-"val" : "5877" } }, {"indice" : "-299" , "value" : {"type" : "Integer" ,
-"val" : "9873" } }, {"indice" : "-24" , "value" : {"type" : "Integer" ,
-"val" : "8888" } }, {"indice" : "5709" , "value" : {"type" : "Integer" ,
-"val" : "8256" } }, {"indice" : "37" , "value" : {"type" : "Integer" ,
-"val" : "9919" } }, {"others" : {"type" : "Integer" ,
+"val" : [{"indice" : "7212" , "value" : {"type" : "Integer" ,
+"val" : "156" } }, {"indice" : "7209" , "value" : {"type" : "Integer" ,
+"val" : "4075" } }, {"indice" : "3018" , "value" : {"type" : "Integer" ,
+"val" : "4590" } }, {"indice" : "-3777" , "value" : {"type" : "Integer" ,
+"val" : "3082" } }, {"indice" : "5475" , "value" : {"type" : "Integer" ,
+"val" : "5476" } }, {"indice" : "7210" , "value" : {"type" : "Integer" ,
+"val" : "-1736" } }, {"indice" : "3019" , "value" : {"type" : "Integer" ,
+"val" : "4589" } }, {"indice" : "5476" , "value" : {"type" : "Integer" ,
+"val" : "7891" } }, {"indice" : "982" , "value" : {"type" : "Integer" ,
+"val" : "4387" } }, {"indice" : "-24" , "value" : {"type" : "Integer" ,
+"val" : "6774" } }, {"indice" : "7211" , "value" : {"type" : "Integer" ,
+"val" : "155" } }, {"indice" : "13846" , "value" : {"type" : "Integer" ,
+"val" : "154" } }, {"indice" : "7208" , "value" : {"type" : "Integer" ,
+"val" : "5737" } }, {"others" : {"type" : "Integer" ,
 "val" : "4" } }] }
 Line 27:
 old a.length, ["model_trace:a.length@old"] = {"type" : "Integer" ,
-"val" : "5874" }
+"val" : "7211" }
 old a.elts, ["model_trace:a.elts@old"] = {"type" : "Array" ,
-"val" : [{"indice" : "-1744" , "value" : {"type" : "Integer" ,
-"val" : "-3798" } }, {"indice" : "-309" , "value" : {"type" : "Integer" ,
-"val" : "-13696" } }, {"indice" : "5864" , "value" : {"type" : "Integer" ,
-"val" : "8257" } }, {"indice" : "2" , "value" : {"type" : "Integer" ,
-"val" : "-13696" } }, {"indice" : "5338" , "value" : {"type" : "Integer" ,
-"val" : "-7249" } }, {"indice" : "0" , "value" : {"type" : "Integer" ,
-"val" : "-1" } }, {"indice" : "5466" , "value" : {"type" : "Integer" ,
-"val" : "5876" } }, {"indice" : "-298" , "value" : {"type" : "Integer" ,
-"val" : "1424" } }, {"indice" : "1" , "value" : {"type" : "Integer" ,
-"val" : "-5876" } }, {"indice" : "-1547" , "value" : {"type" : "Integer" ,
-"val" : "-2419" } }, {"indice" : "-1" , "value" : {"type" : "Integer" ,
-"val" : "-5875" } }, {"indice" : "5875" , "value" : {"type" : "Integer" ,
-"val" : "5877" } }, {"indice" : "-299" , "value" : {"type" : "Integer" ,
-"val" : "9873" } }, {"indice" : "-24" , "value" : {"type" : "Integer" ,
-"val" : "8888" } }, {"indice" : "5709" , "value" : {"type" : "Integer" ,
-"val" : "8256" } }, {"indice" : "37" , "value" : {"type" : "Integer" ,
-"val" : "9919" } }, {"others" : {"type" : "Integer" ,
+"val" : [{"indice" : "7212" , "value" : {"type" : "Integer" ,
+"val" : "156" } }, {"indice" : "7209" , "value" : {"type" : "Integer" ,
+"val" : "4075" } }, {"indice" : "3018" , "value" : {"type" : "Integer" ,
+"val" : "4590" } }, {"indice" : "-3777" , "value" : {"type" : "Integer" ,
+"val" : "3082" } }, {"indice" : "5475" , "value" : {"type" : "Integer" ,
+"val" : "5476" } }, {"indice" : "7210" , "value" : {"type" : "Integer" ,
+"val" : "-1736" } }, {"indice" : "3019" , "value" : {"type" : "Integer" ,
+"val" : "4589" } }, {"indice" : "5476" , "value" : {"type" : "Integer" ,
+"val" : "7891" } }, {"indice" : "982" , "value" : {"type" : "Integer" ,
+"val" : "4387" } }, {"indice" : "-24" , "value" : {"type" : "Integer" ,
+"val" : "6774" } }, {"indice" : "7211" , "value" : {"type" : "Integer" ,
+"val" : "155" } }, {"indice" : "13846" , "value" : {"type" : "Integer" ,
+"val" : "154" } }, {"indice" : "7208" , "value" : {"type" : "Integer" ,
+"val" : "5737" } }, {"others" : {"type" : "Integer" ,
 "val" : "4" } }] }
 
 bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)

bench/ce/jlamp0_CVC4,1.5.oracle

 bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 8:
 b, ["model_trace:b"] = {"type" : "Integer" ,
@@ -16,7 +16,7 @@ a, ["model_trace:a@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 8:
 b, ["model_trace:b"] = {"type" : "Integer" ,
@@ -34,7 +34,7 @@ a, ["model_trace:a@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 8:
 b, ["model_trace:b"] = {"type" : "Integer" ,
@@ -49,7 +49,7 @@ a, ["model_trace:a@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 20:
 c, ["model_trace:c@call"] = {"type" : "Integer" ,
@@ -61,19 +61,19 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 20:
 c, ["model_trace:c@call"] = {"type" : "Integer" ,
 "val" : "1" }
 Line 23:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 
 bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 20:
 c, ["model_trace:c@call"] = {"type" : "Integer" ,
@@ -96,7 +96,7 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 20:
 c, ["model_trace:c@call"] = {"type" : "Integer" ,
@@ -119,7 +119,7 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 20:
 c, ["model_trace:c@call"] = {"type" : "Integer" ,
@@ -139,7 +139,7 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 19:
 a, ["model_trace:a@loop"] = {"type" : "Integer" ,

bench/ce/jlamp0_Z3,4.6.0.oracle

 bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 8:
 b, ["model_trace:b"] = {"type" : "Integer" ,
@@ -16,7 +16,7 @@ a, ["model_trace:a@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "7" }
 Line 8:
 b, ["model_trace:b"] = {"type" : "Integer" ,
@@ -34,7 +34,7 @@ a, ["model_trace:a@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "2" }
 Line 8:
 b, ["model_trace:b"] = {"type" : "Integer" ,
@@ -49,7 +49,7 @@ a, ["model_trace:a@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 20:
 c, ["model_trace:c@call"] = {"type" : "Integer" ,
@@ -61,19 +61,19 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 20:
 c, ["model_trace:c@call"] = {"type" : "Integer" ,
 "val" : "1" }
 Line 23:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 
 bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 20:
 c, ["model_trace:c@call"] = {"type" : "Integer" ,
@@ -96,7 +96,7 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 20:
 c, ["model_trace:c@call"] = {"type" : "Integer" ,
@@ -119,7 +119,7 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 20:
 c, ["model_trace:c@call"] = {"type" : "Integer" ,
@@ -139,7 +139,7 @@ c, ["model_trace:c@call"] = {"type" : "Integer" ,
 bench/ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
 Counter-example model:File jlamp0.mlw:
 Line 6:
-a, ["model_trace:a", "model_trace:a@init"] = {"type" : "Integer" ,
+a, ["model_trace:a@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 19:
 a, ["model_trace:a@loop"] = {"type" : "Integer" ,

bench/ce/jlamp_array_CVC4,1.5.oracle

@@ -19,14 +19,13 @@ a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
 a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
 "val" : [{"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
-a, ["model_trace:a",
-"model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "42" ,
-"value" : {"type" : "Integer" , "val" : "2" } },
+a, ["model_trace:a@call"] = {"type" : "Array" ,
+"val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "2" } },
 {"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
 Line 21:
-a, ["model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
-"val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "2" } },
+a, ["model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "42" ,
+"value" : {"type" : "Integer" , "val" : "2" } },
 {"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
 
@@ -39,14 +38,13 @@ a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
 a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
 "val" : [{"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
-a, ["model_trace:a",
-"model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "42" ,
-"value" : {"type" : "Integer" , "val" : "2" } },
+a, ["model_trace:a@call"] = {"type" : "Array" ,
+"val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "2" } },
 {"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
 Line 27:
-a, ["model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
-"val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "2" } },
+a, ["model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "42" ,
+"value" : {"type" : "Integer" , "val" : "2" } },
 {"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
 
@@ -59,17 +57,17 @@ a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
 a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
 "val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "2" } },
 {"indice" : "17" , "value" : {"type" : "Integer" , "val" : "3" } },
-{"others" : {"type" : "Integer" , "val" : "2" } }] }
-a, ["model_trace:a",
-"model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "42" ,
-"value" : {"type" : "Integer" , "val" : "2" } },
 {"others" : {"type" : "Integer" ,
 "val" : "2" } }] }
-Line 33:
-a, ["model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
+a, ["model_trace:a@call"] = {"type" : "Array" ,
 "val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "2" } },
 {"others" : {"type" : "Integer" ,
 "val" : "2" } }] }
+Line 33:
+a, ["model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "42" ,
+"value" : {"type" : "Integer" , "val" : "2" } },
+{"others" : {"type" : "Integer" ,
+"val" : "2" } }] }
 
 bench/ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
 Counter-example model:File array.mlw:

bench/ce/jlamp_array_Z3,4.6.0.oracle

@@ -8,8 +8,7 @@ Line 18:
 a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
 "val" : "0" }
 a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
-"val" : [{"indice" : "9" , "value" : {"type" : "Integer" , "val" : "3" } },
-{"others" : {"type" : "Integer" ,
+"val" : [{"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
 
 bench/ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
@@ -19,17 +18,17 @@ a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
 "val" : "43" }
 a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
 "val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "3" } },
-{"others" : {"type" : "Integer" , "val" : "3" } }] }
-a, ["model_trace:a",
-"model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "42" ,
-"value" : {"type" : "Integer" , "val" : "2" } },
 {"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
-Line 21:
-a, ["model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
+a, ["model_trace:a@call"] = {"type" : "Array" ,
 "val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "2" } },
 {"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
+Line 21:
+a, ["model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "42" ,
+"value" : {"type" : "Integer" , "val" : "2" } },
+{"others" : {"type" : "Integer" ,
+"val" : "3" } }] }
 
 bench/ce/jlamp_array.mlw Array WP_parameter g : Valid
 bench/ce/jlamp_array.mlw Array WP_parameter g : Unknown (other)
@@ -39,19 +38,19 @@ a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
 "val" : "43" }
 a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
 "val" : [{"indice" : "17" , "value" : {"type" : "Integer" , "val" : "3" } },
-{"others" : {"type" : "Integer" , "val" : "3" } }] }
-a, ["model_trace:a",
-"model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "42" ,
-"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "17" ,
-"value" : {"type" : "Integer" , "val" : "3" } },
 {"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
-Line 27:
-a, ["model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
+a, ["model_trace:a@call"] = {"type" : "Array" ,
 "val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "2" } },
 {"indice" : "17" , "value" : {"type" : "Integer" , "val" : "3" } },
 {"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
+Line 27:
+a, ["model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "42" ,
+"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "17" ,
+"value" : {"type" : "Integer" , "val" : "3" } },
+{"others" : {"type" : "Integer" ,
+"val" : "3" } }] }
 
 bench/ce/jlamp_array.mlw Array WP_parameter h : Valid
 bench/ce/jlamp_array.mlw Array WP_parameter h : Unknown (other)
@@ -62,19 +61,19 @@ a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
 a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
 "val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "3" } },
 {"indice" : "17" , "value" : {"type" : "Integer" , "val" : "3" } },
-{"others" : {"type" : "Integer" , "val" : "3" } }] }
-a, ["model_trace:a",
-"model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "42" ,
-"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "17" ,
-"value" : {"type" : "Integer" , "val" : "2" } },
 {"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
-Line 33:
-a, ["model_trace:a@call", "model_trace:a@old"] = {"type" : "Array" ,
+a, ["model_trace:a@call"] = {"type" : "Array" ,
 "val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "3" } },
 {"indice" : "17" , "value" : {"type" : "Integer" , "val" : "2" } },
 {"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
+Line 33:
+a, ["model_trace:a@call"] = {"type" : "Array" , "val" : [{"indice" : "42" ,
+"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "17" ,
+"value" : {"type" : "Integer" , "val" : "2" } },
+{"others" : {"type" : "Integer" ,
+"val" : "3" } }] }
 
 bench/ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
 Counter-example model:File array.mlw:
@@ -86,8 +85,7 @@ Line 18:
 a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
 "val" : "0" }
 a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
-"val" : [{"indice" : "9" , "value" : {"type" : "Integer" , "val" : "3" } },
-{"others" : {"type" : "Integer" ,
+"val" : [{"others" : {"type" : "Integer" ,
 "val" : "3" } }] }
 
 bench/ce/jlamp_array.mlw Array WP_parameter f : Valid
@@ -95,7 +93,7 @@ bench/ce/jlamp_array.mlw Array WP_parameter f : Unknown (other)
 Counter-example model:File jlamp_array.mlw:
 Line 18:
 a.length, ["model_trace:a.length"] = {"type" : "Integer" ,
-"val" : "0" }
+"val" : "1" }
 a.elts, ["model_trace:a.elts"] = {"type" : "Array" ,
 "val" : [{"indice" : "42" , "value" : {"type" : "Integer" , "val" : "3" } },
 {"others" : {"type" : "Integer" ,

bench/ce/records_CVC4,1.5.oracle

@@ -45,11 +45,9 @@ x.g, ["model_trace:x.g@call"] = {"type" : "Boolean" ,
 bench/ce/records.mlw M WP_parameter test_record_match_eval_test5 : Unknown (other)
 Counter-example model:File ref.mlw:
 Line 18:
-re.my_field_f, ["model_trace:re.my_field_f",
-"model_trace:re@old"] = {"type" : "Integer" ,
+old re.my_field_f, ["model_trace:re.my_field_f@old"] = {"type" : "Integer" ,
 "val" : "5" }
-re.g, ["model_trace:re.g",
-"model_trace:re@old"] = {"type" : "Boolean" ,
+old re.g, ["model_trace:re.g@old"] = {"type" : "Boolean" ,
 "val" : false }
 x.my_field_f, ["model_trace:x.my_field_f@call"] = {"type" : "Integer" ,
 "val" : "6" }
@@ -57,11 +55,9 @@ x.g, ["model_trace:x.g@call"] = {"type" : "Boolean" ,
 "val" : false }
 File records.mlw:
 Line 38:
-re, ["model_trace:re@init",
-"model_trace:re.my_field_f"] = {"type" : "Integer" ,
+re.my_field_f, ["model_trace:re.my_field_f@init"] = {"type" : "Integer" ,
 "val" : "5" }
-re, ["model_trace:re@init",
-"model_trace:re.g"] = {"type" : "Boolean" ,
+re.g, ["model_trace:re.g@init"] = {"type" : "Boolean" ,
 "val" : false }
 Line 40:
 x.g, ["model_trace:x.g"] = {"type" : "Boolean" ,

bench/ce/records_Z3,4.6.0.oracle

@@ -45,11 +45,9 @@ x.g, ["model_trace:x.g@call"] = {"type" : "Boolean" ,
 bench/ce/records.mlw M WP_parameter test_record_match_eval_test5 : Unknown (other)
 Counter-example model:File ref.mlw:
 Line 18:
-re.my_field_f, ["model_trace:re.my_field_f",
-"model_trace:re@old"] = {"type" : "Integer" ,
+old re.my_field_f, ["model_trace:re.my_field_f@old"] = {"type" : "Integer" ,
 "val" : "3" }
-re.g, ["model_trace:re.g",
-"model_trace:re@old"] = {"type" : "Boolean" ,
+old re.g, ["model_trace:re.g@old"] = {"type" : "Boolean" ,
 "val" : false }
 x.my_field_f, ["model_trace:x.my_field_f@call"] = {"type" : "Integer" ,
 "val" : "6" }
@@ -57,11 +55,9 @@ x.g, ["model_trace:x.g@call"] = {"type" : "Boolean" ,
 "val" : false }
 File records.mlw:
 Line 38:
-re, ["model_trace:re@init",
-"model_trace:re.my_field_f"] = {"type" : "Integer" ,
+re.my_field_f, ["model_trace:re.my_field_f@init"] = {"type" : "Integer" ,
 "val" : "3" }
-re, ["model_trace:re@init",
-"model_trace:re.g"] = {"type" : "Boolean" ,
+re.g, ["model_trace:re.g@init"] = {"type" : "Boolean" ,
 "val" : false }
 Line 40:
 x.g, ["model_trace:x.g"] = {"type" : "Boolean" ,

bench/ce/ref_CVC4,1.5.oracle

@@ -35,7 +35,7 @@ y, ["model_trace:y@call"] = {"type" : "Integer" ,
 bench/ce/ref.mlw M WP_parameter incr : Unknown (other)
 Counter-example model:File ref.mlw:
 Line 21:
-y, ["model_trace:y", "model_trace:y@init"] = {"type" : "Integer" ,
+y, ["model_trace:y@init"] = {"type" : "Integer" ,
 "val" : "-2" }
 Line 23:
 x23, ["model_trace:x23"] = {"type" : "Integer" ,

bench/ce/ref_Z3,4.6.0.oracle

@@ -35,7 +35,7 @@ y, ["model_trace:y@call"] = {"type" : "Integer" ,
 bench/ce/ref.mlw M WP_parameter incr : Unknown (other)
 Counter-example model:File ref.mlw:
 Line 21:
-y, ["model_trace:y", "model_trace:y@init"] = {"type" : "Integer" ,
+y, ["model_trace:y@init"] = {"type" : "Integer" ,
 "val" : "0" }
 Line 23:
 x23, ["model_trace:x23"] = {"type" : "Integer" ,

src/whyml/mlw_wp.ml

@@ -322,17 +322,27 @@ let mk_var id ty md =
   let new_labels, loc = match md with
     | None ->
       (* If there is no model data remove model labels (prevents counter-example
-	 projections of this variable, displaying this variable in counterexample, ...) *)
+         projections of this variable, displaying this variable in
+         counterexample, ...) *)
       let new_labels = Ident.remove_model_labels ~labels:id.id_label in
       (new_labels, None)
     | Some md -> begin
         let new_labels =
-          append_to_model_trace_label ~labels:id.id_label
-            ~to_append:("@"^md.md_append_to_model_trace)
+          match md.md_context_labels with
+          | None -> id.id_label
+          | Some ctx_lab ->
+              if Slab.exists is_model_trace_label ctx_lab then
+                (* The right model_trace should be in the md context labels *)
+                let other_labels =
+                  Slab.filter (fun x -> not (is_model_trace_label x)) id.id_label
+                in
+                Slab.union ctx_lab other_labels
+              else
+                Slab.union ctx_lab id.id_label
         in
-        let new_labels = match md.md_context_labels with
-          | None -> new_labels
-          | Some s -> Slab.union s new_labels
+        let new_labels =
+          append_to_model_trace_label ~labels:new_labels
+            ~to_append:("@"^md.md_append_to_model_trace)
         in
         (new_labels, md.md_loc)
     end