We study the automation of the verification of Unity programs with infinite or parameterized state space. This paper presents methods allowing the transformation of some second-order formulas expressing invariants into equivalent formulas expressed in a weaker but decidable logic. Two technics are considered: quantifier elimination and reduction to finite domain.