Input file formats

Alt-ergo supports different input languages:

• The original input language is its native language, based on the language of the Why3 platform and detailed below.

• Alt-ergo supports the SMT-LIB language v2.6. Since version 2.5.0, improved support is provided by the Dolmen frontend, available with the --frontend dolmen option.

• It also (partially) supports the input language of Why3 through the AB-Why3 plugin.

Contents

• Alt-Ergo's native language
  • Summary
  • Declaration of symbols
  • Types
  • Declaration of axioms
  • Setting goals
  • Theories
  • Control Flow
  • Syntax of declarations and expressions
• SMT-LIB 2
  • Bit-vectors