Commit 80605969 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch '268-possible-improvements-in-smt-lib-driver' into 'master'

Resolve "possible improvements in SMT-LIB driver"

Closes #268

See merge request !93
parents 99bd1126 c62462f7
......@@ -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=full;;
# Inconsistent results between two runs
"bench/ce/floats_Z3,4.6.0_SP")
is_xfail=full;;
*) 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" } }
......@@ -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" : "5" }
"val" : "84" }
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" : "5" }
"val" : "84" }
File floats.mlw:
Line 7:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -25,18 +25,14 @@ bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
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 ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Counter-example model:File floats.mlw:
Line 11:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.400000p0" ,
......@@ -46,7 +42,7 @@ bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 13:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -57,7 +53,7 @@ bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 15:
x, [[@introduced]] = {"type" : "Float" ,
......@@ -67,18 +63,18 @@ bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 17:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.800000p32" ,
"value" : -6.44245e+09 } }
"str_hexa" : "-0x1.000000p32" ,
"value" : -4.29497e+09 } }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 19:
x, [[@introduced]] = {"type" : "Float" ,
......@@ -88,7 +84,7 @@ bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 21:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -99,7 +95,7 @@ bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 23:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -110,7 +106,7 @@ bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 31:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -121,7 +117,7 @@ bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 33:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -132,7 +128,7 @@ bench/ce/floats.mlw T64 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 35:
x, [[@introduced]] = {"type" : "Float" ,
......@@ -142,7 +138,7 @@ bench/ce/floats.mlw T64 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 37:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -153,7 +149,7 @@ bench/ce/floats.mlw T64 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 39:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -164,28 +160,24 @@ bench/ce/floats.mlw T64 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
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 ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Counter-example model:File floats.mlw:
Line 43:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.0000000000000p54" ,
"value" : -1.80144e+16 } }
"str_hexa" : "-0x1.0000000040000p512" ,
"value" : -1.34078e+154 } }
bench/ce/floats.mlw T64 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 45:
x, [[@introduced]] = {"type" : "Float" ,
......@@ -195,7 +187,7 @@ bench/ce/floats.mlw T64 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 49:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......
Weakest Precondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Counter-example model:File floats.mlw:
Line 5:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.000002p-126" ,
......@@ -14,7 +10,7 @@ bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 7:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -25,18 +21,14 @@ bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
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 ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Counter-example model:File floats.mlw:
Line 11:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.400000p0" ,
......@@ -46,7 +38,7 @@ bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 13:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -57,7 +49,7 @@ bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 15:
x, [[@introduced]] = {"type" : "Float" ,
......@@ -67,19 +59,15 @@ bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 17:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.800000p32" ,
"value" : -6.44245e+09 } }
"str_hexa" : "-0x1.000000p32" ,
"value" : -4.29497e+09 } }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Counter-example model:File floats.mlw:
Line 19:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
......@@ -88,7 +76,7 @@ bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 21:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -99,7 +87,7 @@ bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 23:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -110,7 +98,7 @@ bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 31:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -121,7 +109,7 @@ bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 33:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -132,18 +120,14 @@ bench/ce/floats.mlw T64 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 35:
x, [[@introduced]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T64 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Counter-example model:File floats.mlw:
Line 37:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "0x1.4000000000000p0" ,
......@@ -153,7 +137,7 @@ bench/ce/floats.mlw T64 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 39:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......@@ -164,7 +148,7 @@ bench/ce/floats.mlw T64 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 41:
x, [[@introduced]] = {"type" : "Float" ,
......@@ -174,18 +158,18 @@ bench/ce/floats.mlw T64 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 43:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
"str_hexa" : "-0x1.0000000000000p54" ,
"value" : -1.80144e+16 } }
"str_hexa" : "-0x1.0000000040000p512" ,
"value" : -1.34078e+154 } }
bench/ce/floats.mlw T64 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 45:
x, [[@introduced]] = {"type" : "Float" ,
......@@ -195,7 +179,7 @@ bench/ce/floats.mlw T64 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "5" }
"val" : "84" }
File floats.mlw:
Line 49:
x, [[@introduced]] = {"type" : "Float" , "val" : {"cons" : "Float_hexa" ,
......
......@@ -112,6 +112,35 @@ theory real.Real
end
theory real.Abs
syntax function abs "(ite (>= %1 0.0) %1 (- %1))"
remove allprops
end
theory real.MinMax
syntax function min "(ite (< %1 %2) %1 %2)"
syntax function max "(ite (< %1 %2) %2 %1)"
remove allprops
end
theory real.FromInt
syntax function from_int "(to_real %1)"
remove allprops
end
theory real.Truncate
syntax function truncate "(ite (>= %1 0.0)
(to_int %1)