1. A computer-implemented method performed by a computerized device, comprising: obtaining invariants with respect to a first unbounded model, wherein the invariants are determined based on the first unbounded model; determining a portion of the invariants that are invariants with respect to a second model; mapping variables of the first unbounded model that are comprised by the invariants to variables of the second model; wherein said determining the portion comprises: for substantially each invariant of the first unbounded model, generating a counterpart invariant candidate with respect to the second model, wherein the counterpart invariant candidate is generated using said mapping; and utilizing the portion of the invariants to check that the second model holds a property.