Commit 916af21b authored by MARCHE Claude's avatar MARCHE Claude
Browse files

run ce bench on Z3

parent a41217ac
......@@ -14,30 +14,33 @@ esac
cd $dir
run_cvc4_15 () {
printf " $1... "
../bin/why3prove.opt -P "CVC4,1.5" --timelimit 1 --get-ce $1 | \
# 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)//' > $1.out
if cmp $1.oracle $1.out > /dev/null 2>&1 ; then
# $1 = prover, $2 = file
run () {
printf " $2 ($1)... "
f="$2_$1"
../bin/why3prove.opt -P "$1" --timelimit 1 --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"
if cmp "$f.oracle" "$f.out" > /dev/null 2>&1 ; then
echo "ok"
else
if $updateoracle; then
echo "Updating oracle for $1"
mv $1.out $1.oracle
echo "Updating oracle for $2, prover $1"
mv "$f.out" "$f.oracle"
else
echo "FAILED!"
echo "diff is the following:"
diff $1.oracle $1.out
diff "$f.oracle" "$f.out"
fi
fi
}
for f in ce/*.mlw; do
run_cvc4_15 $f
for file in ce/*.mlw; do
filebase=`basename $file .mlw`
run CVC4,1.5 ce/$filebase
run Z3,4.5.0 ce/$filebase
run Z3,4.6.0 ce/$filebase
done
ce/int_overflow.mlw ModelInt test0 : Valid
ce/int_overflow.mlw ModelInt test1 : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 9:
x = {"type" : "Integer" ,
"val" : "0" }
ce/int_overflow.mlw ModelInt test2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow : Timeout
ce/int_overflow.mlw ModelInt test_overflow2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Timeout
ce/int_overflow.mlw ModelInt test0 : Valid
ce/int_overflow.mlw ModelInt test1 : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 9:
x = {"type" : "Integer" ,
"val" : "0" }
ce/int_overflow.mlw ModelInt test2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow : Timeout
ce/int_overflow.mlw ModelInt test_overflow2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Timeout
ce/logic.mlw T g0 : Unknown (other)
Counter-example model:File logic.mlw:
Line 6:
x = {"type" : "Integer" ,
"val" : "48" }
ce/logic.mlw T g1 : Unknown (other)
Counter-example model:File logic.mlw:
Line 10:
x = {"type" : "Integer" ,
"val" : "1" }
ce/logic.mlw T g2 : Unknown (other)
Counter-example model:File logic.mlw:
Line 12:
X = {"type" : "Integer" , "val" : "1" }
x2 = {"type" : "Integer" ,
"val" : "1" }
x3 = {"type" : "Integer" ,
"val" : "1" }
x4 = {"type" : "Integer" ,
"val" : "1" }
x5 = {"type" : "Integer" ,
"val" : "1" }
x6 = {"type" : "Integer" ,
"val" : "1" }
x7 = {"type" : "Integer" ,
"val" : "1" }
x8 = {"type" : "Integer" ,
"val" : "1" }
ce/logic.mlw T g0 : Unknown (other)
Counter-example model:File logic.mlw:
Line 6:
x = {"type" : "Integer" ,
"val" : "48" }
ce/logic.mlw T g1 : Unknown (other)
Counter-example model:File logic.mlw:
Line 10:
x = {"type" : "Integer" ,
"val" : "1" }
ce/logic.mlw T g2 : Unknown (other)
Counter-example model:File logic.mlw:
Line 12:
X = {"type" : "Integer" , "val" : "1" }
x2 = {"type" : "Integer" ,
"val" : "1" }
x3 = {"type" : "Integer" ,
"val" : "1" }
x4 = {"type" : "Integer" ,
"val" : "1" }
x5 = {"type" : "Integer" ,
"val" : "1" }
x6 = {"type" : "Integer" ,
"val" : "1" }
x7 = {"type" : "Integer" ,
"val" : "1" }
x8 = {"type" : "Integer" ,
"val" : "1" }
ce/map.mlw M WP_parameter incr : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/map.mlw M WP_parameter test_loop : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/map.mlw M WP_parameter incr : Timeout
ce/map.mlw M WP_parameter test_loop : Timeout
ce/real.mlw ModelReal test1 : Unknown (other)
ce/real.mlw ModelReal test2 : Unknown (other)
Counter-example model:File real.mlw:
Line 7:
x = {"type" : "Decimal" ,
"val" : "0.0" }
ce/real.mlw ModelReal test1 : Timeout
ce/real.mlw ModelReal test2 : Timeout
ce/records.mlw M WP_parameter record_match_eval_test1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter record_match_eval_test2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter record_match_eval_test3 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter record_match_eval_test4 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter test_record_match_eval_test5 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/records.mlw M WP_parameter record_match_eval_test1 : Timeout
ce/records.mlw M WP_parameter record_match_eval_test2 : Timeout
ce/records.mlw M WP_parameter record_match_eval_test3 : Timeout
ce/records.mlw M WP_parameter record_match_eval_test4 : Timeout
ce/records.mlw M WP_parameter test_record_match_eval_test5 : Timeout
ce/ref.mlw M G : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/ref.mlw M WP_parameter test_post : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/ref.mlw M WP_parameter incr : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/ref.mlw M WP_parameter test_loop : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/ref.mlw M G : Timeout
ce/ref.mlw M WP_parameter test_post : Timeout
ce/ref.mlw M WP_parameter incr : Timeout
ce/ref.mlw M WP_parameter test_loop : Timeout
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