Bitwuzla
Aina Niemetz, Mathias Preiner
Abstract
Abstract Bitwuzla is a new SMT solver for the quantifier-free and quantified theories of fixed-size bit-vectors, arrays, floating-point arithmetic, and uninterpreted functions. This paper serves as a comprehensive system description of its architecture and components. We evaluate Bitwuzla’s performance on all benchmarks of supported logics in SMT-LIB and provide a comparison against other state-of-the-art SMT solvers.
Topics & Concepts
Computer scienceSatisfiability modulo theoriesSolverProgramming languageParallel computingArithmeticArchitectureTheoretical computer scienceProblem solverState (computer science)AlgorithmComputational scienceMathematicsArtVisual artsFormal Methods in VerificationLogic, programming, and type systemsLow-power high-performance VLSI design