Default fall-through for function pointer removal

[xbauch]

When the pointer points to neither of the candidates we shouldn't just call the
first one (which does happen if the user does not request pointer-check). This
PR inserts an ASSUME (false) which makes all subsequent assertions
unreachable (and thus reported as not being violated).

A small regression test is included.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[hannes-steffenhagen-diffblue]

FWIW there should probably be an assume(false) after this as well.

[tautschnig]

I do agree with this as it would be consistent with what happens with loop-unwinding assertions (where we add the negated loop condition to the path condition). This would effectively simplify the change here as you'd just unconditionally add the assumption below.

[tautschnig]

This is a very good catch, but I'd agree with what @hannes-steffenhagen-diffblue said, so please fix this before merging the change.

[tautschnig]

I do agree with this as it would be consistent with what happens with loop-unwinding assertions (where we add the negated loop condition to the path condition). This would effectively simplify the change here as you'd just unconditionally add the assumption below.

[martin-cs]

No changes needed other than the ones already requested.