{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T23:50:41Z","timestamp":1776297041776,"version":"3.50.1"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227515","type":"print"},{"value":"9783032227522","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T00:00:00Z","timestamp":1776297600000},"content-version":"vor","delay-in-days":105,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22752-2_8","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T21:51:14Z","timestamp":1776289874000},"page":"150-169","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Exploring the SMT-LIB Benchmark Library"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0829-5056","authenticated-orcid":false,"given":"Hans-J\u00f6rg","family":"Schurr","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6756-0788","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Bobot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7142-6258","authenticated-orcid":false,"given":"Mathias","family":"Preiner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2600-5283","authenticated-orcid":false,"given":"Aina","family":"Niemetz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4700-6031","authenticated-orcid":false,"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,16]]},"reference":[{"key":"8_CR1","unstructured":"2.2 manifold learning \u2013 scikit-learn 1.7.2 documentation. https:\/\/scikit-learn.org\/stable\/modules\/manifold.html#isomap, accessed: 2025-10-16"},{"key":"8_CR2","unstructured":"nan_euclidean_distances \u2013 scikit-learn 1.7.2 documentation. https:\/\/scikit-learn.org\/stable\/modules\/generated\/sklearn.metrics.pairwise.nan_euclidean_distances.html, accessed: 2025-10-16"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022. Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Barrett, C., Deters, M., de\u00a0Moura, L., Oliveras, A., Stump, A.: 6 years of SMT-COMP. vol.\u00a050, pp. 243\u2013277 (Mar 2013). https:\/\/doi.org\/10.1007\/s10817-012-9246-5","DOI":"10.1007\/s10817-012-9246-5"},{"key":"8_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"8_CR6","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.7. Tech. rep., Department of Computer Science, The University of Iowa (2025), available at www.SMT-LIB.org"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06806, pp. 171\u2013177. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Deters, M., de\u00a0Moura, L.M., Oliveras, A., Stump, A.: 6 years of SMT-COMP. J. Autom. Reason. 50(3), 243\u2013277 (2013). https:\/\/doi.org\/10.1007\/S10817-012-9246-5","DOI":"10.1007\/S10817-012-9246-5"},{"key":"8_CR9","unstructured":"Biere, A., Fleury, M., Froleyks, N., Heule, J.M.: The SAT museum. In: J\u00e4rvisalo, M., Le\u00a0Berre, D. (eds.) Proceedings of the 14th International Workshop on Pragmatics of SAT Co-located with the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), Alghero, Italy, July, 4, 2023. CEUR Workshop Proceedings, vol.\u00a03545, pp. 72\u201387. CEUR-WS.org (2023), http:\/\/ceur-ws.org\/Vol-3545\/paper6.pdf"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Bobot, F., Hara, H.R.A.E., Correnson, A., Junke, C.: colibri2 (Jun 2025). https:\/\/doi.org\/10.5281\/zenodo.15769941","DOI":"10.5281\/zenodo.15769941"},{"key":"8_CR11","unstructured":"Bury, G.: Dolmen: A validator for SMT-LIB and much more. In: Nadel, A., Niemetz, A. (eds.) Proceedings of the 19th International Workshop on Satisfiability Modulo Theories. CEUR Workshop Proceedings, vol.\u00a02908, pp. 32\u201339. CEUR-WS.org (2021)"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07795, pp. 93\u2013107. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Cok, D.R., Stump, A., Weber, T.: The 2013 evaluation of SMT-COMP and SMT-LIB. J. Autom. Reason. 55(1), 61\u201390 (2015). https:\/\/doi.org\/10.1007\/S10817-015-9328-2","DOI":"10.1007\/S10817-015-9328-2"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Fu, Z., Su, Z.: Xsat: A fast floating-point satisfiability solver. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol.\u00a09780, pp. 187\u2013209. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_11","DOI":"10.1007\/978-3-319-41540-6_11"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Iser, M., Jabs, C.: Global Benchmark Database. In: Chakraborty, S., Jiang, J.H.R. (eds.) 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0305, pp. 18:1\u201318:10. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2024). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2024.18","DOI":"10.4230\/LIPIcs.SAT.2024.18"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Kulczynski, M., Lotz, K., Manea, F., Poulsen, D.B., Sarnighausen-Cahn, P.: SMTQuery: Analysing SMT-LIB string benchmarks. In: C.\u00a0Nogueira, S., Teodorov, C. (eds.) Formal Methods: Foundations and Applications. pp. 22\u201334. Springer Nature Switzerland, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-78116-2_2","DOI":"10.1007\/978-3-031-78116-2_2"},{"key":"8_CR17","unstructured":"Marre, B., Blanc, B., Mouy, P., Chihani, Z., Vedrine, F., Bobot, F.: Colibri (2019), https:\/\/smt-comp.github.io\/2019\/system-descriptions\/colibri.pdf"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13965, pp. 3\u201317. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_1","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Zohar, Y.: Scalable bit-blasting with abstractions. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 178\u2013200. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_9","DOI":"10.1007\/978-3-031-65627-9_9"},{"key":"8_CR21","unstructured":"Organizers, S.C.: The SMT competition. https:\/\/smt-comp.github.io (2025)"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Preiner, M., Schurr, H.J., Barrett, C., Fontaine, P., Niemetz, A., Tinelli, C.: SMT-LIB release 2025 (incremental benchmarks) (May 2025). https:\/\/doi.org\/10.5281\/zenodo.15493096","DOI":"10.5281\/zenodo.15493096"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Preiner, M., Schurr, H.J., Barrett, C., Fontaine, P., Niemetz, A., Tinelli, C.: SMT-LIB release 2025 (non-incremental benchmarks) (Aug 2025). https:\/\/doi.org\/10.5281\/zenodo.15493089","DOI":"10.5281\/zenodo.15493089"},{"key":"8_CR24","unstructured":"Schurr, H.J., Bobot, F.: Github reporsitory: SMT-LIB \/ SMT-LIB-db. https:\/\/github.com\/SMT-LIB\/SMT-LIB-db\/releases\/tag\/tacas26 (2026)"},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Schurr, H.J., Preiner, M., Niemetz, A., Barrett, C., Fontaine, P., Tinelli, C.: SMT-LIB catalog 2025 (Jul 2025). https:\/\/doi.org\/10.5281\/zenodo.16290040","DOI":"10.5281\/zenodo.16290040"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Scott, J., Niemetz, A., Preiner, M., Nejati, S., Ganesh, V.: Algorithm selection for SMT. Int. J. Softw. Tools Technol. Transf. 25(2), 219\u2013239 (2023https:\/\/doi.org\/10.1007\/S10009-023-00696-0","DOI":"10.1007\/S10009-023-00696-0"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08562, pp. 367\u2013373. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"8_CR28","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","DOI":"10.1007\/s10817-017-9407-7"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Tenenbaum, J.B., de\u00a0Silva, V., Langford, J.C.: A global geometric framework for nonlinear dimensionality reduction. Science 290(5500), 2319\u20132323 (2000). https:\/\/doi.org\/10.1126\/science.290.5500.2319","DOI":"10.1126\/science.290.5500.2319"},{"key":"8_CR30","unstructured":"Weber, T.: Par4 system description (2019), https:\/\/smt-comp.github.io\/2019\/system-descriptions\/Par4.pdf"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Weber, T., Conchon, S., D\u00e9harbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT competition 2015\u20132018. J. Satisf. Boolean Model. Comput. 11(1), 221\u2013259 (2019). https:\/\/doi.org\/10.3233\/SAT190123","DOI":"10.3233\/SAT190123"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22752-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T23:10:23Z","timestamp":1776294623000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22752-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227515","9783032227522"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22752-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"16 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}