A method, apparatus and product for determining invariants in a model. One exemplary embodiments is a computer-implemented method performed by a computerized device, comprising: obtaining a set of candidates of invariants with respect to a model, the model comprising a transition relation axiom and an initial axiom; for substantially each candidate, adding to the model a first auxiliary variable, the first auxiliary variable is defined to be implied from the candidate being held in a predetermined cycle; iteratively trying to prove an inductive step with respect to a subset of the candidates, wherein in response to determining that a candidate is not held inductively removing the candidate from the subset of the candidates, wherein determining which candidate is not held inductively is performed based on values of the first auxiliary variables.