Declarative models are powerful tools for building partial models and automatically checking properties about those models. However, they are susceptible to unintentional overconstraint. "Core extraction" is a new analysis that mitigates this problem in the context of a checker based on reduction to SAT. It exploits a recently developed facility of SAT solvers that provides an "unsatisfiable core" of an unsatisfiable set of clauses, which is often much smaller than the clause set as a whole. The unsatisfiable core is mapped back into the syntax of the original model, showing the user fragments of the model found to be irrelevant. This information can be a great help in discovering and localizing overconstraint, and in some cases pinpoints it immediately. The construction of the mapping is given for a generalized modelling language, along with a justification of the soundness of the claim of irrelevance. Experiences in applying core extraction to a variety of existing models are discussed.