(set-logic UFC) (set-info :status sat) (declare-sort a 0) (declare-fun b () a) (assert (fmf.card b 2)) (check-sat)