Introducing previous counter-examples in the CEGIS loop used to produce
contradictions, because some variables were not properly freshened.