bench test error Alt-Ergo CamlinternalLazy.Undefined
Nummber of tests : 69 Tests: 1021, 1024, 1025, 1084, 1088, 1089, 1093, 1103, 1104, 1111, 1115, 1119, 1157, 1158, 1161, 1175, 1179, 1182, 1191, 1192, 1197, 1201, 1211, 1212, 170, 19, 21, 23, 41, 45, 46, 55, 571, 58, 606, 615, 62, 64, 65, 66, 660, 701, 703, 721, 726, 73, 731, 738, 739, 74, 764, 774, 778, 78, 783, 784, 788, 793, 803, 809, 810, 813, 82, 83, 86, 87, 93, 94, 971 Error: owi: internal error, uncaught exception: CamlinternalLazy.Undefined Raised at Stdlib__Domain.join in file "domain.ml", line 258, characters 16-24 Called from Stdlib__Array.iter in file "array.ml", line 92, characters 31-48 Called from Owi__Wq.read_as_seq in file "src/data_structures/wq.ml", line 17, characters 4-16 Called from Owi__Cmd_sym.print_and_count_failures.aux in file "src/cmd/cmd_sym.ml", line 133, characters 10-20 Called from Owi__Cmd_sym.handle_result in file "src/cmd/cmd_sym.ml", line 199, characters 4-190 Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24 Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44
probably from alt-ergo
Should be fixed by: https://github.com/formalsec/smtml/pull/347
Number of tests: 52 Tests: 100, 103, 1048, 1095, 1097, 1098, 112, 114, 115, 1161, 1163, 1205, 20, 203, 30, 329, 336, 339, 341, 347, 348, 380, 45, 475, 489, 50, 500, 503, 548, 56, 567, 59, 601, 613, 617, 678, 730, 734, 772, 774, 785, 786, 804, 813, 828, 832, 835, 836, 837, 851, 875, 920 Error: owi: internal error, uncaught exception: CamlinternalLazy.Undefined Raised at Stdlib__Domain.join in file "domain.ml", line 258, characters 16-24 Called from Stdlib__Array.iter in file "array.ml", line 92, characters 31-48 Called from Owi__Wq.read_as_seq in file "src/data_structures/wq.ml", line 17, characters 4-16 Called from Owi__Cmd_sym.print_and_count_failures.aux in file "src/cmd/cmd_sym.ml", line 127, characters 10-20 Called from Owi__Cmd_sym.handle_result in file "src/cmd/cmd_sym.ml", line 197, characters 4-190 Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24 Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44
Can you reproduce with a single worker?