  We define a new method for taking advantage of net reductions in combination
with a SMT-based model checker. Our approach consists in transforming a
reachability problem about some Petri net, into the verification of an updated
reachability property on a reduced version of this net. This method relies on a
new state space abstraction based on systems of constraints, called polyhedral
abstraction. We prove the correctness of this method using a new notion of
equivalence between nets. We provide a complete framework to define and check
the correctness of equivalence judgements; prove that this relation is a
congruence; and give examples of basic equivalence relations that derive from
structural reductions. Our approach has been implemented in a tool, named SMPT,
that provides two main procedures: Bounded Model Checking (BMC) and Property
Directed Reachability (PDR). Each procedure has been adapted in order to use
reductions and to work with arbitrary Petri nets. We tested SMPT on a large
collection of queries used in the Model Checking Contest. Our experimental
results show that our approach works well, even when we only have a moderate
amount of reductions.
