Fix string register extended terms (#2597)

 Fix string register extended terms (#2597)

A regress2 benchmark was failing, due to a recent change in our strings rewriter.

The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings.

The fix is to ensure that extended function terms in any assertions *or shared terms* are registered.

This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed.