tamarin performs various optimizations to accelerate proof construction, and we discuss one such optimization in this chapter. Namely, when loading an input theory, tamarin performs pre-computations to speed up constraint solving later on. The idea is to pre-compute larger constraint solving steps for common parts of the search, which tamarin is likely to encounter multiple times. For all protocol facts, tamarin performs a backwards search for their sources, using the constraint solving algorithm described in Section 6.2. The sources of a protocol fact are those partial executions that yield that fact. These executions are usually incomplete, as trying to compute the complete executions could cause non-termination of the precomputations. For example, adversary deduction steps are not fully explored as this might not terminate. Similarly, protocol facts that can appear in loops are also not explored fully.