{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T11:00:40Z","timestamp":1784804440143,"version":"3.55.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325884","type":"print"},{"value":"9783032325891","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\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    SMT solvers increasingly produce proof certificates to meet the trust requirements of safety-critical applications. However, eagerly justifying learned theory lemmas during solving constitutes a major performance bottleneck. Recent work mitigates this cost by emitting proof skeletons that record only SAT reasoning and unannotated theory lemmas, though existing approaches depend on new proof formats and specialized theory-specific tooling. We present a general approach that restricts SMT proof skeletons to core SMT reasoning: preprocessing, clausification, and unannotated theory lemmas. We develop external tools for SAT reasoning and proof trimming that reduce the number of theory lemmas requiring justification. An experimental evaluation using the SMT solver\n                    <jats:sc>cvc5<\/jats:sc>\n                    on SMT-LIB benchmarks across the UF, LIA and LRA theories, with and without quantifiers, demonstrates faster solving and competitive checking performance compared to eager proof production, particularly on quantifier-free problems.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32589-1_10","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:01:37Z","timestamp":1784800897000},"page":"156-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A General Approach for\u00a0SMT Proof Skeletons"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4585-0565","authenticated-orcid":false,"given":"Joseph E.","family":"Reeves","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0188-2300","authenticated-orcid":false,"given":"Haniel","family":"Barbosa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3529-8682","authenticated-orcid":false,"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","unstructured":"Andreotti, B., Lachnitt, H., Barbosa, H.: Carcara: an efficient proof checker and elaborator for SMT proofs in the alethe format. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for Construction and Analysis of Systems (TACAS), Part I. Lecture Notes in Computer Science, vol. 13993, pp. 367\u2013386. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_19","DOI":"10.1007\/978-3-031-30823-9_19"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Backes, J., et al.: Semantic-based automated reasoning for AWS access policies using SMT. In: Bj\u00f8rner, N., Gurfinkel, A. (eds.) Formal Methods in Computer-Aided Design (FMCAD), pp.\u00a01\u20139. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8602994","DOI":"10.23919\/FMCAD.2018.8602994"},{"issue":"10","key":"10_CR3","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3587692","volume":"66","author":"H Barbosa","year":"2023","unstructured":"Barbosa, H., et al.: Generating and exploiting automated reasoning proof certificates. Commun. ACM 66(10), 86\u201395 (2023). https:\/\/doi.org\/10.1145\/3587692","journal-title":"Commun. ACM"},{"issue":"3","key":"10_CR4","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/s10817-018-09502-y","volume":"64","author":"H Barbosa","year":"2019","unstructured":"Barbosa, H., Blanchette, J.C., Fleury, M., Fontaine, P.: Scalable fine-grained proofs for formula processing. J. Autom. Reason. 64(3), 485\u2013510 (2019). https:\/\/doi.org\/10.1007\/s10817-018-09502-y","journal-title":"J. Autom. Reason."},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: Flexible proof production in an industrial-strength SMT solver. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) International Joint Conference on Automated Reasoning (IJCAR). Lecture Notes in Computer Science, vol. 13385, pp. 15\u201335. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_3","DOI":"10.1007\/978-3-031-10769-6_3"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 1267\u20131329. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA201017","DOI":"10.3233\/FAIA201017"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: Cadical 2.0. In: Computer Aided Verification (CAV), pp. 133\u2013152. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_7","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Brown, S.T., Buitrago, P., Hanna, E., Sanielevici, S., Scibek, R., Nystrom, N.A.: Bridges-2: a platform for rapidly-evolving and data intensive research, pp.\u00a01\u20134. Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3437359.3465593","DOI":"10.1145\/3437359.3465593"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories. J. Artif. Int. Res. 40(1), 701\u2013728 (2011). https:\/\/dl.acm.org\/doi\/abs\/10.5555\/2016945.2016964","DOI":"10.1613\/jair.3196"},{"key":"10_CR11","unstructured":"Coltellacci, A., Merz, S., Dowek, G.: Reconstruction of SMT proofs with lambdapi. In: Reger, G., Zohar, Y. (eds.) Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories co-located with the Computer Aided Verification (CAV), Montreal, Canada, 22\u201323 July 2024. CEUR Workshop Proceedings, vol.\u00a03725, pp. 13\u201323. CEUR-WS.org (2024). https:\/\/ceur-ws.org\/Vol-3725\/paper8.pdf"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-63390-9_7","volume-title":"Computer Aided Verification","author":"B Ekici","year":"2017","unstructured":"Ekici, B., et al.: SMTCoq: a plug-in for integrating SMT solvers into Coq. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 126\u2013133. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_7"},{"key":"10_CR13","unstructured":"Farkas, G.: A Fourier-f\u00e9le mechanikai elv alkamaz\u00e1sai. Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtes\u00edt\u00f6 12, 457\u2013472 (1894), reference from Schrijver\u2019s Combinatorial Optimization textbook (Hungarian)"},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"Feng, N., et al.: DRAT proofs of unsatisfiability for SAT modulo monotonic theories. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 3\u201323. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_1","DOI":"10.1007\/978-3-031-57246-3_1"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"10_CR16","unstructured":"Flippo, M., Sidorov, K., Marijnissen, I., Smits, J., Demirovi\u0107, E.: A multi-stage proof logging framework to certify the correctness of CP solvers. In: Shaw, P. (ed.) Constraint Programming (CP). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0307, pp. 11:1\u201311:20. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2024). https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.CP.2024.11"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 167\u2013181. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_11"},{"key":"10_CR18","unstructured":"Hitarth, S., Codel, C., Lachnitt, H., Dutertre, B.: Extending DRAT to SMT (2024). https:\/\/www.amazon.science\/publications\/extending-drat-to-smt"},{"key":"10_CR19","unstructured":"Hoenicke, J., Schindler, T.: A simple proof format for SMT. In: D\u00e9harbe, D., Hyv\u00e4rinen, A.E.J. (eds.) International Workshop on Satisfiability Modulo Theories (SMT). CEUR Workshop Proceedings, vol.\u00a03185, pp. 54\u201370. CEUR-WS.org (2022). http:\/\/ceur-ws.org\/Vol-3185\/paper9527.pdf"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Katz, G., Barrett, C.W., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for DPLL(T)-based SMT solvers. In: Piskac, R., Talupur, M. (eds.) Formal Methods in Computer-Aided Design (FMCAD), pp. 93\u2013100. IEEE (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886666","DOI":"10.1109\/FMCAD.2016.7886666"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Lachnitt, H., et al.: Improving the SMT proof reconstruction pipeline in Isabelle\/HOL. In: Forster, Y., Keller, C. (eds.) Interactive Theorem Proving (ITP). LIPIcs, vol.\u00a0352, pp. 26:1\u201326:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2025). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2025.26","DOI":"10.4230\/LIPICS.ITP.2025.26"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"Lattuada, A., et al.: Verus: a practical foundation for systems verification. In: Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP 2024, pp. 438\u2013454. Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3694715.3695952","DOI":"10.1145\/3694715.3695952"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/978-3-030-81688-9_22","volume-title":"Computer Aided Verification","author":"M Mann","year":"2021","unstructured":"Mann, M., et al.: Pono: a flexible and extensible SMT-based model checker. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 461\u2013474. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_22"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"10_CR27","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Proofs and refutations, and Z3. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) Workshops. CEUR Workshop Proceedings, vol.\u00a0418. CEUR-WS.org (2008)"},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"Mukherjee, R., Kroening, D., Melham, T.: Hardware verification using software analyzers. In: 2015 IEEE Computer Society Annual Symposium on VLSI, pp. 7\u201312 (2015). https:\/\/doi.org\/10.1109\/ISVLSI.2015.107","DOI":"10.1109\/ISVLSI.2015.107"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-32033-3_33","volume-title":"Term Rewriting and Applications","author":"R Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-producing congruence closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 453\u2013468. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_33"},{"issue":"6","key":"10_CR30","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006). https:\/\/doi.org\/10.1145\/1217856.1217859","journal-title":"J. ACM"},{"key":"10_CR31","doi-asserted-by":"publisher","unstructured":"Otoni, R., Blicha, M., Eugster, P., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Theory-specific proof steps witnessing correctness of SMT executions. In: ACM\/IEEE Design Automation Conference (DAC), pp. 541\u2013546 (2021). https:\/\/doi.org\/10.1109\/DAC18074.2021.9586272","DOI":"10.1109\/DAC18074.2021.9586272"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Rawson, M., Voronkov, A., Schoisswohl, J., Komel, A.P.: Ground truth: checking vampire proofs via satisfiability modulo theories. In: Barrett, C.W., Waldmann, U. (eds.) Proceedings of Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 15943, pp. 136\u2013149. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-99984-0_8","DOI":"10.1007\/978-3-031-99984-0_8"},{"key":"10_CR33","doi-asserted-by":"publisher","unstructured":"Reeves, J.E., Kiesl-Reiter, B., Heule, M.J.H.: Propositional proof skeletons. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 329\u2013347. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_17","DOI":"10.1007\/978-3-031-30823-9_17"},{"key":"10_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-89963-3_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Reynolds","year":"2018","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 112\u2013131. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_7"},{"key":"10_CR35","doi-asserted-by":"publisher","unstructured":"Rungta, N.: A billion SMT queries a day (invited paper). In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification (CAV), Part I. Lecture Notes in Computer Science, vol. 13371, pp. 3\u201318. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_1","DOI":"10.1007\/978-3-031-13185-1_1"},{"key":"10_CR36","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley (1998)"},{"key":"10_CR37","unstructured":"Schurr, H., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: towards a generic SMT proof format (extended abstract). CoRR abs\/2107.02354 (2021). https:\/\/arxiv.org\/abs\/2107.02354"},{"key":"10_CR38","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-030-79876-5_26","volume-title":"Automated Deduction \u2013 CADE 28","author":"H-J Schurr","year":"2021","unstructured":"Schurr, H.-J., Fleury, M., Desharnais, M.: Reliable reconstruction of fine-grained proofs in a proof assistant. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 450\u2013467. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_26"},{"key":"10_CR39","doi-asserted-by":"publisher","unstructured":"Tan, Y.K., Heule, M.J.H., Myreen, M.O.: cake_lpr: verified propagation redundancy checking in CakeML. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part II. LNCS, vol. 12652, pp. 223\u2013241 (2021). https:\/\/doi.org\/10.1007\/s10009-022-00690-y","DOI":"10.1007\/s10009-022-00690-y"},{"key":"10_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31"},{"key":"10_CR41","doi-asserted-by":"publisher","unstructured":"Wilson, A., N\u00f6tzli, A., Reynolds, A., Cook, B., Tinelli, C., Barrett, C.W.: Partitioning strategies for distributed SMT solving. In: Nadel, A., Rozier, K.Y. (eds.) Formal Methods In Computer-Aided Design (FMCAD), pp. 199\u2013208. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/ISBN.978-3-85448-060-0_28","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_28"},{"key":"10_CR42","doi-asserted-by":"publisher","unstructured":"Zhou, Y., Bosamiya, J., Takashima, Y., Li, J., Heule, M., Parno, B.: Mariposa: measuring SMT instability in automated program verification. In: Nadel, A., Rozier, K.Y. (eds.) Formal Methods In Computer-Aided Design (FMCAD), pp. 178\u2013188. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/ISBN.978-3-85448-060-0_26","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_26"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32589-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:01:45Z","timestamp":1784800905000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32589-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325884","9783032325891"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32589-1_10","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":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/ijcar","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}