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