Commit a5a64af7 authored by MARCHE Claude's avatar MARCHE Claude

CE: new examples on arrays, including sorted

parent 9dfee805
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 WP_parameter f1 : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length = {"type" : "Integer" ,
"val" : "0" }
bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 10:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] }
a = {"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 = {"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:
Line 26:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 27:
old a.length = {"type" : "Integer" ,
"val" : "2" }
old a.elts = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 32:
old a.length = {"type" : "Integer" ,
"val" : "2" }
old a.elts = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/arrays.mlw A WP_parameter f1 : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length = {"type" : "Integer" ,
"val" : "0" }
bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 10:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 12:
old a.elts = {"type" : "Array" , "val" : [{"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:
Line 26:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 27:
old a.length = {"type" : "Integer" ,
"val" : "2" }
old a.elts = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File array.mlw:
Line 16:
the check fails with all inputs
File arrays.mlw:
Line 31:
a.length = {"type" : "Integer" , "val" : "0" }
a.elts = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "1" } },
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
Line 32:
the check fails with all inputs
bench/ce/arrays.mlw A WP_parameter f1 : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length = {"type" : "Integer" ,
"val" : "0" }
bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 10:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "5" } }] }
a = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "5" } }] }
Line 12:
a = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "5" } }] }
bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length = {"type" : "Integer" ,
"val" : "7646" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "834" ,
"value" : {"type" : "Integer" , "val" : "99" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "103" ,
"value" : {"type" : "Integer" , "val" : "105" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "98" } }, {"indice" : "-2593" ,
"value" : {"type" : "Integer" , "val" : "111" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "-496" ,
"value" : {"type" : "Integer" , "val" : "106" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
Line 27:
old a.length = {"type" : "Integer" ,
"val" : "7646" }
old a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "834" ,
"value" : {"type" : "Integer" , "val" : "99" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "103" ,
"value" : {"type" : "Integer" , "val" : "105" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "98" } }, {"indice" : "-2593" ,
"value" : {"type" : "Integer" , "val" : "111" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "-496" ,
"value" : {"type" : "Integer" , "val" : "106" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length = {"type" : "Integer" ,
"val" : "7646" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "834" ,
"value" : {"type" : "Integer" , "val" : "99" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "103" ,
"value" : {"type" : "Integer" , "val" : "105" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "98" } }, {"indice" : "-2593" ,
"value" : {"type" : "Integer" , "val" : "111" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "-496" ,
"value" : {"type" : "Integer" , "val" : "106" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
Line 32:
old a.length = {"type" : "Integer" ,
"val" : "7646" }
old a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "834" ,
"value" : {"type" : "Integer" , "val" : "99" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "103" ,
"value" : {"type" : "Integer" , "val" : "105" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "98" } }, {"indice" : "-2593" ,
"value" : {"type" : "Integer" , "val" : "111" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "-496" ,
"value" : {"type" : "Integer" , "val" : "106" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
bench/ce/arrays.mlw A WP_parameter f1 : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length = {"type" : "Integer" ,
"val" : "0" }
bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 10:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "5" } }] }
Line 12:
old a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "5" } }] }
bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length = {"type" : "Integer" ,
"val" : "7646" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "834" ,
"value" : {"type" : "Integer" , "val" : "99" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "103" ,
"value" : {"type" : "Integer" , "val" : "105" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "98" } }, {"indice" : "-2593" ,
"value" : {"type" : "Integer" , "val" : "111" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "-496" ,
"value" : {"type" : "Integer" , "val" : "106" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
Line 27:
old a.length = {"type" : "Integer" ,
"val" : "7646" }
old a.elts = {"type" : "Array" , "val" : [{"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "53" } }, {"indice" : "834" ,
"value" : {"type" : "Integer" , "val" : "99" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "52" } }, {"indice" : "103" ,
"value" : {"type" : "Integer" , "val" : "105" } }, {"indice" : "5606" ,
"value" : {"type" : "Integer" , "val" : "11" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "5659" } }, {"indice" : "9087" ,
"value" : {"type" : "Integer" , "val" : "98" } }, {"indice" : "-2593" ,
"value" : {"type" : "Integer" , "val" : "111" } }, {"indice" : "4" ,
"value" : {"type" : "Integer" , "val" : "45" } }, {"indice" : "-496" ,
"value" : {"type" : "Integer" , "val" : "106" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Valid
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length = {"type" : "Integer" ,
"val" : "9281" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "1265" ,
"value" : {"type" : "Integer" , "val" : "-35" } }, {"indice" : "-9735" ,
"value" : {"type" : "Integer" , "val" : "8651" } }, {"indice" : "971" ,
"value" : {"type" : "Integer" , "val" : "-38" } }, {"indice" : "-3769" ,
"value" : {"type" : "Integer" , "val" : "-39" } }, {"indice" : "-9734" ,
"value" : {"type" : "Integer" , "val" : "8650" } }, {"indice" : "1263" ,
"value" : {"type" : "Integer" , "val" : "-37" } }, {"indice" : "9280" ,
"value" : {"type" : "Integer" , "val" : "-502" } }, {"indice" : "1264" ,
"value" : {"type" : "Integer" , "val" : "-36" } }, {"indice" : "-7440" ,
"value" : {"type" : "Integer" , "val" : "-34" } }, {"indice" : "-9736" ,
"value" : {"type" : "Integer" , "val" : "-32" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "-33" } }, {"indice" : "3" ,
"value" : {"type" : "Integer" , "val" : "25" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
Line 32:
the check fails with all inputs
bench/ce/arrays.mlw A WP_parameter f1 : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length = {"type" : "Integer" ,
"val" : "0" }
bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 10:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "5" } }] }
a = {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "5" } }] }
Line 12:
a = {"type" : "Array" , "val" : [{"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "42" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "5" } }] }
bench/ce/arrays.mlw B WP_parameter f1 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 26:
a.length = {"type" : "Integer" ,
"val" : "7646" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "1341" ,
"value" : {"type" : "Integer" , "val" : "1" } }, {"indice" : "-3770" ,
"value" : {"type" : "Integer" , "val" : "1532" } }, {"indice" : "-110" ,
"value" : {"type" : "Integer" , "val" : "8643" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "1913" } }, {"indice" : "-2" ,
"value" : {"type" : "Integer" , "val" : "891" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "945" } }, {"indice" : "-1" ,
"value" : {"type" : "Integer" , "val" : "946" } }, {"indice" : "1914" ,
"value" : {"type" : "Integer" , "val" : "1913" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "1914" } }, {"indice" : "3" ,
"value" : {"type" : "Integer" , "val" : "714" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
Line 27:
old a.length = {"type" : "Integer" ,
"val" : "7646" }
old a.elts = {"type" : "Array" ,
"val" : [{"indice" : "1341" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"indice" : "-3770" , "value" : {"type" : "Integer" ,
"val" : "1532" } }, {"indice" : "-110" , "value" : {"type" : "Integer" ,
"val" : "8643" } }, {"indice" : "1" , "value" : {"type" : "Integer" ,
"val" : "1913" } }, {"indice" : "-2" , "value" : {"type" : "Integer" ,
"val" : "891" } }, {"indice" : "2" , "value" : {"type" : "Integer" ,
"val" : "945" } }, {"indice" : "-1" , "value" : {"type" : "Integer" ,
"val" : "946" } }, {"indice" : "1914" , "value" : {"type" : "Integer" ,
"val" : "1913" } }, {"indice" : "0" , "value" : {"type" : "Integer" ,
"val" : "1914" } }, {"indice" : "3" , "value" : {"type" : "Integer" ,
"val" : "714" } }, {"others" : {"type" : "Integer" ,
"val" : "6" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length = {"type" : "Integer" ,
"val" : "7646" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "1341" ,
"value" : {"type" : "Integer" , "val" : "1" } }, {"indice" : "-3770" ,
"value" : {"type" : "Integer" , "val" : "1532" } }, {"indice" : "-110" ,
"value" : {"type" : "Integer" , "val" : "8643" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "1913" } }, {"indice" : "-2" ,
"value" : {"type" : "Integer" , "val" : "891" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "945" } }, {"indice" : "-1" ,
"value" : {"type" : "Integer" , "val" : "946" } }, {"indice" : "1914" ,
"value" : {"type" : "Integer" , "val" : "1913" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "1914" } }, {"indice" : "3" ,
"value" : {"type" : "Integer" , "val" : "714" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
Line 32:
old a.length = {"type" : "Integer" ,
"val" : "7646" }
old a.elts = {"type" : "Array" ,
"val" : [{"indice" : "1341" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"indice" : "-3770" , "value" : {"type" : "Integer" ,
"val" : "1532" } }, {"indice" : "-110" , "value" : {"type" : "Integer" ,
"val" : "8643" } }, {"indice" : "1" , "value" : {"type" : "Integer" ,
"val" : "1913" } }, {"indice" : "-2" , "value" : {"type" : "Integer" ,
"val" : "891" } }, {"indice" : "2" , "value" : {"type" : "Integer" ,
"val" : "945" } }, {"indice" : "-1" , "value" : {"type" : "Integer" ,
"val" : "946" } }, {"indice" : "1914" , "value" : {"type" : "Integer" ,
"val" : "1913" } }, {"indice" : "0" , "value" : {"type" : "Integer" ,
"val" : "1914" } }, {"indice" : "3" , "value" : {"type" : "Integer" ,
"val" : "714" } }, {"others" : {"type" : "Integer" ,
"val" : "6" } }] }
bench/ce/arrays.mlw A WP_parameter f1 : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" ,
"val" : "0" }
File arrays.mlw:
Line 7:
a.length = {"type" : "Integer" ,
"val" : "0" }
bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Valid
bench/ce/arrays.mlw A WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 10:
a.length = {"type" : "Integer" , "val" : "2" }
a.elts = {"type" : "Array" ,
"val" : [{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
Line 12:
old a.elts = {"type" : "Array" , "val" : [{"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 = {"type" : "Integer" ,
"val" : "7646" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "1341" ,
"value" : {"type" : "Integer" , "val" : "1" } }, {"indice" : "-3770" ,
"value" : {"type" : "Integer" , "val" : "1532" } }, {"indice" : "-110" ,
"value" : {"type" : "Integer" , "val" : "8643" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "1913" } }, {"indice" : "-2" ,
"value" : {"type" : "Integer" , "val" : "891" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "945" } }, {"indice" : "-1" ,
"value" : {"type" : "Integer" , "val" : "946" } }, {"indice" : "1914" ,
"value" : {"type" : "Integer" , "val" : "1913" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "1914" } }, {"indice" : "3" ,
"value" : {"type" : "Integer" , "val" : "714" } },
{"others" : {"type" : "Integer" ,
"val" : "6" } }] }
Line 27:
old a.length = {"type" : "Integer" ,
"val" : "7646" }
old a.elts = {"type" : "Array" ,
"val" : [{"indice" : "1341" , "value" : {"type" : "Integer" ,
"val" : "1" } }, {"indice" : "-3770" , "value" : {"type" : "Integer" ,
"val" : "1532" } }, {"indice" : "-110" , "value" : {"type" : "Integer" ,
"val" : "8643" } }, {"indice" : "1" , "value" : {"type" : "Integer" ,
"val" : "1913" } }, {"indice" : "-2" , "value" : {"type" : "Integer" ,
"val" : "891" } }, {"indice" : "2" , "value" : {"type" : "Integer" ,
"val" : "945" } }, {"indice" : "-1" , "value" : {"type" : "Integer" ,
"val" : "946" } }, {"indice" : "1914" , "value" : {"type" : "Integer" ,
"val" : "1913" } }, {"indice" : "0" , "value" : {"type" : "Integer" ,
"val" : "1914" } }, {"indice" : "3" , "value" : {"type" : "Integer" ,
"val" : "714" } }, {"others" : {"type" : "Integer" ,
"val" : "6" } }] }
bench/ce/arrays.mlw B WP_parameter f2 : Valid
bench/ce/arrays.mlw B WP_parameter f2 : Unknown (other)
Counter-example model:File arrays.mlw:
Line 31:
a.length = {"type" : "Integer" ,
"val" : "2200" }
a.elts = {"type" : "Array" , "val" : [{"indice" : "-340" ,
"value" : {"type" : "Integer" , "val" : "2884" } }, {"indice" : "-2" ,
"value" : {"type" : "Integer" , "val" : "5503" } }, {"indice" : "-400" ,
"value" : {"type" : "Integer" , "val" : "-4508" } }, {"indice" : "2" ,
"value" : {"type" : "Integer" , "val" : "4863" } }, {"indice" : "430" ,
"value" : {"type" : "Integer" , "val" : "4863" } }, {"indice" : "-2514" ,
"value" : {"type" : "Integer" , "val" : "11465" } }, {"indice" : "-2515" ,
"value" : {"type" : "Integer" , "val" : "10325" } }, {"indice" : "0" ,
"value" : {"type" : "Integer" , "val" : "14539" } }, {"indice" : "431" ,
"value" : {"type" : "Integer" , "val" : "4864" } }, {"indice" : "-3239" ,
"value" : {"type" : "Integer" , "val" : "4235" } }, {"indice" : "-1870" ,
"value" : {"type" : "Integer" , "val" : "4234" } }, {"indice" : "1" ,
"value" : {"type" : "Integer" , "val" : "5710" } }, {"indice" : "-8680" ,
"value" : {"type" : "Integer" , "val" : "10253" } }, {"indice" : "9676" ,
"value" : {"type" : "Integer" , "val" : "-2511" } }, {"indice" : "-2510" ,
"value" : {"type" : "Integer" , "val" : "5491" } }, {"indice" : "-2513" ,
"value" : {"type" : "Integer" , "val" : "2507" } }, {"indice" : "-2544" ,
"value" : {"type" : "Integer" , "val" : "2508" } }, {"indice" : "-2511" ,
"value" : {"type" : "Integer" , "val" : "4233" } }, {"indice" : "3" ,
"value" : {"type" : "Integer" , "val" : "23" } },
{"others" : {"type" : "Integer" ,
"val" : "5" } }] }
Line 32:
the check fails with all inputs
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment