[SMT-COMP] Problems with scrambler in QF_FP

[Aina Niemetz]

Hi Martin,

you're right of course, that was a typo (I actually wrote the correct expression in the commit message)... it's too hot today.

Aina

On June 30, 2019 1:17:58 PM GMT+02:00, Martin Suda <martin.suda at gmail.com> wrote:
>Hi Aina,
>
>I am confused. If the purpose of scrambling is to present an equivalent
>form, shouldn't the scramble of
>
> (fp.leq a x b)
>
>be
>
>(fp.geq b x a)
>
>?
>
>This is a different operator and yet another order than in your
>explanation.
>
>I might be asking something stupid though, just guessing the meaning
>from
>the names.
>
>Best,
>
>Martin
>
>On Sun, Jun 30, 2019, 12:09 PM Aina Niemetz <aina.niemetz at gmail.com>
>wrote:
>
>> Hi all,
>>
>> I just realized that my previous email might have been too brief.
>>
>> The issue we found was a problem when flipping anti-symmetric
>operators,
>> e.g., inequalities. An expression (fp.leq a x b) was scrambled to
>(fp.gt
>> x a b) instead of (fp.gt b a x), which resulted in a flipped result
>in
>> the specific case of the two benchmarks in QF_FP.
>>
>> We didn't find any other issues in other completed divisions of the
>> track. Note that the single query track is still running.
>>
>> Aina
>>
>>
>> On 6/30/19 2:40 AM, Aina Niemetz wrote:
>> > Hi all,
>> >
>> > we found an issue with the benchmark scrambler in division QF_FP in
>the
>> > single query track on the following two benchmarks:
>> >
>> > non-incremental/QF_FP/schanda/spark/guarded_div_1.smt2
>> > non-incremental/QF_FP/schanda/spark/average_2.smt2
>> >
>> > This problem already existed in the 2016-2018 competition versions
>of
>> > the scrambler. It is fixed in
>> >
>>
>https://github.com/SMT-COMP/scrambler/commit/053bb79a79b39749284e4bef31ffc6438a52adf8
>> .
>> >
>> > The two benchmarks in question will be excluded from division
>QF_FP.
>> >
>> > Aina
>> >
>> >
>> > _______________________________________________
>> > SMT-COMP mailing list
>> > SMT-COMP at cs.nyu.edu
>> > https://cs.nyu.edu/mailman/listinfo/smt-comp
>> >
>>
>> _______________________________________________
>> SMT-COMP mailing list
>> SMT-COMP at cs.nyu.edu
>> https://cs.nyu.edu/mailman/listinfo/smt-comp
>>