PV4 Q3Bproduces a satisfiability result for a formula

SMT solver, decides satisfiability of quantified bit-vector formulas.

Application domain/field

Type of tool

SMT solver

Expected input

Quantified bit-vector formula

Format:

SMT-LIB 2.5

Expected output

sat or unsat indicating whether the quantified bit-vector formula was satisfiable or not.

Internals

Uses CUDD, ANTLR, SMT-LIB, Z3
BDD SMT

Links

Repository: https://github.com/martinjonas/Q3B

Last commit date

6 March 2019

Related papers

https://doi.org/10.1007/978-3-030-25543-5_4

Last publication date

12 July 2019

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.