Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 5714bbcd authored by MARCHE Claude's avatar MARCHE Claude
Browse files

additional counterexamples returned by Z3

parent 82621efd
......@@ -8,7 +8,13 @@ files=""
while test $# != 0; do
case "$1" in
"-update-oracle")
updateoracle=true;;
updateoracle=true;;
"-"*)
printf "unknown option: %s\n" "$1"
printf "usage: ce-bench [-update-oracle] <files>\n"
printf " <files> must be given without the '.mlw' suffix\n"
printf " if <files> empty, use all files from directory 'ce'\n"
exit 2;;
*)
files="$files $1"
esac
......@@ -16,20 +22,19 @@ shift
done
if test "$files" = "" ; then
files="ce/*.mlw"
files="$dir/ce/*.mlw"
fi
cd $dir
# $1 = prover, $2 = file
run () {
printf " $2 ($1)... "
f="$2_$1"
../bin/why3prove.opt -P "$1" --timelimit 1 -a split_intros_goal_wp --get-ce "$2.mlw" | \
$dir/../bin/why3prove.opt -P "$1" --timelimit 1 -a split_intros_goal_wp --get-ce "$2.mlw" | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed 's/ ([0-9]\+\.[0-9]\+s)//' > "$f.out"
../bin/why3prove.opt -P "$1" --timelimit 1 --debug fast_wp -a split_intros_goal_wp --get-ce "$2.mlw" | \
$dir/../bin/why3prove.opt -P "$1" --timelimit 1 --debug fast_wp -a split_intros_goal_wp --get-ce "$2.mlw" | \
sed 's/ ([0-9]\+\.[0-9]\+s)//' >> "$f.out"
if cmp "$f.oracle" "$f.out" > /dev/null 2>&1 ; then
echo "ok"
......@@ -48,8 +53,10 @@ run () {
for file in $files; do
filedir=`dirname $file`
filebase=`basename $file .mlw`
run CVC4,1.5 ce/$filebase
run Z3,4.5.0 ce/$filebase
run Z3,4.6.0 ce/$filebase
printf "Running provers on $filedir/$filebase.mlw\n";
run CVC4,1.5 $filedir/$filebase
run Z3,4.5.0 $filedir/$filebase
run Z3,4.6.0 $filedir/$filebase
done
ce/algebraic_type.mlw M G : Unknown (other)
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" }] } }
ce/algebraic_type.mlw M G : Unknown (other)
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
......
ce/algebraic_type.mlw M G : Unknown (other)
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" }] } }
ce/algebraic_type.mlw M G : Unknown (other)
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
......
ce/algebraic_type.mlw M G : Unknown (other)
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" }] } }
ce/algebraic_type.mlw M G : Unknown (other)
bench/ce/algebraic_type.mlw M G : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x = {"type" : "Apply" , "val" : {"apply" : "Integer" ,
......
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
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" }
......@@ -10,19 +10,19 @@ a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
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" }
......@@ -32,7 +32,7 @@ Line 25:
old i = {"type" : "Integer" ,
"val" : "0" }
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
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" }
......@@ -44,8 +44,8 @@ a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
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" }
......@@ -57,8 +57,8 @@ a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
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" }
......@@ -70,8 +70,8 @@ a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
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" }
......@@ -83,9 +83,9 @@ a.length = {"type" : "Integer" , "val" : "0" }
i = {"type" : "Integer" ,
"val" : "-1" }
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
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" }
......
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
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" }
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Valid
ce/array_records.mlw Array_records WP_parameter var_overwrite : Unknown (other)
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" : "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" : "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" : "1" }
i = {"type" : "Integer" ,
"val" : "1" }
Line 25:
old i = {"type" : "Integer" ,
"val" : "1" }
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
Counter-example model:File int32.mlw:
Line 6:
r = {"type" : "Integer" , "val" : "22" }
......@@ -12,9 +12,9 @@ Line 10:
r = {"type" : "Integer" ,
"val" : "84" }
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
Counter-example model:File int32.mlw:
Line 6:
r = {"type" : "Integer" , "val" : "22" }
......
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Valid
bench/ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
ce/int.mlw T g_no_lab : Unknown (other)
bench/ce/int.mlw T g_no_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 5:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g_lab0 : Unknown (other)
bench/ce/int.mlw T g_lab0 : Unknown (other)
Counter-example model:File int.mlw:
Line 7:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g2_lab : Unknown (other)
bench/ce/int.mlw T g2_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 12:
x = {"type" : "Integer" ,
"val" : "0" }
ce/int.mlw T newgoal : Unknown (other)
bench/ce/int.mlw T newgoal : Unknown (other)
Counter-example model:File int.mlw:
Line 14:
x2 = {"type" : "Integer" , "val" : "1" }
......@@ -33,25 +33,25 @@ x7 = {"type" : "Integer" ,
x8 = {"type" : "Integer" ,
"val" : "1" }
ce/int.mlw T g_no_lab : Unknown (other)
bench/ce/int.mlw T g_no_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 5:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g_lab0 : Unknown (other)
bench/ce/int.mlw T g_lab0 : Unknown (other)
Counter-example model:File int.mlw:
Line 7:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g2_lab : Unknown (other)
bench/ce/int.mlw T g2_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 12:
x = {"type" : "Integer" ,
"val" : "0" }
ce/int.mlw T newgoal : Unknown (other)
bench/ce/int.mlw T newgoal : Unknown (other)
Counter-example model:File int.mlw:
Line 14:
x2 = {"type" : "Integer" , "val" : "1" }
......
ce/int.mlw T g_no_lab : Unknown (other)
bench/ce/int.mlw T g_no_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 5:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g_lab0 : Unknown (other)
bench/ce/int.mlw T g_lab0 : Unknown (other)
Counter-example model:File int.mlw:
Line 7:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g2_lab : Unknown (other)
bench/ce/int.mlw T g2_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 12:
x = {"type" : "Integer" ,
"val" : "1" }
ce/int.mlw T newgoal : Unknown (other)
bench/ce/int.mlw T newgoal : Unknown (other)
Counter-example model:File int.mlw:
Line 14:
x2 = {"type" : "Integer" , "val" : "1" }
......@@ -33,25 +33,25 @@ x7 = {"type" : "Integer" ,
x8 = {"type" : "Integer" ,
"val" : "1" }
ce/int.mlw T g_no_lab : Unknown (other)
bench/ce/int.mlw T g_no_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 5:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g_lab0 : Unknown (other)
bench/ce/int.mlw T g_lab0 : Unknown (other)
Counter-example model:File int.mlw:
Line 7:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g2_lab : Unknown (other)
bench/ce/int.mlw T g2_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 12:
x = {"type" : "Integer" ,
"val" : "1" }
ce/int.mlw T newgoal : Unknown (other)
bench/ce/int.mlw T newgoal : Unknown (other)
Counter-example model:File int.mlw:
Line 14:
x2 = {"type" : "Integer" , "val" : "1" }
......
ce/int.mlw T g_no_lab : Unknown (other)
bench/ce/int.mlw T g_no_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 5:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g_lab0 : Unknown (other)
bench/ce/int.mlw T g_lab0 : Unknown (other)
Counter-example model:File int.mlw:
Line 7:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g2_lab : Unknown (other)
bench/ce/int.mlw T g2_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 12:
x = {"type" : "Integer" ,
"val" : "1" }
ce/int.mlw T newgoal : Unknown (other)
bench/ce/int.mlw T newgoal : Unknown (other)
Counter-example model:File int.mlw:
Line 14:
x2 = {"type" : "Integer" , "val" : "1" }
......@@ -33,25 +33,25 @@ x7 = {"type" : "Integer" ,
x8 = {"type" : "Integer" ,
"val" : "1" }
ce/int.mlw T g_no_lab : Unknown (other)
bench/ce/int.mlw T g_no_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 5:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g_lab0 : Unknown (other)
bench/ce/int.mlw T g_lab0 : Unknown (other)
Counter-example model:File int.mlw:
Line 7:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g2_lab : Unknown (other)
bench/ce/int.mlw T g2_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 12: