This paper presents an application of retiming to model checking, a branch of formal verification. Retiming can change the transition relation of a circuit without changing its input-output behaviour by relocating its registers. With the retiming, a given circuit can have a different structure more adequate for model checking. This paper proposes a cost function to reflect the number of registers and the characteristic of its transition relation and develops a heuristic annealing algorithm to search efficiently the circuit structures obtained by retiming. Experimental results show that the proposed method can improve the model checking performance.