Formal reasoning about finite sets and cardinality is an important tool for\nmany applications, including software verification, where very often one needs\nto reason about the size of a given data structure and not only about what its\nelements are. The Constraint Logic Programming tool {log} provides a decision\nprocedure for deciding the satisfiability of formulas involving very general\nforms of finite sets, without cardinality. In this paper we adapt and integrate\na decision procedure for a theory of finite sets with cardinality into {log}.\nThe proposed solver is proved to be a decision procedure for its formulas.\nBesides, the new CLP instance is implemented as part of the {log} tool. In\nturn, the implementation uses Howe and King's Prolog SAT solver and Prolog's\nCLP(Q) library, as an integer linear programming solver. The empirical\nevaluation of this implementation based on +250 real verification conditions\nshows that it can be useful in practice.\n