SMT Solving for Program Verification