What's going on with this TransitiveClosure?

[rayegun]

I've asked this over on StackOverflow but thought I'd ping the experts here!
I'm trying to model subgraph connectivity (or just graph connectivity in general). But I'm not sure I understand what's going on with my encoding. Here's an MWE:

s = Solver()
N = DeclareSort('N')
A,B,C = Consts('A B C', N)
F = Function(N,N,BoolSort())
s.add(F(A,B) == True)
s.add(F(B,A) == True)

s.add(F(B,C) == False)
s.add(F(C,B) == False)
s.add(F(A,C) == False)
s.add(F(C,A) == False)

s.add(A != B, B != C, C != A)

FX = TransitiveClosure(F)
s.add(FX(A,C))

I get SAT whether that last line is set to True or False. Shouldn't FX(A,C) be False when we construct the transitive closure?

A follow up question would be how to read the member and connected outputs in the model. They're not documented as far as I can tell.

[vladi7]

I am working with tclosures as well and found this helpful: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-transitive-closure

Maybe there is an answer to your 2nd question as well.