Félix LOYAU-KAHN

That error seems to be fixed.

with alt-ergo w1 and w56 : Number of tests: 5 Tests: 822, 823, 824, 825, 826 Error: owi: internal error, uncaught exception: Z.Overflow Raised at Stdlib__Domain.join in file "domain.ml", line...

Error not present anymore, must have been fixed by Hichem.

I ran the bench tests with alt-ergo v2.6.2, smtml main and owi main branch. Nummber of tests : 27 Tests: 1045, 1069, 1165, 1170, 1176, 1180, 1184, 1189, 1193, 1195,...

Number of tests: 2 Tests: 898, 1010 Error: owi: internal error, uncaught exception: File "src/lib/reasoners/bitv.ml", line 696, characters 44-50: Assertion failed Raised at Stdlib__Domain.join in file "domain.ml", line 299, characters...

Number of tests: 33 Tests: 1081, 1130, 1131, 298, 300, 323, 357, 359, 388, 390, 394, 398, 413, 419, 421, 474, 487, 493, 500, 504, 506, 512, 524, 539, 543,...

Number of tests: 6 Tests: 1074, 284, 64, 660, 741, 789 Error: owi: internal error, uncaught exception: File "src/lib/structures/expr.ml", line 1055, characters 6-12: Assertion failed Raised at Stdlib__Domain.join in file...

Number of tests: 11 Tests: 1132, 1138, 192, 322, 350, 352, 408, 420, 510, 698, 840 Error: owi: internal error, uncaught exception: Dolmen_std.Expr.Term.Wrong_type(_, _) Raised at Stdlib__Domain.join in file "domain.ml",...

Number of tests: 155 Tests: 1006, 1008, 101, 1011, 1017, 102, 1032, 1037, 104, 1067, 1069, 1071, 1073, 1084, 1085, 1087, 1090, 1091, 1092, 1100, 111, 1119, 1120, 1125, 1128,...

Number of tests: 83 Tests: 1002, 1015, 103, 1035, 1039, 1048, 105, 1053, 1058, 106, 1064, 1072, 1089, 1095, 1097, 1098, 1105, 1107, 1109, 1111, 1116, 1137, 1147, 1150, 1180,...