alt-ergo icon indicating copy to clipboard operation
alt-ergo copied to clipboard

Published 20 hours ago • verified publisher icon OCamlPro

unsound answer on wintersteiger

Open florianschanda opened this issue 7 years ago • 1 comments

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 :)

florianschanda avatar Feb 06 '18 15:02 florianschanda

Yes, we noticed this and looked at it in the past. We are almost sure that the bug is in the translator.

iguerNL avatar Feb 07 '18 07:02 iguerNL