Z3 output containing the full model

gistfile1.txt

sat
(model
  ;; universe for A:
  ;;   A!val!1 A!val!0
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun A!val!1 () A)
  (declare-fun A!val!0 () A)
  ;; cardinality constraint:
  (forall ((x A)) (or (= x A!val!1) (= x A!val!0)))
  ;; -----------
  (define-fun s1 () Bool
    false)
  (define-fun s0 () Int
    0)
  (define-fun int2A ((x!1 Int)) A
    (ite (= x!1 0) A!val!0
      A!val!0))
  (define-fun prop ((x!1 A)) Bool
    (ite (= x!1 A!val!0) true
    (ite (= x!1 A!val!1) true
      true)))
  (define-fun bool2A ((x!1 Bool)) A
    (ite (= x!1 false) A!val!1
      A!val!1))
)