[BV] Fix strategy for `RewriteExtract` (#8011)

[BV] Fix strategy for `RewriteExtract` (#8011)

`RewriteExtract` was being too eager to return `REWRITE_DONE`. In
particular, it could happen that a term could be rewritten by a series
of `ExtractExtract` and `ExtractConcat` rewrites, but the method would
return `REWRITE_AGAIN` after the first application of `ExtractExtract`.
This commit fixes the method to be more conservative and return
`REWRITE_AGAIN` whenever a rewrite changed the node being rewritten.
Additionally, the commit makes constant folding the last step (to
maximize the chances that it applies) and makes `ExtractExtract` rewrite
multiple nested applications of `extract` with a single application.