Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob
Dominik Schreiber, Aina Niemetz, Mathias Preiner · Lecture notes in computer science · 2026
We present a distributed platform for massively parallel SMT solving that supports various theories for bit-precise reasoning, with and without quantifiers and push-pop incrementality. Our system is based on an integration of the state-of-the-art SMT solver Bitwuzla into the distributed job scheduling and automated reasoning platform Mallob, which allows Bitwuzla to make heavy use of Mallob ’s distributed incremental SAT solving engine. Our experimental evaluation shows that this approach outperforms prior SMT parallelization approaches and achieves unprecedented speedups at up to 768 cores.