Draft: Collect functional values from prover model
Functional values are collected fine (as seen by debug flag cntex_collection
) but they are not transmitted in the candidate counterexample, hence they cannot be used for checking the counterexample using the RAC.
This MR aims at transmitting these functional values as well in the candidate CE