PV4 Barcelogicproduces a satisfiability result for a formula

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula


SMT-LIB format

Expected output

If satisfiable, then a model (in SMT-LIB format) which describes the truth value for each Boolean variable, a concrete integer or real for each numeric variable and a partial mapping for each uninterpreted function symbol in the formula Else, unsatisfiable


Related papers

The Barcelogic SMT Solver

Last publication date


ProVerB specific

Markdown description: view/edit

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