How to define higher inductive types in Z3

Question

Higher Inductive Types are very important tools in Homotopy Type Theory. I am trying to define some kinds of higher inductive types using Z3-SMT-LIB. One example is the circle, which is freely generated by a point, base, and a path, loop, from baseto itself. I am using the code

(declare-datatypes () ((Circle base (loop (Circle Circle)))))
(declare-fun x1 () Circle)
(declare-fun x2 () Circle)
(assert (not (= x1 x2)))
(check-sat)
(get-model)

and the output is

sat 
(model 
 (define-fun x2 () Circle (loop base)) 
 (define-fun x1 () Circle base) )

The question is: I am really defining the higher inductive type named circle?

Answer 1

Note that Z3 supports only first-order inductive types. The one you provided is also first-order.