Commit bf5118ff authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'new_ide'

parents cd5c33a0 e6e8afd9
......@@ -211,6 +211,9 @@ LIB_PARSER = ptree glob typing parser_messages parser typing report lexer
LIB_TRANSFORM = simplify_formula inlining split_goal \
args_wrapper detect_polymorphism reduction_engine compute \
eliminate_definition eliminate_algebraic \
abstract_quantifiers eliminate_unknown_types \
eliminate_unknown_lsymbols \
eliminate_symbol \
eliminate_inductive eliminate_let eliminate_if \
libencoding discriminate encoding encoding_select \
encoding_guards_full encoding_tags_full \
......
......@@ -30,7 +30,7 @@ fi
run () {
printf " $2 ($1)... "
f="$2_$1"
$dir/../bin/why3prove.opt -P "$1,counterexamples" --timelimit 1 -a split_vc "$2.mlw" | \
$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"
......
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" ,
x, [[@model], [@introduced], [@model_trace: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" ,
x, [[@model], [@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "0" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
Line 31:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "0" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
Line 25:
old i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-1" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "2" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "2" }
Line 31:
i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "2" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "2" }
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "2" }
Line 25:
old i = {"type" : "Integer" ,
i, [[@model], [@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "2" }
bench/ce/floats.mlw T32 g1: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g2: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g3: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g4: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g5: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g6: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g7: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g8: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g9: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g10: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g1: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g2: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g3: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g4: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g5: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g6: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g7: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g8: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g9: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g10: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g1: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 5:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.000002p-126" ,
x, [[@model], [@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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 7:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.008000p-127" ,
x, [[@model], [@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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 9:
x = {"type" : "Float" ,
x, [[@model], [@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T32 g4: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 11:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.400000p0" ,
x, [[@model], [@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.400000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T32 g5: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 13:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.000002p65" ,
x, [[@model], [@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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 15:
x = {"type" : "Float" ,
x, [[@model], [@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T32 g7: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 17:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.800000p32" ,
x, [[@model], [@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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 19:
x = {"type" : "Float" ,
x, [[@model], [@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T32 g9: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 21:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x0.000002p-127" ,
x, [[@model], [@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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 23:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.99999ap-4" ,
x, [[@model], [@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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 31:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.0000000000001p-1022" ,
x, [[@model], [@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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 33:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.0000040000000p-1023" ,
x, [[@model], [@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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 35:
x = {"type" : "Float" ,
x, [[@model], [@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T64 g4: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 37:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.4000000000000p0" ,
x, [[@model], [@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 39:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.0000000000001p513" ,
x, [[@model], [@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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 41:
x = {"type" : "Float" ,
x, [[@model], [@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T64 g7: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 43:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.0000000000000p54" ,
x, [[@model], [@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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 45:
x = {"type" : "Float" ,
x, [[@model], [@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 218:
max_int = {"type" : "Integer" ,
max_int, [[@model], [@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 47:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x0.0000000000001p-1023" ,
x, [[@model], [@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x0.0000000000001p-1023" ,
"value" : 0 } }
bench/ce/floats.mlw T64 g10: Timeout
Counter-example model:File ieee_float.mlw: