owi icon indicating copy to clipboard operation
owi copied to clipboard

bench test error Alt-Ergo lib/reasoners/bitv.ml 3

Open felixL-K opened this issue 8 months ago • 1 comments

Nummber of tests : 26 Tests: 1181, 1193, 198, 27, 280, 284, 294, 306, 318, 374, 376, 427, 452, 494, 497, 525, 546, 573, 586, 621, 646, 775, 814, 819, 848, 849 Error: owi: internal error, uncaught exception: File "src/lib/reasoners/bitv.ml", line 399, characters 16-22: 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

felixL-K avatar Apr 28 '25 14:04 felixL-K

alt-ergo or mappings bugs?

redianthus avatar Apr 29 '25 13:04 redianthus

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

hra687261 avatar May 16 '25 13:05 hra687261

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

Nummber of tests : 17 Tests: 1085, 202, 325, 378, 409, 430, 439, 497, 544, 570, 588, 626, 644, 733, 794, 819, 844 Error: owi: internal error, uncaught exception: File "src/lib/reasoners/bitv.ml", line 399, characters 16-22: 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

felixL-K avatar May 19 '25 09:05 felixL-K