test/regress/regress0/fmf/issue4872-qf_ufc.smt2

   1 (set-logic QF_UFC)
   2 (set-info :status sat)
   3 (declare-sort S0 0)
   4 (declare-const S0-0 S0)
   5 (assert (_ fmf.card S0 1))
   6 (assert (_ fmf.card S0 4))
   7 (check-sat)