Murphy Berzish

It doesn't look like a syntax error to me. It is most likely a performance issue with the way Z3str3 handles the operators you've used. I'll take a look and...

I will investigate this.

I've identified the issue and will open a PR once I have run tests on my end.

Opened #1385. This at least fixes the incorrect solution; I'll work on the performance of this encoding next.

I have a fix in progress for this, and it will be opened as a pull request soon.

This case times out as of the latest commit. Do you know the expected response from the solver?

It occurs to me that I have never thought about the semantics of asserting that two `RegLan` terms are equal or unequal before. Is this meaningful according to the SMT-LIB...

Thanks -- taking a look

Still diverges but I'm curious about how z3str3 should interact with `seq.unit` here

I'll look into this.