From a given implementation, we generate tests + verify it. We then try
to refactor (or repair if verification failed) by invoking synthesis on
the spec + tests.