An automatic software testing machine may be configured to provide an advanced symbolic execution approach to software testing that combines dynamic symbolic execution and static symbolic execution, leveraging the strengths of each and avoiding the vulnerabilities of each. One or more software testing machines within a software testing system may be configured to automatically and dynamically alternate between dynamic symbolic execution and static symbolic execution, based on partial control flow graphs of portions of the software code to be tested. In some example embodiments, a software testing machine begins with dynamic symbolic execution, but switches to static symbolic execution opportunistically. In static mode, instead of checking entire programs for verification, the software testing machine may only check one or more program fragments for testing purposes. Thus, the software testing machine may benefit from the strengths of both dynamic and static symbolic execution.