Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers