horn_string_benchnchmarks

[hongjianjiang]

HornStr is a solver for invariant synthesis forRegular Model Checking (RMC) with the specification provided in the SMT-LIB 2.6 theory of strings.

This is a set of benchmarks derived from the verification of distributed systems and
string rewriting systems.

Benchmarks are extracted by running HornStr https://arg-git.informatik.uni-kl.de/pub/string-chc-lib on all benchmarks
provided in the repository and gathering the string queries sent to the string solvers.

The benchmarks are divided in incremental and non-incremental queries. We derive the non-incremental benchmarks from the incremental ones. The whole set of non-incremental benchmarks is too big (30000), so we submit only a subset of ~700.

[hansjoergschurr]

Thank you for the submission.

It seems like some benchmarks are duplicates of others. You can find them by running:

find . ! -empty -type f -name *smt2 -exec md5sum {} + | sort | uniq -w32 -d 

[hongjianjiang]

Hi, I remove the duplicated files now, thanks.

[hansjoergschurr]

Ah there are leftover .DS_Store files that the system complains about. You will have to remove those too.

[hansjoergschurr]

I think there are still some left ^^

[hansjoergschurr]

I think there a bunch of edit tasks to do.
Benchmarks with only one check-sat command should be in the non-incremental older. Those benchmarks should also not contain any pop commands, and the status should be at the beginning of the file
Furthermore, some headers are missing (see the README for an example)

[OliverMa1]

I've added the missing headers and removed incremental benchmarks with only 1 (check-sat). I believe the benchmarks should be in the right format now

[hansjoergschurr]

Thank you again for the benchmarks! I will merge the pull request. We will run some solvers on them to see if anything odd comes up, but most likely they will be included in this years release.