fixed bug of computing butlast of a sequence

[veanes]

This bug was found by @NikolajBjorner.
It shows up in dealing with derivatives of the reverse of a sequence that then uses butlast
The fix takes care of the following case in #5591

(declare-fun a () String)
(assert (str.in_re (str.++ a "AA") (re.++ (re.* (str.to_re "B")) (str.to_re (str.substr (str.++ "B" a) (str.len a) (str.len a))))))
(check-sat)

now returns unsat as expected.