Commit 9455b44a authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'fix_example_iee_float' into 'master'

Fix example iee float

See merge request !102
parents f43c653a a9e83562
......@@ -44,6 +44,12 @@ decide_fail () {
# Inconsistent results between two runs
"bench/ce/ref_mono_Z3,4.6.0_SP")
is_xfail=integer_values;;
# Inconsistent results between two runs
"bench/ce/floats_Z3,4.6.0_WP")
is_xfail=integer_values;;
# Inconsistent results between two runs
"bench/ce/floats_Z3,4.6.0_SP")
is_xfail=integer_values;;
*) is_xfail=none;;
esac
}
......
......@@ -7,7 +7,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 5:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -22,7 +22,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "5\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 7:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -37,7 +37,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 9:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -52,7 +52,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "5\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 11:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -67,7 +67,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "17\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 13:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -82,7 +82,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 15:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -97,7 +97,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 17:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -112,7 +112,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 19:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -124,30 +124,30 @@ Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 21:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 23:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
"val" : "1" } }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
......@@ -157,7 +157,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 31:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -172,7 +172,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "5\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 33:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -187,7 +187,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 35:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -202,7 +202,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "5\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 37:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -217,7 +217,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "17\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 39:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -232,7 +232,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 41:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -247,7 +247,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 43:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -262,7 +262,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 45:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -274,13 +274,13 @@ Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 49:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
"val" : "1" } }
......@@ -7,7 +7,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 5:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -22,7 +22,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "5\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 7:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -37,7 +37,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 9:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -52,7 +52,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "5\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 11:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -67,7 +67,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "17\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 13:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -82,7 +82,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 15:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -97,7 +97,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 17:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -112,7 +112,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 19:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -124,30 +124,30 @@ Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 21:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 23:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
"val" : "1" } }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
......@@ -157,7 +157,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 31:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -172,7 +172,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "5\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 33:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -187,7 +187,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 35:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -202,7 +202,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "5\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 37:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -217,7 +217,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "17\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 39:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -232,7 +232,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 41:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -247,7 +247,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 43:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -262,7 +262,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 45:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -274,13 +274,13 @@ Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 49:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
"val" : "1" } }
Strongest Postcondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
bench/ce/floats.mlw T32 g1: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 5:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.000002p-126" ,
"value" : -1.17549e-38 } }
bench/ce/floats.mlw T32 g2: Timeout or Unknown
bench/ce/floats.mlw T32 g2: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 7:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.008000p-127" ,
"value" : -1.14794e-41 } }
bench/ce/floats.mlw T32 g3: Timeout or Unknown
bench/ce/floats.mlw T32 g3: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 9:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T32 g4: Timeout or Unknown
bench/ce/floats.mlw T32 g4: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 11:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.400000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T32 g5: Timeout or Unknown
bench/ce/floats.mlw T32 g5: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 13:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.000002p65" ,
"value" : 3.68935e+19 } }
bench/ce/floats.mlw T32 g6: Timeout or Unknown
bench/ce/floats.mlw T32 g6: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 15:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T32 g7: Timeout or Unknown
bench/ce/floats.mlw T32 g7: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 17:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.800000p32" ,
"value" : -6.44245e+09 } }
"str_hexa" : "-0x1.000000p65" ,
"value" : -3.68935e+19 } }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
bench/ce/floats.mlw T32 g8: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 19:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T32 g9: Timeout or Unknown
bench/ce/floats.mlw T32 g9: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 21:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x0.000002p-127" ,
"value" : 7.00649e-46 } }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
bench/ce/floats.mlw T32 g10: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 23:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.99999ap-4" ,
"value" : 0.1 } }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
bench/ce/floats.mlw T64 g1: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 31:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.0000000000001p-1022" ,
"value" : -2.22507e-308 } }
bench/ce/floats.mlw T64 g2: Timeout or Unknown
bench/ce/floats.mlw T64 g2: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 33:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.0000040000000p-1023" ,
"value" : -2.65249e-315 } }
bench/ce/floats.mlw T64 g3: Timeout or Unknown
bench/ce/floats.mlw T64 g3: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 35:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T64 g4: Timeout or Unknown
bench/ce/floats.mlw T64 g4: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 37:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5: Timeout or Unknown
bench/ce/floats.mlw T64 g5: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 39:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.0000000000001p513" ,
"value" : 2.68156e+154 } }
bench/ce/floats.mlw T64 g6: Timeout or Unknown
bench/ce/floats.mlw T64 g6: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 41:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T64 g7: Timeout or Unknown
bench/ce/floats.mlw T64 g7: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 43:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.0000000000000p54" ,
"value" : -1.80144e+16 } }
bench/ce/floats.mlw T64 g8: Timeout or Unknown
bench/ce/floats.mlw T64 g8: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 45:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T64 g10: Timeout or Unknown
bench/ce/floats.mlw T64 g10: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 49:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......
Weakest Precondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
bench/ce/floats.mlw T32 g1: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 5:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.000002p-126" ,
"value" : -1.17549e-38 } }
bench/ce/floats.mlw T32 g2: Timeout or Unknown
bench/ce/floats.mlw T32 g2: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 7:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x0.008000p-127" ,
"value" : -1.14794e-41 } }
bench/ce/floats.mlw T32 g3: Timeout or Unknown
bench/ce/floats.mlw T32 g3: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 9:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T32 g4: Timeout or Unknown
bench/ce/floats.mlw T32 g4: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 11:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.400000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T32 g5: Timeout or Unknown
bench/ce/floats.mlw T32 g5: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 13:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.000002p65" ,
"value" : 3.68935e+19 } }
bench/ce/floats.mlw T32 g6: Timeout or Unknown
bench/ce/floats.mlw T32 g6: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 15:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T32 g7: Timeout or Unknown
bench/ce/floats.mlw T32 g7: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 17:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.800000p32" ,
"value" : -6.44245e+09 } }
"str_hexa" : "-0x1.000000p65" ,
"value" : -3.68935e+19 } }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
bench/ce/floats.mlw T32 g8: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 19:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T32 g9: Timeout or Unknown
bench/ce/floats.mlw T32 g9: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 21:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x0.000002p-127" ,
"value" : 7.00649e-46 } }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
bench/ce/floats.mlw T32 g10: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }
File floats.mlw:
Line 23:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.99999ap-4" ,
"value" : 0.1 } }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
bench/ce/floats.mlw T64 g1: Unknown (sat)
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "0" }