How do we find that a condition exists that will cause a program to have a predicted outcome? — Using an SAT solver (using logic tests) and an SMT solver (that plugs in numbers), and tells the SAT solver where it got it wrong. They provide feedback in a cycle to each other until a condition can be found.