Skip to content
Release 0.3


initial release

  * polymorphism, recursive definitions
  * quantifiers (eager, multi-triggers)
  * algebraic datatypes (except cycle detection)
  * Reals: union of interval domain (proved in why3 with Colibrilib)
  * Reals: normalization sum, product, some factorization, Fourier-Motskin
    or Simplex
  * Reals: abs
  * Int: floor, ceil, abs, Real <-> Int
  * Floating point: evaluation and some simple propagation (Arthur Correnson)
  * Bitvectors: only evaluation

  * engine
  * simple constraints

  * interval
  * union of interval
  * congruence