Draft: CE values for function calls

The first 7 commits lay the basics by generating result variables (up to commit "fix oracles), the following commits are about the integration with CE checking and the experiments.

Many sessions in the bench are broken due to the additional variables.

Replaying the Petiot (2018) experiments requires !525 (merged) and !526 (merged).