bench test error Alt-Ergo AltErgoLib.Errors

[felixL-K]

Nummber of tests : 39 Tests: 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 728, 729, 730, 795, 796, 797, 798, 799, 800, 801 Error: owi: internal error, uncaught exception: AltErgoLib.Errors.Error(_) 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]

Still happens but smtml cannot parse the last path condition (needs https://github.com/OCamlPro/owi/issues/631)

[redianthus]

Can you put the path-condition here? (Along with what's on the stack just before)

[hra687261]

Ok I took a closer look and the issues is Alt-Ergo's lack of support for smt-lib floating-point arithmetic (there might be another way to encore them but I'll have to investigate more). Here's the output:

owi: [INFO] stack         : [ (i32.of_bool (f64.lt_s symbol_0 2.68156230462e+154)) ]
owi: [INFO] running instr : br_if 0
owi: [DEBUG] path condition: [  ]
check [fp.lt symbol_0 (to_fp RoundTowardZero 2.68156230462e+154)]
owi: internal error, uncaught exception:
     Fatal Error: Unsupported Feature: Type FloatingPoint_11_53

[redianthus]

Thanks! Why are the two errors different? Is it that the first one got fixed by your PR on smtml and now we are hitting a new one?

Also, I thought alt-ergo had support for floating-point but was only missing model generation. Isn't it the case?

[hra687261]

Why are the two errors different? Is it that the first one got fixed by your PR on smtml and now we are hitting a new one?

The error is the same, I just added a printer for the exception in https://github.com/formalsec/smtml/pull/349. But now that you mention, maybe I should have kept the exceptions prefix.

Also, I thought alt-ergo had support for floating-point but was only missing model generation. Isn't it the case?

Alt-Ergo doesn't support the SMT-LIB's floating point arithmetic theory, it has its own theory that works by converting back and from reals, but it doesn't have the same signature as the SMT-LIB's FPA theory. Although there are plans to support that one as well.