Mentions légales du service

Skip to content

Collect functional values from prover model

MOREAU Solene requested to merge collect-functional-values into master

Note: Easier to start again in a new branch instead of trying to merge the master branch into !683 (closed) because of all the changes brought with !728 (merged).

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.

Merge request reports