Skip to content

GitLab

why3
why3
Commit 150c6993 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files
Options

Update ce bench 

Fix example incremental.
parent 885f3247
Hide whitespace changes
Inline Side-by-side
Showing with 229 additions and 1622 deletions
bench/ce/algebraic_type_CVC4,1.5.oracle
View file @ 150c6993
......@@ -5,10 +5,3 @@ 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" ,
"val" : "0" }] } }
bench/ce/algebraic_type_Z3,4.6.0.oracle
View file @ 150c6993
......@@ -5,10 +5,3 @@ 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" ,
"val" : "0" }] } }
bench/ce/array_records_CVC4,1.5.oracle
View file @ 150c6993
......@@ -110,115 +110,3 @@ Line 25:
old 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" : "-1" }
Line 27:
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" }
Line 27:
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" }
Line 27:
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" }
Line 28:
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" }
Line 28:
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" }
Line 28:
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" }
Line 29:
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" }
Line 29:
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" }
Line 29:
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" }
Line 30:
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" }
Line 30:
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" }
Line 30:
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" }
Line 31:
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" }
Line 25:
old i = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records_Z3,4.6.0.oracle
View file @ 150c6993
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
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" }
......@@ -6,7 +6,7 @@ Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
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" }
......@@ -14,7 +14,7 @@ Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
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" }
......@@ -22,7 +22,7 @@ Line 27:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
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" }
......@@ -30,7 +30,7 @@ Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
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" }
......@@ -38,7 +38,7 @@ Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
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" }
......@@ -46,7 +46,7 @@ Line 28:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
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" }
......@@ -54,7 +54,7 @@ Line 29:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
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" }
......@@ -62,7 +62,7 @@ Line 29:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
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" }
......@@ -70,7 +70,7 @@ Line 29:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
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" }
......@@ -78,7 +78,7 @@ Line 30:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
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" }
......@@ -86,7 +86,7 @@ Line 30:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
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" }
......@@ -94,133 +94,19 @@ Line 30:
i = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" , "val" : "-176" }
i = {"type" : "Integer" , "val" : "2" }
Line 31:
i = {"type" : "Integer" ,
"val" : "-176" }
"val" : "2" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i = {"type" : "Integer" ,
"val" : "-176" }
Line 25:
old i = {"type" : "Integer" ,
"val" : "-176" }
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" }
Line 27:
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" }
Line 27:
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" }
Line 27:
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" }
Line 28:
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" }
Line 28:
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" }
Line 28:
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" }
Line 29:
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" }
Line 29:
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" }
Line 29:
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" }
Line 30:
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" }
Line 30:
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" }
Line 30:
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" : "-176" }
Line 31:
i = {"type" : "Integer" ,
"val" : "-176" }
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" : "-176" }
i = {"type" : "Integer" , "val" : "2" }
Line 25:
old i = {"type" : "Integer" ,
"val" : "-176" }
"val" : "2" }
bench/ce/arrays_CVC4,1.5.oracle
View file @ 150c6993
......@@ -3,8 +3,3 @@ bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Unknown (other)
bench/ce/arrays.mlw B VC f1: Unknown (other)
bench/ce/arrays.mlw B VC f2: Unknown (other)
bench/ce/arrays.mlw A VC f1: Unknown (other)
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Unknown (other)
bench/ce/arrays.mlw B VC f1: Unknown (other)
bench/ce/arrays.mlw B VC f2: Unknown (other)
bench/ce/arrays_Z3,4.6.0.oracle
View file @ 150c6993
......@@ -3,8 +3,3 @@ 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 f1: Timeout
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/floats_CVC4,1.5.oracle
View file @ 150c6993
bench/ce/floats.mlw T32 g1: Unknown (other)
bench/ce/floats.mlw T32 g2: Unknown (other)
bench/ce/floats.mlw T32 g3: Unknown (other)
bench/ce/floats.mlw T32 g4: Unknown (other)
bench/ce/floats.mlw T32 g5: Unknown (other)
bench/ce/floats.mlw T32 g6: Unknown (other)
bench/ce/floats.mlw T32 g7: Unknown (other)
bench/ce/floats.mlw T32 g8: Unknown (other)
bench/ce/floats.mlw T32 g9: Unknown (other)
bench/ce/floats.mlw T32 g10: Unknown (other)
bench/ce/floats.mlw T64 g1: Unknown (other)
bench/ce/floats.mlw T64 g2: Unknown (other)
bench/ce/floats.mlw T64 g3: Unknown (other)
bench/ce/floats.mlw T64 g4: Unknown (other)
bench/ce/floats.mlw T64 g5: Unknown (other)
bench/ce/floats.mlw T64 g6: Unknown (other)
bench/ce/floats.mlw T64 g7: Unknown (other)
bench/ce/floats.mlw T64 g8: Unknown (other)
bench/ce/floats.mlw T64 g9: Unknown (other)
bench/ce/floats.mlw T64 g10: Unknown (other)
bench/ce/floats.mlw T32 g1: Unknown (other)
bench/ce/floats.mlw T32 g2: Unknown (other)
bench/ce/floats.mlw T32 g3: Unknown (other)
bench/ce/floats.mlw T32 g4: Unknown (other)
bench/ce/floats.mlw T32 g5: Unknown (other)
bench/ce/floats.mlw T32 g6: Unknown (other)
bench/ce/floats.mlw T32 g7: Unknown (other)
bench/ce/floats.mlw T32 g8: Unknown (other)
bench/ce/floats.mlw T32 g9: Unknown (other)
bench/ce/floats.mlw T32 g10: Unknown (other)
bench/ce/floats.mlw T64 g1: Unknown (other)
bench/ce/floats.mlw T64 g2: Unknown (other)
bench/ce/floats.mlw T64 g3: Unknown (other)
bench/ce/floats.mlw T64 g4: Unknown (other)
bench/ce/floats.mlw T64 g5: Unknown (other)
bench/ce/floats.mlw T64 g6: Unknown (other)
bench/ce/floats.mlw T64 g7: Unknown (other)
bench/ce/floats.mlw T64 g8: Unknown (other)
bench/ce/floats.mlw T64 g9: Unknown (other)
bench/ce/floats.mlw T64 g10: Unknown (other)
bench/ce/floats.mlw T32 g1: Timeout
bench/ce/floats.mlw T32 g2: Timeout
bench/ce/floats.mlw T32 g3: Timeout
bench/ce/floats.mlw T32 g4: Timeout
bench/ce/floats.mlw T32 g5: Timeout
bench/ce/floats.mlw T32 g6: Timeout
bench/ce/floats.mlw T32 g7: Timeout
bench/ce/floats.mlw T32 g8: Timeout
bench/ce/floats.mlw T32 g9: Timeout
bench/ce/floats.mlw T32 g10: Timeout
bench/ce/floats.mlw T64 g1: Timeout
bench/ce/floats.mlw T64 g2: Timeout
bench/ce/floats.mlw T64 g3: Timeout
bench/ce/floats.mlw T64 g4: Timeout
bench/ce/floats.mlw T64 g5: Timeout
bench/ce/floats.mlw T64 g6: Timeout
bench/ce/floats.mlw T64 g7: Timeout
bench/ce/floats.mlw T64 g8: Timeout
bench/ce/floats.mlw T64 g9: Timeout
bench/ce/floats.mlw T64 g10: Timeout
bench/ce/floats_Z3,4.6.0.oracle
View file @ 150c6993
bench/ce/floats.mlw T32 g1: Unknown (other)
bench/ce/floats.mlw T32 g1: Timeout
Counter-example model:File floats.mlw:
Line 5:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.800000p-126" ,
"value" : -1.76324e-38 } }
"str_hexa" : "-0x1.000002p-126" ,
"value" : -1.17549e-38 } }
bench/ce/floats.mlw T32 g2: Unknown (other)
bench/ce/floats.mlw T32 g2: Timeout
Counter-example model:File floats.mlw:
Line 7:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.000002p-127" ,
"value" : -7.00649e-46 } }
"str_hexa" : "-0x0.008000p-127" ,
"value" : -1.14794e-41 } }
bench/ce/floats.mlw T32 g3: Unknown (other)
bench/ce/floats.mlw T32 g3: Timeout
Counter-example model:File floats.mlw:
Line 9:
x = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T32 g4: Unknown (other)
bench/ce/floats.mlw T32 g4: Timeout
Counter-example model:File floats.mlw:
Line 11:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.400000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T32 g5: Unknown (other)
bench/ce/floats.mlw T32 g5: Timeout
Counter-example model:File floats.mlw:
Line 13:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.000002p65" ,
"value" : 3.68935e+19 } }
bench/ce/floats.mlw T32 g6: Unknown (other)
bench/ce/floats.mlw T32 g6: Timeout
Counter-example model:File floats.mlw:
Line 15:
x = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T32 g7: Unknown (other)
bench/ce/floats.mlw T32 g7: Timeout
Counter-example model:File floats.mlw:
Line 17:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.c00110p24" ,
"value" : -2.93604e+07 } }
"str_hexa" : "-0x1.800000p32" ,
"value" : -6.44245e+09 } }
bench/ce/floats.mlw T32 g8: Unknown (other)
bench/ce/floats.mlw T32 g8: Timeout
Counter-example model:File floats.mlw:
Line 19:
x = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T32 g9: Unknown (other)
bench/ce/floats.mlw T32 g9: Timeout
Counter-example model:File floats.mlw:
Line 21:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x0.000002p-127" ,
"value" : 7.00649e-46 } }
bench/ce/floats.mlw T32 g10: Unknown (other)
bench/ce/floats.mlw T32 g10: Timeout
Counter-example model:File floats.mlw:
Line 23:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.99999ap-4" ,
"value" : 0.1 } }
bench/ce/floats.mlw T64 g1: Unknown (other)
bench/ce/floats.mlw T64 g1: Timeout
Counter-example model:File floats.mlw:
Line 31:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.0000010000000p-1022" ,
"str_hexa" : "-0x1.0000000000001p-1022" ,
"value" : -2.22507e-308 } }
bench/ce/floats.mlw T64 g2: Unknown (other)
bench/ce/floats.mlw T64 g2: Timeout
Counter-example model:File floats.mlw:
Line 33:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.0000000000200p-1023" ,
"value" : -1.26481e-321 } }
"str_hexa" : "-0x0.0000040000000p-1023" ,
"value" : -2.65249e-315 } }
bench/ce/floats.mlw T64 g3: Unknown (other)
bench/ce/floats.mlw T64 g3: Timeout
Counter-example model:File floats.mlw:
Line 35:
x = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T64 g4: Unknown (other)
bench/ce/floats.mlw T64 g4: Timeout
Counter-example model:File floats.mlw:
Line 37:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5: Unknown (other)
bench/ce/floats.mlw T64 g5: Timeout
Counter-example model:File floats.mlw:
Line 39:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.0000000000001p513" ,
"value" : 2.68156e+154 } }
bench/ce/floats.mlw T64 g6: Unknown (other)
bench/ce/floats.mlw T64 g6: Timeout
Counter-example model:File floats.mlw:
Line 41:
x = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T64 g7: Unknown (other)
bench/ce/floats.mlw T64 g7: Timeout
Counter-example model:File floats.mlw:
Line 43:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.0000000000000p54" ,
"value" : -1.80144e+16 } }
bench/ce/floats.mlw T64 g8: Unknown (other)
bench/ce/floats.mlw T64 g8: Timeout
Counter-example model:File floats.mlw:
Line 45:
x = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T64 g9: Unknown (other)
bench/ce/floats.mlw T64 g10: Unknown (other)
bench/ce/floats.mlw T64 g9: Timeout
Counter-example model:File floats.mlw:
Line 49:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.999999999999ap-4" ,
"value" : 0.1 } }
bench/ce/floats.mlw T32 g1: Unknown (other)
Counter-example model:File floats.mlw:
Line 5:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.800000p-126" ,
"value" : -1.76324e-38 } }
bench/ce/floats.mlw T32 g2: Unknown (other)
Counter-example model:File floats.mlw:
Line 7:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.000002p-127" ,
"value" : -7.00649e-46 } }
bench/ce/floats.mlw T32 g3: Unknown (other)
Counter-example model:File floats.mlw:
Line 9:
x = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T32 g4: Unknown (other)
Counter-example model:File floats.mlw: