+@article{DBLP:journals/tocl/CimattiGIRS18,
+ author = {Alessandro Cimatti and
+ Alberto Griggio and
+ Ahmed Irfan and
+ Marco Roveri and
+ Roberto Sebastiani},
+ title = {Incremental Linearization for Satisfiability and Verification Modulo
+ Nonlinear Arithmetic and Transcendental Functions},
+ journal = {{ACM} Trans. Comput. Log.},
+ volume = {19},
+ number = {3},
+ pages = {19:1--19:52},
+ year = {2018},
+ doi = {10.1145/3230639},
+ timestamp = {Fri, 09 Apr 2021 18:33:35 +0200},
+ biburl = {https://dblp.org/rec/journals/tocl/CimattiGIRS18.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+
@article{IEEE754,
author={IEEE},
journal={IEEE Std 754-2019 (Revision of IEEE 754-2008)},
pages={1-84},
doi={10.1109/IEEESTD.2019.8766229}
}
+
+@article{BansalBRT17,
+ author = {Kshitij Bansal and
+ Clark W. Barrett and
+ Andrew Reynolds and
+ Cesare Tinelli},
+ title = {A New Decision Procedure for Finite Sets and Cardinality Constraints
+ in {SMT}},
+ journal = {CoRR},
+ volume = {abs/1702.06259},
+ year = {2017},
+ archivePrefix = {arXiv},
+ eprint = {1702.06259},
+ timestamp = {Mon, 13 Aug 2018 16:47:11 +0200},
+ biburl = {https://dblp.org/rec/journals/corr/BansalBRT17.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{MengRTB17,
+ author = {Baoluo Meng and
+ Andrew Reynolds and
+ Cesare Tinelli and
+ Clark W. Barrett},
+ editor = {Leonardo de Moura},
+ title = {Relational Constraint Solving in {SMT}},
+ booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on
+ Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
+ series = {Lecture Notes in Computer Science},
+ volume = {10395},
+ pages = {148--165},
+ publisher = {Springer},
+ year = {2017},
+ doi = {10.1007/978-3-319-63046-5_10},
+ timestamp = {Wed, 25 Sep 2019 18:19:14 +0200},
+ biburl = {https://dblp.org/rec/conf/cade/MengRTB17.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{ReynoldsISK16,
+ author = {Andrew Reynolds and
+ Radu Iosif and
+ Cristina Serban and
+ Tim King},
+ editor = {Cyrille Artho and
+ Axel Legay and
+ Doron Peled},
+ title = {A Decision Procedure for Separation Logic in {SMT}},
+ booktitle = {Automated Technology for Verification and Analysis - 14th International
+ Symposium, {ATVA} 2016, Chiba, Japan, October 17-20, 2016, Proceedings},
+ series = {Lecture Notes in Computer Science},
+ volume = {9938},
+ pages = {244--261},
+ year = {2016},
+ doi = {10.1007/978-3-319-46520-3_16},
+ timestamp = {Tue, 14 May 2019 10:00:49 +0200},
+ biburl = {https://dblp.org/rec/conf/atva/ReynoldsIS016.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{ReynoldsB15,
+ author = {Andrew Reynolds and
+ Jasmin Christian Blanchette},
+ editor = {Amy P. Felty and
+ Aart Middeldorp},
+ title = {A Decision Procedure for (Co)datatypes in {SMT} Solvers},
+ booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on
+ Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
+ series = {Lecture Notes in Computer Science},
+ volume = {9195},
+ pages = {197--213},
+ publisher = {Springer},
+ year = {2015},
+ doi = {10.1007/978-3-319-21401-6_13},
+ timestamp = {Tue, 14 May 2019 10:00:39 +0200},
+ biburl = {https://dblp.org/rec/conf/cade/ReynoldsB15.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{BarrettST07,
+ author = {Clark W. Barrett and
+ Igor Shikanian and
+ Cesare Tinelli},
+ title = {An Abstract Decision Procedure for a Theory of Inductive Data Types},
+ journal = {J. Satisf. Boolean Model. Comput.},
+ volume = {3},
+ number = {1-2},
+ pages = {21--46},
+ year = {2007},
+ doi = {10.3233/sat190028},
+ timestamp = {Mon, 17 Aug 2020 18:32:39 +0200},
+ biburl = {https://dblp.org/rec/journals/jsat/BarrettST07.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}