Commit 688d958f authored by Sylvain Dailler's avatar Sylvain Dailler

Fix ce-bench for diffs between platforms

This makes Timeout and Unknown equivalent and remove the diff on floats
that differs on moloch and CI.
parent 9457babc
......@@ -34,7 +34,10 @@ run () {
$dir/../bin/why3prove.opt --debug print_attrs -P "$1,counterexamples" --timelimit 1 -a split_vc "$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"
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
# This ad hoc sed removes diff between Timeout and Unknown (unknown)
# when running from platform with different speed.
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' > "$f.out"
if cmp "$f.oracle" "$f.out" > /dev/null 2>&1 ; then
echo "ok"
else
......
bench/ce/algebraic_type.mlw M G: Unknown (unknown)
bench/ce/algebraic_type.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
......
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -7,7 +7,7 @@ Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -16,7 +16,7 @@ Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -25,7 +25,7 @@ Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -34,7 +34,7 @@ Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -43,7 +43,7 @@ Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -52,7 +52,7 @@ Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -61,7 +61,7 @@ Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -70,7 +70,7 @@ Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -79,7 +79,7 @@ Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -88,7 +88,7 @@ Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -97,7 +97,7 @@ Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -106,7 +106,7 @@ Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -115,7 +115,7 @@ Line 31:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (unknown)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -7,7 +7,7 @@ Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -16,7 +16,7 @@ Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -25,7 +25,7 @@ Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -34,7 +34,7 @@ Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -43,7 +43,7 @@ Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -52,7 +52,7 @@ Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -61,7 +61,7 @@ Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -70,7 +70,7 @@ Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -79,7 +79,7 @@ Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -88,7 +88,7 @@ Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -97,7 +97,7 @@ Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -106,7 +106,7 @@ Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......@@ -115,7 +115,7 @@ Line 31:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-176" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
......
bench/ce/arrays.mlw A VC f1: Unknown (unknown)
bench/ce/arrays.mlw A VC f1: Timeout or Unknown
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Unknown (unknown)
bench/ce/arrays.mlw B VC f1: Unknown (unknown)
bench/ce/arrays.mlw B VC f2: Unknown (unknown)
bench/ce/arrays.mlw A VC f2: Timeout or Unknown
bench/ce/arrays.mlw B VC f1: Timeout or Unknown
bench/ce/arrays.mlw B VC f2: Timeout or Unknown
bench/ce/arrays.mlw A VC f1: Timeout
bench/ce/arrays.mlw A VC f1: Timeout or Unknown
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Timeout
bench/ce/arrays.mlw B VC f1: Timeout
bench/ce/arrays.mlw B VC f2: Timeout
bench/ce/arrays.mlw A VC f2: Timeout or Unknown
bench/ce/arrays.mlw B VC f1: Timeout or Unknown
bench/ce/arrays.mlw B VC f2: Timeout or Unknown
......@@ -44,8 +44,8 @@ theory T64
goal g8 : forall x:t. not (eq x (div RNE (1.0:t) (0.0:t)))
goal g9 : forall x:t. gt x (0.0:t) -> gt (div RNE x (2.0:t)) (0.0:t)
(* TODO: Removed due to differences amongst platforms:
goal g9 : forall x:t. gt x (0.0:t) -> gt (div RNE x (2.0:t)) (0.0:t)*)
goal g10: forall x:t. not (ge (mul RNE (10.0:t) x) (1.0:t) /\ (le (mul RTZ (10.0:t) x) (1.0:t)))
end
bench/ce/floats.mlw T32 g1: Timeout
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g2: Timeout
bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g3: Timeout
bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g4: Timeout
bench/ce/floats.mlw T32 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g5: Timeout
bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g6: Timeout
bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g7: Timeout
bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g8: Timeout
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g9: Timeout
bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g10: Timeout
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g1: Timeout
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g2: Timeout
bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g3: Timeout
bench/ce/floats.mlw T64 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g4: Timeout
bench/ce/floats.mlw T64 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g5: Timeout
bench/ce/floats.mlw T64 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g6: Timeout
bench/ce/floats.mlw T64 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g7: Timeout
bench/ce/floats.mlw T64 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g8: Timeout
bench/ce/floats.mlw T64 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g9: Timeout
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g10: Timeout
bench/ce/floats.mlw T64 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......
bench/ce/floats.mlw T32 g1: Timeout
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -9,7 +9,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.000002p-126" ,
"value" : -1.17549e-38 } }
bench/ce/floats.mlw T32 g2: Timeout
bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -20,7 +20,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x0.008000p-127" ,
"value" : -1.14794e-41 } }
bench/ce/floats.mlw T32 g3: Timeout
bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -30,7 +30,7 @@ Line 9:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T32 g4: Timeout
bench/ce/floats.mlw T32 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -41,7 +41,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.400000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T32 g5: Timeout
bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -52,7 +52,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.000002p65" ,
"value" : 3.68935e+19 } }
bench/ce/floats.mlw T32 g6: Timeout
bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -62,7 +62,7 @@ Line 15:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T32 g7: Timeout
bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -73,7 +73,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.800000p32" ,
"value" : -6.44245e+09 } }
bench/ce/floats.mlw T32 g8: Timeout
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -83,7 +83,7 @@ Line 19:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T32 g9: Timeout
bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -94,7 +94,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x0.000002p-127" ,
"value" : 7.00649e-46 } }
bench/ce/floats.mlw T32 g10: Timeout
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -105,7 +105,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.99999ap-4" ,
"value" : 0.1 } }
bench/ce/floats.mlw T64 g1: Timeout
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -116,7 +116,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.0000000000001p-1022" ,
"value" : -2.22507e-308 } }
bench/ce/floats.mlw T64 g2: Timeout
bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -127,7 +127,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x0.0000040000000p-1023" ,
"value" : -2.65249e-315 } }
bench/ce/floats.mlw T64 g3: Timeout
bench/ce/floats.mlw T64 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -137,7 +137,7 @@ Line 35:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T64 g4: Timeout
bench/ce/floats.mlw T64 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -148,7 +148,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5: Timeout
bench/ce/floats.mlw T64 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -159,7 +159,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.0000000000001p513" ,
"value" : 2.68156e+154 } }
bench/ce/floats.mlw T64 g6: Timeout
bench/ce/floats.mlw T64 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -169,7 +169,7 @@ Line 41:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T64 g7: Timeout
bench/ce/floats.mlw T64 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -180,7 +180,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.0000000000000p54" ,
"value" : -1.80144e+16 } }
bench/ce/floats.mlw T64 g8: Timeout
bench/ce/floats.mlw T64 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......@@ -190,18 +190,7 @@ Line 45:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T64 g9: Timeout
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 47:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x0.0000000000001p-1023" ,
"value" : 0 } }
bench/ce/floats.mlw T64 g10: Timeout
bench/ce/floats.mlw T64 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
......
bench/ce/if_decision_branch.mlw Other VC f: Valid
bench/ce/if_decision_branch.mlw Other VC f: Unknown (unknown)
bench/ce/if_decision_branch.mlw Other VC f: Timeout or Unknown
Counter-example model:File if_decision_branch.mlw:
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
......
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Unknown (unknown)
bench/ce/int32.mlw Ce_int32 VC dummy_update: Timeout or Unknown
Counter-example model:File int32.mlw:
Line 6:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
......
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Timeout
bench/ce/int32.mlw Ce_int32 VC dummy_update: Timeout or Unknown
Counter-example model:File int32.mlw:
Line 6:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
......
bench/ce/int.mlw T g_lab: Unknown (unknown)
bench/ce/int.mlw T g_lab: Timeout or Unknown
Counter-example model:File int.mlw:
Line 5:
x, [[@introduced], [@model_trace:x], [@model]] = {"type" : "Integer" ,
"val" : "48" }
bench/ce/int.mlw T g_no_lab: Unknown (unknown)
bench/ce/int.mlw T g_no_lab: Timeout or Unknown
Counter-example model:File int.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "48" }
bench/ce/int.mlw T g2_lab: Unknown (unknown)
bench/ce/int.mlw T g2_lab: Timeout or Unknown
Counter-example model:File int.mlw:
Line 9:
g, [[@model_trace:g]] = {"type" : "Integer" ,
......@@ -19,7 +19,7 @@ Line 11:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/int.mlw T newgoal: Unknown (unknown)
bench/ce/int.mlw T newgoal: Timeout or Unknown
Counter-example model:File int.mlw:
Line 9:
g, [[@model_trace:g]] = {"type" : "Integer" ,
......
bench/ce/int_overflow.mlw ModelInt test0: Valid
bench/ce/int_overflow.mlw ModelInt test1: Unknown (unknown)
bench/ce/int_overflow.mlw ModelInt test1: Timeout or Unknown
Counter-example model:File int_overflow.mlw:
Line 9:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/int_overflow.mlw ModelInt test2: Unknown (unknown)
bench/ce/int_overflow.mlw ModelInt test2: Timeout or Unknown
Counter-example model:File int_overflow.mlw:
Line 14:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/int_overflow.mlw ModelInt test_overflow: Valid
bench/ce/int_overflow.mlw ModelInt test_overflow: Unknown (unknown)
bench/ce/int_overflow.mlw ModelInt test_overflow: Timeout or Unknown
Counter-example model:File int_overflow.mlw:
Line 18:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
......@@ -21,7 +21,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "1" }
bench/ce/int_overflow.mlw ModelInt test_overflow2: Unknown (unknown)
bench/ce/int_overflow.mlw ModelInt test_overflow2: Timeout or Unknown
Counter-example model:File int_overflow.mlw:
Line 23:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
......@@ -29,7 +29,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/int_overflow.mlw ModelInt test_overflow2: Unknown (unknown)
bench/ce/int_overflow.mlw ModelInt test_overflow2: Timeout or Unknown
Counter-example model:File int_overflow.mlw:
Line 23:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
......@@ -38,7 +38,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "1" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int16: Unknown (unknown)
bench/ce/int_overflow.mlw ModelInt test_overflow_int16: Timeout or Unknown
Counter-example model:File int_overflow.mlw:
Line 30:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
......@@ -47,7 +47,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int16_alt: Unknown (unknown)
bench/ce/int_overflow.mlw ModelInt test_overflow_int16_alt: Timeout or Unknown
Counter-example model:File int_overflow.mlw:
Line 35:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
......@@ -56,7 +56,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int16_alt: Unknown (unknown)
bench/ce/int_overflow.mlw ModelInt test_overflow_int16_alt: Timeout or Unknown
Counter-example model:File int_overflow.mlw:
Line 35:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
......@@ -65,7 +65,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "1" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int16_bis: Unknown (unknown)
bench/ce/int_overflow.mlw ModelInt test_overflow_int16_bis: Timeout or Unknown
Counter-example model:File int_overflow.mlw:
Line 40:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
......@@ -74,7 +74,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "32768" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int32: Unknown (unknown)
bench/ce/int_overflow.mlw ModelInt test_overflow_int32: Timeout or Unknown
Counter-example model:File int_overflow.mlw: