Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob

Abstract

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.