GoRRiLA and hard reality

We call a theory problem a conjunction of theory literals and a theory solver any system that solves theory problems. For implementing efficient theory solvers one needs benchmark problems, and especially hard ones. Unfortunately, hard benchmarks for theory solvers are notoriously difficult to obtain. In this paper we present two tools: Hard Reality for generating theory problems from real-life problems with non-trivial boolean structure and GoRRiLA for generating random theory problems for linear arithmetic. Using GoRRiLA one can generate problems containing only a few variables, which however are difficult for all state-of-the-art solvers we tried. Such problems can be useful for debugging and evaluating solvers on small but hard problems. Using Hard Reality one can generate hard theory problems which are similar to problems found in real-life applications, for example, those taken from SMT-LIB [2]. © 2012 Springer-Verlag Berlin Heidelberg.