Benchmarking Bit-vector Arithmetic in Z3

This record contains the results of my experiments on how well Z3 is able to handle bit-vector arithmetic and how well it is able to use mulitcore CPU architectures. For more information about the project, read the associated thesis paper. For more information about these results and how to analyze them, have a look at the supporting repository. Satisfiability modulo theories solvers serve as the backbone of software verifiers, static analyzers, and proof assistants; the versatile bit-vector arithmetic theory is particularly important for these applications. As solvers continue to be developed, they become more capable but also more difficult to configure optimally. The widely-used Z3 prover offers a multitude of configurable techniques for solving bit-vector problems, however, the pace of development has not allowed for a comprehensive comparative analysis of them. We study the available bit-vector algorithms and parallelization methods, on established sets of problems. Through an experimental evaluation, we find that properly configuring Z3 for a specific use case can have significant effects on performance. We offer guidance to developers on how to go about that, which should help to make formal verification tools more efficient.