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