Fix the generation of proof taks by the RAC
The RAC generates proof tasks for checking assertion. This task generation is implemented by some ad-hoc cloning of the module from which the executed function comes from. This cloning is incorrect in general, as shown by various error messages that appear in the check-ce bench after the MR !992 (merged) is merged.