PV4 Z3produces a satisfiability result for a formula

Application domain/field

Type of tool

SMT solver

Expected input

SMT formula

Format:

SMT-LIB v2 format There are bindings for .NET, C, C++, Java, OCaml, Python, Julia and Web Assembly

Expected output

sat, unsat or unknown
SMT

Links

https://github.com/Z3Prover/z3

Last commit date

30 September 2021

Related papers

Last publication date

April 2015

ProVerB specific

View/edit source (Markdown)



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