Mentions légales du service

Skip to content

Draft: Collect functional values from prover model

MARCHE Claude requested to merge collect_logic_functions_from_prover_model into master

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