Add longer symbolic partial string benchmarks

The new benchmarks cause the SMT solver to be called much more often.
For this to be achieved, the CKA expressions are always by an order of
magnitude longer than in the previous benchmark. Our implementation of
programs can only handle these longer ones because we now generate
partial strings lazily (commit eb9aed1f826a1cd5fdf2a6f4f9711509bc29e517).