Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions

Citations of this article
Mendeley users who have this article in their library.

This artice is free to access.


Recent experiments have shown that satisfiability of a quantified bit-vector formula coming from practical applications almost never changes after reducing all bit-widths in the formula to a small number of bits. This paper proposes a novel technique based on this observation. Roughly speaking, a given quantified bit-vector formula is reduced and sent to a solver, an obtained model is then extended to the original bit-widths and verified against the original formula. We also present an experimental evaluation demonstrating that this technique can significantly improve the performance of state-of-the-art smt solvers Boolector, CVC4, and Q3B on quantified bit-vector formulas from the smt-lib repository.




Jonáš, M., & Strejček, J. (2020). Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12178 LNCS, pp. 378–393). Springer. https://doi.org/10.1007/978-3-030-51825-7_27

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free