Asserting a TransitiveClosure before checking results in "unknown" with reason "unclassified exception" #7103
Description
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