Regex performance regression from 4.8.12 to 4.8.13

[ahelwer]

This concerns comparing the regexes (ab)*a(ab)*a and a(ba)*a(ba)* (doubled versions of (ab)*a and a(ba)*). 4.8.12 compares them almost instantaneously (even handling tripled versions) but on 4.8.13 and the 12/1/2021 nightly build it times out, running for up to 6 hours (discovered with a github action test runner timing out). Here is python code to reproduce:

from z3 import *

a = Re('a')
b = Re('b')
r1 = Concat(a, Star(Concat(b, a))) # a(ba)*
r1 = Concat(r1, r1)
r2 = Concat(Star(Concat(a, b)), a) # (ab)*a
r2 = Concat(r2, r2)

s = Solver()
s.add(Distinct(r1, r2))
print(s.check())

[NikolajBjorner]

@ahelwer - could you collect these benchmarks as SMTLIB2 (use print(s.sexpr() + "\n(check-sat)\n")) and submit them to the z3test repository? This makes it easier to catch regressions relevant to your use case.

[NikolajBjorner]

See https://github.com/Z3Prover/z3test/blob/master/regressions/issues/5693.smt2

[NikolajBjorner]

it is fixed