Smart contracts are immutable programs deployed on the blockchain that can manage significant assets. Because of this, verification and validation of smart contracts is of vital importance. Indeed, it is industrial practice to contract independent specialized companies to audit smart contracts before deployment. Auditors typically rely on a combination of tools and built up experience but still fail to identify problems in smart contracts before deployment, causing significant losses. In this paper, we propose using predicate abstraction to construct behaviour models for supporting auditor validation of smart contracts. These abstractions can be built automatically from combinations of predicates extracted from the source code and predicates provided by auditors based on exploration hypotheses they elaborate during an audit. We present an Alloy prototype for generating abstractions and an evaluation on two benchmarks to show the feasibility of exposing known bugs in smart contracts using predicate abstractions.