Lattice-Based Refinement in Bounded Model Checking