Cmodels is a system that computes answer sets for either disjunctive logic programs or logic programs containing choice rules. Answer set solver Cmodels uses SAT solvers as a search engine for enumerating models of the logic program -- possible solutions. The system Cmodels is based on the relation between two semantics: the answer set and the completion semantics for logic programs.