Symbolic Model Checking has proven to be a powerful technique for the verification of reactive systems. BDDs have traditionally been used as a symbolic representation of the system. In this paper we show how boolean decision procedures, like Stillmarck's Method or the Davis and Putnam Procedure, can replace BDDs. This new technique avoids the space blow up of BDDs, generates counterexamples much faster, and sometimes speeds up the verification. In addition, it produces counterexamples of minimal length. We introduce a bounded model checking procedure for Lit which reduces model checking to propositional satisfiability. We show that bounded Lit model checking can be done without a tableau construction. We have implemented a model checkerBMC, based on bounded model checking, and preliminary results are presented.