Abstract
This paper presents a non-standard execution model and its propositional encoding for effective bounded model checking of reachability properties. The execution model allows several visible actions from a single system component to be merged dynamically to an atomic block. Thus the bound needed to detect a violation of a property can be reduced. An implementation and results from several test cases are provided.