***********************************************
 *                  IMITATOR                   *
 *                              Etienne ANDRE  *
 *                                2008 - 2009  *
 *  Laboratoire Specification et Verification  *
 *               ENS de Cachan & CNRS, France  *
 ***********************************************
 Tue, 07 Apr 2009 13:09:27
 Step 1
 Step 2
 Step 3
   Randomly choosing an inequality among 2 possible pi_0-incompatible inequalities
   Adding inequality               0 < b
   Adding inequality               0 < a
 Step 4
   Adding inequality               a <= b
 Step 5
   Adding inequality               2a <= b
 Step 6
 Step 7
 Step 8
 Step 9
 Step 10
 Step 11
 Step 12
 Step 13
 Step 14
 Step 15
 Step 16
 Step 17
 Step 18
 Step 19

 Post* was reached at step 18 with 456 states (from 8 different locations)

 Intersection of the inequalities of all states in post* (after simplification):
      & 0 < a
      & 2a <= b
      & 2b <= t

 IMITATOR ended with success :-)

 IMITATOR ended after 995.86 seconds
   Python execution time : 1.49s
   HyTech execution time : 992.13s (23 calls)
 ***********************************************