{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T06:51:57Z","timestamp":1775803917470,"version":"3.50.1"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T00:00:00Z","timestamp":1775779200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T00:00:00Z","timestamp":1775779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005722","name":"Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005722","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2026,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Bit-vector operations are ubiquitous in programming languages and formal verification, but their complex semantics pose challenges for SMT solvers. Although bit-blasting\u2014translating bit-vectors to Boolean variables\u2014is widely used, it struggles with arithmetic bit-vector operations on large bit-widths (e.g., 64-bit or 256-bit variables) due to exponential blowup. Int-blasting, which maps bit-vectors to integer arithmetic, offers a scalable alternative for arithmetic bit-vector operations, but introduces many modulo operations of which some are redundant. This article presents a modular three-step translation from bit-vector formulas to integer formulas, designed to keep the amount of modulo operations low, while preserving correctness. In the first step, we translate bit-vector operations to integer operations. Thereby, we introduce the two functions\n                    <jats:inline-formula>\n                      <jats:tex-math>$$\\texttt {bv2nat}$$<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    and\n                    <jats:inline-formula>\n                      <jats:tex-math>$$\\texttt {nat2bv}_k$$<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    as explicit operators in the SMT-LIB theory of bit-vectors. Each integer operation is wrapped by\n                    <jats:inline-formula>\n                      <jats:tex-math>$$\\texttt {bv2nat}$$<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    and\n                    <jats:inline-formula>\n                      <jats:tex-math>$$\\texttt {nat2bv}_k$$<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    . Hence, the sort of all bit-vector terms is preserved. Therefore, the first translation step is an equivalence transformation. In the second step, we simplify the formula by replacing the composition\n                    <jats:inline-formula>\n                      <jats:tex-math>$$\\texttt {bv2nat} \\circ \\texttt {nat2bv}_k$$<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    with a modulo operation. These modulo operations are added lazily, i.e., if the modulo does not change the result of the operation, it is omitted. In our experiments this reduced the average amount of modulo operations by 51%. In the third step, we introduce lemmas to precisely capture the meaning of\n                    <jats:inline-formula>\n                      <jats:tex-math>$$\\texttt {bv2nat}$$<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    and\n                    <jats:inline-formula>\n                      <jats:tex-math>$$\\texttt {nat2bv}_k$$<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    . We prove that these lemmas suffice to solve bit-vector formulas. Furthermore, we illustrate that these lemmas are also sufficient for bit-vector formulas with quantifiers, arrays and uninterpreted functions. We implement our translation in\n                    <jats:sc>SMTInterpol<\/jats:sc>\n                    and evaluate it on 19570 SMT-LIB benchmarks. Results show that our lazy int-blasting solves 15% more tasks than an eager int-blasting, with 35% faster average runtime and 12% lower memory usage.\n                  <\/jats:p>","DOI":"10.1007\/s00236-026-00529-y","type":"journal-article","created":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T05:55:31Z","timestamp":1775800531000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A lazy and modular approach to int-blasting"],"prefix":"10.1007","volume":"63","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-7716-3898","authenticated-orcid":false,"given":"Max","family":"Barth","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4252-3558","authenticated-orcid":false,"given":"Matthias","family":"Heizmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6314-1041","authenticated-orcid":false,"given":"Jochen","family":"Hoenicke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,10]]},"reference":[{"key":"529_CR1","doi-asserted-by":"crossref","unstructured":"Alt, L., Reitwie\u00dfner, C.: Smt-based verification of solidity smart contracts. In: ISoLA (4), volume 11247 of Lecture Notes in Computer Science, pp. 376\u2013388. Springer (2018)","DOI":"10.1007\/978-3-030-03427-6_28"},{"key":"529_CR2","unstructured":"Aniva, L., Barbosa, H., Barrett, C., Brain, M., Camillo, V., Kremer, G., Lachnitt, H., Mohamed, A., Mohamed, M., Niemetz, A., et al.: CVC5 at the SMT competition 2023. https:\/\/smt-comp.github.io\/2023\/system-descriptions\/cvc5.pdf\u00a0(2023). Accessed 2024-11-25\u00a0"},{"key":"529_CR3","doi-asserted-by":"crossref","unstructured":"Backeman, P., R\u00fcmmer, P., Zeljic, A.: Bit-vector interpolation and quantifier elimination by lazy reduction. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, pp. 1\u201310. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603023"},{"key":"529_CR4","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Barrett, C\u00a0W., 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, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pp. 415\u2013442. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"529_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org (2017)"},{"key":"529_CR6","unstructured":"Barth, M., Heizmann, M.: Ultimate IntBlastingWrapper. https:\/\/smt-comp.github.io\/2023\/system-descriptions\/UltimateIntBlastingWrapper%2BSMTInterpol.pdf (2023). Accessed 2024-11-25"},{"key":"529_CR7","unstructured":"Barth, M., Heizmann, M.: A bit-vector to integer translation with bv2nat and nat2bv. In: Reger, G., Zohar, Y. (eds.) Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories co-located with the 36th International Conference on Computer Aided Verification (CAV 2024), Montreal, Canada, July, 22-23, 2024, volume 3725 of CEUR Workshop Proceedings, pp. 53\u201363. CEUR-WS.org (2024)"},{"key":"529_CR8","unstructured":"Barth, M., Heizmann, M., Hoenicke, J.: Replication package for the paper \u201cA lazy and modular approach to int-blasting\u201d. https:\/\/zenodo.org\/records\/14258298 (2024)"},{"key":"529_CR9","unstructured":"Barth, M., Hoenicke, J., Schindler, T.: SMTInterpol version 2.5-1381-g0e9bd0bf. https:\/\/ultimate.informatik.uni-freiburg.de\/smtinterpol\/sysdesc2024.pdf (2024). Accessed 2024-11-25"},{"key":"529_CR10","doi-asserted-by":"crossref","unstructured":"Beyer, D., Chien, P., Lee, N.: Bridging hardware and software analysis with Btor2C: A word-level-circuit-to-c translator. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, volume 13994 of Lecture Notes in Computer Science, pp. 152\u2013172. Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_12"},{"issue":"1","key":"529_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2019","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. STTT 21(1), 1\u201329 (2019)","journal-title":"STTT"},{"key":"529_CR12","doi-asserted-by":"crossref","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL 2.0. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pp. 133\u2013152. Springer (2024)","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"529_CR13","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT competition 2024. In: Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions, p.\u00a08. Department of Computer Science, University of Helsinki (2024)"},{"key":"529_CR14","doi-asserted-by":"crossref","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An interpolating SMT solver. In: Donaldson, A.F., Parker, D. (eds.) Model Checking Software - 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings, volume 7385 of Lecture Notes in Computer Science, pp. 248\u2013254. Springer (2012)","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"529_CR15","volume-title":"A mathematical introduction to logic","author":"HB Enderton","year":"1972","unstructured":"Enderton, H.B.: A mathematical introduction to logic. Academic Press (1972)"},{"key":"529_CR16","unstructured":"Griggio, A.: Effective word-level interpolation for software verification. In: Bjesse, P., Slobodov\u00e1, A. (eds.) International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911, Austin, TX, USA, October 30 - November 02, 2011, pp. 28\u201336. FMCAD Inc. (2011)"},{"issue":"OOPSLA2","key":"529_CR17","doi-asserted-by":"publisher","first-page":"2402","DOI":"10.1145\/3689796","volume":"8","author":"S Grossman","year":"2024","unstructured":"Grossman, S., Toman, J., Bakst, A., Arora, S., Sagiv, M., Nandi, C.: Practical verification of smart contracts using memory splitting. Proc. ACM Program. Lang. 8(OOPSLA2), 2402\u20132433 (2024)","journal-title":"Proc. ACM Program. Lang."},{"key":"529_CR18","unstructured":"Gurfinkel, A., Belov, A., Marques-Silva, J.: Synthesizing safe bit-precise invariants. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science, pp. 93\u2013108. Springer (2014)"},{"key":"529_CR19","unstructured":"Heule, M.J.H., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.): Proceedings of SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science, University of Helsinki (2024)"},{"key":"529_CR20","unstructured":"Liu, Y.C., Pang, C., Dietsch, D., Koskinen, E., Le, T-C., Portokalidis, G., Xu, J.: Source-level bitwise branching for temporal verification of lifted binaries. CoRR, abs\/2105.05159 (2021)"},{"key":"529_CR21","unstructured":"Nelson, C.G.: Techniques for program verification. PhD thesis, Stanford University, Stanford, CA, USA (1980). AAI8011683"},{"issue":"2","key":"529_CR22","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"key":"529_CR23","doi-asserted-by":"crossref","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, volume 13965 of Lecture Notes in Computer Science, pp. 3\u201317. Springer (2023)","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"529_CR24","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C.W., Tinelli, C.: Towards bit-width-independent proofs in SMT solvers. In: Fontaine, P. (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, volume 11716 of Lecture Notes in Computer Science, pp. 366\u2013384. Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_22"},{"key":"529_CR25","doi-asserted-by":"crossref","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, volume 14681 of Lecture Notes in Computer Science, pp. 178\u2013200. Springer (2024)","DOI":"10.1007\/978-3-031-65627-9_9"},{"key":"529_CR26","doi-asserted-by":"crossref","unstructured":"Okudono, T., King, A.: Mind the gap: Bit-vector interpolation recast over linear integer arithmetic. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I, volume 12078 of Lecture Notes in Computer Science, pp. 79\u201396. Springer (2020)","DOI":"10.1007\/978-3-030-45190-5_5"},{"key":"529_CR27","doi-asserted-by":"crossref","unstructured":"Rath, J., Eisenhofer, C., Kaufmann, D., Bj\u00f8rner, N., Kov\u00e1cs, L.: PolySAT: Word-level bit-vector reasoning in Z3 (2024)","DOI":"10.1007\/978-3-031-86695-1_4"},{"key":"529_CR28","unstructured":"Reger, G., Zohar, Y. (eds.): Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories co-located with the 36th International Conference on Computer Aided Verification (CAV 2024), Montreal, Canada, July, 22-23, 2024, volume 3725 of CEUR Workshop Proceedings. CEUR-WS.org (2024)"},{"key":"529_CR29","unstructured":"SMT-COMP 2025. https:\/\/smt-comp.github.io\/2025\/. Accessed 2025-11-24"},{"key":"529_CR30","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: Alferes, J.J., Leite, J.A. (eds.) Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27-30, 2004, Proceedings, volume 3229 of Lecture Notes in Computer Science, pp. 641\u2013653. Springer 2004","DOI":"10.1007\/978-3-540-30227-8_53"},{"issue":"1","key":"529_CR31","first-page":"221","volume":"11","author":"T Weber","year":"2019","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)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"529_CR32","unstructured":"Wood, G.: Ethereum: A secure decentralised generalised transaction ledger. https:\/\/ethereum.github.io\/yellowpaper\/paper.pdf (2025). Last updated 2025-02-04"},{"key":"529_CR33","doi-asserted-by":"crossref","unstructured":"Zohar, Y., Irfan, A., Mann, M., Niemetz, A., N\u00f6tzli, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Bit-precise reasoning via int-blasting. In: Finkbeiner, B., Wies, T. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 496\u2013518. Springer International Publishing, Cham (2022)","DOI":"10.1007\/978-3-030-94583-1_24"},{"key":"529_CR34","unstructured":"Zohar, Y., Irfan, A., Mann, M., Notzli, A., Reynolds, A., Barrett, C.: lazybvtoint at the SMT competition 2020. arXiv preprint arXiv:2105.09743 (2021)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-026-00529-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-026-00529-y","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-026-00529-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T05:55:54Z","timestamp":1775800554000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-026-00529-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,10]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["529"],"URL":"https:\/\/doi.org\/10.1007\/s00236-026-00529-y","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,4,10]]},"assertion":[{"value":"2 December 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 March 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 April 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"16"}}