[SMT-COMP] Problems with scrambler in QF_FP

[Aina Niemetz]

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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: </pipermail/smt-comp/attachments/20190630/569dc885/attachment.asc>