Mentions légales du service

Skip to content
Snippets Groups Projects

Fix example iee float

Merged Fix example iee float
fix_example_iee_float into master
1 unresolved thread
Merged MARCHE Claude requested to merge fix_example_iee_float into master
1 unresolved thread
Compare
and
9 files
+ 208
− 149
Compare changes
  • Side-by-side
  • Inline
Files
9
bench/ce/oracles/floats_CVC4,1.5_SP.oracle
+ 25
− 25
@@ -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" } }