Commit 98da222c authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge branch 'new_ide'

# Conflicts:
#	bench/ce/jlamp_array.mlw
#	bench/ce/jlamp_projections.mlw
#	bench/ce/jlamp_projections_CVC4,1.5.oracle
#	bench/ce/jlamp_projections_Z3,4.5.0.oracle
#	bench/ce/jlamp_projections_Z3,4.6.0.oracle
#	bench/ce/map.mlw
#	bench/ce/map_CVC4,1.5.oracle
#	bench/ce/map_Z3,4.5.0.oracle
#	bench/ce/map_Z3,4.6.0.oracle
#	bench/ce/records.mlw
#	bench/ce/records_CVC4,1.5.oracle
#	bench/ce/records_Z3,4.5.0.oracle
#	bench/ce/records_Z3,4.6.0.oracle
#	examples/verifythis_fm2012_LRS/why3session.xml
#	examples/verifythis_fm2012_LRS/why3shapes.gz
parents a6d6cb69 a5a64af7
module A
use import int.Int
use import array.Array
let f1 (a:array int) : int
= a[0]
let f2 (a:array int) : unit
requires { a.length >= 2 }
ensures { a[0] <> a[1] }
= a[0] <- 42
end
module B
use import int.Int
use import array.Array
clone import array.Sorted with
type elt=int,
predicate le=(<=)
let f1 (a:array int) : unit
ensures { sorted a }
= ()
let f2 (a:array int) : array int
ensures { sorted result }
= a
end
\ No newline at end of file
bench/ce/arrays.mlw A VC f1: Unknown (other)
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Unknown (other)
bench/ce/arrays.mlw B VC f1: Unknown (other)
bench/ce/arrays.mlw B VC f2: Unknown (other)
bench/ce/arrays.mlw A VC f1: Unknown (other)
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Unknown (other)
bench/ce/arrays.mlw B VC f1: Unknown (other)
bench/ce/arrays.mlw B VC f2: Unknown (other)
bench/ce/arrays.mlw A VC f1: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/arrays.mlw B VC f1: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/arrays.mlw B VC f2: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/arrays.mlw A VC f1: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/arrays.mlw B VC f1: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/arrays.mlw B VC f2: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/arrays.mlw A VC f1: Timeout
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Timeout
bench/ce/arrays.mlw B VC f1: Timeout
bench/ce/arrays.mlw B VC f2: Timeout
bench/ce/arrays.mlw A VC f1: Timeout
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Timeout
bench/ce/arrays.mlw B VC f1: Timeout
bench/ce/arrays.mlw B VC f2: Timeout
......@@ -15,22 +15,22 @@ module Array
axiom three_def : to_int three = 3
let f (a [@model] [@model_projected] :array t) : unit
let f (a : array t) : unit
requires { a[42] = three }
writes { a }
ensures { [@model_vc] a[42] = three }
ensures { a[42] = three }
= a[42] <- two
let g (a [@model] [@model_projected] :array t) : unit
let g (a : array t) : unit
requires { a.length >= 43 /\ a[17] = three }
writes { a }
ensures { [@model_vc] a[42] = three }
ensures { a[42] = three }
= a[42] <- two
let h (a [@model] [@model_projected] :array t) : unit
let h (a : array t) : unit
requires { a.length >= 43 /\ a[17] = three }
writes { a }
ensures { [@model_vc] a[42] = three }
ensures { a[42] = three }
= a[17] <- two
end
......@@ -20,7 +20,7 @@ val add (x y : byte) : byte
use import ref.Ref
let p3 (a [@model_projected] : ref byte) =
let p3 (a : ref byte) =
a := add !a (of_int 1)
end
......@@ -32,12 +32,7 @@ use import Abstract
type r = {mutable f : byte; mutable g : bool}
function get_f (x:r) : byte = x.f
function get_g (x:r) : bool = x.g
meta model_projection function get_f
meta model_projection function get_g
let p4 (b [@model_projected] : r) =
let p4 (b : r) =
if b.g then b.f <- add b.f (of_int 1)
end
bench/ce/jlamp_projections.mlw Abstract VC p3: Valid
bench/ce/jlamp_projections.mlw Abstract VC p3: Unknown (other)
bench/ce/jlamp_projections.mlw Abstract VC p3: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Unknown (other)
bench/ce/jlamp_projections.mlw Record VC p4: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/jlamp_projections.mlw Abstract VC p3: Valid
bench/ce/jlamp_projections.mlw Abstract VC p3: Unknown (other)
bench/ce/jlamp_projections.mlw Abstract VC p3: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Unknown (other)
bench/ce/jlamp_projections.mlw Record VC p4: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/jlamp_projections.mlw Abstract VC p3: Valid
bench/ce/jlamp_projections.mlw Abstract VC p3: Unknown (other)
bench/ce/jlamp_projections.mlw Abstract VC p3: Timeout
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Unknown (other)
bench/ce/jlamp_projections.mlw Record VC p4: Timeout
bench/ce/jlamp_projections.mlw Abstract VC p3: Valid
bench/ce/jlamp_projections.mlw Abstract VC p3: Unknown (other)
bench/ce/jlamp_projections.mlw Abstract VC p3: Timeout
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Unknown (other)
bench/ce/jlamp_projections.mlw Record VC p4: Timeout
module List_int
use import int.Int
type list = Nil | Cons int list
function length (l:list) : int =
match l with
| Nil -> 0
| Cons _ l -> 1 + length l
end
goal g1: forall l:list. length l <> 0
goal g2: forall l:list. length l <> 1
end
module List_poly
use import list.List
use import list.Length
goal g1: forall l:list int. length l <> 0
goal g2: forall l:list int. length l <> 1
end
\ No newline at end of file
bench/ce/list.mlw List_int g1 : Unknown (other)
bench/ce/list.mlw List_int g2 : Unknown (other)
bench/ce/list.mlw List_poly g1 : Unknown (other)
bench/ce/list.mlw List_poly g2 : Unknown (other)
bench/ce/list.mlw List_int g1 : Unknown (other)
bench/ce/list.mlw List_int g2 : Unknown (other)
bench/ce/list.mlw List_poly g1 : Unknown (other)
bench/ce/list.mlw List_poly g2 : Unknown (other)
bench/ce/list.mlw List_int g1 : Unknown (other)
bench/ce/list.mlw List_int g2 : Unknown (other)
bench/ce/list.mlw List_poly g1 : Unknown (other)
bench/ce/list.mlw List_poly g2 : Unknown (other)
bench/ce/list.mlw List_int g1 : Unknown (other)
bench/ce/list.mlw List_int g2 : Unknown (other)
bench/ce/list.mlw List_poly g1 : Unknown (other)
bench/ce/list.mlw List_poly g2 : Unknown (other)
bench/ce/list.mlw List_int g1 : Unknown (other)
bench/ce/list.mlw List_int g2 : Unknown (other)
bench/ce/list.mlw List_poly g1 : Unknown (other)
bench/ce/list.mlw List_poly g2 : Unknown (other)
bench/ce/list.mlw List_int g1 : Unknown (other)
bench/ce/list.mlw List_int g2 : Unknown (other)
bench/ce/list.mlw List_poly g1 : Unknown (other)
bench/ce/list.mlw List_poly g2 : Unknown (other)
......@@ -11,68 +11,34 @@ module M
use import int.Int
use import ref.Ref
(**************************************
** Getting counterexamples for maps **
**************************************)
use import map.Map
let ghost test_map (ghost 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 ghost test_map_multidim1 (ghost 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 ghost test_map_multidim2 (ghost 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
=
l > 0
function projf2 [@model_trace:.projf2] (l : int) : bool
ensures { !x[0][0] <> !x[1][1] }
=
l <= 0
meta "inline:no" function projf1
meta "model_projection" function projf1
meta "inline:no" function projf2
meta "model_projection" function projf2
(*******************************************************
** Getting counterexamples for maps with projections **
******************************************************)
let x0 = Map.get !x 0 in
let x0 = Map.set x0 0 3 in
x := Map.set !x 0 x0
(* Both indices and range of map will be projected using
projfi, projf1, and projf2
Warning: cvc4 is not able to handle projections there *)
let ghost proj_map_test1 (ghost x [@model_projected] : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
let ghost proj_map_test1 (ghost x : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
x := Map.set !x 0 3
(* No projection function for bool -> the array should be
present in counterexample as it is. *)
let ghost proj_map_test2 (ghost x [@model_projected] : ref (map int bool)) : unit
ensures { !x[0] <> !x[1] }
let ghost proj_map_test2 (ghost 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,13 +9,13 @@ t = {"type" : "Array" ,
bench/ce/map.mlw M VC test_map: Unknown (other)
Counter-example model:File map.mlw:
Line 19:
Line 16:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 20:
Line 17:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -24,18 +24,18 @@ old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M VC 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:
old x = {"type" : "Array" , "val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
bench/ce/map.mlw M VC 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" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -45,7 +45,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
Line 31:
Line 28:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -58,13 +58,13 @@ old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M VC proj_map_test1: Unknown (other)
Counter-example model:File map.mlw:
Line 64:
Line 34:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 65:
Line 35:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -73,13 +73,13 @@ old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M VC proj_map_test2: Unknown (other)
Counter-example model:File map.mlw:
Line 71:
Line 39:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 72:
Line 40:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
......@@ -97,13 +97,13 @@ t = {"type" : "Array" ,
bench/ce/map.mlw M VC test_map: Unknown (other)
Counter-example model:File map.mlw:
Line 19:
Line 16:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 20:
Line 17:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -112,18 +112,18 @@ old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M VC 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:
old x = {"type" : "Array" , "val" : [{"others" : {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
bench/ce/map.mlw M VC 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" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -133,7 +133,7 @@ x = {"type" : "Array" , "val" : [{"indice" : "0" ,
{"others" : {"type" : "Integer" , "val" : "0" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
Line 31:
Line 28:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -146,13 +146,13 @@ old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M VC proj_map_test1: Unknown (other)
Counter-example model:File map.mlw:
Line 64:
Line 34:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 65:
Line 35:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
......@@ -161,13 +161,13 @@ old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
bench/ce/map.mlw M VC proj_map_test2: Unknown (other)
Counter-example model:File map.mlw:
Line 71:
Line 39:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 72:
Line 40:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
......
......@@ -7,100 +7,30 @@ t = {"type" : "Array" ,
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
bench/ce/map.mlw M VC test_map: Unknown (other)
Counter-example model:File map.mlw:
Line 19:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 20:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
bench/ce/map.mlw M VC test_map: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/map.mlw M VC test_map_multidim1: Unknown (other)
Counter-example model:File map.mlw:
Line 25:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "2" } },
{"others" : {"type" : "Integer" , "val" : "3" } }] } }, {"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "2" } },
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] }
Line 26:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "2" } },
{"others" : {"type" : "Integer" , "val" : "3" } }] } }, {"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "2" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "2" } },
{"others" : {"type" : "Integer" , "val" : "3" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "4" } }] } }] }
bench/ce/map.mlw M VC test_map_multidim2: Unknown (other)
Counter-example model:File map.mlw:
Line 30:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] }
Line 31:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"indice" : "1" ,
"value" : {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" , "val" : "2" } }] } },
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "5" } }] } }] }
bench/ce/map.mlw M VC proj_map_test1: Unknown (other)
Counter-example model:File map.mlw:
Line 64:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 65:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
bench/ce/map.mlw M VC proj_map_test2: Unknown (other)
Counter-example model:File map.mlw:
Line 71:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
Line 72:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Boolean" , "val" : true } }, {"indice" : "1" ,
"value" : {"type" : "Boolean" , "val" : true } },
{"others" : {"type" : "Boolean" ,
"val" : false } }] }
bench/ce/map.mlw M VC test_map_multidim1: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/map.mlw M VC test_map_multidim2: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/map.mlw M VC proj_map_test1: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/map.mlw M VC proj_map_test2: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/map.mlw ModelMap t1: Unknown (other)
Counter-example model:File map.mlw:
......@@ -111,98 +41,28 @@ t = {"type" : "Array" ,
{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
bench/ce/map.mlw M VC test_map: Unknown (other)
Counter-example model:File map.mlw:
Line 19:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
Line 20:
old x = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "3" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "3" } },
{"others" : {"type" : "Integer" ,
"val" : "2" } }] }
bench/ce/map.mlw M VC test_map: HighFailure
Prover exit status: exited with status 1
Prover output:
bench/ce/map.mlw M VC test_map_multidim1: Unknown (other)
Counter-example model:File map.mlw:
Line 25:
x = {"type" : "Array" , "val" : [{"indice" : "0" ,