1. A method comprising: by one or more computing devices, using a source code-to-source code rewrite to optimize a C++ function comprising one or more loops for symbolic execution, comprising: for a first loop of the one or more loops, the first loop comprising a first branching condition, performing semantics preserving source code-to-source code rewrite to convert the first loop to move the first branching condition outside the loop; and for a second loop of the one or more loops, the second loop comprising a second branching condition, rewriting the second loop to include a symbolic variable representing a return value and to replace the second loop with an equivalent logical formula relating the symbolic variable with inputs of the C++ function; and wherein: the C++ function comprises a C++ library function, the C++ function further comprises one or more conditional branches, using the source code-to-source code rewrite to optimize the C++ function comprises using a hack-in function to access the symbolic executor to move the exploration of the multiple paths from within the symbolic executor to within the solver, and using the source code-to-source code rewrite for the first loop and the second loop moves the exploration of multiple paths from within a symbolic executor to within a solver.