The VLSAT-3 (Very Large SAT) Benchmark Suite

The VLSAT-3 benchmark suite (where "VL" stands for "Very Large") is a collection of 1200 SMT formulas to be used as benchmarks in scientific experiments and software competitions. These SMT formulas have been obtained from the automatic conversion into Nested-Unit Petri Nets (NUPNs) of a large collection of Petri nets modelling real-life problems, such as communication protocols and concurrent systems. More than 90% of these benchmarks have been used during the 16th International Satisfiability Modulo Theories Competition (SMT-COMP 2021).