Skip to content

GitLab

why3
why3
Commit ea09c807 authored by Sylvain Dailler's avatar Sylvain Dailler
2 Browse files
Options

This reverts the commits from branch 268-possible-improvements-[...] 

The merge commit associated was 80605969.
The reason is that these changes to the drivers were badly tested so they
triggered regressions in the nightly-bench
parent a634b6b4
Hide whitespace changes
Inline Side-by-side
Showing with 120 additions and 131 deletions
bench/ce-bench
View file @ ea09c807
......@@ -44,12 +44,6 @@ 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=full;;
# Inconsistent results between two runs
"bench/ce/floats_Z3,4.6.0_SP")
is_xfail=full;;
*) is_xfail=none;;
esac
}
......
bench/ce/oracles/floats_CVC4,1.5_SP.oracle
View file @ ea09c807
......@@ -7,7 +7,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "0" } }
"val" : "2" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "340282346638528859811704183484516925440" }
"val" : "-1" }
File floats.mlw:
Line 21:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
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" : "1" } }
"val" : "10" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "340282346638528859811704183484516925440" }
"val" : "-1" }
File floats.mlw:
Line 23:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
"val" : "10" } }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "1" } }
"val" : "10" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
File floats.mlw:
Line 49:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
"val" : "10" } }
bench/ce/oracles/floats_CVC4,1.5_WP.oracle
View file @ ea09c807
......@@ -7,7 +7,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "340282346638528859811704183484516925440" }
"val" : "-1" }
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" : "0" } }
"val" : "2" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "340282346638528859811704183484516925440" }
"val" : "-1" }
File floats.mlw:
Line 21:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "0" } }
"val" : "2" } }
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" : "1" } }
"val" : "10" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "340282346638528859811704183484516925440" }
"val" : "-1" }
File floats.mlw:
Line 23:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
"val" : "10" } }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
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" : "1" } }
"val" : "10" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
"val" : "-1" }
File floats.mlw:
Line 49:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "1" } }
"val" : "10" } }
bench/ce/oracles/floats_Z3,4.6.0_SP.oracle
View file @ ea09c807
......@@ -3,7 +3,7 @@ bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 5:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -14,7 +14,7 @@ bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 7:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -25,14 +25,18 @@ bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 9:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T32 g4: Timeout or Unknown
Counter-example model:File floats.mlw:
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 11:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.400000p0" ,
......@@ -42,7 +46,7 @@ bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 13:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -53,7 +57,7 @@ bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 15:
x, [[@introduced]] = {"type" : "Float" ,
......@@ -63,18 +67,18 @@ bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 17:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.000000p32" ,
"value" : -4.29497e+09 } }
"str_hexa" : "-0x1.800000p32" ,
"value" : -6.44245e+09 } }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 19:
x, [[@introduced]] = {"type" : "Float" ,
......@@ -84,7 +88,7 @@ bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 21:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -95,7 +99,7 @@ bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 23:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -106,7 +110,7 @@ bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 31:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -117,7 +121,7 @@ bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 33:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -128,7 +132,7 @@ bench/ce/floats.mlw T64 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 35:
x, [[@introduced]] = {"type" : "Float" ,
......@@ -138,7 +142,7 @@ bench/ce/floats.mlw T64 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 37:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -149,7 +153,7 @@ bench/ce/floats.mlw T64 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 39:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -160,24 +164,28 @@ bench/ce/floats.mlw T64 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 41:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T64 g7: Timeout or Unknown
Counter-example model:File floats.mlw:
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 43:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.0000000040000p512" ,
"value" : -1.34078e+154 } }
"str_hexa" : "-0x1.0000000000000p54" ,
"value" : -1.80144e+16 } }
bench/ce/floats.mlw T64 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 45:
x, [[@introduced]] = {"type" : "Float" ,
......@@ -187,7 +195,7 @@ bench/ce/floats.mlw T64 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 49:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......
bench/ce/oracles/floats_Z3,4.6.0_WP.oracle
View file @ ea09c807
Weakest Precondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File floats.mlw:
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 5:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.000002p-126" ,
......@@ -10,7 +14,7 @@ bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 7:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -21,14 +25,18 @@ bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 9:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T32 g4: Timeout or Unknown
Counter-example model:File floats.mlw:
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 11:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.400000p0" ,
......@@ -38,7 +46,7 @@ bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 13:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -49,7 +57,7 @@ bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 15:
x, [[@introduced]] = {"type" : "Float" ,
......@@ -59,15 +67,19 @@ bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 17:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.000000p32" ,
"value" : -4.29497e+09 } }
"str_hexa" : "-0x1.800000p32" ,
"value" : -6.44245e+09 } }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File floats.mlw:
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 19:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
......@@ -76,7 +88,7 @@ bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 21:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -87,7 +99,7 @@ bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 23:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -98,7 +110,7 @@ bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "84" }
"val" : "5" }
File floats.mlw:
Line 31:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -109,7 +121,7 @@ bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222: