PV4 ⊧ Alt-Ergoproduces a satisfiability result for a formula

SMT solver

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula

Format:

One of the following:

• .ae file for its native input language
• .why: deprecated but still accepted
• .mlw: deprecated but still accepted
• .psmt2: polymorphic extension of the SMT-LIB 2 format
• .smt2: SMT-LIB 2 format

Expected output

Valid, Invalid or I don't know if the user used its native input language (.ae files). It can also output in the SMT-LIB 2 form if asked. unsat, sat or unknown if the user used the SMT-LIB 2 input format (i.e. .psmt2 or .smt2 files)

Internals

Alt-Ergo is used by Frama-C, SPARK, Why3, Atelier-B and Caveat.