4 citations · 8 across the 4 of their papers we have counts for
7 papers
Satisfiability Modulo Extensional Constant Arrays (Extended Version)
Mathias Preiner, Aina Niemetz, Clark Barrett
Reasoning about array data structures is a key requirement for many applications in hardware and software verification, especially in combination with machine integers. The Satisfi…
Towards SMT Solver Stability via Input Normalization
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz +4
In many applications, SMT solvers are utilized to solve similar or identical tasks over time. Significant variations in performance due to small changes in the input are not uncomm…
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…
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…
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…
CVC4 at the SMT Competition 2018
Clark Barrett, Haniel Barbosa, Martin Brain +8
This paper is a description of the CVC4 SMT solver as entered into the 2018 SMT Competition. We only list important differences from the 2017 SMT Competition version of CVC4. For f…