References 

[ AFGregoire+11 ]

Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. A modular integration of SAT\slash SMT solvers to Coq through proof witnesses. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs (CPP) , volume 7086 of Lecture Notes in Computer Science, 135–150. Springer, 2011. doi:10.1007/978-3-642-25379-9_12 .

[ BBRT17 ]

Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, and Cesare Tinelli. A new decision procedure for finite sets and cardinality constraints in SMT. CoRR , 2017. arXiv:1702.06259 .

[ BBFF20 ]

Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, and Pascal Fontaine. Scalable fine-grained proofs for formula processing. Journal of Automated Reasoning , 64(3):485–510, 2020. URL: https://doi.org/10.1007/s10817-018-09502-y , doi:10.1007/s10817-018-09502-y .

[ BFT17 ]

Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.6. Technical Report, Department of Computer Science, The University of Iowa, 2017. Available at \tt www.SMT-LIB.org.

[ BST07 ]

Clark W. Barrett, Igor Shikanian, and Cesare Tinelli. An abstract decision procedure for a theory of inductive data types. J. Satisf. Boolean Model. Comput. , 3(1-2):21–46, 2007. doi:10.3233/sat190028 .

[ BdODeharbeF09 ]

Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, and Pascal Fontaine. veriT: An Open, Trustable and Efficient SMT-Solver. In Renate A. Schmidt, editor, Conference on Automated Deduction (CADE) , volume 5663 of Lecture Notes in Computer Science, 151–156. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02959-2_12 , doi:10.1007/978-3-642-02959-2_12 .

[ CGI+18 ]

Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log. , 19(3):19:1–19:52, 2018. doi:10.1145/3230639 .

[ EMT+17 ]

Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark W. Barrett. Smtcoq: A plug-in for integrating SMT solvers into coq. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification (CAV) , volume 10427 of Lecture Notes in Computer Science, 126–133. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_7 , doi:10.1007/978-3-319-63390-9_7 .

[ MRTB17 ]

Baoluo Meng, Andrew Reynolds, Cesare Tinelli, and Clark W. Barrett. Relational constraint solving in SMT. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings , volume 10395 of Lecture Notes in Computer Science, 148–165. Springer, 2017. doi:10.1007/978-3-319-63046-5_10 .

[ RB15 ]

Andrew Reynolds and Jasmin Christian Blanchette. A decision procedure for (co)datatypes in SMT solvers. In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings , volume 9195 of Lecture Notes in Computer Science, 197–213. Springer, 2015. doi:10.1007/978-3-319-21401-6_13 .

[ RISK16 ]

Andrew Reynolds, Radu Iosif, Cristina Serban, and Tim King. A decision procedure for separation logic in SMT. In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings , volume 9938 of Lecture Notes in Computer Science, 244–261. 2016. doi:10.1007/978-3-319-46520-3_16 .

[ SFD21 ]

Hans-Jörg Schurr, Mathias Fleury, and Martin Desharnais. Reliable reconstruction of fine-grained proofs in a proof assistant. In André Platzer and Geoff Sutcliffe, editors, Conference on Automated Deduction (CADE) , volume 12699 of Lecture Notes in Computer Science, 450–467. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_26 , doi:10.1007/978-3-030-79876-5_26 .

[ SOR+13 ]

Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, and Cesare Tinelli. SMT proof checking using a logical framework. Formal Methods Syst. Des. , 42(1):91–118, 2013. URL: https://doi.org/10.1007/s10703-012-0163-3 , doi:10.1007/s10703-012-0163-3 .