Sascha Böhme, Michał Moskal
Software verification is one of the most prominent application areas for automated reasoning systems, but their potential improvement is limited by shortage of good benchmarks. Current benchmarks are usually large but shallow, require decision procedures, or have soundness problems. In contrast, we propose a family of benchmarks in first-order logic with equality which is scalable, relatively simple to understand, yet closely resembles difficult verification conditions stemming from real-world C code. Based on this benchmark, we present a detailed comparison of different heap encodings using a number of SMT and ATP systems. Our results led to a performance gain of an order of magnitude for the C code verifier VCC.