Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers