************************************************************
    *  IMITATOR 2.9.2-working "Butter Incaberry"               *
    *                                                          *
    *                     Etienne Andre, Ulrich Kuehne et al.  *
    *                                             2009 - 2017  *
    *                       LSV, ENS de Cachan & CNRS, France  *
    *                       LIPN, Universite Paris 13, France  *
    *                                         www.imitator.fr  *
    *                                                          *
    *                   Build: 2363 (2017-06-08 17:40:33 UTC)  *
    *                                       explorder/5c40e39  *
    ************************************************************
    Analysis time: Sat Jun 17, 2017 12:58:41
    
    Model: /media/gia/Data/Example-Models/critical-region4/critical-region4.imi
    Mode: EF-synthesis.
    Exploration order: layer-based BFS.
    Considering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality).
    Merging technique of [AFS13] enabled.
    The cartography will be drawn.
    The result will be written to a file.
    The trace set(s) will be generated in a graphical mode.
    Description of states will be output.
    
    Abstract model built after 0.010 second.
    Memory for abstract model: 1084.414 KiB (i.e., 277610 words)
    
    Starting running algorithm AGsafe…
    
    Computing post^1 from 1 state.
    Computing post^2 from 5 states.
      6 states merged within 25 states.
    Computing post^3 from 19 states.
      26 states merged within 85 states.
    Computing post^4 from 59 states.
      87 states merged within 260 states.
    Computing post^5 from 173 states.
      [AGsafe] Found a new state violating the property.
      218 states merged within 508 states.
    Computing post^6 from 342 states.
      197 states merged within 453 states.
    Computing post^7 from 268 states.
      242 states merged within 613 states.
    Computing post^8 from 392 states.
      340 states merged within 861 states.
    Computing post^9 from 561 states.
      533 states merged within 1206 states.
    Computing post^10 from 747 states.
      557 states merged within 1423 states.
    Computing post^11 from 981 states.
      844 states merged within 1924 states.
    Computing post^12 from 1265 states.
      1084 states merged within 2433 states.
    Computing post^13 from 1655 states.
      1431 states merged within 3084 states.
    Computing post^14 from 2100 states.
      1626 states merged within 3653 states.
    Computing post^15 from 2617 states.
      2079 states merged within 4425 states.
    Computing post^16 from 3145 states.
      2195 states merged within 4939 states.
    Computing post^17 from 3782 states.
      2783 states merged within 5867 states.
    
    State space exploration stopped at a depth of 18: 39576 states with 102967 transitions in the final state space.
    
      [AGsafe] Algorithm completed after 1176.810 seconds.
    
    Final constraint such that the system is correct:
     A >= 0
    & B >= 0
    & 1 > A
    This good constraint is an over-approximation of the actual result (or the actual result itself)

    73.690 GiB (i.e., 9890599207 words of size 8)
    
    Result written to file '/media/gia/Data/Example-Models/critical-region4/critical-region4-layerBFS-incl-merge-EF.res'.
    
    ------------------------------------------------------------
    Statistics: State space
    ------------------------------------------------------------
    Number of states                        : 39576
    Number of transitions                   : 102967
    Number of computed states               : 112288
    Total computation time                  : 1176.800 seconds
    States/second in state space            : 33.6 (39576/1176.800 seconds)
    Computed states/second                  : 95.4 (112288/1176.800 seconds)
    Estimated memory                        : 73.690 GiB (i.e., 9890612851 words of size 8)