Can BDDs compete with SAT solvers on Bounded Model Checking?