The longest path search problem is particularly important in the context of low-level worst-case execution time analysis. This implies that all program executions are exhibited and inspected, via convenient abstractions, for their timing behavior. In this paper we present a definitional program unfolder, that is based on the formal executable semantics of a target language. We work with K, a rewrite-based framework for design and analysis of programming languages. Our methodology has two phases. First, it extracts, via reachability analysis, a safe control-flow graph (CFG) approximation, directly from the executable semantics of the language. Second, it unfolds the control-flow graph, annotated with loop bounds, and outputs the set of all possible program executions. The two-phased methodology describes, what we call, a definitional program unfolder and is implemented using the K-Maude tool, a prototype implementation of the K framework.