A Precise Memory Model for Low-Level Bounded Model Checking