Transitive Closure produces incorrect sat, hangs on eval

[Bickio]

from z3 import *

B = BoolSort()
NodeSort = DeclareSort('Node')

R = Function('R', NodeSort, NodeSort, B)
TC_R = TransitiveClosure(R)

s = Solver()

na, nb, nc = Consts('na nb nc', NodeSort)
s.add(R(na, nb))
s.add(R(nb, na))
s.add(Not(R(na, nc)))
s.add(Not(R(nb, nc)))
s.add(Not(R(nc, na)))
s.add(Not(R(nc, nb)))
s.add(TC_R(na, nc))

print(s.check())
m = s.model()
print(m.eval(TC_R(na, nc)))

Result: sat, process hang when running eval

[NikolajBjorner]

(declare-sort Node)
(declare-fun R (Node Node) Bool)
(define-fun tc ((a Node) (b Node)) Bool ((_ transitive-closure R) a b))

(declare-const na Node)
(declare-const nb Node)
(declare-const nc Node)
(assert (R na nb))
(assert (R nb na))
(assert (not (R na nc)))
(assert (not (R nb nc)))
(assert (not (R nc na)))
(assert (not (R nc nb)))
(assert (tc na nc))
(check-sat)
(get-model)

The formula is satisfiable: the universe is not closed so there is a model with a fourth element that is reachable from a and can reach c.

There is a non-termination bug in evaluation.