Hey all, Is there an SMTlib equivilant of the Enumerated types theory used in CVC3?? If not, I would like to know what is the most effecient way to deal with an enumerated user defined sort. Thanks in advance. Yours, Mohammad Abdul Aziz