Allow giant-step only in `Check_ce.select_model`
This a feature wish concerning the function Check_ce.select_model
(or propose an extra function if simpler): only executing the giant-step RAC on potential CEs and return the list of pairs (CE, giant-step result).
This missing feature is currently worked around in the SPARK front-end, by using Check_ce.select_model_last_non_empty
and running the giant-step using lower level functions.
This feature would be useful to other front-ends too (like J3)