Recursive Functions

SMTLIB2 standard: Page 62

You can define recursive functions

Z3 unfolds the definition of recursive functions incrementally by iterative deepening: it attempts first to establish satisfiability modulo a fixed bound on number of unfoldings; if the resulting formula is unsatisfiable and the reason for unsatisfiability is due to the bound restriction, it increases the fixed bound incrementally. Note that this approach does not involve reasoning by induction that is often required to prove deeper properties of recursive functions. This scheme allows to decide satisfiability and unsatisfiability for a limited, but often useful, class of formulas.

Mutually Recursive Functions

You can also define functions that are mutually recursive. The syntax requires to declare all functions first in one block, and then define the bodies of the recursive functions in a second block.