4 citations · 4 across the 1 of their papers we have counts for
3 papers
cs.LO2020★ 4 cited
Bitwuzla at the SMT-COMP 2020
Aina Niemetz, Mathias Preiner
In this paper, we present Bitwuzla, our Satisfiability Modulo Theories (SMT) solver for the theories of bit-vectors, floating-points, arrays and uninterpreted functions and their c…
cs.LO2019
DRAT-based Bit-Vector Proofs in CVC4
Alex Ozdemir, Aina Niemetz, Mathias Preiner +2
Many state-of-the-art Satisfiability Modulo Theories (SMT) solvers for the theory of fixed-size bit-vectors employ an approach called bit-blasting, where a given formula is transla…
cs.LO2019
Towards Bit-Width-Independent Proofs in SMT Solvers
Aina Niemetz, Mathias Preiner, Andrew Reynolds +3
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…