The automatic exploit generation challenge we address is given a program, automatically find security-critical bugs and generate exploits. Our approach uses a novel formal verification technique called preconditioned symbolic execution to make automatic exploit generation more scalable to real-world programs than without it.