GoRRiLA is a generator of random problems in the SMT format for for linear rational/integer arithmetic and propositional logic (in both SMT and DIMACS formats).

GoRRiLA can be used to evaluate solvers on the generated problems.

There are a number of parameters which allow to generate small and at the same time hard random problems.

If you have any questions/suggestions please email: korovincs.man.ac.uk