We address the Worst-Case Execution Time (WCET) Path Analysis problem for bounded programs, formalized as discovering a tight upper bound of a resource variable. A key challenge is posed by complicated loops whose iterations exhibit non-uniform behavior. We adopt a brute-force strategy by simply unrolling them, and show how to make this scalable while preserving accuracy. Our algorithm performs symbolic simulation of the pro- gram. It maintains accuracy because it preserves, at critical points, path-sensitivity. In other words, the simulation detects infeasible paths. Scalability, on the other hand, is dealt with by using summarizations, compact representations of the analyses of loop iterations. They are obtained by a judi- cious use of abstraction which preserves critical information flowing from one iteration to another. These summariza- tions can be compounded in order for the simulation to have linear complexity: the symbolic execution can in fact be asymptotically shorter than a concrete execution. Finally, we present a comprehensive experimental evaluation using a standard benchmark suite. We show that our algorithm is fast, and importantly, we often obtain not just accurate but exact results.