{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T16:56:41Z","timestamp":1775840201527,"version":"3.50.1"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031866944","type":"print"},{"value":"9783031866951","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-86695-1_4","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T02:06:44Z","timestamp":1746151604000},"page":"47-69","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["PolySAT: Word-level Bit-vector Reasoning in\u00a0Z3"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0346-6749","authenticated-orcid":false,"given":"Jakob","family":"Rath","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0339-1580","authenticated-orcid":false,"given":"Clemens","family":"Eisenhofer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5645-0292","authenticated-orcid":false,"given":"Daniela","family":"Kaufmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1695-2810","authenticated-orcid":false,"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,3]]},"reference":[{"issue":"OOPSLA","key":"4_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3428277","volume":"4","author":"E Albert","year":"2020","unstructured":"Albert, E., Grossman, S., Rinetzky, N., Rodr\u00edguez-N\u00fa\u00f1ez, C., Rubio, A., Sagiv, M.: Taming callbacks for smart contract modularity. Proc. ACM Program. Lang. 4(OOPSLA), 1\u201330 (2020). https:\/\/doi.org\/10.1145\/3428277","journal-title":"Proc. ACM Program. Lang."},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Proceedings of TACAS, pp. 415\u2013442 (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"4_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability Modulo theories library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"4_CR4","unstructured":"Bayardo, Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of AAAI and IAAI, pp. 203\u2013208 (1997)"},{"issue":"1","key":"4_CR5","first-page":"1","volume":"21","author":"D Beyer","year":"2017","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2017)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N.S., Pichora, M.C.: Deciding fixed and non-fixed size Bit-vectors. In: Proceedings of TACAS, pp. 376\u2013392 (1998). https:\/\/doi.org\/10.1007\/BFB0054184","DOI":"10.1007\/BFB0054184"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Bruttomesso, R., et al.: A lazy and layered SMT($$\\cal{BV}$$) solver for hard industrial verification problems. In: Proceedings of CAV. LNCS, vol.\u00a04590, pp. 547\u2013560. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_54","DOI":"10.1007\/978-3-540-73368-3_54"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Bruttomesso, R., Sharygina, N.: A scalable decision procedure for fixed-width Bit-vectors. In: Proceedings of ICCAD, pp. 13\u201320 (2009). https:\/\/doi.org\/10.1145\/1687399.1687403","DOI":"10.1145\/1687399.1687403"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Experimenting on solving nonlinear integer arithmetic with incremental linearization. In: Proceedings of SAT, pp. 383\u2013398 (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_23","DOI":"10.1007\/978-3-319-94144-8_23"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Proceedings of TACAS, pp. 93\u2013107 (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Proceedings of TACAS, pp. 168\u2013176 (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"issue":"3","key":"4_CR12","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005). https:\/\/doi.org\/10.1145\/1066100.1066102","journal-title":"J. ACM"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: Proceedings of CAV, pp. 737\u2013744 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Fr\u00f6hlich, A., Biere, A., Wintersteiger, C.M., Hamadi, Y.: Stochastic local search for satisfiability Modulo theories. In: Proceedings of AAAI, pp. 1136\u20131143 (2015). http:\/\/www.aaai.org\/ocs\/index.php\/AAAI\/AAAI15\/paper\/view\/9896","DOI":"10.1609\/aaai.v29i1.9372"},{"key":"4_CR15","unstructured":"Fr\u00f6hlich, A., Kov\u00e1sznai, G., Biere, A.: Efficiently solving Bit-vector problems using model checkers. In: Proceedings of Workshop on SMT, pp. 6\u201315 (2013). https:\/\/fmv.jku.at\/bv2smv\/"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for Bit-vectors and arrays. In: Proceedings of CAV, pp. 519\u2013531 (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_52","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Graham-Lengrand, S., Jovanovic, D., Dutertre, B.: Solving Bitvectors with MCSAT: explanations from bits and pieces. In: Proceedings of IJCAR, pp. 103\u2013121 (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_7","DOI":"10.1007\/978-3-030-51074-9_7"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Hadarean, L., Bansal, K., Jovanovic, D., Barrett, C.W., Tinelli, C.: A tale of two solvers: eager and lazy approaches to bit-vectors. In: Procrrdings of CAV. LNCS, vol.\u00a08559, pp. 680\u2013695. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_45","DOI":"10.1007\/978-3-319-08867-9_45"},{"issue":"3","key":"4_CR19","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/s10703-016-0260-9","volume":"49","author":"AK John","year":"2016","unstructured":"John, A.K., Chakraborty, S.: A layered algorithm for quantifier elimination from linear modular constraints. Formal Methods Syst. Des. 49(3), 272\u2013323 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0260-9","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"4_CR20","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s00224-015-9653-1","volume":"59","author":"G Kov\u00e1sznai","year":"2016","unstructured":"Kov\u00e1sznai, G., Fr\u00f6hlich, A., Biere, A.: Complexity of fixed-size bit-vector logics. Theory Comput. Syst. 59(2), 323\u2013376 (2016). https:\/\/doi.org\/10.1007\/s00224-015-9653-1","journal-title":"Theory Comput. Syst."},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-74105-3","DOI":"10.1007\/978-3-540-74105-3"},{"issue":"2","key":"4_CR22","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/S10601-015-9183-0","volume":"21","author":"MH Liffiton","year":"2016","unstructured":"Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints An. Int. J. 21(2), 223\u2013250 (2016). https:\/\/doi.org\/10.1007\/S10601-015-9183-0","journal-title":"Constraints An. Int. J."},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Lopes, N.P., Lee, J., Hur, C.K., Liu, Z., Regehr, J.: Alive2: bounded translation validation for LLVM. In: Proceedings of PLDI, pp. 65\u201379 (2021). https:\/\/doi.org\/10.1145\/3453483.3454030","DOI":"10.1145\/3453483.3454030"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"M\u00f6ller, M.O., Rue\u00df, H.: Solving bit-vector equations. In: Proceedings of FMCAD, pp. 36\u201348 (1998). https:\/\/doi.org\/10.1007\/3-540-49519-3_4","DOI":"10.1007\/3-540-49519-3_4"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Proceedings of TACAS, pp. 337\u2013340 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Jovanovic, D.: A model-constructing satisfiability calculus. In: International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol.\u00a07737, pp. 1\u201312. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_1","DOI":"10.1007\/978-3-642-35873-9_1"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M.: Ternary propagation-based local search for more bit-precise reasoning. In: Proceedings of FMCAD, pp. 214\u2013224 (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_29","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_29"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: Proceedings of CAV, pp. 3\u201317 (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_1","DOI":"10.1007\/978-3-031-37703-7_1"},{"issue":"3","key":"4_CR29","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1007\/s10703-017-0295-6","volume":"51","author":"A Niemetz","year":"2017","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Propagation based local search for bit-precise reasoning. Formal Methods Syst. Design 51(3), 608\u2013636 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0295-6","journal-title":"Formal Methods Syst. Design"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Zohar, Y.: Scalable bit-blasting with abstractions. In: Proceedings of CAV, pp. 178\u2013200 (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_9","DOI":"10.1007\/978-3-031-65627-9_9"},{"issue":"5","key":"4_CR31","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J Silva","year":"1999","unstructured":"Silva, J., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999). https:\/\/doi.org\/10.1109\/12.769433","journal-title":"IEEE Trans. Comput."},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Tange, O.: GNU Parallel 20240122 (\u2019Frederik X\u2019), GNU Parallel is a general parallelizer to run multiple serial command line programs in parallel without changing them (2024). https:\/\/doi.org\/10.5281\/zenodo.10558745","DOI":"10.5281\/zenodo.10558745"},{"issue":"3","key":"4_CR33","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1007\/s10817-018-9493-1","volume":"63","author":"W Wang","year":"2019","unstructured":"Wang, W., S\u00f8ndergaard, H., Stuckey, P.J.: Wombit: a portfolio bitvector solver using word-level propagation. J. Autom. Reason. 63(3), 723\u2013762 (2019). https:\/\/doi.org\/10.1007\/s10817-018-9493-1","journal-title":"J. Autom. Reason."},{"issue":"POPL","key":"4_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3434304","volume":"5","author":"M Willsey","year":"2021","unstructured":"Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: egg: fast and extensible equality saturation. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3434304","journal-title":"Proc. ACM Program. Lang."},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Zeljic, A., Wintersteiger, C.M., R\u00fcmmer, P.: Deciding Bit-Vector Formulas with mcSAT. In: Proceedings of SAT, pp. 249\u2013266 (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_16","DOI":"10.1007\/978-3-319-40970-2_16"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"Zohar, Y., et al.: Bit-precise reasoning via Int-blasting. In: Proceedings of VMCAI, pp. 496\u2013518 (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_24","DOI":"10.1007\/978-3-030-94583-1_24"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-86695-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T03:15:48Z","timestamp":1746155748000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-86695-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031866944","9783031866951"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-86695-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"3 May 2025","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\u00a0the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.soundandcomplete.org\/vstte2024.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}