Asserting a TransitiveClosure before checking results in "unknown" with reason "unclassified exception"

[kendfrey]

Steps to reproduce

from z3 import *

R = Function("R", IntSort(), IntSort(), BoolSort())
solver = Solver()
# solver.check()
solver.add(TransitiveClosure(R)(0, 1))
print(solver.check())
print(solver.reason_unknown())

Note that uncommenting the first solver.check() line produces the expected behaviour.

Expected behaviour

sat
<irrelevant>

Actual behaviour

unknown
unclassified exception

[kendfrey]

After some more experimentation, I found that, after uncommenting solver.check() and getting sat, if I then call solver.model() I get the following error:

    print(solver.model())
          ^^^^^^^^^^^^^^
  File "C:\Users\Kendall\AppData\Local\Programs\Python\Python311\Lib\site-packages\z3\z3.py", line 7192, in model
    return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\Kendall\AppData\Local\Programs\Python\Python311\Lib\site-packages\z3\z3core.py", line 4255, in Z3_solver_get_model
    r = _elems.f(a0, a1)
        ^^^^^^^^^^^^^^^^
OSError: [WinError -529697949] Windows Error 0xe06d7363

I don't know if it's related or not.