PV4 Boolectorproduces a satisfiability result for a formula

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula


One of the following:

Expected output


This is an SMT solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. It has a C and Python API.


Related papers

Last publication date

July 2019

Related tools

Bitwuzla is a successor

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.