# Towards Bit-Width-Independent Proofs in SMT Solvers

## TL;DR

This paper introduces a translation method that enables SMT solvers to reason about bit-vectors of symbolic, non-fixed bit-widths by leveraging advanced solving techniques for a more expressive logic.

## Contribution

The authors propose a novel translation from fixed-size bit-vector formulas to a richer logic supporting non-linear arithmetic and quantification, enabling bit-width-independent reasoning.

## Key findings

- Effective in verifying invertibility conditions
- Applicable to compiler optimizations
- Successful in bit-vector rewrites

## Abstract

Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These approaches, however, cannot be used directly to reason about bit-vectors of symbolic bit-width. To address this shortcoming, we propose a translation from bit-vector formulas of non-fixed bit-width to formulas in a logic supported by SMT solvers that includes non-linear integer arithmetic, uninterpreted functions, and universal quantification. While this logic is undecidable, this approach can still solve many formulas by capitalizing on advancements in SMT solving for non-linear arithmetic and universally quantified formulas. We provide several case studies in which we have applied this approach with promising results, including the bit-width independent verification of invertibility conditions, compiler optimizations, and bit-vector rewrites.