Commit 323d99cd authored by MARCHE Claude's avatar MARCHE Claude

CE: support for floats binary 32, and more tests on floats

parent 7173bbcb
......@@ -12,6 +12,15 @@ theory T32
goal g5 : forall x:t. not (ge x (4.25:t))
goal g6 : forall x:t. eq x x
goal g7 : forall x:t. t'isFinite x -> gt (add RNE x (1.0:t)) x
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)
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
......@@ -29,5 +38,14 @@ theory T64
goal g5 : forall x:t. not (ge x (4.25:t))
goal g6 : forall x:t. eq x x
goal g7 : forall x:t. t'isFinite x -> gt (add RNE x (1.0:t)) x
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)
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
......@@ -28,33 +28,93 @@ Line 13:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g6 : Unknown (other)
Counter-example model:File floats.mlw:
Line 15:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g7 : Unknown (other)
Counter-example model:File floats.mlw:
Line 17:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g8 : Unknown (other)
Counter-example model:File floats.mlw:
Line 19:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g9 : Unknown (other)
Counter-example model:File floats.mlw:
Line 21:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g10 : Unknown (other)
Counter-example model:File floats.mlw:
Line 23:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g1 : Unknown (other)
Counter-example model:File floats.mlw:
Line 22:
Line 31:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 24:
Line 33:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g3 : Unknown (other)
Counter-example model:File floats.mlw:
Line 26:
Line 35:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 28:
Line 37:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 30:
Line 39:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g6 : Unknown (other)
Counter-example model:File floats.mlw:
Line 41:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g7 : Unknown (other)
Counter-example model:File floats.mlw:
Line 43:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g8 : Unknown (other)
Counter-example model:File floats.mlw:
Line 45:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g9 : Unknown (other)
Counter-example model:File floats.mlw:
Line 47:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g10 : Unknown (other)
Counter-example model:File floats.mlw:
Line 49:
x = {"type" : "Integer" ,
"val" : "0" }
......@@ -88,33 +148,93 @@ Line 13:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g6 : Unknown (other)
Counter-example model:File floats.mlw:
Line 15:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g7 : Unknown (other)
Counter-example model:File floats.mlw:
Line 17:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g8 : Unknown (other)
Counter-example model:File floats.mlw:
Line 19:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g9 : Unknown (other)
Counter-example model:File floats.mlw:
Line 21:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g10 : Unknown (other)
Counter-example model:File floats.mlw:
Line 23:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g1 : Unknown (other)
Counter-example model:File floats.mlw:
Line 22:
Line 31:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 24:
Line 33:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g3 : Unknown (other)
Counter-example model:File floats.mlw:
Line 26:
Line 35:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 28:
Line 37:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 30:
Line 39:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g6 : Unknown (other)
Counter-example model:File floats.mlw:
Line 41:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g7 : Unknown (other)
Counter-example model:File floats.mlw:
Line 43:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g8 : Unknown (other)
Counter-example model:File floats.mlw:
Line 45:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g9 : Unknown (other)
Counter-example model:File floats.mlw:
Line 47:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T64 g10 : Unknown (other)
Counter-example model:File floats.mlw:
Line 49:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/floats.mlw T32 g1 : Unknown (other)
Counter-example model:File floats.mlw:
Line 5:
x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
"exponent" : "#x01" , "sign" : "#b1" ,
"significand" : "#b01000000000000000000000" } }
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.400000p-126" ,
"value" : -1.46937e-38 } }
bench/ce/floats.mlw T32 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 7:
x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
"exponent" : "#x00" , "sign" : "#b1" ,
"significand" : "#b10000000000000000000000" } }
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.800000p-127" ,
"value" : -2.93874e-39 } }
bench/ce/floats.mlw T32 g3 : Unknown (other)
Counter-example model:File floats.mlw:
......@@ -21,64 +21,124 @@ x = {"type" : "Float" ,
bench/ce/floats.mlw T32 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 11:
x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
"exponent" : "#x7f" , "sign" : "#b0" ,
"significand" : "#b01000000000000000000000" } }
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.400000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T32 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 13:
x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
"exponent" : "#x81" , "sign" : "#b0" ,
"significand" : "#b00010000000000000000000" } }
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.100000p2" ,
"value" : 4.25 } }
bench/ce/floats.mlw T32 g6 : Unknown (other)
Counter-example model:File floats.mlw:
Line 15:
x = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T32 g7 : Unknown (other)
Counter-example model:File floats.mlw:
Line 17:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.000000p25" ,
"value" : -3.35544e+07 } }
bench/ce/floats.mlw T32 g8 : Unknown (other)
Counter-example model:File floats.mlw:
Line 19:
x = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T32 g9 : Unknown (other)
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)
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)
Counter-example model:File floats.mlw:
Line 22:
Line 31:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.0000008000000p-1022" ,
"value" : -2.22507e-308 } }
bench/ce/floats.mlw T64 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 24:
Line 33:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.0000010000000p-1023" ,
"value" : -6.63124e-316 } }
bench/ce/floats.mlw T64 g3 : Unknown (other)
Counter-example model:File floats.mlw:
Line 26:
Line 35:
x = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T64 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 28:
Line 37:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 30:
Line 39:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.0800000000000p513" ,
"value" : 2.76536e+154 } }
bench/ce/floats.mlw T64 g6 : Unknown (other)
Counter-example model:File floats.mlw:
Line 41:
x = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T64 g7 : Unknown (other)
Counter-example model:File floats.mlw:
Line 43:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.0000000000000p761" ,
"value" : 1.2129e+229 } }
bench/ce/floats.mlw T64 g8 : Unknown (other)
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)
Counter-example model:File floats.mlw:
Line 49:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.999999999999bp-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_value" ,
"exponent" : "#x01" , "sign" : "#b1" ,
"significand" : "#b01000000000000000000000" } }
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.400000p-126" ,
"value" : -1.46937e-38 } }
bench/ce/floats.mlw T32 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 7:
x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
"exponent" : "#x00" , "sign" : "#b1" ,
"significand" : "#b10000000000000000000000" } }
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.800000p-127" ,
"value" : -2.93874e-39 } }
bench/ce/floats.mlw T32 g3 : Unknown (other)
Counter-example model:File floats.mlw:
......@@ -89,48 +149,108 @@ x = {"type" : "Float" ,
bench/ce/floats.mlw T32 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 11:
x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
"exponent" : "#x7f" , "sign" : "#b0" ,
"significand" : "#b01000000000000000000000" } }
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.400000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T32 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 13:
x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
"exponent" : "#x81" , "sign" : "#b0" ,
"significand" : "#b00010000000000000000000" } }
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.100000p2" ,
"value" : 4.25 } }
bench/ce/floats.mlw T32 g6 : Unknown (other)
Counter-example model:File floats.mlw:
Line 15:
x = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T32 g7 : Unknown (other)
Counter-example model:File floats.mlw:
Line 17:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.000000p25" ,
"value" : -3.35544e+07 } }
bench/ce/floats.mlw T32 g8 : Unknown (other)
Counter-example model:File floats.mlw:
Line 19:
x = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T32 g9 : Unknown (other)
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)
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)
Counter-example model:File floats.mlw:
Line 22:
Line 31:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.0000008000000p-1022" ,
"value" : -2.22507e-308 } }
bench/ce/floats.mlw T64 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 24:
Line 33:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.0000010000000p-1023" ,
"value" : -6.63124e-316 } }
bench/ce/floats.mlw T64 g3 : Unknown (other)
Counter-example model:File floats.mlw:
Line 26:
Line 35:
x = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T64 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 28:
Line 37:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 30:
Line 39:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.0800000000000p513" ,
"value" : 2.76536e+154 } }
bench/ce/floats.mlw T64 g6 : Unknown (other)
Counter-example model:File floats.mlw:
Line 41:
x = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T64 g7 : Unknown (other)
Counter-example model:File floats.mlw:
Line 43:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.0000000000000p761" ,
"value" : 1.2129e+229 } }
bench/ce/floats.mlw T64 g8 : Unknown (other)
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)
Counter-example model:File floats.mlw:
Line 49:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.999999999999bp-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_value" ,
"exponent" : "#x01" , "sign" : "#b1" ,
"significand" : "#b00100000000000000000000" } }
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.200000p-126" ,
"value" : -1.32243e-38 } }
bench/ce/floats.mlw T32 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 7:
x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
"exponent" : "#x00" , "sign" : "#b1" ,
"significand" : "#b00000000000000000000001" } }
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:
......@@ -21,64 +21,124 @@ x = {"type" : "Float" ,
bench/ce/floats.mlw T32 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 11:
x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
"exponent" : "#x7f" , "sign" : "#b0" ,
"significand" : "#b01000000000000000000000" } }
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.400000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T32 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 13:
x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
"exponent" : "#xc0" , "sign" : "#b0" ,
"significand" : "#b00000000000000000000001" } }
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.000002p65" ,
"value" : 3.68935e+19 } }
bench/ce/floats.mlw T32 g6 : Unknown (other)
Counter-example model:File floats.mlw:
Line 15:
x = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T32 g7 : Unknown (other)
Counter-example model:File floats.mlw:
Line 17:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.000000p65" ,
"value" : -3.68935e+19 } }
bench/ce/floats.mlw T32 g8 : Unknown (other)
Counter-example model:File floats.mlw:
Line 19:
x = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T32 g9 : Unknown (other)
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)
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)
Counter-example model:File floats.mlw:
Line 22:
Line 31:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.0100000000000p-1022" ,
"value" : -2.23377e-308 } }
bench/ce/floats.mlw T64 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 24:
Line 33:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.0000000000400p-1023" ,
"value" : -2.52962e-321 } }
bench/ce/floats.mlw T64 g3 : Unknown (other)
Counter-example model:File floats.mlw:
Line 26:
Line 35:
x = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T64 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 28:
Line 37:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5 : Unknown (other)
Counter-example model:File floats.mlw:
Line 30:
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)
Counter-example model:File floats.mlw:
Line 41:
x = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T64 g7 : Unknown (other)
Counter-example model:File floats.mlw:
Line 43:
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.0408000000000p113" ,
"value" : 1.05481e+34 } }
bench/ce/floats.mlw T64 g8 : Unknown (other)
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)
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_value" ,
"exponent" : "#x01" , "sign" : "#b1" ,
"significand" : "#b00100000000000000000000" } }
x = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.200000p-126" ,
"value" : -1.32243e-38 } }
bench/ce/floats.mlw T32 g2 : Unknown (other)
Counter-example model:File floats.mlw:
Line 7:
x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
"exponent" : "#x00" , "sign" : "#b1" ,
"significand" : "#b00000000000000000000001" } }
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:
......@@ -89,48 +149,108 @@ x = {"type" : "Float" ,
bench/ce/floats.mlw T32 g4 : Unknown (other)
Counter-example model:File floats.mlw:
Line 11:
x = {"type" : "Float" , "val" : {"cons" : "Float_value" ,
"exponent" : "#x7f" , "sign" : "#b0" ,