z3 - Z3 で SMTLIB 形式のセット メンバーシップを表現するにはどうすればよいですか?

Question

Z3 でセット メンバーシップを表現するために SMTLIB 形式を使用しようとしています。

(declare-const a (Set Int))

;; the next two lines parse correctly in CVC4, but not Z3:
(assert (= a (as emptyset (Set Int))))
(assert (member 12 a))

;; these work in both solvers
(assert (= a (union a a)))
(assert (subset a a))
(assert (= a (intersection a a)))
(check-sat)

関数emptysetとmemberは、CVC4 では期待どおりに解析されるようですが、Z3 ではそうではありません。

API を確認すると (例: https://z3prover.github.io/api/html/group__capi.html )、Z3は空のセットとメンバーシップをプログラムでサポートしていますが、これらを SMTLIB 構文でどのように表現するのでしょうか?