1. A method for refining an abstract model, the method comprising: receiving an abstract model which is a subset of a logic design which can be represented using a set of variables and a set of Boolean functions; receiving a safety property for the logic design which is desired to be proven; receiving a set of counter-examples, wherein a counter-example is a sequence of states that violates the safety property, wherein a state is an assignment of values to the variables, wherein the variable values are determined using the set of Boolean functions and the variable values in the previous state; determining a set of cooperative variables using the set of counter-examples, wherein a cooperative variable is a variable that can help invalidate a counter-example; and refining the abstract model using the set of cooperative variables.