# PV2 ⊧ CoqQFBVproduces a satisfiability formula for a query

SMT solver for`QF_BV`

(quantifier-free bit-vector) logic.
### Application domain/field

- SMT solving
- Quantifier-Free Bit-Vector (
`QF_BV`

) logic

### Type of tool

SMT solver for`QF_BV`

logic
### Expected input

SMT`QF_BV`

query
Format:

SMT-LIB v2### Expected output

Boolean formula such that the query is satisfiable if and only if the Boolean formula is satisfiable. Output is generated in the DIMACS format.### Internals

This is a certified SMT solver for quantifier-free bit-vector (`QF_BV`

) formulas. It has been specified and verified in the proof assistant Coq.
It takes a `QF_BV`

query in SMT-LIB format. This is converted into a formal `QF_BV`

expression. Then a CNF formula is constructed. Then it uses Kissat to solve the CNF formula. If the result is unsat with a certificate, then the certificate is verified with GRAT. If the results is sat with assignments, then this is translated back to SMT assignments and the tool will verify whether these assignments satisfy the `QF_BV`

expression.