Commit eaba8837 authored by MARCHE Claude's avatar MARCHE Claude

New setting for counterexample generation

- no option -get-ce and option in IDE anymore

  instead counterexamples are generated using prover alternatives

- for counterexamples, smt printer always prints incrementally: first the goal,
  then the ground hypotheses, then the others
parent ce93b961
......@@ -57,8 +57,5 @@ for file in $files; do
filebase=`basename $file .mlw`
printf "Running provers on $filedir/$filebase.mlw\n";
run CVC4,1.5 $filedir/$filebase
run CVC4,1.5,incremental $filedir/$filebase
run Z3,4.5.0 $filedir/$filebase
run Z3,4.6.0 $filedir/$filebase
run Z3,4.6.0,incremental $filedir/$filebase
done
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
"list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "1" }
i = {"type" : "Integer" ,
"val" : "0" }
Line 25:
old i = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "0" }
Line 25:
old i = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "10" }
i = {"type" : "Integer" ,
"val" : "4" }
Line 25:
old i = {"type" : "Integer" ,
"val" : "4" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "2" }
Line 25:
old i = {"type" : "Integer" ,
"val" : "2" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "1" }
i = {"type" : "Integer" ,
"val" : "0" }
Line 25:
old i = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
Line 28:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "-1" }
File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "2" }
Line 25:
old i = {"type" : "Integer" ,
"val" : "2" }
......@@ -25,12 +25,12 @@ bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "10" }
a.length = {"type" : "Integer" , "val" : "1" }
i = {"type" : "Integer" ,
"val" : "4" }
"val" : "0" }
Line 25:
old i = {"type" : "Integer" ,
"val" : "4" }
"val" : "0" }
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array.mlw:
......@@ -88,7 +88,7 @@ bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
bench/ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
a.length = {"type" : "Integer" , "val" : "1" }
a.length = {"type" : "Integer" , "val" : "175" }
i = {"type" : "Integer" ,
"val" : "2" }
Line 25:
......
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
This diff is collapsed.
This diff is collapsed.
bench/ce/floats.mlw T32 g1 : Unknown (other)
Counter-example model:File floats.mlw:
Line 5:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 7:
x = {"type" : "Fraction" ,
"val" : "5\/4" }
bench/ce/floats.mlw T32 g3 : Unknown (other)
Counter-example model:File floats.mlw:
Line 9:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 11:
x = {"type" : "Fraction" ,
"val" : "5\/4" }
bench/ce/floats.mlw T32 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 13:
x = {"type" : "Fraction" ,
"val" : "17\/4" }
bench/ce/floats.mlw T32 g6 : Unknown (other)
Counter-example model:File floats.mlw:
Line 15:
x = {"type" : "Integer" ,