Stanford researchers did something similar for superoptimization: http://cs.stanford.edu/people/eschkufz/research/asplos291-sc...

They separate the problem into two phases: the first is only worried about correctness, then the second deals with optimization while (eventually) preserving correctness.