bv2int: caching introduced terms (#5283)

bv2int: caching introduced terms (#5283)

The bv-to-int preprocessing pass has a cache that maps each BV node to its translated integer node.
In case the BV node is a function symbol, it's translated integer node is a fresh function symbol.
On current master, if we later process this fresh function symbol in the preprocessing pass, we again create a fresh function symbol as its translation. This is unsound, and was discovered in #5281, whose benchmark is added to regressions.
Closes #5281 if merged.