1. A system comprising: a hardware memory; and one or more hardware processors coupled to the hardware memory and configured to perform operations comprising: selecting a portion of a symbolic memory resource based on an analysis of symbolic memory cells of the symbolic memory resource; by symbolic execution, determining a set of values that are referenced by the selected portion of the symbolic memory resource; performing symbolic execution of a target program by utilizing the determined set of values that are referenced by the selected portion of the symbolic memory resource, the performing of the symbolic execution including causing the symbolic execution to switch from a first mode to a second mode, the first mode using multiple interpreters at a branch point in the execution path and continuing the symbolic execution after the branch point without symbolic re-execution of any portion of the execution path prior to the branch point, the second mode initiating a separate symbolic execution of the target program in response to the branch point in the execution path; and creating an input formula for the target program based on the performed symbolic execution that switched from the first mode to the second mode.