Arithmetic Solving in Z3 - Bjørner, Nikolaj; Nachmanson, Lev (Computer Aided Verification (CAV 2024), 2024)
The theory of arithmetic is integral to many uses of SMT solvers. Z3 has implemented native solvers for arithmetic reasoning since its first release. We present a full re-implementation of Z3’s original arithmetic solver. It is based on substantial experiences from user feedback, engineering and experimentation. While providing a comprehensive overview of the main components we emphasize selected new insights we arrived at while developing and testing the solver.