1. A method for test case generation, comprising: verifying a first property of a system with a model checker; automatically generating a second property to reach an initial state of a negation of the first property from an initial state of the system; producing a debug sequence for the second property; adding at least one internal signal from a last time step of the debug sequence for the second property to an assume part of the negated first property to produce a third property; and producing a final debug sequence using a concatenation of the second and third properties.