Skip to content
Snippets Groups Projects
Commit 0080ce31 authored by DAILLER Sylvain's avatar DAILLER Sylvain
Browse files

Merge branch 'ce_bench_error' into 'master' 

ce-bench now fails when there is a diff

See merge request why3/why3!25
parents 0558b653 2f4c5d86
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
bench/ce-bench
+ 7
− 0
View file @ 0080ce31
...@@ -4,6 +4,7 @@ dir=`dirname $0` ...@@ -4,6 +4,7 @@ dir=`dirname $0`
updateoracle=false updateoracle=false
files="" files=""
success=true
while test $# != 0; do while test $# != 0; do
case "$1" in case "$1" in
...@@ -44,6 +45,7 @@ run () { ...@@ -44,6 +45,7 @@ run () {
echo "FAILED!" echo "FAILED!"
echo "diff is the following:" echo "diff is the following:"
diff "$f.oracle" "$f.out" diff "$f.oracle" "$f.out"
success=false
fi fi
fi fi
} }
...@@ -57,3 +59,8 @@ for file in $files; do ...@@ -57,3 +59,8 @@ for file in $files; do
run CVC4,1.5 $filedir/$filebase run CVC4,1.5 $filedir/$filebase
run Z3,4.6.0 $filedir/$filebase run Z3,4.6.0 $filedir/$filebase
done done
if $success; then
exit 0
else
exit 1
fi
bench/ce/floats_CVC4,1.5.oracle
+ 20
− 20
View file @ 0080ce31
bench/ce/floats.mlw T32 g1: Timeout bench/ce/floats.mlw T32 g1: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T32 g2: Timeout bench/ce/floats.mlw T32 g2: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T32 g3: Timeout bench/ce/floats.mlw T32 g3: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T32 g4: Timeout bench/ce/floats.mlw T32 g4: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T32 g5: Timeout bench/ce/floats.mlw T32 g5: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T32 g6: Timeout bench/ce/floats.mlw T32 g6: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T32 g7: Timeout bench/ce/floats.mlw T32 g7: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T32 g8: Timeout bench/ce/floats.mlw T32 g8: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T32 g9: Timeout bench/ce/floats.mlw T32 g9: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T32 g10: Timeout bench/ce/floats.mlw T32 g10: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T64 g1: Timeout bench/ce/floats.mlw T64 g1: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T64 g2: Timeout bench/ce/floats.mlw T64 g2: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T64 g3: Timeout bench/ce/floats.mlw T64 g3: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T64 g4: Timeout bench/ce/floats.mlw T64 g4: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T64 g5: Timeout bench/ce/floats.mlw T64 g5: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T64 g6: Timeout bench/ce/floats.mlw T64 g6: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T64 g7: Timeout bench/ce/floats.mlw T64 g7: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T64 g8: Timeout bench/ce/floats.mlw T64 g8: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T64 g9: Timeout bench/ce/floats.mlw T64 g9: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats.mlw T64 g10: Timeout bench/ce/floats.mlw T64 g10: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" } "val" : "-1" }
bench/ce/floats_Z3,4.6.0.oracle
+ 20
− 20
View file @ 0080ce31
bench/ce/floats.mlw T32 g1: Timeout bench/ce/floats.mlw T32 g1: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -11,7 +11,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -11,7 +11,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g2: Timeout bench/ce/floats.mlw T32 g2: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -22,7 +22,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -22,7 +22,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g3: Timeout bench/ce/floats.mlw T32 g3: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -32,7 +32,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -32,7 +32,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g4: Timeout bench/ce/floats.mlw T32 g4: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -43,7 +43,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -43,7 +43,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g5: Timeout bench/ce/floats.mlw T32 g5: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -54,7 +54,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -54,7 +54,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g6: Timeout bench/ce/floats.mlw T32 g6: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -64,7 +64,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -64,7 +64,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g7: Timeout bench/ce/floats.mlw T32 g7: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -75,7 +75,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -75,7 +75,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g8: Timeout bench/ce/floats.mlw T32 g8: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -85,7 +85,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -85,7 +85,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g9: Timeout bench/ce/floats.mlw T32 g9: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -96,7 +96,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -96,7 +96,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T32 g10: Timeout bench/ce/floats.mlw T32 g10: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -107,7 +107,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -107,7 +107,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g1: Timeout bench/ce/floats.mlw T64 g1: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -118,7 +118,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -118,7 +118,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g2: Timeout bench/ce/floats.mlw T64 g2: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -129,7 +129,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -129,7 +129,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g3: Timeout bench/ce/floats.mlw T64 g3: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -139,7 +139,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -139,7 +139,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g4: Timeout bench/ce/floats.mlw T64 g4: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -150,7 +150,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -150,7 +150,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g5: Timeout bench/ce/floats.mlw T64 g5: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -161,7 +161,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -161,7 +161,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g6: Timeout bench/ce/floats.mlw T64 g6: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -171,7 +171,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -171,7 +171,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g7: Timeout bench/ce/floats.mlw T64 g7: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -182,7 +182,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -182,7 +182,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g8: Timeout bench/ce/floats.mlw T64 g8: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -192,7 +192,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -192,7 +192,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g9: Timeout bench/ce/floats.mlw T64 g9: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
...@@ -203,7 +203,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" , ...@@ -203,7 +203,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
bench/ce/floats.mlw T64 g10: Timeout bench/ce/floats.mlw T64 g10: Timeout
Counter-example model:File ieee_float.mlw: Counter-example model:File ieee_float.mlw:
Line 218: Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" , max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" } "val" : "5" }
File floats.mlw: File floats.mlw:
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment