Skip to content
Tags give the ability to mark specific points in history as being important
  • 0.4
    a70aa378 · Update Changes ·
    Release: Release 0.4
    Release 0.4
    
    CHANGES:
    
      * Decision: Fix delayed decisions handling
      * Array: experimental theory
      * Quantifier: Improve eager instanciation heuristic
      * Quantifier: Avoid creating new term
      * Simplex: Fix redundant run
      * Fix compilation in 32bit
      * Fix sign of sqrt
  • 0.3.3
    091be73f · Cleanup repository ·
    Release: Release 0.3.3
    Release 0.3.3
    
    CHANGES:
    
      * Bump cmdliner version
      * Bump OCaml version
      * Remove some warnings in 4.14
      * Fix OUnit2 dependency
      * Support 32bit by removing large integer constant
  • 0.3.2
    c7a21cc9 · Fix missing dependencies ·
    Release: Release 0.3.2
    Release 0.3.2
    
    CHANGES:
    
      * Add missing dependencies
  • 0.3.1
    Release 0.3.1
    
    CHANGES:
    
      * Add lower bounds for dependencies
      * Attach tests to corresponding packages
  • 0.3
    7683751d · Add CHANGES file ·
    Release: 0.3
    Release 0.3
    
    CHANGES:
    
    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