Enforce QP receiver injectivity checks on inhale

[mschwerhoff]

Until now, injectivity of QP receivers has been checked on exhale, and assumed on inhale.

Now (see commit cd75e4b), checking on inhale can be enabled via --checkInjectivity.

Eventually, checking on inhale will be enabled by default. Probably in the first 2022 release.

[mschwerhoff]

Tests cases (currently ignored) can be found in commit 8be053e in test file quantifiedcombinations/injectivity_on_inhale.vpr .

[mschwerhoff]

Todos from a Viper meeting:

• Inform VerCors about upcoming change
• Suggest forall r in xs :: acc(r.f) instead of forall 0 <= i < |xs| :: acc(xs[i].f) to avoid having to specify injectivity of sequences (to Vercors; in tutorial?)
• Historically, r in xs performed worse. Still the case? Problem for, e.g. VerCors?

[marcoeilers]

This has been done a few releases ago so I'll close it.