Benchmarks of Separation Logic entailments for the prover SLS,
compiled for the POPL'18 paper "Automated Lemma Synthesis in Symbolic-Heap Separation Logic".

They include 4 benchmarks, with all files are converted into
the input syntax format of SLS. The SLS syntax of the test cases
can be referred to: https://songbird-prover.github.io/lemma-synthesis/.
The original benchmarks can be found in the corresponding URL of 
each benchmark.

* slrd-lm:
    The manually created entailment benchmark for SLS.
    Separated to interpreted examples (with integers, int) and uninterpreted examples (unint).
    URL: https://songbird-prover.github.io/lemma-synthesis/


* sll-valid:
    Benchmark of valid entailments about the singly linked list data structure,
    collected from the SL-COMP'14 competition.
    URL: https://github.com/mihasighi/smtcomp14-sl

* slrd-valid:
    Benchmark of valid entailments about various inductive data structures,
    collected from the SL-COMP'14 competition.
    URL: https://github.com/mihasighi/smtcomp14-sl

* slrd-ind:
    Benchmark of entailments from the mutual induction proof paper.
    URL: http://loris-5.d2.comp.nus.edu.sg/songbird/
