2026-07-20T11:15:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23738 2025-11-12T12:59:57Z ddc:004 open_access

Bit-Precise Reasoning with Parametric Bit-Vectors Berger, Zvika Zohar, Yoni Niemetz, Aina Preiner, Mathias Reynolds, Andrew Barrett, Clark Tinelli, Cesare Satisfiability Modulo Theories Bit-precise Reasoning Parametric Bit-vectors The SMT-LIB theory of bit-vectors is restricted to bit-vectors of fixed width. However, several important applications can benefit from reasoning about bit-vectors of symbolic widths, i.e., parametric bit-vectors. Recent work has introduced an approach for solving formulas over parametric bit-vectors, via an eager translation to quantified integer arithmetic with uninterpreted functions. The approach was shown to be successful for several applications, including the bit-width independent verification of compiler optimizations, invertibility conditions, and rewrite rules. We extend and improve that approach in several aspects. Theoretically, we improve expressiveness by defining a new theory of parametric bit-vectors that supports more operators and allows reasoning about the bit-widths themselves. Algorithmically, we introduce a lazy algorithm that avoids the use of uninterpreted functions and quantified axioms for them. Empirically, we show a significant improvement by implementing and evaluating our approach, and comparing it experimentally to the previous one. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Zvika Berger and Yoni Zohar and Aina Niemetz and Mathias Preiner and Andrew Reynolds and Clark Barrett and Cesare Tinelli 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.4 urn:nbn:de:0030-drops-237385 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.4 eng https://creativecommons.org/licenses/by/4.0/legalcode