Explain non-emptiness by non-zero length in strings (#4257)

Explain non-emptiness by non-zero length in strings (#4257)

Several kinds of splitting lemmas in the strings solver can sometimes be avoided by observing that str.len(x) != 0 implies that x is non-empty. This generalizes the check for whether x is non-empty is explainable in the current context.