Fix --ackermann in the presence on syntactically different but possibly equal selects...

Fix --ackermann in the presence on syntactically different but possibly equal selects (#4981)

The implementation of --ackermann mishandled selects in a subtle way:
If select is applied to two syntactically different arrays (that may be semantically equal), the ackermann preprocessing failed to generate the "all arguments equal implies terms equal" lemmas.
The problem is that we used the first argument (that is: the array) as lookup to identify terms that need to be considered for these lemmas. Instead we now use their operator (select) just like for uninterpreted function applications.

Fixes #4957 . Also adds a regression.