receiving an abstract model which is a subset of a logic design, wherein the abstract model is 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 helps invalidate a counter-example; and

refining the abstract model using the set of cooperative variables;

wherein the safety property specifies an initial state and a fail variable;

wherein a counter-example is a sequence of states which begins with the initial state, and ends with a state in which the fail variable is true;

wherein the safety property is proven for the logic design if and only if there does not exist a counter-example for the safety property; and

wherein proving the safety property for the abstract model is equivalent to proving the safety property for the logic design.