bench test error Alt-Ergo lib/structures/expr.ml

[felixL-K]

Nummber of tests : 31 Tests: 1160, 1163, 1166, 1167, 1171, 1172, 1173, 1177, 1180, 1184, 1194, 26, 31, 33, 36, 42, 542, 59, 68, 70, 72, 761, 763, 766, 808, 818, 824, 827, 828, 84, 97 Error: owi: internal error, uncaught exception: File "src/lib/structures/expr.ml", line 1018, characters 6-12: Assertion failed 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

[redianthus]

alt-ergo or mappings bugs?

[hra687261]

Should be fixed by: https://github.com/formalsec/smtml/pull/347

[felixL-K]

I ran the bench tests with alt-ergo v2.6.2, smtml main and owi main branch.

Nummber of tests : 4 Tests: 1033, 1073, 401, 426 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 "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

[hra687261]

What timeout did you use @felixL-K? I can't seem to reproduce them

[felixL-K]

I used a timeout of 1. Sorry I thought that I pulled the last commits of smtml, is this more accurate : I ran the bench tests with alt-ergo's branch v2.6.2, smtml main branch and owi main branch.

Nummber of tests : 3 Tests: 1082, 197, 447 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 "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