[SMT-LIB] Redundancy in SMT-LIB benchmarks

[Mohamed Iguernlala]

Hi,

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.

I compared files (1) by comparing their md5sum hash, and (2) with
diff command when hashes are equal.

For instance, the most redundant scripts (more than 100
occurrences) have the following hashes:

885 occ : 82c2c6a0adfa7c85ee4d774788ee0e68
536 occ : df9940475c51d91200a7b5e735b9c1b8
523 occ : 043b887419c9b98c0f6c5ce2739b90f8
522 occ : 6c85ddd445725ef5cd4c07a885fc8a06
498 occ : 1313ae28a142091dfcddb7e230d5d158
467 occ : 2e8b7a61841fb06076408b1f47afd16a
403 occ : eef8047dfa3fcfdaec3794c325b8318a
328 occ : 1c26765ccaf1b19043a70f1a5e9f0331
266 occ : 92bc21ee421dae2ee72b10fb5df238f6
229 occ : 0b811652a2dff55b5206f6e025653ab5
196 occ : 225b4206dff63de52152662a5383833a
183 occ : 88500e9a674f5dc96b41534c840ececd
177 occ : d63ac4021d2e426ded1e7e5e04612d83
177 occ : bc01d25a9b5cf8473e9b2e34665cf02d
169 occ : d62ea91f258b4707bab83e1744c3acff

- Mohamed Iguernlala

Senior R&D Engineer, OCamlPro SAS
Research Associate, VALS team, LRI
Webpage: http://www.iguer.xyz
LinkedIn: https://fr.linkedin.com/in/mohamed-iguernlala-71515979