CHANGES

1.1.2 2018-01-15
    IMPROVEMENTS
    * Cubicle Emacs mode on MELPA (package-install cubicle-mode)

    BUG FIXES
    * Compatibility with OCaml 4.06.0
    * Fix arithmetic buc in solver usage (set_cc)
    * Configure with OCaml 4.03.0 minimum
    * Fix issue with spurious trace replay

1.1.1 2017-06-13
    NEW FEATURES
    * Option -noqe to disable elimination of constants

    BUG FIXES
    * Parsing floats and negative reals/integers
    * Fix too broad over-approximation with non-deterministic updates
    * Fix type bool is now an enumerative data type

1.1   2016-03-17
    NEW FEATURES
    * Murphi (external tool) as an oracle for performing enumerative forward
      (Experimental)
    * Macros for predicates/formulas (Experimental)
    * Symmetry reduction by normalization in enumerative forward. Can be
      disabled with -forward-nosym.
    
    IMPROVEMENTS
    * Report solver errors
    * Indentation in Why3 certificates
    * Stop forward exploration with Ctrl-C and continue with backward
    * Sort transitions to not depend on order
    
    BUG FIXES
    * Renaming bug in forward
    * Certificates: reals/constants and user supplied invariants
    * Various fixes in reporting of spurious traces
    * Add user supplied invariants in initial formula
    * Various fixes in arithmetic
    
1.0.2 2015-02-09
    BUG FIXES
    * Create correct actions for preservation of values in Enumerative
    * Fix incorrect computation of subtypes in presence of non-deterministic
      updates
    * Fix replaying of error traces with non-deterministic updates

1.0.1 2014-11-05
    NEW FEATURES
    * Certificates in Why3 format (Experimental)
    * Case constructs for updating global variables
    * Disjunctions in transitions' requirements (only dnf for now)
    * Option -candheur to (partially) control heuristic for candidate
      invarariants extraction

    IMPROVEMENTS
    * Simplifications in initial formula

    BUG FIXES
    * Ignore signal USR1 in Windows because it does not exist

1.0   2014-07-21
    NEW FEATURES
    * New modular architecture with cleaner and more efficient operations
    * Code documentation with ocamldoc
    * Use of ? instead of . for non-deterministic assignments (conservative
      extension: the old syntax is still possible)

    IMPROVEMENTS
    * More efficient forward (with GC parameters)
    * Faster filter when a lot of candidates are not suitable
    * New options for controlling candidates generation
    * More options for dot search graphs and color by exploration time
    * More efficient tries (less allocation)

    BUG FIXES
    * Report typing errors (at transition level)
    * Relevant permutations for multi-dimensional arrays

0.6   2014-01-27
    NEW FEATURES
    * Refine universal guards by symbolic forward replay to prevent spurious
      traces when using BRAB (experimental)
    * Certificates (of inductiveness) generation for Alt-Ergo and Why3
    * Specify max number of processes with keyword : number_procs
    * Show spurious error traces
    
    IMPROVEMENTS
    * Use generic parameterized hash functions: faster with OCaml >= 4.00
    * Do not add spurious nodes in visited
    * More efficient computation of pre-images
    * Use ocamlfind for configure

    BUG FIXES
    * Arithmetic simplifications


0.5   2013-09-04
    NEW FEATURES
    * BRAB algorithm on top of classical backward reachability
    * Generation of search graph in dot (graphviz) format thanks to unsat cores
    * Allow non deterministic updates of variables of type other than proc
    * Enumerative statefull forward exploration
    * Multi-dimensionnal arrays

    IMPROVEMENTS
    * Copy of cyclic data-structures
    * Only use features of the SMT solver that are necessary: congruence
      closureand arith are deactivated when not needed
    * SAT solver (alt-ergo zero): delay case split once a full propositional
      model is found
    * Tries for maintaining set of visited nodes (cubes)
    * Memoization of (SMT) formula construction
    * Check other candidates on faulty traces

    BUG FIXES
    * SAT solver (alt-ergo zero): Raise sat if full model to avoid vec assert
    * Raise error on duplicate updates

0.2.5 2012-04-12
    NEW FEATURES
    * Complete error traces
    
    BUG FIXES
    * Fix bug in initial formula instantiation with global variables

0.2.4 2012-04-11
    NEW FEATURES
    * Syntactic sugar for simple array updates (A[i] := v)
    
    BUG FIXES
    * Pre with correct number of arguments

0.2.3 2012-04-02
    BUG FIXES
    * Computation of pre for terms of the form A[G]

0.2.2 2012-03-23
    NEW FEATURES
    * Multiple unsafe properties
    * Allow terms of the form A[G] where A is an array and G is a global
      variable

0.2.1 2012-01-25
    IMPROVEMENTS
    * Approximations in arithmetic simplifications

0.2   2012-01-23
    * First public release of Cubicle