**************************************************
 *  HYMITATOR 1.0                                 *
 *   Etienne ANDRE, Ulrich KUEHNE, Romain SOULAT  *
 *                                   2009 - 2012  *
 *     Laboratoire Specification et Verification  *
 *                  ENS de Cachan & CNRS, France  *
 **************************************************
 Mode: inverse method.
 *** Warning: Considering a limit of 30 for the depth of the Post operation.
 
 Parsing done after 0.007 second.
 Program checked and converted after 0.017 second.
 
 Computing post^1
   Adding the following inequality:
   O_2 > 0
   0 states merged.
 Computing post^2
   Adding the following inequality:
   O_2 < 10
   Adding the following inequality:
   6 < C_1 + C_2
   0 states merged.
 Computing post^3
   Adding the following inequality (randomly selected among 2 inequalities):
   O_2 + 6 < 2*C_1 + C_2
   1 states merged.
 Computing post^4
   2 states merged.
 Computing post^5
   Adding the following inequality:
   C_1 < 5
   3 states merged.
 Computing post^6
   4 states merged.
 Computing post^7
   Adding the following inequality:
   7 < 3*C_1
   8 states merged.
 Computing post^8
   8 states merged.
 Computing post^9
   0 states merged.
 Computing post^10
   0 states merged.
 Computing post^11
   4 states merged.
 Computing post^12
   0 states merged.
 Computing post^13
   0 states merged.
 Computing post^14
   5 states merged.
 Computing post^15
   0 states merged.
 Computing post^16
   Adding the following inequality:
   17 < 6*C_1
   0 states merged.
 Computing post^17
   5 states merged.
 Computing post^18
   0 states merged.
 Computing post^19
   0 states merged.
 Computing post^20
   6 states merged.
 Computing post^21
   0 states merged.
 Computing post^22
   0 states merged.
 Computing post^23
   7 states merged.
 Computing post^24
   0 states merged.
 Computing post^25
   0 states merged.
 Computing post^26
   8 states merged.
 Computing post^27
   0 states merged.
 Computing post^28
   0 states merged.
 Computing post^29
   9 states merged.
 Computing post^30
   0 states merged.
 *** Warning: The limit number of iterations (30) has been reached. Post^* now stops, although there were still 27 states to explore at this iteration.
 
 Final constraint K  :
   6*C_1 > 17
 & O_2 > 0
 & C_1 + C_2 > 6
 & 5 > C_1
 & 2*C_1 + C_2 > 6 + O_2
 & 10 > O_2
 
 Fixpoint reached after 30 iterations in 23.264 seconds: 369 reachable states with 485 transitions.
 
 Final constraint K0 :
   6 >= C_2
 & 3 >= C_1
 & 6*C_1 > 17
 & 2*C_1 + C_2 > 6 + O_2
 & O_2 >= C_1
 & 10 >= O_2 + C_2
 & O_1 = 0
 & D_1 = 7
 & D_2 = 6
 & T_1 = 10
 & T_2 = 10

 HYMITATOR successfully terminated (after 23.531 seconds)