Evolving SMT Strategies

StratEVO is an evolutionary algorithm that aims at generating strategies for the SMT solver Z3. Solving SAT modulo theories instance requires to define complex combinations of solvers, heuristics and proof checking tools that require expert knowledge. Our purpose is thus to show that an automated strategy generation process can be efficient and allows end-users to avoid difficult configuration tasks when using such solvers. StratEVO is evaluated on benchmarks from the 2014 and 2015 SMT competitions.