Skip to content
Snippets Groups Projects
Select Git revision
  • 2f4c5d8634ad2bc2e543d11ded7552076082171b
  • master default protected
  • rust
  • extract-fix-master
  • extract-fix
  • extract-fix-1.0.0
6 results

floats_Z3,4.6.0.oracle

Blame
    • floats_Z3,4.6.0.oracle 6.31 KiB 
    bench/ce/floats.mlw T32 g1: Timeout
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 5:
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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 9:
x, [[@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 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 11:
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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 13:
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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 15:
x, [[@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 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
    Line 17:
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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 19:
x, [[@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 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 21:
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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 23:
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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 31:
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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 33:
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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 35:
x, [[@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 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 37:
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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 39:
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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 41:
x, [[@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 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 43:
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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
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
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 49:
    x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.999999999999ap-4" ,
"value" : 0.1 } }