[SMT-LIB] Redundancy in SMT-LIB benchmarks

[Tjark Weber]

Mohamed,

On Fri, 2017-02-10 at 10:17 +0100, Mohamed Iguernlala wrote:
> I don't know if there is some effort in star-exec to detect
> redundant SMT2 scripts. I noticed that the AProVE benchmark of
> QF-NIA category contains a lot of identical formulas. The bench
> contains 8829 files, but only 2409 seem to be different.

Thanks for pointing this out! I intend to remove duplicate benchmarks
from the SMT Library some time before SMT-COMP 2017.

My paper on "Scrambling and Descrambling SMT-LIB Benchmarks" (at SMT
2016) contains a more detailed discussion.

Best,
Tjark