While many of the existing approaches to the logical formalization of legal artefacts focus on issues of expressiveness, adequateness and non-automated reasoning, our interest lies in a Computer Science and System Analysis perspective. In particular, we aim at developing tools that build on mechanized logics and perform automated consistency analysis for legal contract documents. Inconsistencies in legal contracts can be static, which means that they include contradictory textual information, or they can be dynamic, leading to (a potential) non-executability of the contract during its dynamic execution. We will present a method and tool called ContractCheck, which performs static and dynamic logical consistency analyses of Share Purchase Agreements (SPAs) based on the SMT solver Z3. We focus on its application to SPAs in the acquisition of corporations, since these are typically shielded from many of the implicit legal background facts implied by legal dogmatics. Starting from the denition of an ontology for SPAs, we provide structured text blocks in ContractCheck from which the contract can be composed. ContractCheck encodes the relevant legal facts from each of the blocks of an SPA in a logic encompassing decidable fragments of rst-order logic (linear real arithmetic, uninterpreted functions). The logical model, together with the applicable logical consistency constraints, are handed over to the SMT solver, and the analysis results are then depicted by ContractCheck. In addition to the computation of inconsistencies, the model construction capabilities of the SMT solver synthesize dynamic contract executions consistent with the contractual constraints. The MaxSMT capabilities even permit to compute preferable orders of claim executions. We view our work as an illustration of how far mechanized logic can take us in understanding and improving even the non-technical facets of the world that we live in.