PV4 dRealproduces a satisfiability result for a formula

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula

Format:

SMT-LIB v2

Expected output

"unsat" or "δ-sat"

Internals

It uses IBEX-lib, CLP, NLopt, PicoSAT and capd
SMT

Links

Last commit date

4 June 2021

Related papers

https://doi.org/10.1007/978-3-319-96142-2_15

Last publication date

18 July 2018

ProVerB specific

View/edit source (Markdown)



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