Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 4543a604 authored by MARCHE Claude's avatar MARCHE Claude

removed useless labels

parent ca07a3cc
......@@ -11,68 +11,34 @@ module M
use import int.Int
use import ref.Ref
(**************************************
** Getting counterexamples for maps **
**************************************)
use import map.Map
let test_map (x : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
x := Map.set !x 0 3
(* Multi-dimensional maps *)
let test_map_multidim1 (x : ref (map int (map int int))) : unit
ensures { !x[0][0] <> !x[1][1] }
ensures { !x[0][0] <> !x[1][1] }
=
x := Map.set !x 0 (Map.get !x 1)
x := Map.set !x 0 (Map.get !x 1)
let test_map_multidim2 (x : ref (map int (map int int))) : unit
ensures { !x[0][0] <> !x[1][1] }
=
let x0 = Map.get !x 0 in
let x0 = Map.set x0 0 3 in
x := Map.set !x 0 x0
(*******************************************
** Definitions of projections used below **
*******************************************)
function projfi "model_trace:.projfi" (l : int) : int
= l
meta "inline : no" function projfi
meta "model_projection" function projfi
function projf1 "model_trace:.projf1" (l : int) : bool
ensures { !x[0][0] <> !x[1][1] }
=
l > 0
function projf2 "model_trace:.projf2" (l : int) : bool
let x0 = Map.get !x 0 in
let x0 = Map.set x0 0 3 in
x := Map.set !x 0 x0
let proj_map_test1 (x : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
=
l <= 0
meta "inline : no" function projf1
meta "model_projection" function projf1
meta "inline : no" function projf2
meta "model_projection" function projf2
x := Map.set !x 0 3
(*******************************************************
** Getting counterexamples for maps with projections **
******************************************************)
(* Both indices and range of map will be projected using
projfi, projf1, and projf2
Warning: cvc4 is not able to handle projections there *)
let proj_map_test1 (x "model_projected" : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
(* No projection function for bool -> the array should be
present in counterexample as it is. *)
let proj_map_test2 (x "model_projected" : ref (map int bool)) : unit
ensures { !x[0] <> !x[1] }
let proj_map_test2 (x : ref (map int bool)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 true
x := Map.set !x 0 true
end
......@@ -9,18 +9,18 @@ t = {"type" : "Array" ,
bench/ce/map.mlw M WP_parameter test_map : Unknown (other)
Counter-example model:File map.mlw:
Line 19:
Line 16:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 20:
Line 17:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 22:
Line 19:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -29,29 +29,29 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter test_map_multidim1 : Unknown (other)
Counter-example model:File map.mlw:
Line 25:
Line 22:
x = {"type" : "Array" , "val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
Line 26:
Line 23:
x = {"type" : "Array" , "val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
Line 28:
Line 25:
x = {"type" : "Array" , "val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
bench/ce/map.mlw M WP_parameter test_map_multidim2 : Unknown (other)
Counter-example model:File map.mlw:
Line 30:
Line 27:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
Line 31:
Line 28:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -61,7 +61,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
Line 35:
Line 32:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -74,18 +74,18 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter proj_map_test1 : Unknown (other)
Counter-example model:File map.mlw:
Line 64:
Line 34:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 65:
Line 35:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 67:
Line 37:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -94,18 +94,18 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter proj_map_test2 : Unknown (other)
Counter-example model:File map.mlw:
Line 71:
Line 39:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 72:
Line 40:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 74:
Line 42:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
......@@ -123,18 +123,18 @@ t = {"type" : "Array" ,
bench/ce/map.mlw M WP_parameter test_map : Unknown (other)
Counter-example model:File map.mlw:
Line 19:
Line 16:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 20:
Line 17:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 22:
Line 19:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -143,29 +143,29 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter test_map_multidim1 : Unknown (other)
Counter-example model:File map.mlw:
Line 25:
Line 22:
x = {"type" : "Array" , "val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
Line 26:
Line 23:
x = {"type" : "Array" , "val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
Line 28:
Line 25:
x = {"type" : "Array" , "val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
bench/ce/map.mlw M WP_parameter test_map_multidim2 : Unknown (other)
Counter-example model:File map.mlw:
Line 30:
Line 27:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
Line 31:
Line 28:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -175,7 +175,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
Line 35:
Line 32:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -188,18 +188,18 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter proj_map_test1 : Unknown (other)
Counter-example model:File map.mlw:
Line 64:
Line 34:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 65:
Line 35:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 67:
Line 37:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -208,18 +208,18 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter proj_map_test2 : Unknown (other)
Counter-example model:File map.mlw:
Line 71:
Line 39:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 72:
Line 40:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 74:
Line 42:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
......
......@@ -9,18 +9,18 @@ t = {"type" : "Array" ,
bench/ce/map.mlw M WP_parameter test_map : Unknown (other)
Counter-example model:File map.mlw:
Line 19:
Line 16:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 20:
Line 17:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 22:
Line 19:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -29,7 +29,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter test_map_multidim1 : Unknown (other)
Counter-example model:File map.mlw:
Line 25:
Line 22:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
......@@ -37,7 +37,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "1" ,
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] }
Line 26:
Line 23:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
......@@ -49,7 +49,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] }
Line 28:
Line 25:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
......@@ -64,7 +64,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter test_map_multidim2 : Unknown (other)
Counter-example model:File map.mlw:
Line 30:
Line 27:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }, {"indice" : "1" , "value" : {"type" : "Array" ,
......@@ -72,7 +72,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] }
Line 31:
Line 28:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -82,7 +82,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] }
Line 35:
Line 32:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -95,18 +95,18 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter proj_map_test1 : Unknown (other)
Counter-example model:File map.mlw:
Line 64:
Line 34:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 65:
Line 35:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 67:
Line 37:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -115,18 +115,18 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter proj_map_test2 : Unknown (other)
Counter-example model:File map.mlw:
Line 71:
Line 39:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 72:
Line 40:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 74:
Line 42:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
......@@ -144,18 +144,18 @@ t = {"type" : "Array" ,
bench/ce/map.mlw M WP_parameter test_map : Unknown (other)
Counter-example model:File map.mlw:
Line 19:
Line 16:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 20:
Line 17:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 22:
Line 19:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -164,7 +164,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter test_map_multidim1 : Unknown (other)
Counter-example model:File map.mlw:
Line 25:
Line 22:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
......@@ -172,7 +172,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "1" ,
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] }
Line 26:
Line 23:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
......@@ -184,7 +184,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] }
Line 28:
Line 25:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
......@@ -199,7 +199,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter test_map_multidim2 : Unknown (other)
Counter-example model:File map.mlw:
Line 30:
Line 27:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }, {"indice" : "1" , "value" : {"type" : "Array" ,
......@@ -207,7 +207,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] }
Line 31:
Line 28:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -217,7 +217,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] }
Line 35:
Line 32:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -230,18 +230,18 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter proj_map_test1 : Unknown (other)
Counter-example model:File map.mlw:
Line 64:
Line 34:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 65:
Line 35:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 67:
Line 37:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -250,18 +250,18 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter proj_map_test2 : Unknown (other)
Counter-example model:File map.mlw:
Line 71:
Line 39:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 72:
Line 40:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 74:
Line 42:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
......
......@@ -9,18 +9,18 @@ t = {"type" : "Array" ,
bench/ce/map.mlw M WP_parameter test_map : Unknown (other)
Counter-example model:File map.mlw:
Line 19:
Line 16:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 20:
Line 17:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 22:
Line 19:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -29,7 +29,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter test_map_multidim1 : Unknown (other)
Counter-example model:File map.mlw:
Line 25:
Line 22:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
......@@ -37,7 +37,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "1" ,
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] }
Line 26:
Line 23:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
......@@ -49,7 +49,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] }
Line 28:
Line 25:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
......@@ -64,7 +64,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter test_map_multidim2 : Unknown (other)
Counter-example model:File map.mlw:
Line 30:
Line 27:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }, {"indice" : "1" , "value" : {"type" : "Array" ,
......@@ -72,7 +72,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] }
Line 31:
Line 28:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -82,7 +82,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] }
Line 35:
Line 32:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -95,18 +95,18 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter proj_map_test1 : Unknown (other)
Counter-example model:File map.mlw:
Line 64:
Line 34:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 65:
Line 35:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 67:
Line 37:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -115,18 +115,18 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M WP_parameter proj_map_test2 : Unknown (other)
Counter-example model:File map.mlw:
Line 71:
Line 39:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 72:
Line 40:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 74:
Line 42:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
......@@ -144,18 +144,18 @@ t = {"type" : "Array" ,
bench/ce/map.mlw M WP_parameter test_map : Unknown (other)
Counter-example model:File map.mlw:
Line 19:
Line 16:
x = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 20:
Line 17:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 22: