Skip to content

Make CAS slightly more realistic

Ralf Jung requested to merge ralf/cas into gen_proofmode

This restricts CAS to only be able to compare literals with literals, NONEV with NONEV and NONEV with SOMEV for a literal.

In particular, we can no longer CAS pairs.

Merge request reports