Oren Ish Shalom

@NikolajBjorner thanks, most kinds of queries we generate have **similar** running times for z3 and z3str3. The above example is strictly in favor of z3str3, and #1678 is clearly in...

Thanks!! I looked at the resulting CRs (pasted below), and understood the following: - `out = V_out_0`, `a = V__0` and `b = V__01` - The CRs are mutually recursive,...