The Strategy Challenge in Satisfiability Modulo Theories (SMT) claims to build theoretical and practical tools allowing users to exert strategic control over core heuristic aspects of high-performance SMT solvers. In this work, we focus on Z3 Theorem Prover: one of the most efficient SMT solvers according to the SMT Competition, SMT-COMP. In SMT solvers, the definition of a strategy relies on a set of tools that can be scheduled and configured in order to guide the search for a (un)satisfiability proof of a given instance. Given these concepts, this challenge could be seen as: • Artificial Intelligence topic, building an algorithm selection procedure to select and order heuristics components to improve SMT solver performance. • Automated Deduction topic, aiming to build more efficient and robust theorem proving solvers. • Search-Based Software Engineering (SBSE) topic, improving SMT software performance by generating a practical tool to manage its own critical code. And also enhancing the resolution of several SBSE problems which are commonly mapped as SMT instances. In this thesis, we address the Strategy Challenge in SMT defining a framework for the autonomous generation of strategies in Z3, i.e., a practical system to automatically generate SMT strategies without the use of expert knowledge. This framework is applied through an incremental evolutionary approach starting from basic algorithms to more complex genetic constructions. The steps include the following: 1. A set of one-task algorithms for SMT strategies: • A simple Parameter Tuner for SMT Strategies (StraTUNE). • A simple Evolutionary Strategy Generator (StratGEN), a skeleton-based evolutionary algorithm to generate SMT strategies. 2. StratEVO, a Tree-based Genetic Programming algorithm that generates complex SMT strategies. 3. A set of cooperative algorithms: • SequencEVO, an off-line sequential cooperative algorithm between StratEVO and StraTUNE. • HybridEVO, a set of StratEVO variations, which used different online cooperative schemes. 4. ExpandEVO, a variety of algorithms that includes time expansion rules in order to generate strategies semantically valid for hard solving contexts. This framework formalises strategies modification as rewriting rules, where algorithms act as engines to apply them. This intermediate layer will allow applying any algorithm or operator with no need to be structurally modified, in order to introduce new information in strategies. Validation is done through experiments on classic benchmarks of the SMT-COMP.