State-of-the-art solvers for constrained Horn clauses (CHC) are successfully used to generate reachability facts for software using its symbolic encoding. In this talk, I will present a new application of CHCs to test-case generation, a problem of finding a set of tuples of input values to a program under which the program visits as many branches as possible. The key insight to achieve maximality is to identify and skip blocks of code that are provably unreachable. The new approach to test case generation called HORNTINUUM uses CHC to incrementally construct different program unrollings and extract test cases from models of satisfiable formulas. At the same time, a CHC solver keeps track of CHCs that represent unreachable blocks of code which makes the unrolling process more efficient. In practice, this lets HORNTINUUM terminate early while guaranteeing maximal coverage. HORNTINUUM exhibits promising performance: it generates high coverage in the majority of cases and spends less time on average than state-of-the-art based on bounded model checking, concolic execution, and/or fuzzing.