In [4],
we benchmarked the tools against three types of scalable formulas:
random formulas, counter formulas, and pattern formulas. Scalability
played an important role in our experiment, since the goal was to
challenge the tools with large formulas and state spaces.