We consider the problem of bounding the worst-caseresourse usage of loop-bounded programs, where assertions about valid program executions may be enforced at selected program points. It is folklore that to be precise, path-sensitivity is needed. This entails unrolling loops in the manner of symbolic simulation. This in turn suggests that the treatment of the individual loop iterations must be greedy in the sense once analysis is finished on one iteration, we cannot backtrack to change it. We show that under these conditions, enforcing assertions produces unsound results. We then present a two-phase algorithm with first uses a greedy strat- egy in the unrolling of loops. This phase explores what is conceptually a symbolic execution tree, which is of enormous size, while eliminates infeasible paths and dominated paths that guaranteed not to contribute to the worst case bound. A compact representation is produced at the end of this phase. Finally, the second phase attacks the remaining problem, to determine the worst-case path in the simplified tree, excluding all paths that violate the assertions from bound calculation. Scalability is achieved via an adaptation of a dynamic programming algorithm.