Fix policy for rewriting string equalities (#6916)

Fix policy for rewriting string equalities (#6916)

This PR simplifies our rewriter for string equalities. We do not try to rewrite equalities to true/false by default.

This prevents cases where lemmas may contain vacuous premises that rewrite to false, hence making a lemma rewrite to true.

This PR reorganizes the interplay between the rewrite and the post-processing of rewrites via extended equality rewriting.

Fixes #6913. Also adds benchmarks from #6101 which appear related but were fixed in previous commits, thus fixes #6101 as well.