Symbolic Detection of Assertion Dependencies for Bounded Model Checking