Proof search tactic unfold applies non-branching propositional reasoning and symbolically executes programs (branches on conjunctions to make progress on programs). Stops at loops and differential equations.
See also