SMT Benchmarks used in

"Computing Optimized Representations for Non-Convex Polyhedra by Detection and Removal of Redundant Linear Constraints"

Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid

On this webpage you can find the benchmarks used in section 4.3 Comparison of the LinAIG based quantifier elimination vs. other solvers.

If you have any questions, feel free to contact Stefan Disch.

Formulas from our Model-Checker for Hybrid Linear Systems

The following formulas stem form the domain of linear hybrid systems. They are automatically generated by our model-checker when computing a continuous pre-image of the state set. We extracted the formulas from 4 different hybrid models and from different pre-image computation steps. The formulas contain an universal as well as an existential quantifier and are composed of variables that range over the reals and the booleans.

The benchmarks are given in the SMT-LIB format.

Download: tacas09-smt.tar.gz (9.8 MB).

Last update: 2008-10-08