TransitiveClosure + Quantifiers extremely slow

[tzlils]

from z3 import *

Bool = BoolSort()
S = FiniteDomainSort("S", 2)
R = Function("R", S, S, Bool)
TC_R = TransitiveClosure(R)
x,y = Consts("x y", S)
s = Solver()
s.add(ForAll([x, y], TC_R(x, y)))
print(s.check())
m = s.model()
print(m[R])

takes an unreasonable amount of time (i did not run it to completion) using (z3 4.13.0)

[atlasyonatan]

Any updates on this?