  We define a method for taking advantage of net reductions in combination with
a SMT-based model checker. We prove the correctness of this method using a new
notion of equivalence between nets that we call polyhedral abstraction. 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
during the 2020 edition of the Model Checking Contest. Our experimental results
show that our approach works well, even when we only have a moderate amount of
reductions.
