iguerNL
commented
6 years ago Yes, we noticed this and looked at it in the past. We are almost sure that the bug is in the translator.
Closed florianschanda closed 2 years ago
iguerNL
commented
6 years ago Yes, we noticed this and looked at it in the past. We are almost sure that the bug is in the translator.
Hi,
benchmark wintersteiger/min/min-has-solution-13472.smt2 produces the wrong answer when using the benchmark conversion script from https://gitlab.com/OCamlPro-Iguernlala/Three-Tier-FPA-Benchs/tree/master/translators/fp-smt2-to-why3
I am not sure if its an issue with the translator or alt-ergo as I am not entirely sure how to read the input for alt-ergo, so I am afraid there is a bit more detective work for you guys :)