Require `--strings-exp` when using `str.substr` (#4916)

Require `--strings-exp` when using `str.substr` (#4916)

Fixes #4915. Previously, `str.substr` did not require `--strings-exp`.
However, when `--strings-exp` is not active, we do not send terms to the
extended solver for registration, which meant that `str.substr` was
never reduced. This commit adds `str.substr` to the operators that
require `--strings-exp`.