Hard Reality Tool

HRT is a tool for randomly extracting hard and realistic theory problems (conjunctive constraints) from SMT problems with a non-trivial boolean structure.
HRT is a free software distributed under The GNU General Public License.

README Download

Some generated problems: QF_LRA_gen.tar.gz, QF_LIA_gen.tar.gz, QF_BV_gen.tar.gz, QF_AUFBV_gen.tar.gz

See also GoRRiLA -- a generator of random problems for linear arithmetic.

Konstantin Korovin and Andrei Voronkov