Closed Columpio closed 3 years ago
false/productive_use_of_failure_app_inj2.smt2
is also safe, because it is a duplicate of tip2015/list_append_inj_1.smt2
(flipping ys
and zs
)
The benchmark sets come from different sources (e.g. different papers and different people), and have been translated into the TIP notation as they originally appeared (for ease of comparison with the literature, we wanted to include all problems in each set). We have not had the resources to check for overlaps between different benchmark sets I'm afraid, so thank you for this information.
The "true" false property you point out has been removed already, please check out the latest version of the repository.
There a lot of duplicates in benchmarks, which probably should be eliminated. They can be detected with
rdfind
(rdfind -dryrun true TIP
). Consider the full list of duplicates: results.txt