Fix replace_symbolt for non-lvalues

[tautschnig]

Previously only literal constants were considered non-lvalues, which is insufficient as the unit test shows.

[kroening]

This requires something entirely different.

This should not consider the "lvalue" case, i.e., replacing should always be done.

If this is to be used on the lhs of an assignment, or the like, then some other function, say replace_expr_lvalue, or whatnot, should be defined.

[tautschnig]

This should not consider the "lvalue" case, i.e., replacing should always be done.

Ok, but that's been in the code base for a fair while and is not what this PR newly introduces. I'm happy to fix it though, if I could please get comments on two distinct cases:

1. The lhs of an assignment: arguably this could be done via a separate function rather than controlling it via a parameter as is done now.
2. Within an expression, where an lvalue must be maintained (such as the argument to address-of). What would be a case where substitution should be performed even when that would result in an ill-formed expression?

[tautschnig]

The unit test (first commit in here) has now been moved to #2724, I'll rebase once that's in.

[tautschnig]

This is now based on #2723 with only the very last commit being new. Marking as do-not-merge until #2723 is merged.

[tautschnig]

@kroening This has now been rebased and I'd hope your concerns have been addressed (though mainly that happened in #2723).

[smowton]

Looks sensible