title: How to express set membership in SMTLIB format in Z3?
body: <p>I'm trying to use the SMTLIB format to express set membership in Z3:</p>
  <pre><code>(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)
  </code></pre>
  <p>The functions <code>emptyset</code> and <code>member</code> seem to parse as expected in CVC4, but not in Z3.</p>
  <p>From checking the API (e.g., here: <a href="https://z3prover.github.io/api/html/group__capi.html" rel="nofollow noreferrer">https://z3prover.github.io/api/html/group__capi.html</a>), Z3 <strong>does</strong> support empty sets and membership programatically, but how does one express these in SMTLIB syntax?</p>