A computer-implemented method to verify a property for a circuit design, wherein the property defines the correct functionality of the circuit design under verification, and the property specifies a set of constraints that must or must not be satisfied by the circuit design under verification during normal operating conditions, where the property is defined using a set of state variables, wherein each state variable is associated with a sequential element in the circuit design, wherein the length of a path between two sequential elements is based in part on the number of sequential elements in the path, and wherein the distance between two state variables is equal to the length of a shortest path between two sequential elements that are associated with the two state variables, the method comprising the computer-implemented steps of: determining a first counter-example for the property using a first abstract model of the circuit design, wherein the first abstract model includes at least all state variables whose distance from a state variable in the set of state variables is less than or equal to a lower-bound-distance; and verifying the property using an abstraction-refinement technique which comprises: determining an upper-bound-distance for a second abstract model of the circuit design, wherein the upper-bound-distance is equal to the largest distance in a set of distances, and wherein the set of distances includes distances between a first state variable in the set of state variables and a second state variable in the second abstract model; and in response to determining that the lower-bound-distance is greater than or equal to the upper-bound-distance, determining a second counter-example for the property without performing a reachability analysis on the second abstract model. determining a first counter-example for the property using a first abstract model of the circuit design, wherein the first abstract model includes at least all state variables whose distance from a state variable in the set of state variables is less than or equal to a lower-bound-distance; and verifying the property using an abstraction-refinement technique which comprises: determining an upper-bound-distance for a second abstract model of the circuit design, wherein the upper-bound-distance is equal to the largest distance in a set of distances, and wherein the set of distances includes distances between a first state variable in the set of state variables and a second state variable in the second abstract model; and in response to determining that the lower-bound-distance is greater than or equal to the upper-bound-distance, determining a second counter-example for the property without performing a reachability analysis on the second abstract model. determining an upper-bound-distance for a second abstract model of the circuit design, wherein the upper-bound-distance is equal to the largest distance in a set of distances, and wherein the set of distances includes distances between a first state variable in the set of state variables and a second state variable in the second abstract model; and in response to determining that the lower-bound-distance is greater than or equal to the upper-bound-distance, determining a second counter-example for the property without performing a reachability analysis on the second abstract model.