We propose the redundancy identification of wire replacement faults. The solutions rely on the satisfiability (SAT) formulation of redundancy identification, augmented with the means to effectively use any single stuck-at-value redundancy identification in the approximate schemes. In the latter, we employ the novel use of don't care approximations that detect many redundant faults and quickly identify those that can be detected by stuck-at value identifications. A test generation scheme that uses the error-correcting properties of Arithmetic Transform is incorporated into the overall verification procedure. The test set provides high fault coverage.