@inproceedings{bjrner2024arithmetic,
author = {Bjørner, Nikolaj and Nachmanson, Lev},
title = {Arithmetic Solving in Z3},
booktitle = {Computer Aided Verification (CAV 2024)},
year = {2024},
month = {July},
abstract = {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.},
url = {http://approjects.co.za/?big=en-us/research/publication/arithmetic-solving-in-z3/},
pages = {26-41},
}