In the course of exploring a program's paths, a symbolic execution-based testing engine frequently ends up re-exploring code that was visited before (e.g., functions that get called from multiple places in the code). This presents an opportunity for speeding up the overall exploration by either doing some extra work a priori, or by caching/memoizing. The Bouncer paper presented one way of doing this. In your OP, propose an alternate way of leveraging this opportunity for saving time by reducing redundant work.