/bat0/stac/Code/icra/WALi-OpenNWA/../icra -cra_newton_basic -cra-split-loops

Passing command-line option -cra-split-loops to duet.
<Unique State Name, 22> -> <Unique State Name, 27>	Base relation: 
{j := 0
 when i:64 < n:65}	
<Unique State Name, 22> -> <Unique State Name, 85>	Base relation: 
{when n:65 <= i:64}	
<Unique State Name, 40> -> <Unique State Name, 27>	Base relation: 
{j := (j:66 + 1)
 when n:65 <= k:67}	
<Unique State Name, 40> -> <Unique State Name, 45>	Base relation: 
{l := 0
 when k:67 < n:65}	
<Unique State Name, 58> -> <Unique State Name, 45>	Base relation: 
{l := (l:68 + 1)
 when n:65 <= m:69}	
<Unique State Name, 58> -> <Unique State Name, 54>	Base relation: 
{__cost := (__cost:70 + 1)
 m := (m:69 + 1)
 when (m:69 < n:65 /\ 0 <= __cost:70 /\ 0 <= (__cost:70 + 1))}	
<Unique State Name, 96> -> <Unique State Name, 101 95>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 9> -> <Unique State Name, 92>	Base relation: 
{param0 := tmp___0:8
 param0@pos := type_err:37
 param0@width := type_err:38}	
<Unique State Name, 101> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 36> -> <Unique State Name, 104>	Base relation: 
{when (1 <= n:65 /\ 0 <= k:67 /\ i:64 < n:65 /\ j:66 < n:65)}	
<Unique State Name, 8> -> <Unique State Name, 9>	Base relation: 
{tmp___0 := 0
 when (0 <= tr:7 /\ tr:6 <= 0)}	
<Unique State Name, 8> -> <Unique State Name, 96>	Base relation: 
{param0 := tr:39
 param0@pos := type_err:40
 param0@width := type_err:41
 when (tr:5 < 0 \/ 0 < tr:4)}	
<Unique State Name, 97> -> <Unique State Name, 8>	Base relation: 
{__cost := 0
 argv := param1:30
 argv@pos := param1@pos:29
 argv@width := param1@width:28}	
<Unique State Name, 54> -> <Unique State Name, 102>	Base relation: 
{when (1 <= n:65 /\ 0 <= m:69 /\ i:64 < n:65 /\ j:66 < n:65 /\ k:67 < n:65
         /\ l:68 < n:65)}	
<Unique State Name, 45> -> <Unique State Name, 103>	Base relation: 
{when (1 <= n:65 /\ 0 <= l:68 /\ i:64 < n:65 /\ j:66 < n:65 /\ k:67 < n:65)}	
<Unique State Name, 104> -> <Unique State Name, 40>	Base relation: 
{}	
<Unique State Name, 49> -> <Unique State Name, 36>	Base relation: 
{k := (k:67 + 1)
 when n:65 <= l:68}	
<Unique State Name, 49> -> <Unique State Name, 54>	Base relation: 
{m := 0
 when l:68 < n:65}	
<Unique State Name, 100> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 91> -> <Unique State Name, 100>	Base relation: 
{return := 0
 return@pos := type_err:35
 return@width := type_err:36}	
<Unique State Name, 103> -> <Unique State Name, 49>	Base relation: 
{}	
<Unique State Name, 105> -> <Unique State Name, 31>	Base relation: 
{}	
<Unique State Name, 99> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 31> -> <Unique State Name, 18>	Base relation: 
{i := (i:64 + 1)
 when n:65 <= j:66}	
<Unique State Name, 31> -> <Unique State Name, 36>	Base relation: 
{k := 0
 when j:66 < n:65}	
<Unique State Name, 85> -> <Unique State Name, 99>	Base relation: 
{return := havoc:71
 return@pos := type_err:74
 return@width := type_err:75}	
<Unique State Name, 18> -> <Unique State Name, 106>	Base relation: 
{when 0 <= i:64}	
<Unique State Name, 95> -> <Unique State Name, 9>	Base relation: 
{tmp___0 := havoc:19}	
<Unique State Name, 102> -> <Unique State Name, 58>	Base relation: 
{}	
<Unique State Name, 106> -> <Unique State Name, 22>	Base relation: 
{}	
<Unique State Name, 89> -> <Unique State Name, 18>	Base relation: 
{i := 0
 n := param0:27}	
<Unique State Name, 27> -> <Unique State Name, 105>	Base relation: 
{when (1 <= n:65 /\ 0 <= j:66 /\ i:64 < n:65)}	
<Unique State Name, 92> -> <Unique State Name, 89 91>	Base relation: 
{}	MergeFn[Base relation: 
{}]
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:70 + 1)
 m := (m:69 + 1)
 when (1 <= n:65 /\ 0 <= m:69 /\ i:64 < n:65 /\ j:66 < n:65 /\ k:67 < n:65
         /\ l:68 < n:65 /\ m:69 < n:65 /\ 0 <= __cost:70
         /\ 0 <= (__cost:70 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':2464) = (1)*(__cost:70) + 1
           (m':2465) = (1)*(m:69) + 1
           }
          pre:
            [|__cost:70>=0; m:69>=0; n:65-l:68-1>=0; n:65-k:67-1>=0;
              n:65-j:66-1>=0; n:65-i:64-1>=0; n:65-m:69-1>=0|]
          post:
            [|m':2465-1>=0; __cost':2464-1>=0; n:65-l:68-1>=0;
              n:65-k:67-1>=0; n:65-j:66-1>=0; n:65-i:64-1>=0; n:65-m':2465>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':2464
   m := m':2465
   when ((!(0 <= K:2478) \/ mid___cost:2481 = (__cost:70 + K:2478))
           /\ (!(0 <= K:2478) \/ mid_m:2480 = (m:69 + K:2478))
           /\ ((K:2478 = 0 /\ m:69 = mid_m:2480
                  /\ __cost:70 = mid___cost:2481)
                 \/ (1 <= K:2478 /\ 0 <= __cost:70 /\ 0 <= m:69
                       /\ 0 <= (-1 + n:65 + -l:68)
                       /\ 0 <= (-1 + n:65 + -k:67)
                       /\ 0 <= (-1 + n:65 + -j:66)
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (-1 + n:65 + -m:69) /\ 0 <= (-1 + mid_m:2480)
                       /\ 0 <= (-1 + mid___cost:2481)
                       /\ 0 <= (-1 + n:65 + -l:68)
                       /\ 0 <= (-1 + n:65 + -k:67)
                       /\ 0 <= (-1 + n:65 + -j:66)
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (n:65 + -mid_m:2480))) /\ K:2479 = 0
           /\ mid_m:2480 = m':2465 /\ mid___cost:2481 = __cost':2464
           /\ 0 = K:2479 /\ (K:2478 + K:2479) = K:2477 /\ 0 <= K:2477)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':2494
 l := (l:68 + 1)
 m := m':2493
 when (1 <= n:65 /\ 0 <= l:68 /\ i:64 < n:65 /\ j:66 < n:65 /\ k:67 < n:65
         /\ l:68 < n:65
         /\ (!(0 <= K:2489) \/ mid___cost:2490 = (__cost:70 + K:2489))
         /\ (!(0 <= K:2489) \/ mid_m:2491 = K:2489)
         /\ ((K:2489 = 0 /\ 0 = mid_m:2491 /\ __cost:70 = mid___cost:2490)
               \/ (1 <= K:2489 /\ 0 <= __cost:70 /\ 0 <= (-1 + n:65 + -l:68)
                     /\ 0 <= (-1 + n:65 + -k:67) /\ 0 <= (-1 + n:65 + -j:66)
                     /\ 0 <= (-1 + n:65 + -i:64) /\ 0 <= (-1 + n:65)
                     /\ 0 <= (-1 + mid_m:2491) /\ 0 <= (-1 + mid___cost:2490)
                     /\ 0 <= (-1 + n:65 + -l:68) /\ 0 <= (-1 + n:65 + -k:67)
                     /\ 0 <= (-1 + n:65 + -j:66) /\ 0 <= (-1 + n:65 + -i:64)
                     /\ 0 <= (n:65 + -mid_m:2491))) /\ K:2492 = 0
         /\ mid_m:2491 = m':2493 /\ mid___cost:2490 = __cost':2494
         /\ 0 = K:2492 /\ (K:2489 + K:2492) = K:2495 /\ 0 <= K:2495
         /\ 1 <= n:65 /\ 0 <= m':2493 /\ i:64 < n:65 /\ j:66 < n:65
         /\ k:67 < n:65 /\ l:68 < n:65 /\ n:65 <= m':2493)}
**** alpha hat: 
  {<Split [true
            (l':2496) = (1)*(l:68) + 1
           (__cost':2464) = (1)*(__cost:70) + n:65
           (m':2465) = n:65
           (-__cost':2464) <= (1)*(-__cost:70) + (-1)*1 + (-1)*k:67
           (-__cost':2464) <= (1)*(-__cost:70) + (-1)*1 + (-1)*j:66
           (-__cost':2464) <= (1)*(-__cost:70) + (-1)*1 + (-1)*i:64
           (-__cost':2464) <= (1)*(-__cost:70) + (-1)*1 + (-1)*l:68
           }
          pre:
            [|__cost:70>=0; l:68>=0; n:65-k:67-1>=0; n:65-j:66-1>=0;
              n:65-i:64-1>=0; n:65-l:68-1>=0|]
          post:
            [|-n:65+m':2465=0; -n:65+__cost':2464>=0; l':2496-1>=0;
              n:65-k:67-1>=0; n:65-j:66-1>=0; n:65-i:64-1>=0; n:65-l':2496>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':2464
   l := l':2496
   m := m':2465
   when ((!(0 <= K:2511) \/ mid_l:2514 = (l:68 + K:2511))
           /\ (!(0 <= K:2511)
                 \/ mid___cost:2515 = (__cost:70 + (n:65 * K:2511)))
           /\ (!((0 <= K:2511 /\ K:2511 <= 0)) \/ mid_m:2513 = m:69)
           /\ (!(1 <= K:2511) \/ mid_m:2513 = n:65)
           /\ (!(0 <= K:2511)
                 \/ -mid___cost:2515 <= (-__cost:70 + -K:2511
                                           + -((k:67 * K:2511))))
           /\ (!(0 <= K:2511)
                 \/ -mid___cost:2515 <= (-__cost:70 + -K:2511
                                           + -((j:66 * K:2511))))
           /\ (!(0 <= K:2511)
                 \/ -mid___cost:2515 <= (-__cost:70 + -K:2511
                                           + -((i:64 * K:2511))))
           /\ (!(0 <= K:2511)
                 \/ -mid___cost:2515 <= (-__cost:70 + (-1/2 * K:2511)
                                           + -((l:68 * K:2511))
                                           + (-1/2 * (K:2511 * K:2511))))
           /\ ((K:2511 = 0 /\ m:69 = mid_m:2513 /\ l:68 = mid_l:2514
                  /\ __cost:70 = mid___cost:2515)
                 \/ (1 <= K:2511 /\ 0 <= __cost:70 /\ 0 <= l:68
                       /\ 0 <= (-1 + n:65 + -k:67)
                       /\ 0 <= (-1 + n:65 + -j:66)
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (-1 + n:65 + -l:68)
                       /\ (-n:65 + mid_m:2513) = 0
                       /\ 0 <= (-n:65 + mid___cost:2515)
                       /\ 0 <= (-1 + mid_l:2514) /\ 0 <= (-1 + n:65 + -k:67)
                       /\ 0 <= (-1 + n:65 + -j:66)
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (n:65 + -mid_l:2514))) /\ K:2512 = 0
           /\ mid_m:2513 = m':2465 /\ mid_l:2514 = l':2496
           /\ mid___cost:2515 = __cost':2464 /\ 0 = K:2512
           /\ (K:2511 + K:2512) = K:2510 /\ 0 <= K:2510)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':2532
 k := (k:67 + 1)
 l := l':2531
 m := m':2530
 when (1 <= n:65 /\ 0 <= k:67 /\ i:64 < n:65 /\ j:66 < n:65 /\ k:67 < n:65
         /\ (!(0 <= K:2525) \/ mid_l:2526 = K:2525)
         /\ (!(0 <= K:2525)
               \/ mid___cost:2527 = (__cost:70 + (n:65 * K:2525)))
         /\ (!((0 <= K:2525 /\ K:2525 <= 0)) \/ mid_m:2528 = m:69)
         /\ (!(1 <= K:2525) \/ mid_m:2528 = n:65)
         /\ (!(0 <= K:2525)
               \/ -mid___cost:2527 <= (-__cost:70 + -K:2525
                                         + -((k:67 * K:2525))))
         /\ (!(0 <= K:2525)
               \/ -mid___cost:2527 <= (-__cost:70 + -K:2525
                                         + -((j:66 * K:2525))))
         /\ (!(0 <= K:2525)
               \/ -mid___cost:2527 <= (-__cost:70 + -K:2525
                                         + -((i:64 * K:2525))))
         /\ (!(0 <= K:2525)
               \/ -mid___cost:2527 <= (-__cost:70 + (-1/2 * K:2525)
                                         + (-1/2 * (K:2525 * K:2525))))
         /\ ((K:2525 = 0 /\ m:69 = mid_m:2528 /\ 0 = mid_l:2526
                /\ __cost:70 = mid___cost:2527)
               \/ (1 <= K:2525 /\ 0 <= __cost:70 /\ 0 <= (-1 + n:65 + -k:67)
                     /\ 0 <= (-1 + n:65 + -j:66) /\ 0 <= (-1 + n:65 + -i:64)
                     /\ 0 <= (-1 + n:65) /\ (-n:65 + mid_m:2528) = 0
                     /\ 0 <= (-n:65 + mid___cost:2527)
                     /\ 0 <= (-1 + mid_l:2526) /\ 0 <= (-1 + n:65 + -k:67)
                     /\ 0 <= (-1 + n:65 + -j:66) /\ 0 <= (-1 + n:65 + -i:64)
                     /\ 0 <= (n:65 + -mid_l:2526))) /\ K:2529 = 0
         /\ mid_m:2528 = m':2530 /\ mid_l:2526 = l':2531
         /\ mid___cost:2527 = __cost':2532 /\ 0 = K:2529
         /\ (K:2525 + K:2529) = K:2533 /\ 0 <= K:2533 /\ 1 <= n:65
         /\ 0 <= l':2531 /\ i:64 < n:65 /\ j:66 < n:65 /\ k:67 < n:65
         /\ n:65 <= l':2531)}
**** alpha hat: 
  {<Split [true
            (l':2496) = n:65
           (__cost':2464) = (1)*(__cost:70) + n:65^2
           (m':2465) = n:65
           (k':2534) = (1)*(k:67) + 1
           (-__cost':2464) <= (1)*(-__cost:70) + (-1)*n:65
                               + (-1)*(n:65 * i:64)
           (-__cost':2464) <= (1)*(-__cost:70) + (-1)*n:65
                               + (-1)*(n:65 * j:66)
           (-__cost':2464) <= (1)*(-__cost:70) + (-1)*n:65 + (-1)*n:65*k:67
           }
          pre:
            [|-n:65+(n:65 * n:65)-(n:65 * i:64)>=0;
              -n:65+(n:65 * n:65)-(n:65 * j:66)>=0;
              -n:65+(n:65 * n:65)-(n:65 * k:67)>=0; -k:67+(n:65 * k:67)>=0;
              __cost:70>=0; k:67>=0; n:65-j:66-1>=0; n:65-i:64-1>=0;
              n:65-k:67-1>=0|]
          post:
            [|-n:65+m':2465=0; -n:65+l':2496=0;
              -n:65+(n:65 * n:65)-(n:65 * i:64)>=0;
              -n:65+(n:65 * n:65)-(n:65 * j:66)>=0;
              -n:65+(n:65 * n:65)-(n:65 * (-1 + k':2534))>=0;
              -(n:65 * n:65)+__cost':2464>=0;
              -k':2534+(n:65 * (-1 + k':2534))+1>=0; k':2534-1>=0;
              n:65-j:66-1>=0; n:65-i:64-1>=0; n:65-k':2534>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':2464
   k := k':2534
   l := l':2496
   m := m':2465
   when ((!((0 <= K:2559 /\ K:2559 <= 0)) \/ mid_l:2562 = l:68)
           /\ (!(1 <= K:2559) \/ mid_l:2562 = n:65)
           /\ (!(0 <= K:2559)
                 \/ mid___cost:2564 = (__cost:70 + ((n:65 * n:65) * K:2559)))
           /\ (!((0 <= K:2559 /\ K:2559 <= 0)) \/ mid_m:2561 = m:69)
           /\ (!(1 <= K:2559) \/ mid_m:2561 = n:65)
           /\ (!(0 <= K:2559) \/ mid_k:2563 = (k:67 + K:2559))
           /\ (!(0 <= K:2559)
                 \/ -mid___cost:2564 <= (-__cost:70 + -((n:65 * K:2559))
                                           + -(((n:65 * i:64) * K:2559))))
           /\ (!(0 <= K:2559)
                 \/ -mid___cost:2564 <= (-__cost:70 + -((n:65 * K:2559))
                                           + -(((n:65 * j:66) * K:2559))))
           /\ (!(0 <= K:2559)
                 \/ -mid___cost:2564 <= (-__cost:70 + (-1/2 * n:65 * K:2559)
                                           + -((n:65 * k:67 * K:2559))
                                           + (-1/2 * n:65 * (K:2559 * K:2559))))
           /\ ((K:2559 = 0 /\ m:69 = mid_m:2561 /\ l:68 = mid_l:2562
                  /\ k:67 = mid_k:2563 /\ __cost:70 = mid___cost:2564)
                 \/ (1 <= K:2559
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * j:66)))
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * k:67)))
                       /\ 0 <= (-k:67 + (n:65 * k:67)) /\ 0 <= __cost:70
                       /\ 0 <= k:67 /\ 0 <= (-1 + n:65 + -j:66)
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (-1 + n:65 + -k:67)
                       /\ (-n:65 + mid_m:2561) = 0
                       /\ (-n:65 + mid_l:2562) = 0
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * j:66)))
                       /\ 0 <= (-n:65 + (n:65 * n:65)
                                  + -((n:65 * (-1 + mid_k:2563))))
                       /\ 0 <= (-((n:65 * n:65)) + mid___cost:2564)
                       /\ 0 <= (1 + -mid_k:2563 + (n:65 * (-1 + mid_k:2563)))
                       /\ 0 <= (-1 + mid_k:2563) /\ 0 <= (-1 + n:65 + -j:66)
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (n:65 + -mid_k:2563))) /\ K:2560 = 0
           /\ mid_m:2561 = m':2465 /\ mid_l:2562 = l':2496
           /\ mid_k:2563 = k':2534 /\ mid___cost:2564 = __cost':2464
           /\ 0 = K:2560 /\ (K:2559 + K:2560) = K:2558 /\ 0 <= K:2558)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':2585
 j := (j:66 + 1)
 k := k':2584
 l := l':2583
 m := m':2582
 when (1 <= n:65 /\ 0 <= j:66 /\ i:64 < n:65 /\ j:66 < n:65
         /\ (!((0 <= K:2576 /\ K:2576 <= 0)) \/ mid_l:2577 = l:68)
         /\ (!(1 <= K:2576) \/ mid_l:2577 = n:65)
         /\ (!(0 <= K:2576)
               \/ mid___cost:2578 = (__cost:70 + ((n:65 * n:65) * K:2576)))
         /\ (!((0 <= K:2576 /\ K:2576 <= 0)) \/ mid_m:2579 = m:69)
         /\ (!(1 <= K:2576) \/ mid_m:2579 = n:65)
         /\ (!(0 <= K:2576) \/ mid_k:2580 = K:2576)
         /\ (!(0 <= K:2576)
               \/ -mid___cost:2578 <= (-__cost:70 + -((n:65 * K:2576))
                                         + -(((n:65 * i:64) * K:2576))))
         /\ (!(0 <= K:2576)
               \/ -mid___cost:2578 <= (-__cost:70 + -((n:65 * K:2576))
                                         + -(((n:65 * j:66) * K:2576))))
         /\ (!(0 <= K:2576)
               \/ -mid___cost:2578 <= (-__cost:70 + (-1/2 * n:65 * K:2576)
                                         + (-1/2 * n:65 * (K:2576 * K:2576))))
         /\ ((K:2576 = 0 /\ m:69 = mid_m:2579 /\ l:68 = mid_l:2577
                /\ 0 = mid_k:2580 /\ __cost:70 = mid___cost:2578)
               \/ (1 <= K:2576
                     /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                     /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * j:66)))
                     /\ 0 <= (-n:65 + (n:65 * n:65)) /\ 0 <= __cost:70
                     /\ 0 <= (-1 + n:65 + -j:66) /\ 0 <= (-1 + n:65 + -i:64)
                     /\ 0 <= (-1 + n:65) /\ (-n:65 + mid_m:2579) = 0
                     /\ (-n:65 + mid_l:2577) = 0
                     /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                     /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * j:66)))
                     /\ 0 <= (-n:65 + (n:65 * n:65)
                                + -((n:65 * (-1 + mid_k:2580))))
                     /\ 0 <= (-((n:65 * n:65)) + mid___cost:2578)
                     /\ 0 <= (1 + -mid_k:2580 + (n:65 * (-1 + mid_k:2580)))
                     /\ 0 <= (-1 + mid_k:2580) /\ 0 <= (-1 + n:65 + -j:66)
                     /\ 0 <= (-1 + n:65 + -i:64) /\ 0 <= (n:65 + -mid_k:2580)))
         /\ K:2581 = 0 /\ mid_m:2579 = m':2582 /\ mid_l:2577 = l':2583
         /\ mid_k:2580 = k':2584 /\ mid___cost:2578 = __cost':2585
         /\ 0 = K:2581 /\ (K:2576 + K:2581) = K:2586 /\ 0 <= K:2586
         /\ 1 <= n:65 /\ 0 <= k':2584 /\ i:64 < n:65 /\ j:66 < n:65
         /\ n:65 <= k':2584)}
**** alpha hat: 
  {<Split [true
            (m':2465) = n:65
           (l':2496) = n:65
           (__cost':2464) = (1)*(__cost:70) + n:65^3
           (j':2587) = (1)*(j:66) + 1
           (k':2534) = n:65
           (-__cost':2464) <= (1)*(-__cost:70) + (-1)*(n:65 * n:65)
                               + (-1)*((i:64 * n:65) * n:65)
           (-__cost':2464) <= (1)*(-__cost:70) + (-1)*n:65^2*j:66
                               + (-1)*(n:65 * n:65)
           (-__cost':2464) <= (1)*(-__cost:70) + (-1)*1 + 3*n:65 + (-1)*i:64
                               + (-3)*(n:65 * n:65) + 2*(n:65 * i:64)
                               + (-1)*((i:64 * n:65) * n:65)
           (-__cost':2464) <= (1)*(-__cost:70) + (-1)*1 + 3*n:65
                               + 2*n:65*j:66 + (-1)*n:65^2*j:66
                               + (-3)*(n:65 * n:65) + (-1)*j:66
           }
          pre:
            [|-(n:65 * j:66)+(j:66 * n:65)=0; -(n:65 * i:64)+(i:64 * n:65)=0;
              -2n:65+(n:65 * n:65)+1>=0;
              -n:65+(n:65 * n:65)-(n:65 * j:66)>=0;
              -n:65+(n:65 * n:65)-(n:65 * i:64)>=0; -j:66+(n:65 * j:66)>=0;
              -(n:65 * n:65)+((n:65 * n:65) * n:65)-((j:66 * n:65) * n:65)>=0;
              -(n:65 * n:65)+((n:65 * n:65) * n:65)-((i:64 * n:65) * n:65)>=0;
              __cost:70>=0; j:66-2(n:65 * j:66)+((j:66 * n:65) * n:65)>=0;
              j:66>=0; n:65-i:64-1>=0; n:65-j:66-1>=0;
              3n:65-i:64-3(n:65 * n:65)+((n:65 * n:65) * n:65)+2(n:65 * i:64)
              -((i:64 * n:65) * n:65)-1>=0;
              3n:65-j:66-3(n:65 * n:65)+((n:65 * n:65) * n:65)+2(n:65 * j:66)
              -((j:66 * n:65) * n:65)-1>=0|]
          post:
            [|-n:65+m':2465=0; -n:65+l':2496=0; -n:65+k':2534=0;
              -(n:65 * (-1 + j':2587))+((-1 + j':2587) * n:65)=0;
              -(n:65 * i:64)+(i:64 * n:65)=0; -2n:65+(n:65 * n:65)+1>=0;
              -n:65+(n:65 * n:65)-(n:65 * (-1 + j':2587))>=0;
              -n:65+(n:65 * n:65)-(n:65 * i:64)>=0;
              -(n:65 * n:65)+((n:65 * n:65) * n:65)
              -((-n:65 + (j':2587 * n:65)) * n:65)>=0;
              -(n:65 * n:65)+((n:65 * n:65) * n:65)-((i:64 * n:65) * n:65)>=0;
              -((n:65 * n:65) * n:65)+__cost':2464>=0;
              -j':2587+(n:65 * (-1 + j':2587))+1>=0;
              j':2587-2(n:65 * (-1 + j':2587))
              +((-n:65 + (j':2587 * n:65)) * n:65)-1>=0; j':2587-1>=0;
              n:65-i:64-1>=0; n:65-j':2587>=0;
              3n:65-i:64-3(n:65 * n:65)+((n:65 * n:65) * n:65)+2(n:65 * i:64)
              -((i:64 * n:65) * n:65)-1>=0;
              3n:65-3(n:65 * n:65)+((n:65 * n:65) * n:65)-j':2587
              +2(n:65 * (-1 + j':2587))-((-n:65 + (j':2587 * n:65)) * n:65)>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':2464
   j := j':2587
   k := k':2534
   l := l':2496
   m := m':2465
   when ((!((0 <= K:2623 /\ K:2623 <= 0)) \/ mid_m:2625 = m:69)
           /\ (!(1 <= K:2623) \/ mid_m:2625 = n:65)
           /\ (!((0 <= K:2623 /\ K:2623 <= 0)) \/ mid_l:2626 = l:68)
           /\ (!(1 <= K:2623) \/ mid_l:2626 = n:65)
           /\ (!(0 <= K:2623)
                 \/ mid___cost:2629 = (__cost:70
                                         + ((n:65 * (n:65 * n:65)) * K:2623)))
           /\ (!(0 <= K:2623) \/ mid_j:2628 = (j:66 + K:2623))
           /\ (!((0 <= K:2623 /\ K:2623 <= 0)) \/ mid_k:2627 = k:67)
           /\ (!(1 <= K:2623) \/ mid_k:2627 = n:65)
           /\ (!(0 <= K:2623)
                 \/ -mid___cost:2629 <= (-__cost:70
                                           + -(((n:65 * n:65) * K:2623))
                                           + -((((i:64 * n:65) * n:65)
                                                  * K:2623))))
           /\ (!(0 <= K:2623)
                 \/ -mid___cost:2629 <= (-__cost:70
                                           + -(((n:65 * n:65) * K:2623))
                                           + (1/2 * (n:65 * n:65) * K:2623)
                                           + -((j:66 * (n:65 * n:65) * K:2623))
                                           + (-1/2 * (n:65 * n:65)
                                                * (K:2623 * K:2623))))
           /\ (!(0 <= K:2623)
                 \/ -mid___cost:2629 <= (-__cost:70 + -K:2623
                                           + (3 * n:65 * K:2623)
                                           + -((i:64 * K:2623))
                                           + (-3 * (n:65 * n:65) * K:2623)
                                           + (2 * (n:65 * i:64) * K:2623)
                                           + -((((i:64 * n:65) * n:65)
                                                  * K:2623))))
           /\ (!(0 <= K:2623)
                 \/ -mid___cost:2629 <= (-__cost:70 + (-1/2 * K:2623)
                                           + (2 * n:65 * K:2623)
                                           + -((j:66 * K:2623))
                                           + (2 * n:65 * j:66 * K:2623)
                                           + (-3 * (n:65 * n:65) * K:2623)
                                           + (1/2 * (n:65 * n:65) * K:2623)
                                           + -((j:66 * (n:65 * n:65) * K:2623))
                                           + (-1/2 * (K:2623 * K:2623))
                                           + (n:65 * (K:2623 * K:2623))
                                           + (-1/2 * (n:65 * n:65)
                                                * (K:2623 * K:2623))))
           /\ ((K:2623 = 0 /\ m:69 = mid_m:2625 /\ l:68 = mid_l:2626
                  /\ k:67 = mid_k:2627 /\ j:66 = mid_j:2628
                  /\ __cost:70 = mid___cost:2629)
                 \/ (1 <= K:2623 /\ (-((n:65 * j:66)) + (j:66 * n:65)) = 0
                       /\ (-((n:65 * i:64)) + (i:64 * n:65)) = 0
                       /\ 0 <= (1 + (-2 * n:65) + (n:65 * n:65))
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * j:66)))
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                       /\ 0 <= (-j:66 + (n:65 * j:66))
                       /\ 0 <= (-((n:65 * n:65)) + ((n:65 * n:65) * n:65)
                                  + -(((j:66 * n:65) * n:65)))
                       /\ 0 <= (-((n:65 * n:65)) + ((n:65 * n:65) * n:65)
                                  + -(((i:64 * n:65) * n:65)))
                       /\ 0 <= __cost:70
                       /\ 0 <= (j:66 + (-2 * (n:65 * j:66))
                                  + ((j:66 * n:65) * n:65)) /\ 0 <= j:66
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (-1 + n:65 + -j:66)
                       /\ 0 <= (-1 + (3 * n:65) + -i:64
                                  + (-3 * (n:65 * n:65))
                                  + ((n:65 * n:65) * n:65)
                                  + (2 * (n:65 * i:64))
                                  + -(((i:64 * n:65) * n:65)))
                       /\ 0 <= (-1 + (3 * n:65) + -j:66
                                  + (-3 * (n:65 * n:65))
                                  + ((n:65 * n:65) * n:65)
                                  + (2 * (n:65 * j:66))
                                  + -(((j:66 * n:65) * n:65)))
                       /\ (-n:65 + mid_m:2625) = 0
                       /\ (-n:65 + mid_l:2626) = 0
                       /\ (-n:65 + mid_k:2627) = 0
                       /\ (-((n:65 * (-1 + mid_j:2628)))
                             + ((-1 + mid_j:2628) * n:65)) = 0
                       /\ (-((n:65 * i:64)) + (i:64 * n:65)) = 0
                       /\ 0 <= (1 + (-2 * n:65) + (n:65 * n:65))
                       /\ 0 <= (-n:65 + (n:65 * n:65)
                                  + -((n:65 * (-1 + mid_j:2628))))
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                       /\ 0 <= (-((n:65 * n:65)) + ((n:65 * n:65) * n:65)
                                  + -(((-n:65 + (mid_j:2628 * n:65)) * n:65)))
                       /\ 0 <= (-((n:65 * n:65)) + ((n:65 * n:65) * n:65)
                                  + -(((i:64 * n:65) * n:65)))
                       /\ 0 <= (-(((n:65 * n:65) * n:65)) + mid___cost:2629)
                       /\ 0 <= (1 + -mid_j:2628 + (n:65 * (-1 + mid_j:2628)))
                       /\ 0 <= (-1 + mid_j:2628
                                  + (-2 * (n:65 * (-1 + mid_j:2628)))
                                  + ((-n:65 + (mid_j:2628 * n:65)) * n:65))
                       /\ 0 <= (-1 + mid_j:2628) /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (n:65 + -mid_j:2628)
                       /\ 0 <= (-1 + (3 * n:65) + -i:64
                                  + (-3 * (n:65 * n:65))
                                  + ((n:65 * n:65) * n:65)
                                  + (2 * (n:65 * i:64))
                                  + -(((i:64 * n:65) * n:65)))
                       /\ 0 <= ((3 * n:65) + (-3 * (n:65 * n:65))
                                  + ((n:65 * n:65) * n:65) + -mid_j:2628
                                  + (2 * (n:65 * (-1 + mid_j:2628)))
                                  + -(((-n:65 + (mid_j:2628 * n:65)) * n:65)))))
           /\ K:2624 = 0 /\ mid_m:2625 = m':2465 /\ mid_l:2626 = l':2496
           /\ mid_k:2627 = k':2534 /\ mid_j:2628 = j':2587
           /\ mid___cost:2629 = __cost':2464 /\ 0 = K:2624
           /\ (K:2623 + K:2624) = K:2622 /\ 0 <= K:2622)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':2654
 i := (i:64 + 1)
 j := j':2653
 k := k':2652
 l := l':2651
 m := m':2650
 when (0 <= i:64 /\ i:64 < n:65
         /\ (!((0 <= K:2643 /\ K:2643 <= 0)) \/ mid_m:2644 = m:69)
         /\ (!(1 <= K:2643) \/ mid_m:2644 = n:65)
         /\ (!((0 <= K:2643 /\ K:2643 <= 0)) \/ mid_l:2645 = l:68)
         /\ (!(1 <= K:2643) \/ mid_l:2645 = n:65)
         /\ (!(0 <= K:2643)
               \/ mid___cost:2646 = (__cost:70
                                       + ((n:65 * (n:65 * n:65)) * K:2643)))
         /\ (!(0 <= K:2643) \/ mid_j:2647 = K:2643)
         /\ (!((0 <= K:2643 /\ K:2643 <= 0)) \/ mid_k:2648 = k:67)
         /\ (!(1 <= K:2643) \/ mid_k:2648 = n:65)
         /\ (!(0 <= K:2643)
               \/ -mid___cost:2646 <= (-__cost:70
                                         + -(((n:65 * n:65) * K:2643))
                                         + -((((i:64 * n:65) * n:65) * K:2643))))
         /\ (!(0 <= K:2643)
               \/ -mid___cost:2646 <= (-__cost:70
                                         + -(((n:65 * n:65) * K:2643))
                                         + (1/2 * (n:65 * n:65) * K:2643)
                                         + (-1/2 * (n:65 * n:65)
                                              * (K:2643 * K:2643))))
         /\ (!(0 <= K:2643)
               \/ -mid___cost:2646 <= (-__cost:70 + -K:2643
                                         + (3 * n:65 * K:2643)
                                         + -((i:64 * K:2643))
                                         + (-3 * (n:65 * n:65) * K:2643)
                                         + (2 * (n:65 * i:64) * K:2643)
                                         + -((((i:64 * n:65) * n:65) * K:2643))))
         /\ (!(0 <= K:2643)
               \/ -mid___cost:2646 <= (-__cost:70 + (-1/2 * K:2643)
                                         + (2 * n:65 * K:2643)
                                         + (-3 * (n:65 * n:65) * K:2643)
                                         + (1/2 * (n:65 * n:65) * K:2643)
                                         + (-1/2 * (K:2643 * K:2643))
                                         + (n:65 * (K:2643 * K:2643))
                                         + (-1/2 * (n:65 * n:65)
                                              * (K:2643 * K:2643))))
         /\ ((K:2643 = 0 /\ m:69 = mid_m:2644 /\ l:68 = mid_l:2645
                /\ k:67 = mid_k:2648 /\ 0 = mid_j:2647
                /\ __cost:70 = mid___cost:2646)
               \/ (1 <= K:2643 /\ (-((n:65 * i:64)) + (i:64 * n:65)) = 0
                     /\ 0 <= (1 + (-2 * n:65) + (n:65 * n:65))
                     /\ 0 <= (-n:65 + (n:65 * n:65))
                     /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                     /\ 0 <= (-((n:65 * n:65)) + ((n:65 * n:65) * n:65))
                     /\ 0 <= (-((n:65 * n:65)) + ((n:65 * n:65) * n:65)
                                + -(((i:64 * n:65) * n:65)))
                     /\ 0 <= __cost:70 /\ 0 <= (-1 + n:65 + -i:64)
                     /\ 0 <= (-1 + n:65)
                     /\ 0 <= (-1 + (3 * n:65) + -i:64 + (-3 * (n:65 * n:65))
                                + ((n:65 * n:65) * n:65)
                                + (2 * (n:65 * i:64))
                                + -(((i:64 * n:65) * n:65)))
                     /\ 0 <= (-1 + (3 * n:65) + (-3 * (n:65 * n:65))
                                + ((n:65 * n:65) * n:65))
                     /\ (-n:65 + mid_m:2644) = 0 /\ (-n:65 + mid_l:2645) = 0
                     /\ (-n:65 + mid_k:2648) = 0
                     /\ (-((n:65 * (-1 + mid_j:2647)))
                           + ((-1 + mid_j:2647) * n:65)) = 0
                     /\ (-((n:65 * i:64)) + (i:64 * n:65)) = 0
                     /\ 0 <= (1 + (-2 * n:65) + (n:65 * n:65))
                     /\ 0 <= (-n:65 + (n:65 * n:65)
                                + -((n:65 * (-1 + mid_j:2647))))
                     /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                     /\ 0 <= (-((n:65 * n:65)) + ((n:65 * n:65) * n:65)
                                + -(((-n:65 + (mid_j:2647 * n:65)) * n:65)))
                     /\ 0 <= (-((n:65 * n:65)) + ((n:65 * n:65) * n:65)
                                + -(((i:64 * n:65) * n:65)))
                     /\ 0 <= (-(((n:65 * n:65) * n:65)) + mid___cost:2646)
                     /\ 0 <= (1 + -mid_j:2647 + (n:65 * (-1 + mid_j:2647)))
                     /\ 0 <= (-1 + mid_j:2647
                                + (-2 * (n:65 * (-1 + mid_j:2647)))
                                + ((-n:65 + (mid_j:2647 * n:65)) * n:65))
                     /\ 0 <= (-1 + mid_j:2647) /\ 0 <= (-1 + n:65 + -i:64)
                     /\ 0 <= (n:65 + -mid_j:2647)
                     /\ 0 <= (-1 + (3 * n:65) + -i:64 + (-3 * (n:65 * n:65))
                                + ((n:65 * n:65) * n:65)
                                + (2 * (n:65 * i:64))
                                + -(((i:64 * n:65) * n:65)))
                     /\ 0 <= ((3 * n:65) + (-3 * (n:65 * n:65))
                                + ((n:65 * n:65) * n:65) + -mid_j:2647
                                + (2 * (n:65 * (-1 + mid_j:2647)))
                                + -(((-n:65 + (mid_j:2647 * n:65)) * n:65)))))
         /\ K:2649 = 0 /\ mid_m:2644 = m':2650 /\ mid_l:2645 = l':2651
         /\ mid_k:2648 = k':2652 /\ mid_j:2647 = j':2653
         /\ mid___cost:2646 = __cost':2654 /\ 0 = K:2649
         /\ (K:2643 + K:2649) = K:2655 /\ 0 <= K:2655 /\ 1 <= n:65
         /\ 0 <= j':2653 /\ i:64 < n:65 /\ n:65 <= j':2653)}
**** alpha hat: 
  {<Split [true
            (j':2587) = n:65
           (i':2656) = (1)*(i:64) + 1
           (__cost':2464) = (1)*(__cost:70) + n:65^4
           (m':2465) = n:65
           (l':2496) = n:65
           (k':2534) = n:65
           (-__cost':2464) <= (1)*(-__cost:70) + 1 + (-4)*n:65
                               + (-3)*n:65*i:64 + 6*(n:65 * n:65)
                               + 3*(n:65 * n:65)*i:64
                               + (-4)*((n:65 * n:65) * n:65)
                               + (-1)*((n:65 * n:65) * n:65)*i:64 + i:64
           (-__cost':2464) <= (1)*(-__cost:70) + (-1)*((n:65 * n:65) * n:65)
                               + (-1)*((n:65 * n:65) * n:65)*i:64
           }
          pre:
            [|-i:64-3((n:65 * n:65) * i:64)+(((n:65 * n:65) * n:65) * i:64)
              +3(n:65 * i:64)>=0; -i:64+(n:65 * i:64)>=0; -i:64+n:65-1>=0;
              -i:64+3n:65-3(n:65 * n:65)+((n:65 * n:65) * n:65)
              -((n:65 * n:65) * i:64)+2(n:65 * i:64)-1>=0;
              -2n:65+(n:65 * n:65)+1>=0;
              -n:65+(n:65 * n:65)-(n:65 * i:64)>=0;
              -(n:65 * n:65)+((n:65 * n:65) * n:65)-((n:65 * n:65) * i:64)>=0;
              -((n:65 * n:65) * n:65)+(((n:65 * n:65) * n:65) * n:65)
              -(((n:65 * n:65) * n:65) * i:64)>=0; __cost:70>=0;
              i:64-4n:65+6(n:65 * n:65)-4((n:65 * n:65) * n:65)
              +3((n:65 * n:65) * i:64)+(((n:65 * n:65) * n:65) * n:65)
              -(((n:65 * n:65) * n:65) * i:64)-3(n:65 * i:64)+1>=0; i:64>=0;
              i:64+((n:65 * n:65) * i:64)-2(n:65 * i:64)>=0|]
          post:
            [|-n:65+m':2465=0; -n:65+l':2496=0; -n:65+k':2534=0;
              -n:65+j':2587=0;
              -4n:65+6(n:65 * n:65)-4((n:65 * n:65) * n:65)+i':2656
              +3((n:65 * n:65) * (-1 + i':2656))
              +(((n:65 * n:65) * n:65) * n:65)
              -(((n:65 * n:65) * n:65) * (-1 + i':2656))
              -3(n:65 * (-1 + i':2656))>=0; -2n:65+(n:65 * n:65)+1>=0;
              -n:65+(n:65 * n:65)-(n:65 * (-1 + i':2656))>=0;
              -(n:65 * n:65)+((n:65 * n:65) * n:65)
              -((n:65 * n:65) * (-1 + i':2656))>=0;
              -((n:65 * n:65) * n:65)+(((n:65 * n:65) * n:65) * n:65)
              -(((n:65 * n:65) * n:65) * (-1 + i':2656))>=0;
              -i':2656-3((n:65 * n:65) * (-1 + i':2656))
              +(((n:65 * n:65) * n:65) * (-1 + i':2656))
              +3(n:65 * (-1 + i':2656))+1>=0;
              -i':2656+(n:65 * (-1 + i':2656))+1>=0;
              -(((n:65 * n:65) * n:65) * n:65)+__cost':2464>=0; i':2656-1>=0;
              i':2656+((n:65 * n:65) * (-1 + i':2656))
              -2(n:65 * (-1 + i':2656))-1>=0; n:65-i':2656>=0;
              3n:65-3(n:65 * n:65)+((n:65 * n:65) * n:65)-i':2656
              -((n:65 * n:65) * (-1 + i':2656))+2(n:65 * (-1 + i':2656))>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':2464
   i := i':2656
   j := j':2587
   k := k':2534
   l := l':2496
   m := m':2465
   when ((!((0 <= K:2695 /\ K:2695 <= 0)) \/ mid_j:2700 = j:66)
           /\ (!(1 <= K:2695) \/ mid_j:2700 = n:65)
           /\ (!(0 <= K:2695) \/ mid_i:2701 = (i:64 + K:2695))
           /\ (!(0 <= K:2695)
                 \/ mid___cost:2702 = (__cost:70
                                         + (((n:65 * n:65) * (n:65 * n:65))
                                              * K:2695)))
           /\ (!((0 <= K:2695 /\ K:2695 <= 0)) \/ mid_m:2697 = m:69)
           /\ (!(1 <= K:2695) \/ mid_m:2697 = n:65)
           /\ (!((0 <= K:2695 /\ K:2695 <= 0)) \/ mid_l:2698 = l:68)
           /\ (!(1 <= K:2695) \/ mid_l:2698 = n:65)
           /\ (!((0 <= K:2695 /\ K:2695 <= 0)) \/ mid_k:2699 = k:67)
           /\ (!(1 <= K:2695) \/ mid_k:2699 = n:65)
           /\ (!(0 <= K:2695)
                 \/ -mid___cost:2702 <= (-__cost:70 + (1/2 * K:2695)
                                           + (-5/2 * n:65 * K:2695)
                                           + (9/2 * (n:65 * n:65) * K:2695)
                                           + (-7/2 * ((n:65 * n:65) * n:65)
                                                * K:2695) + (i:64 * K:2695)
                                           + (-3 * n:65 * i:64 * K:2695)
                                           + (3 * (n:65 * n:65) * i:64
                                                * K:2695)
                                           + -((((n:65 * n:65) * n:65) * i:64
                                                  * K:2695))
                                           + (1/2 * (K:2695 * K:2695))
                                           + (-3/2 * n:65 * (K:2695 * K:2695))
                                           + (3/2 * (n:65 * n:65)
                                                * (K:2695 * K:2695))
                                           + (-1/2 * ((n:65 * n:65) * n:65)
                                                * (K:2695 * K:2695))))
           /\ (!(0 <= K:2695)
                 \/ -mid___cost:2702 <= (-__cost:70
                                           + (-1/2 * ((n:65 * n:65) * n:65)
                                                * K:2695)
                                           + -((((n:65 * n:65) * n:65) * i:64
                                                  * K:2695))
                                           + (-1/2 * ((n:65 * n:65) * n:65)
                                                * (K:2695 * K:2695))))
           /\ ((K:2695 = 0 /\ m:69 = mid_m:2697 /\ l:68 = mid_l:2698
                  /\ k:67 = mid_k:2699 /\ j:66 = mid_j:2700
                  /\ i:64 = mid_i:2701 /\ __cost:70 = mid___cost:2702)
                 \/ (1 <= K:2695
                       /\ 0 <= (-i:64 + (-3 * ((n:65 * n:65) * i:64))
                                  + (((n:65 * n:65) * n:65) * i:64)
                                  + (3 * (n:65 * i:64)))
                       /\ 0 <= (-i:64 + (n:65 * i:64))
                       /\ 0 <= (-1 + -i:64 + n:65)
                       /\ 0 <= (-1 + -i:64 + (3 * n:65)
                                  + (-3 * (n:65 * n:65))
                                  + ((n:65 * n:65) * n:65)
                                  + -(((n:65 * n:65) * i:64))
                                  + (2 * (n:65 * i:64)))
                       /\ 0 <= (1 + (-2 * n:65) + (n:65 * n:65))
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                       /\ 0 <= (-((n:65 * n:65)) + ((n:65 * n:65) * n:65)
                                  + -(((n:65 * n:65) * i:64)))
                       /\ 0 <= (-(((n:65 * n:65) * n:65))
                                  + (((n:65 * n:65) * n:65) * n:65)
                                  + -((((n:65 * n:65) * n:65) * i:64)))
                       /\ 0 <= __cost:70
                       /\ 0 <= (1 + i:64 + (-4 * n:65) + (6 * (n:65 * n:65))
                                  + (-4 * ((n:65 * n:65) * n:65))
                                  + (3 * ((n:65 * n:65) * i:64))
                                  + (((n:65 * n:65) * n:65) * n:65)
                                  + -((((n:65 * n:65) * n:65) * i:64))
                                  + (-3 * (n:65 * i:64))) /\ 0 <= i:64
                       /\ 0 <= (i:64 + ((n:65 * n:65) * i:64)
                                  + (-2 * (n:65 * i:64)))
                       /\ (-n:65 + mid_m:2697) = 0
                       /\ (-n:65 + mid_l:2698) = 0
                       /\ (-n:65 + mid_k:2699) = 0
                       /\ (-n:65 + mid_j:2700) = 0
                       /\ 0 <= ((-4 * n:65) + (6 * (n:65 * n:65))
                                  + (-4 * ((n:65 * n:65) * n:65))
                                  + mid_i:2701
                                  + (3 * ((n:65 * n:65) * (-1 + mid_i:2701)))
                                  + (((n:65 * n:65) * n:65) * n:65)
                                  + -((((n:65 * n:65) * n:65)
                                         * (-1 + mid_i:2701)))
                                  + (-3 * (n:65 * (-1 + mid_i:2701))))
                       /\ 0 <= (1 + (-2 * n:65) + (n:65 * n:65))
                       /\ 0 <= (-n:65 + (n:65 * n:65)
                                  + -((n:65 * (-1 + mid_i:2701))))
                       /\ 0 <= (-((n:65 * n:65)) + ((n:65 * n:65) * n:65)
                                  + -(((n:65 * n:65) * (-1 + mid_i:2701))))
                       /\ 0 <= (-(((n:65 * n:65) * n:65))
                                  + (((n:65 * n:65) * n:65) * n:65)
                                  + -((((n:65 * n:65) * n:65)
                                         * (-1 + mid_i:2701))))
                       /\ 0 <= (1 + -mid_i:2701
                                  + (-3 * ((n:65 * n:65) * (-1 + mid_i:2701)))
                                  + (((n:65 * n:65) * n:65)
                                       * (-1 + mid_i:2701))
                                  + (3 * (n:65 * (-1 + mid_i:2701))))
                       /\ 0 <= (1 + -mid_i:2701 + (n:65 * (-1 + mid_i:2701)))
                       /\ 0 <= (-((((n:65 * n:65) * n:65) * n:65))
                                  + mid___cost:2702)
                       /\ 0 <= (-1 + mid_i:2701)
                       /\ 0 <= (-1 + mid_i:2701
                                  + ((n:65 * n:65) * (-1 + mid_i:2701))
                                  + (-2 * (n:65 * (-1 + mid_i:2701))))
                       /\ 0 <= (n:65 + -mid_i:2701)
                       /\ 0 <= ((3 * n:65) + (-3 * (n:65 * n:65))
                                  + ((n:65 * n:65) * n:65) + -mid_i:2701
                                  + -(((n:65 * n:65) * (-1 + mid_i:2701)))
                                  + (2 * (n:65 * (-1 + mid_i:2701))))))
           /\ K:2696 = 0 /\ mid_m:2697 = m':2465 /\ mid_l:2698 = l':2496
           /\ mid_k:2699 = k':2534 /\ mid_j:2700 = j':2587
           /\ mid_i:2701 = i':2656 /\ mid___cost:2702 = __cost':2464
           /\ 0 = K:2696 /\ (K:2695 + K:2696) = K:2694 /\ 0 <= K:2694)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
11  13  21  


New-style (IRE) regular expression in IREregExpMap for reID=11: 
Dot(
  Dot(
    Dot(
      Plus(
        Weight(Base relation: 
          {__cost := 0
           tmp___0 := 0
           argv := param1:30
           argv@pos := param1@pos:29
           argv@width := param1@width:28
           when (0 <= tr:2457 /\ tr:2458 <= 0)}        )
        ,
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := 0
               argv := param1:30
               param0 := tr:2461
               argv@pos := param1@pos:29
               param0@pos := type_err:2462
               argv@width := param1@width:28
               param0@width := type_err:2463
               when (tr:2459 < 0 \/ 0 < tr:2460)}            )
            ,
            Var(13)
          )
          ,
          Weight(Base relation: 
            {tmp___0 := havoc:19}          )
        )
      )
      ,
      Weight(Base relation: 
        {param0 := tmp___0:8
         param0@pos := type_err:37
         param0@width := type_err:38}      )
    )
    ,
    Var(21)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:35
     return@width := type_err:36}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
One()


New-style (IRE) regular expression in IREregExpMap for reID=21: 
Weight(Base relation: 
  {__cost := __cost':2716
   i := i':2715
   j := j':2714
   k := k':2713
   l := l':2712
   m := m':2711
   n := param0:27
   return := havoc:2718
   return@pos := type_err:2719
   return@width := type_err:2720
   when ((!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_j:2704 = j:66)
           /\ (!(1 <= K:2703) \/ mid_j:2704 = param0:27)
           /\ (!(0 <= K:2703) \/ mid_i:2705 = K:2703)
           /\ (!(0 <= K:2703)
                 \/ mid___cost:2706 = (__cost:70
                                         + (((param0:27 * param0:27)
                                               * (param0:27 * param0:27))
                                              * K:2703)))
           /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_m:2707 = m:69)
           /\ (!(1 <= K:2703) \/ mid_m:2707 = param0:27)
           /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_l:2708 = l:68)
           /\ (!(1 <= K:2703) \/ mid_l:2708 = param0:27)
           /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_k:2709 = k:67)
           /\ (!(1 <= K:2703) \/ mid_k:2709 = param0:27)
           /\ (!(0 <= K:2703)
                 \/ -mid___cost:2706 <= (-__cost:70 + (1/2 * K:2703)
                                           + (-5/2 * param0:27 * K:2703)
                                           + (9/2 * (param0:27 * param0:27)
                                                * K:2703)
                                           + (-7/2
                                                * ((param0:27 * param0:27)
                                                     * param0:27) * K:2703)
                                           + (1/2 * (K:2703 * K:2703))
                                           + (-3/2 * param0:27
                                                * (K:2703 * K:2703))
                                           + (3/2 * (param0:27 * param0:27)
                                                * (K:2703 * K:2703))
                                           + (-1/2
                                                * ((param0:27 * param0:27)
                                                     * param0:27)
                                                * (K:2703 * K:2703))))
           /\ (!(0 <= K:2703)
                 \/ -mid___cost:2706 <= (-__cost:70
                                           + (-1/2
                                                * ((param0:27 * param0:27)
                                                     * param0:27) * K:2703)
                                           + (-1/2
                                                * ((param0:27 * param0:27)
                                                     * param0:27)
                                                * (K:2703 * K:2703))))
           /\ ((K:2703 = 0 /\ m:69 = mid_m:2707 /\ l:68 = mid_l:2708
                  /\ k:67 = mid_k:2709 /\ j:66 = mid_j:2704 /\ 0 = mid_i:2705
                  /\ __cost:70 = mid___cost:2706)
                 \/ (1 <= K:2703 /\ 0 <= (-1 + param0:27)
                       /\ 0 <= (-1 + (3 * param0:27)
                                  + (-3 * (param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27))
                       /\ 0 <= (1 + (-2 * param0:27)
                                  + (param0:27 * param0:27))
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27))
                       /\ 0 <= (-((param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27))
                       /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * param0:27)) /\ 0 <= __cost:70
                       /\ 0 <= (1 + (-4 * param0:27)
                                  + (6 * (param0:27 * param0:27))
                                  + (-4
                                       * ((param0:27 * param0:27) * param0:27))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * param0:27))
                       /\ (-param0:27 + mid_m:2707) = 0
                       /\ (-param0:27 + mid_l:2708) = 0
                       /\ (-param0:27 + mid_k:2709) = 0
                       /\ (-param0:27 + mid_j:2704) = 0
                       /\ 0 <= ((-4 * param0:27)
                                  + (6 * (param0:27 * param0:27))
                                  + (-4
                                       * ((param0:27 * param0:27) * param0:27))
                                  + mid_i:2705
                                  + (3
                                       * ((param0:27 * param0:27)
                                            * (-1 + mid_i:2705)))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * param0:27)
                                  + -((((param0:27 * param0:27) * param0:27)
                                         * (-1 + mid_i:2705)))
                                  + (-3 * (param0:27 * (-1 + mid_i:2705))))
                       /\ 0 <= (1 + (-2 * param0:27)
                                  + (param0:27 * param0:27))
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                  + -((param0:27 * (-1 + mid_i:2705))))
                       /\ 0 <= (-((param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27)
                                  + -(((param0:27 * param0:27)
                                         * (-1 + mid_i:2705))))
                       /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * param0:27)
                                  + -((((param0:27 * param0:27) * param0:27)
                                         * (-1 + mid_i:2705))))
                       /\ 0 <= (1 + -mid_i:2705
                                  + (-3
                                       * ((param0:27 * param0:27)
                                            * (-1 + mid_i:2705)))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * (-1 + mid_i:2705))
                                  + (3 * (param0:27 * (-1 + mid_i:2705))))
                       /\ 0 <= (1 + -mid_i:2705
                                  + (param0:27 * (-1 + mid_i:2705)))
                       /\ 0 <= (-((((param0:27 * param0:27) * param0:27)
                                     * param0:27)) + mid___cost:2706)
                       /\ 0 <= (-1 + mid_i:2705)
                       /\ 0 <= (-1 + mid_i:2705
                                  + ((param0:27 * param0:27)
                                       * (-1 + mid_i:2705))
                                  + (-2 * (param0:27 * (-1 + mid_i:2705))))
                       /\ 0 <= (param0:27 + -mid_i:2705)
                       /\ 0 <= ((3 * param0:27)
                                  + (-3 * (param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27)
                                  + -mid_i:2705
                                  + -(((param0:27 * param0:27)
                                         * (-1 + mid_i:2705)))
                                  + (2 * (param0:27 * (-1 + mid_i:2705))))))
           /\ K:2710 = 0 /\ mid_m:2707 = m':2711 /\ mid_l:2708 = l':2712
           /\ mid_k:2709 = k':2713 /\ mid_j:2704 = j':2714
           /\ mid_i:2705 = i':2715 /\ mid___cost:2706 = __cost':2716
           /\ 0 = K:2710 /\ (K:2703 + K:2710) = K:2717 /\ 0 <= K:2717
           /\ 0 <= i':2715 /\ param0:27 <= i':2715)})



Performing Gaussian Elimination.


  ------------------------------ 
Working on variable 11
  New-style (IRE) regular expression for 11 just before isolating it: 

Project(
  Dot(
    Dot(
      Dot(
        Plus(
          Weight(Base relation: 
            {__cost := 0
             tmp___0 := 0
             argv := param1:30
             argv@pos := param1@pos:29
             argv@width := param1@width:28
             when (0 <= tr:2457 /\ tr:2458 <= 0)}          )
          ,
          Dot(
            Dot(
              Weight(Base relation: 
                {__cost := 0
                 argv := param1:30
                 param0 := tr:2461
                 argv@pos := param1@pos:29
                 param0@pos := type_err:2462
                 argv@width := param1@width:28
                 param0@width := type_err:2463
                 when (tr:2459 < 0 \/ 0 < tr:2460)}              )
              ,
              Var(13)
            )
            ,
            Weight(Base relation: 
              {tmp___0 := havoc:19}            )
          )
        )
        ,
        Weight(Base relation: 
          {param0 := tmp___0:8
           param0@pos := type_err:37
           param0@width := type_err:38}        )
      )
      ,
      Var(21)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:35
       return@width := type_err:36}    )
  )
)



  ------------------------------ 
Working on variable 13
  New-style (IRE) regular expression for 13 just before isolating it: 

One()



  ------------------------------ 
Working on variable 21
  New-style (IRE) regular expression for 21 just before isolating it: 

Weight(Base relation: 
  {__cost := __cost':2716
   return := havoc:2718
   return@pos := type_err:2719
   return@width := type_err:2720
   when ((!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_j:2704 = j:2801)
           /\ (!(1 <= K:2703) \/ mid_j:2704 = param0:27)
           /\ (!(0 <= K:2703) \/ mid_i:2705 = K:2703)
           /\ (!(0 <= K:2703)
                 \/ mid___cost:2706 = (__cost:70
                                         + (((param0:27 * param0:27)
                                               * (param0:27 * param0:27))
                                              * K:2703)))
           /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_m:2707 = m:2802)
           /\ (!(1 <= K:2703) \/ mid_m:2707 = param0:27)
           /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_l:2708 = l:2803)
           /\ (!(1 <= K:2703) \/ mid_l:2708 = param0:27)
           /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_k:2709 = k:2804)
           /\ (!(1 <= K:2703) \/ mid_k:2709 = param0:27)
           /\ (!(0 <= K:2703)
                 \/ -mid___cost:2706 <= (-__cost:70 + (1/2 * K:2703)
                                           + (-5/2 * param0:27 * K:2703)
                                           + (9/2 * (param0:27 * param0:27)
                                                * K:2703)
                                           + (-7/2
                                                * ((param0:27 * param0:27)
                                                     * param0:27) * K:2703)
                                           + (1/2 * (K:2703 * K:2703))
                                           + (-3/2 * param0:27
                                                * (K:2703 * K:2703))
                                           + (3/2 * (param0:27 * param0:27)
                                                * (K:2703 * K:2703))
                                           + (-1/2
                                                * ((param0:27 * param0:27)
                                                     * param0:27)
                                                * (K:2703 * K:2703))))
           /\ (!(0 <= K:2703)
                 \/ -mid___cost:2706 <= (-__cost:70
                                           + (-1/2
                                                * ((param0:27 * param0:27)
                                                     * param0:27) * K:2703)
                                           + (-1/2
                                                * ((param0:27 * param0:27)
                                                     * param0:27)
                                                * (K:2703 * K:2703))))
           /\ ((K:2703 = 0 /\ m:2802 = mid_m:2707 /\ l:2803 = mid_l:2708
                  /\ k:2804 = mid_k:2709 /\ j:2801 = mid_j:2704
                  /\ 0 = mid_i:2705 /\ __cost:70 = mid___cost:2706)
                 \/ (1 <= K:2703 /\ 0 <= (-1 + param0:27)
                       /\ 0 <= (-1 + (3 * param0:27)
                                  + (-3 * (param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27))
                       /\ 0 <= (1 + (-2 * param0:27)
                                  + (param0:27 * param0:27))
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27))
                       /\ 0 <= (-((param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27))
                       /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * param0:27)) /\ 0 <= __cost:70
                       /\ 0 <= (1 + (-4 * param0:27)
                                  + (6 * (param0:27 * param0:27))
                                  + (-4
                                       * ((param0:27 * param0:27) * param0:27))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * param0:27))
                       /\ (-param0:27 + mid_m:2707) = 0
                       /\ (-param0:27 + mid_l:2708) = 0
                       /\ (-param0:27 + mid_k:2709) = 0
                       /\ (-param0:27 + mid_j:2704) = 0
                       /\ 0 <= ((-4 * param0:27)
                                  + (6 * (param0:27 * param0:27))
                                  + (-4
                                       * ((param0:27 * param0:27) * param0:27))
                                  + mid_i:2705
                                  + (3
                                       * ((param0:27 * param0:27)
                                            * (-1 + mid_i:2705)))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * param0:27)
                                  + -((((param0:27 * param0:27) * param0:27)
                                         * (-1 + mid_i:2705)))
                                  + (-3 * (param0:27 * (-1 + mid_i:2705))))
                       /\ 0 <= (1 + (-2 * param0:27)
                                  + (param0:27 * param0:27))
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                  + -((param0:27 * (-1 + mid_i:2705))))
                       /\ 0 <= (-((param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27)
                                  + -(((param0:27 * param0:27)
                                         * (-1 + mid_i:2705))))
                       /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * param0:27)
                                  + -((((param0:27 * param0:27) * param0:27)
                                         * (-1 + mid_i:2705))))
                       /\ 0 <= (1 + -mid_i:2705
                                  + (-3
                                       * ((param0:27 * param0:27)
                                            * (-1 + mid_i:2705)))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * (-1 + mid_i:2705))
                                  + (3 * (param0:27 * (-1 + mid_i:2705))))
                       /\ 0 <= (1 + -mid_i:2705
                                  + (param0:27 * (-1 + mid_i:2705)))
                       /\ 0 <= (-((((param0:27 * param0:27) * param0:27)
                                     * param0:27)) + mid___cost:2706)
                       /\ 0 <= (-1 + mid_i:2705)
                       /\ 0 <= (-1 + mid_i:2705
                                  + ((param0:27 * param0:27)
                                       * (-1 + mid_i:2705))
                                  + (-2 * (param0:27 * (-1 + mid_i:2705))))
                       /\ 0 <= (param0:27 + -mid_i:2705)
                       /\ 0 <= ((3 * param0:27)
                                  + (-3 * (param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27)
                                  + -mid_i:2705
                                  + -(((param0:27 * param0:27)
                                         * (-1 + mid_i:2705)))
                                  + (2 * (param0:27 * (-1 + mid_i:2705))))))
           /\ K:2710 = 0 /\ mid_m:2707 = m':2711 /\ mid_l:2708 = l':2712
           /\ mid_k:2709 = k':2713 /\ mid_j:2704 = j':2714
           /\ mid_i:2705 = i':2715 /\ mid___cost:2706 = __cost':2716
           /\ 0 = K:2710 /\ (K:2703 + K:2710) = K:2717 /\ 0 <= K:2717
           /\ 0 <= i':2715 /\ param0:27 <= i':2715)})



 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=11: 
Weight(Base relation: 
  {__cost := __cost':2829
   return := 0
   param0 := phi_tmp___0:2809
   return@pos := type_err:2834
   param0@pos := type_err:2810
   return@width := type_err:2835
   param0@width := type_err:2811
   when (((0 <= tr:2457 /\ tr:2458 <= 0 /\ 0 = phi_tmp___0:2809
             /\ param0:27 = phi_param0:2808
             /\ param0@pos:26 = phi_param0@pos:2807
             /\ param0@width:25 = phi_param0@width:2806)
            \/ ((tr:2459 < 0 \/ 0 < tr:2460) /\ havoc:2805 = phi_tmp___0:2809
                  /\ tr:2461 = phi_param0:2808
                  /\ type_err:2462 = phi_param0@pos:2807
                  /\ type_err:2463 = phi_param0@width:2806))
           /\ (!((0 <= K:2812 /\ K:2812 <= 0)) \/ mid_j:2813 = j:2814)
           /\ (!(1 <= K:2812) \/ mid_j:2813 = phi_tmp___0:2809)
           /\ (!(0 <= K:2812) \/ mid_i:2815 = K:2812)
           /\ (!(0 <= K:2812)
                 \/ mid___cost:2816 = (((phi_tmp___0:2809 * phi_tmp___0:2809)
                                          * (phi_tmp___0:2809
                                               * phi_tmp___0:2809)) * K:2812))
           /\ (!((0 <= K:2812 /\ K:2812 <= 0)) \/ mid_m:2817 = m:2818)
           /\ (!(1 <= K:2812) \/ mid_m:2817 = phi_tmp___0:2809)
           /\ (!((0 <= K:2812 /\ K:2812 <= 0)) \/ mid_l:2819 = l:2820)
           /\ (!(1 <= K:2812) \/ mid_l:2819 = phi_tmp___0:2809)
           /\ (!((0 <= K:2812 /\ K:2812 <= 0)) \/ mid_k:2821 = k:2822)
           /\ (!(1 <= K:2812) \/ mid_k:2821 = phi_tmp___0:2809)
           /\ (!(0 <= K:2812)
                 \/ -mid___cost:2816 <= ((1/2 * K:2812)
                                           + (-5/2 * phi_tmp___0:2809
                                                * K:2812)
                                           + (9/2
                                                * (phi_tmp___0:2809
                                                     * phi_tmp___0:2809)
                                                * K:2812)
                                           + (-7/2
                                                * ((phi_tmp___0:2809
                                                      * phi_tmp___0:2809)
                                                     * phi_tmp___0:2809)
                                                * K:2812)
                                           + (1/2 * (K:2812 * K:2812))
                                           + (-3/2 * phi_tmp___0:2809
                                                * (K:2812 * K:2812))
                                           + (3/2
                                                * (phi_tmp___0:2809
                                                     * phi_tmp___0:2809)
                                                * (K:2812 * K:2812))
                                           + (-1/2
                                                * ((phi_tmp___0:2809
                                                      * phi_tmp___0:2809)
                                                     * phi_tmp___0:2809)
                                                * (K:2812 * K:2812))))
           /\ (!(0 <= K:2812)
                 \/ -mid___cost:2816 <= ((-1/2
                                            * ((phi_tmp___0:2809
                                                  * phi_tmp___0:2809)
                                                 * phi_tmp___0:2809) * K:2812)
                                           + (-1/2
                                                * ((phi_tmp___0:2809
                                                      * phi_tmp___0:2809)
                                                     * phi_tmp___0:2809)
                                                * (K:2812 * K:2812))))
           /\ ((K:2812 = 0 /\ m:2818 = mid_m:2817 /\ l:2820 = mid_l:2819
                  /\ k:2822 = mid_k:2821 /\ j:2814 = mid_j:2813
                  /\ 0 = mid_i:2815 /\ 0 = mid___cost:2816)
                 \/ (1 <= K:2812 /\ 0 <= (-1 + phi_tmp___0:2809)
                       /\ 0 <= (-1 + (3 * phi_tmp___0:2809)
                                  + (-3
                                       * (phi_tmp___0:2809 * phi_tmp___0:2809))
                                  + ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                       * phi_tmp___0:2809))
                       /\ 0 <= (1 + (-2 * phi_tmp___0:2809)
                                  + (phi_tmp___0:2809 * phi_tmp___0:2809))
                       /\ 0 <= (-phi_tmp___0:2809
                                  + (phi_tmp___0:2809 * phi_tmp___0:2809))
                       /\ 0 <= (-((phi_tmp___0:2809 * phi_tmp___0:2809))
                                  + ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                       * phi_tmp___0:2809))
                       /\ 0 <= (-(((phi_tmp___0:2809 * phi_tmp___0:2809)
                                     * phi_tmp___0:2809))
                                  + (((phi_tmp___0:2809 * phi_tmp___0:2809)
                                        * phi_tmp___0:2809)
                                       * phi_tmp___0:2809))
                       /\ 0 <= (1 + (-4 * phi_tmp___0:2809)
                                  + (6
                                       * (phi_tmp___0:2809 * phi_tmp___0:2809))
                                  + (-4
                                       * ((phi_tmp___0:2809
                                             * phi_tmp___0:2809)
                                            * phi_tmp___0:2809))
                                  + (((phi_tmp___0:2809 * phi_tmp___0:2809)
                                        * phi_tmp___0:2809)
                                       * phi_tmp___0:2809))
                       /\ (-phi_tmp___0:2809 + mid_m:2817) = 0
                       /\ (-phi_tmp___0:2809 + mid_l:2819) = 0
                       /\ (-phi_tmp___0:2809 + mid_k:2821) = 0
                       /\ (-phi_tmp___0:2809 + mid_j:2813) = 0
                       /\ 0 <= ((-4 * phi_tmp___0:2809)
                                  + (6
                                       * (phi_tmp___0:2809 * phi_tmp___0:2809))
                                  + (-4
                                       * ((phi_tmp___0:2809
                                             * phi_tmp___0:2809)
                                            * phi_tmp___0:2809)) + mid_i:2815
                                  + (3
                                       * ((phi_tmp___0:2809
                                             * phi_tmp___0:2809)
                                            * (-1 + mid_i:2815)))
                                  + (((phi_tmp___0:2809 * phi_tmp___0:2809)
                                        * phi_tmp___0:2809)
                                       * phi_tmp___0:2809)
                                  + -((((phi_tmp___0:2809 * phi_tmp___0:2809)
                                          * phi_tmp___0:2809)
                                         * (-1 + mid_i:2815)))
                                  + (-3
                                       * (phi_tmp___0:2809
                                            * (-1 + mid_i:2815))))
                       /\ 0 <= (1 + (-2 * phi_tmp___0:2809)
                                  + (phi_tmp___0:2809 * phi_tmp___0:2809))
                       /\ 0 <= (-phi_tmp___0:2809
                                  + (phi_tmp___0:2809 * phi_tmp___0:2809)
                                  + -((phi_tmp___0:2809 * (-1 + mid_i:2815))))
                       /\ 0 <= (-((phi_tmp___0:2809 * phi_tmp___0:2809))
                                  + ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                       * phi_tmp___0:2809)
                                  + -(((phi_tmp___0:2809 * phi_tmp___0:2809)
                                         * (-1 + mid_i:2815))))
                       /\ 0 <= (-(((phi_tmp___0:2809 * phi_tmp___0:2809)
                                     * phi_tmp___0:2809))
                                  + (((phi_tmp___0:2809 * phi_tmp___0:2809)
                                        * phi_tmp___0:2809)
                                       * phi_tmp___0:2809)
                                  + -((((phi_tmp___0:2809 * phi_tmp___0:2809)
                                          * phi_tmp___0:2809)
                                         * (-1 + mid_i:2815))))
                       /\ 0 <= (1 + -mid_i:2815
                                  + (-3
                                       * ((phi_tmp___0:2809
                                             * phi_tmp___0:2809)
                                            * (-1 + mid_i:2815)))
                                  + (((phi_tmp___0:2809 * phi_tmp___0:2809)
                                        * phi_tmp___0:2809)
                                       * (-1 + mid_i:2815))
                                  + (3
                                       * (phi_tmp___0:2809
                                            * (-1 + mid_i:2815))))
                       /\ 0 <= (1 + -mid_i:2815
                                  + (phi_tmp___0:2809 * (-1 + mid_i:2815)))
                       /\ 0 <= (-((((phi_tmp___0:2809 * phi_tmp___0:2809)
                                      * phi_tmp___0:2809) * phi_tmp___0:2809))
                                  + mid___cost:2816)
                       /\ 0 <= (-1 + mid_i:2815)
                       /\ 0 <= (-1 + mid_i:2815
                                  + ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                       * (-1 + mid_i:2815))
                                  + (-2
                                       * (phi_tmp___0:2809
                                            * (-1 + mid_i:2815))))
                       /\ 0 <= (phi_tmp___0:2809 + -mid_i:2815)
                       /\ 0 <= ((3 * phi_tmp___0:2809)
                                  + (-3
                                       * (phi_tmp___0:2809 * phi_tmp___0:2809))
                                  + ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                       * phi_tmp___0:2809) + -mid_i:2815
                                  + -(((phi_tmp___0:2809 * phi_tmp___0:2809)
                                         * (-1 + mid_i:2815)))
                                  + (2
                                       * (phi_tmp___0:2809
                                            * (-1 + mid_i:2815))))))
           /\ K:2823 = 0 /\ mid_m:2817 = m':2824 /\ mid_l:2819 = l':2825
           /\ mid_k:2821 = k':2826 /\ mid_j:2813 = j':2827
           /\ mid_i:2815 = i':2828 /\ mid___cost:2816 = __cost':2829
           /\ 0 = K:2823 /\ (K:2812 + K:2823) = K:2830 /\ 0 <= K:2830
           /\ 0 <= i':2828 /\ phi_tmp___0:2809 <= i':2828)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
One()


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=21: 
Weight(Base relation: 
  {__cost := __cost':2716
   return := havoc:2718
   return@pos := type_err:2719
   return@width := type_err:2720
   when ((!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_j:2704 = j:2801)
           /\ (!(1 <= K:2703) \/ mid_j:2704 = param0:27)
           /\ (!(0 <= K:2703) \/ mid_i:2705 = K:2703)
           /\ (!(0 <= K:2703)
                 \/ mid___cost:2706 = (__cost:70
                                         + (((param0:27 * param0:27)
                                               * (param0:27 * param0:27))
                                              * K:2703)))
           /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_m:2707 = m:2802)
           /\ (!(1 <= K:2703) \/ mid_m:2707 = param0:27)
           /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_l:2708 = l:2803)
           /\ (!(1 <= K:2703) \/ mid_l:2708 = param0:27)
           /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_k:2709 = k:2804)
           /\ (!(1 <= K:2703) \/ mid_k:2709 = param0:27)
           /\ (!(0 <= K:2703)
                 \/ -mid___cost:2706 <= (-__cost:70 + (1/2 * K:2703)
                                           + (-5/2 * param0:27 * K:2703)
                                           + (9/2 * (param0:27 * param0:27)
                                                * K:2703)
                                           + (-7/2
                                                * ((param0:27 * param0:27)
                                                     * param0:27) * K:2703)
                                           + (1/2 * (K:2703 * K:2703))
                                           + (-3/2 * param0:27
                                                * (K:2703 * K:2703))
                                           + (3/2 * (param0:27 * param0:27)
                                                * (K:2703 * K:2703))
                                           + (-1/2
                                                * ((param0:27 * param0:27)
                                                     * param0:27)
                                                * (K:2703 * K:2703))))
           /\ (!(0 <= K:2703)
                 \/ -mid___cost:2706 <= (-__cost:70
                                           + (-1/2
                                                * ((param0:27 * param0:27)
                                                     * param0:27) * K:2703)
                                           + (-1/2
                                                * ((param0:27 * param0:27)
                                                     * param0:27)
                                                * (K:2703 * K:2703))))
           /\ ((K:2703 = 0 /\ m:2802 = mid_m:2707 /\ l:2803 = mid_l:2708
                  /\ k:2804 = mid_k:2709 /\ j:2801 = mid_j:2704
                  /\ 0 = mid_i:2705 /\ __cost:70 = mid___cost:2706)
                 \/ (1 <= K:2703 /\ 0 <= (-1 + param0:27)
                       /\ 0 <= (-1 + (3 * param0:27)
                                  + (-3 * (param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27))
                       /\ 0 <= (1 + (-2 * param0:27)
                                  + (param0:27 * param0:27))
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27))
                       /\ 0 <= (-((param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27))
                       /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * param0:27)) /\ 0 <= __cost:70
                       /\ 0 <= (1 + (-4 * param0:27)
                                  + (6 * (param0:27 * param0:27))
                                  + (-4
                                       * ((param0:27 * param0:27) * param0:27))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * param0:27))
                       /\ (-param0:27 + mid_m:2707) = 0
                       /\ (-param0:27 + mid_l:2708) = 0
                       /\ (-param0:27 + mid_k:2709) = 0
                       /\ (-param0:27 + mid_j:2704) = 0
                       /\ 0 <= ((-4 * param0:27)
                                  + (6 * (param0:27 * param0:27))
                                  + (-4
                                       * ((param0:27 * param0:27) * param0:27))
                                  + mid_i:2705
                                  + (3
                                       * ((param0:27 * param0:27)
                                            * (-1 + mid_i:2705)))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * param0:27)
                                  + -((((param0:27 * param0:27) * param0:27)
                                         * (-1 + mid_i:2705)))
                                  + (-3 * (param0:27 * (-1 + mid_i:2705))))
                       /\ 0 <= (1 + (-2 * param0:27)
                                  + (param0:27 * param0:27))
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                  + -((param0:27 * (-1 + mid_i:2705))))
                       /\ 0 <= (-((param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27)
                                  + -(((param0:27 * param0:27)
                                         * (-1 + mid_i:2705))))
                       /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * param0:27)
                                  + -((((param0:27 * param0:27) * param0:27)
                                         * (-1 + mid_i:2705))))
                       /\ 0 <= (1 + -mid_i:2705
                                  + (-3
                                       * ((param0:27 * param0:27)
                                            * (-1 + mid_i:2705)))
                                  + (((param0:27 * param0:27) * param0:27)
                                       * (-1 + mid_i:2705))
                                  + (3 * (param0:27 * (-1 + mid_i:2705))))
                       /\ 0 <= (1 + -mid_i:2705
                                  + (param0:27 * (-1 + mid_i:2705)))
                       /\ 0 <= (-((((param0:27 * param0:27) * param0:27)
                                     * param0:27)) + mid___cost:2706)
                       /\ 0 <= (-1 + mid_i:2705)
                       /\ 0 <= (-1 + mid_i:2705
                                  + ((param0:27 * param0:27)
                                       * (-1 + mid_i:2705))
                                  + (-2 * (param0:27 * (-1 + mid_i:2705))))
                       /\ 0 <= (param0:27 + -mid_i:2705)
                       /\ 0 <= ((3 * param0:27)
                                  + (-3 * (param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27)
                                  + -mid_i:2705
                                  + -(((param0:27 * param0:27)
                                         * (-1 + mid_i:2705)))
                                  + (2 * (param0:27 * (-1 + mid_i:2705))))))
           /\ K:2710 = 0 /\ mid_m:2707 = m':2711 /\ mid_l:2708 = l':2712
           /\ mid_k:2709 = k':2713 /\ mid_j:2704 = j':2714
           /\ mid_i:2705 = i':2715 /\ mid___cost:2706 = __cost':2716
           /\ 0 = K:2710 /\ (K:2703 + K:2710) = K:2717 /\ 0 <= K:2717
           /\ 0 <= i':2715 /\ param0:27 <= i':2715)})


Step 5: =========================================================
[Newton] Running Newton
-------------------------------------------------------------------------------
Round 0:
Evaluating variable number 11 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':2829
 return := 0
 param0 := phi_tmp___0:2809
 return@pos := type_err:2834
 param0@pos := type_err:2810
 return@width := type_err:2835
 param0@width := type_err:2811
 when (((0 <= tr:2457 /\ tr:2458 <= 0 /\ 0 = phi_tmp___0:2809
           /\ param0:27 = phi_param0:2808
           /\ param0@pos:26 = phi_param0@pos:2807
           /\ param0@width:25 = phi_param0@width:2806)
          \/ ((tr:2459 < 0 \/ 0 < tr:2460) /\ havoc:2805 = phi_tmp___0:2809
                /\ tr:2461 = phi_param0:2808
                /\ type_err:2462 = phi_param0@pos:2807
                /\ type_err:2463 = phi_param0@width:2806))
         /\ (!((0 <= K:2812 /\ K:2812 <= 0)) \/ mid_j:2813 = j:2814)
         /\ (!(1 <= K:2812) \/ mid_j:2813 = phi_tmp___0:2809)
         /\ (!(0 <= K:2812) \/ mid_i:2815 = K:2812)
         /\ (!(0 <= K:2812)
               \/ mid___cost:2816 = (((phi_tmp___0:2809 * phi_tmp___0:2809)
                                        * (phi_tmp___0:2809
                                             * phi_tmp___0:2809)) * K:2812))
         /\ (!((0 <= K:2812 /\ K:2812 <= 0)) \/ mid_m:2817 = m:2818)
         /\ (!(1 <= K:2812) \/ mid_m:2817 = phi_tmp___0:2809)
         /\ (!((0 <= K:2812 /\ K:2812 <= 0)) \/ mid_l:2819 = l:2820)
         /\ (!(1 <= K:2812) \/ mid_l:2819 = phi_tmp___0:2809)
         /\ (!((0 <= K:2812 /\ K:2812 <= 0)) \/ mid_k:2821 = k:2822)
         /\ (!(1 <= K:2812) \/ mid_k:2821 = phi_tmp___0:2809)
         /\ (!(0 <= K:2812)
               \/ -mid___cost:2816 <= ((1/2 * K:2812)
                                         + (-5/2 * phi_tmp___0:2809 * K:2812)
                                         + (9/2
                                              * (phi_tmp___0:2809
                                                   * phi_tmp___0:2809)
                                              * K:2812)
                                         + (-7/2
                                              * ((phi_tmp___0:2809
                                                    * phi_tmp___0:2809)
                                                   * phi_tmp___0:2809)
                                              * K:2812)
                                         + (1/2 * (K:2812 * K:2812))
                                         + (-3/2 * phi_tmp___0:2809
                                              * (K:2812 * K:2812))
                                         + (3/2
                                              * (phi_tmp___0:2809
                                                   * phi_tmp___0:2809)
                                              * (K:2812 * K:2812))
                                         + (-1/2
                                              * ((phi_tmp___0:2809
                                                    * phi_tmp___0:2809)
                                                   * phi_tmp___0:2809)
                                              * (K:2812 * K:2812))))
         /\ (!(0 <= K:2812)
               \/ -mid___cost:2816 <= ((-1/2
                                          * ((phi_tmp___0:2809
                                                * phi_tmp___0:2809)
                                               * phi_tmp___0:2809) * K:2812)
                                         + (-1/2
                                              * ((phi_tmp___0:2809
                                                    * phi_tmp___0:2809)
                                                   * phi_tmp___0:2809)
                                              * (K:2812 * K:2812))))
         /\ ((K:2812 = 0 /\ m:2818 = mid_m:2817 /\ l:2820 = mid_l:2819
                /\ k:2822 = mid_k:2821 /\ j:2814 = mid_j:2813
                /\ 0 = mid_i:2815 /\ 0 = mid___cost:2816)
               \/ (1 <= K:2812 /\ 0 <= (-1 + phi_tmp___0:2809)
                     /\ 0 <= (-1 + (3 * phi_tmp___0:2809)
                                + (-3 * (phi_tmp___0:2809 * phi_tmp___0:2809))
                                + ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                     * phi_tmp___0:2809))
                     /\ 0 <= (1 + (-2 * phi_tmp___0:2809)
                                + (phi_tmp___0:2809 * phi_tmp___0:2809))
                     /\ 0 <= (-phi_tmp___0:2809
                                + (phi_tmp___0:2809 * phi_tmp___0:2809))
                     /\ 0 <= (-((phi_tmp___0:2809 * phi_tmp___0:2809))
                                + ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                     * phi_tmp___0:2809))
                     /\ 0 <= (-(((phi_tmp___0:2809 * phi_tmp___0:2809)
                                   * phi_tmp___0:2809))
                                + (((phi_tmp___0:2809 * phi_tmp___0:2809)
                                      * phi_tmp___0:2809) * phi_tmp___0:2809))
                     /\ 0 <= (1 + (-4 * phi_tmp___0:2809)
                                + (6 * (phi_tmp___0:2809 * phi_tmp___0:2809))
                                + (-4
                                     * ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                          * phi_tmp___0:2809))
                                + (((phi_tmp___0:2809 * phi_tmp___0:2809)
                                      * phi_tmp___0:2809) * phi_tmp___0:2809))
                     /\ (-phi_tmp___0:2809 + mid_m:2817) = 0
                     /\ (-phi_tmp___0:2809 + mid_l:2819) = 0
                     /\ (-phi_tmp___0:2809 + mid_k:2821) = 0
                     /\ (-phi_tmp___0:2809 + mid_j:2813) = 0
                     /\ 0 <= ((-4 * phi_tmp___0:2809)
                                + (6 * (phi_tmp___0:2809 * phi_tmp___0:2809))
                                + (-4
                                     * ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                          * phi_tmp___0:2809)) + mid_i:2815
                                + (3
                                     * ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                          * (-1 + mid_i:2815)))
                                + (((phi_tmp___0:2809 * phi_tmp___0:2809)
                                      * phi_tmp___0:2809) * phi_tmp___0:2809)
                                + -((((phi_tmp___0:2809 * phi_tmp___0:2809)
                                        * phi_tmp___0:2809)
                                       * (-1 + mid_i:2815)))
                                + (-3
                                     * (phi_tmp___0:2809 * (-1 + mid_i:2815))))
                     /\ 0 <= (1 + (-2 * phi_tmp___0:2809)
                                + (phi_tmp___0:2809 * phi_tmp___0:2809))
                     /\ 0 <= (-phi_tmp___0:2809
                                + (phi_tmp___0:2809 * phi_tmp___0:2809)
                                + -((phi_tmp___0:2809 * (-1 + mid_i:2815))))
                     /\ 0 <= (-((phi_tmp___0:2809 * phi_tmp___0:2809))
                                + ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                     * phi_tmp___0:2809)
                                + -(((phi_tmp___0:2809 * phi_tmp___0:2809)
                                       * (-1 + mid_i:2815))))
                     /\ 0 <= (-(((phi_tmp___0:2809 * phi_tmp___0:2809)
                                   * phi_tmp___0:2809))
                                + (((phi_tmp___0:2809 * phi_tmp___0:2809)
                                      * phi_tmp___0:2809) * phi_tmp___0:2809)
                                + -((((phi_tmp___0:2809 * phi_tmp___0:2809)
                                        * phi_tmp___0:2809)
                                       * (-1 + mid_i:2815))))
                     /\ 0 <= (1 + -mid_i:2815
                                + (-3
                                     * ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                          * (-1 + mid_i:2815)))
                                + (((phi_tmp___0:2809 * phi_tmp___0:2809)
                                      * phi_tmp___0:2809) * (-1 + mid_i:2815))
                                + (3 * (phi_tmp___0:2809 * (-1 + mid_i:2815))))
                     /\ 0 <= (1 + -mid_i:2815
                                + (phi_tmp___0:2809 * (-1 + mid_i:2815)))
                     /\ 0 <= (-((((phi_tmp___0:2809 * phi_tmp___0:2809)
                                    * phi_tmp___0:2809) * phi_tmp___0:2809))
                                + mid___cost:2816) /\ 0 <= (-1 + mid_i:2815)
                     /\ 0 <= (-1 + mid_i:2815
                                + ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                     * (-1 + mid_i:2815))
                                + (-2
                                     * (phi_tmp___0:2809 * (-1 + mid_i:2815))))
                     /\ 0 <= (phi_tmp___0:2809 + -mid_i:2815)
                     /\ 0 <= ((3 * phi_tmp___0:2809)
                                + (-3 * (phi_tmp___0:2809 * phi_tmp___0:2809))
                                + ((phi_tmp___0:2809 * phi_tmp___0:2809)
                                     * phi_tmp___0:2809) + -mid_i:2815
                                + -(((phi_tmp___0:2809 * phi_tmp___0:2809)
                                       * (-1 + mid_i:2815)))
                                + (2 * (phi_tmp___0:2809 * (-1 + mid_i:2815))))))
         /\ K:2823 = 0 /\ mid_m:2817 = m':2824 /\ mid_l:2819 = l':2825
         /\ mid_k:2821 = k':2826 /\ mid_j:2813 = j':2827
         /\ mid_i:2815 = i':2828 /\ mid___cost:2816 = __cost':2829
         /\ 0 = K:2823 /\ (K:2812 + K:2823) = K:2830 /\ 0 <= K:2830
         /\ 0 <= i':2828 /\ phi_tmp___0:2809 <= i':2828)}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

Evaluating variable number 21 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':2716
 return := havoc:2718
 return@pos := type_err:2719
 return@width := type_err:2720
 when ((!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_j:2704 = j:2801)
         /\ (!(1 <= K:2703) \/ mid_j:2704 = param0:27)
         /\ (!(0 <= K:2703) \/ mid_i:2705 = K:2703)
         /\ (!(0 <= K:2703)
               \/ mid___cost:2706 = (__cost:70
                                       + (((param0:27 * param0:27)
                                             * (param0:27 * param0:27))
                                            * K:2703)))
         /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_m:2707 = m:2802)
         /\ (!(1 <= K:2703) \/ mid_m:2707 = param0:27)
         /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_l:2708 = l:2803)
         /\ (!(1 <= K:2703) \/ mid_l:2708 = param0:27)
         /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_k:2709 = k:2804)
         /\ (!(1 <= K:2703) \/ mid_k:2709 = param0:27)
         /\ (!(0 <= K:2703)
               \/ -mid___cost:2706 <= (-__cost:70 + (1/2 * K:2703)
                                         + (-5/2 * param0:27 * K:2703)
                                         + (9/2 * (param0:27 * param0:27)
                                              * K:2703)
                                         + (-7/2
                                              * ((param0:27 * param0:27)
                                                   * param0:27) * K:2703)
                                         + (1/2 * (K:2703 * K:2703))
                                         + (-3/2 * param0:27
                                              * (K:2703 * K:2703))
                                         + (3/2 * (param0:27 * param0:27)
                                              * (K:2703 * K:2703))
                                         + (-1/2
                                              * ((param0:27 * param0:27)
                                                   * param0:27)
                                              * (K:2703 * K:2703))))
         /\ (!(0 <= K:2703)
               \/ -mid___cost:2706 <= (-__cost:70
                                         + (-1/2
                                              * ((param0:27 * param0:27)
                                                   * param0:27) * K:2703)
                                         + (-1/2
                                              * ((param0:27 * param0:27)
                                                   * param0:27)
                                              * (K:2703 * K:2703))))
         /\ ((K:2703 = 0 /\ m:2802 = mid_m:2707 /\ l:2803 = mid_l:2708
                /\ k:2804 = mid_k:2709 /\ j:2801 = mid_j:2704
                /\ 0 = mid_i:2705 /\ __cost:70 = mid___cost:2706)
               \/ (1 <= K:2703 /\ 0 <= (-1 + param0:27)
                     /\ 0 <= (-1 + (3 * param0:27)
                                + (-3 * (param0:27 * param0:27))
                                + ((param0:27 * param0:27) * param0:27))
                     /\ 0 <= (1 + (-2 * param0:27) + (param0:27 * param0:27))
                     /\ 0 <= (-param0:27 + (param0:27 * param0:27))
                     /\ 0 <= (-((param0:27 * param0:27))
                                + ((param0:27 * param0:27) * param0:27))
                     /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                + (((param0:27 * param0:27) * param0:27)
                                     * param0:27)) /\ 0 <= __cost:70
                     /\ 0 <= (1 + (-4 * param0:27)
                                + (6 * (param0:27 * param0:27))
                                + (-4 * ((param0:27 * param0:27) * param0:27))
                                + (((param0:27 * param0:27) * param0:27)
                                     * param0:27))
                     /\ (-param0:27 + mid_m:2707) = 0
                     /\ (-param0:27 + mid_l:2708) = 0
                     /\ (-param0:27 + mid_k:2709) = 0
                     /\ (-param0:27 + mid_j:2704) = 0
                     /\ 0 <= ((-4 * param0:27)
                                + (6 * (param0:27 * param0:27))
                                + (-4 * ((param0:27 * param0:27) * param0:27))
                                + mid_i:2705
                                + (3
                                     * ((param0:27 * param0:27)
                                          * (-1 + mid_i:2705)))
                                + (((param0:27 * param0:27) * param0:27)
                                     * param0:27)
                                + -((((param0:27 * param0:27) * param0:27)
                                       * (-1 + mid_i:2705)))
                                + (-3 * (param0:27 * (-1 + mid_i:2705))))
                     /\ 0 <= (1 + (-2 * param0:27) + (param0:27 * param0:27))
                     /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                + -((param0:27 * (-1 + mid_i:2705))))
                     /\ 0 <= (-((param0:27 * param0:27))
                                + ((param0:27 * param0:27) * param0:27)
                                + -(((param0:27 * param0:27)
                                       * (-1 + mid_i:2705))))
                     /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                + (((param0:27 * param0:27) * param0:27)
                                     * param0:27)
                                + -((((param0:27 * param0:27) * param0:27)
                                       * (-1 + mid_i:2705))))
                     /\ 0 <= (1 + -mid_i:2705
                                + (-3
                                     * ((param0:27 * param0:27)
                                          * (-1 + mid_i:2705)))
                                + (((param0:27 * param0:27) * param0:27)
                                     * (-1 + mid_i:2705))
                                + (3 * (param0:27 * (-1 + mid_i:2705))))
                     /\ 0 <= (1 + -mid_i:2705
                                + (param0:27 * (-1 + mid_i:2705)))
                     /\ 0 <= (-((((param0:27 * param0:27) * param0:27)
                                   * param0:27)) + mid___cost:2706)
                     /\ 0 <= (-1 + mid_i:2705)
                     /\ 0 <= (-1 + mid_i:2705
                                + ((param0:27 * param0:27)
                                     * (-1 + mid_i:2705))
                                + (-2 * (param0:27 * (-1 + mid_i:2705))))
                     /\ 0 <= (param0:27 + -mid_i:2705)
                     /\ 0 <= ((3 * param0:27)
                                + (-3 * (param0:27 * param0:27))
                                + ((param0:27 * param0:27) * param0:27)
                                + -mid_i:2705
                                + -(((param0:27 * param0:27)
                                       * (-1 + mid_i:2705)))
                                + (2 * (param0:27 * (-1 + mid_i:2705))))))
         /\ K:2710 = 0 /\ mid_m:2707 = m':2711 /\ mid_l:2708 = l':2712
         /\ mid_k:2709 = k':2713 /\ mid_j:2704 = j':2714
         /\ mid_i:2705 = i':2715 /\ mid___cost:2706 = __cost':2716
         /\ 0 = K:2710 /\ (K:2703 + K:2710) = K:2717 /\ 0 <= K:2717
         /\ 0 <= i':2715 /\ param0:27 <= i':2715)}

    (IRE-tc) Checking termination condition.
    (IRE-tc)     >> All star bodies equivalent.

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, accept> -> <__pstate, (Unique State Name,101)_g1>	Base relation: 
{__cost := 0
 argv := param1:30
 param0 := tr:2461
 argv@pos := param1@pos:29
 param0@pos := type_err:2462
 argv@width := param1@width:28
 param0@width := type_err:2463
 when (tr:2459 < 0 \/ 0 < tr:2460)}	
<__pstate, accept> -> <__pstate, (Unique State Name,89)_g1>	Base relation: 
{__cost := 0
 tmp___0 := phi_tmp___0:2840
 argv := param1:30
 param0 := phi_tmp___0:2840
 argv@pos := param1@pos:29
 param0@pos := type_err:2841
 argv@width := param1@width:28
 param0@width := type_err:2842
 when ((0 <= tr:2457 /\ tr:2458 <= 0 /\ 0 = phi_tmp___0:2840
          /\ param0:27 = phi_param0:2839
          /\ param0@pos:26 = phi_param0@pos:2838
          /\ param0@width:25 = phi_param0@width:2837)
         \/ ((tr:2459 < 0 \/ 0 < tr:2460) /\ havoc:2836 = phi_tmp___0:2840
               /\ tr:2461 = phi_param0:2839
               /\ type_err:2462 = phi_param0@pos:2838
               /\ type_err:2463 = phi_param0@width:2837))}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x3163faa0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x3127f4e0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
##### ANS
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}
    ( __pstate , (Unique State Name,101)_g1 , __done )	Base relation: 
{__cost := 0
 argv := param1:30
 param0 := tr:2461
 argv@pos := param1@pos:29
 param0@pos := type_err:2462
 argv@width := param1@width:28
 param0@width := type_err:2463
 when (tr:2459 < 0 \/ 0 < tr:2460)}
    ( __pstate , (Unique State Name,89)_g1 , __done )	Base relation: 
{__cost := 0
 tmp___0 := phi_tmp___0:2840
 argv := param1:30
 param0 := phi_tmp___0:2840
 argv@pos := param1@pos:29
 param0@pos := type_err:2841
 argv@width := param1@width:28
 param0@width := type_err:2842
 when ((0 <= tr:2457 /\ tr:2458 <= 0 /\ 0 = phi_tmp___0:2840
          /\ param0:27 = phi_param0:2839
          /\ param0@pos:26 = phi_param0@pos:2838
          /\ param0@width:25 = phi_param0@width:2837)
         \/ ((tr:2459 < 0 \/ 0 < tr:2460) /\ havoc:2836 = phi_tmp___0:2840
               /\ tr:2461 = phi_param0:2839
               /\ type_err:2462 = phi_param0@pos:2838
               /\ type_err:2463 = phi_param0@width:2837))}

Weights on states: 
__pstate 0x31441ed0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x31445050: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
================================================
Procedure Summaries

------------------------------------------------
Procedure summary for atoi

Base relation: 
{}

------------------------------------------------
Procedure summary for main

Base relation: 
{__cost := __cost':2860
 tmp___0 := phi_tmp___0:2840
 argv := param1:30
 return := 0
 param0 := phi_tmp___0:2840
 argv@pos := param1@pos:29
 return@pos := type_err:2865
 param0@pos := type_err:2841
 argv@width := param1@width:28
 return@width := type_err:2866
 param0@width := type_err:2842
 when (((0 <= tr:2457 /\ tr:2458 <= 0 /\ 0 = phi_tmp___0:2840
           /\ param0:27 = phi_param0:2839
           /\ param0@pos:26 = phi_param0@pos:2838
           /\ param0@width:25 = phi_param0@width:2837)
          \/ ((tr:2459 < 0 \/ 0 < tr:2460) /\ havoc:2836 = phi_tmp___0:2840
                /\ tr:2461 = phi_param0:2839
                /\ type_err:2462 = phi_param0@pos:2838
                /\ type_err:2463 = phi_param0@width:2837))
         /\ (!((0 <= K:2843 /\ K:2843 <= 0)) \/ mid_j:2844 = j:2845)
         /\ (!(1 <= K:2843) \/ mid_j:2844 = phi_tmp___0:2840)
         /\ (!(0 <= K:2843) \/ mid_i:2846 = K:2843)
         /\ (!(0 <= K:2843)
               \/ mid___cost:2847 = (((phi_tmp___0:2840 * phi_tmp___0:2840)
                                        * (phi_tmp___0:2840
                                             * phi_tmp___0:2840)) * K:2843))
         /\ (!((0 <= K:2843 /\ K:2843 <= 0)) \/ mid_m:2848 = m:2849)
         /\ (!(1 <= K:2843) \/ mid_m:2848 = phi_tmp___0:2840)
         /\ (!((0 <= K:2843 /\ K:2843 <= 0)) \/ mid_l:2850 = l:2851)
         /\ (!(1 <= K:2843) \/ mid_l:2850 = phi_tmp___0:2840)
         /\ (!((0 <= K:2843 /\ K:2843 <= 0)) \/ mid_k:2852 = k:2853)
         /\ (!(1 <= K:2843) \/ mid_k:2852 = phi_tmp___0:2840)
         /\ (!(0 <= K:2843)
               \/ -mid___cost:2847 <= ((1/2 * K:2843)
                                         + (-5/2 * phi_tmp___0:2840 * K:2843)
                                         + (9/2
                                              * (phi_tmp___0:2840
                                                   * phi_tmp___0:2840)
                                              * K:2843)
                                         + (-7/2
                                              * ((phi_tmp___0:2840
                                                    * phi_tmp___0:2840)
                                                   * phi_tmp___0:2840)
                                              * K:2843)
                                         + (1/2 * (K:2843 * K:2843))
                                         + (-3/2 * phi_tmp___0:2840
                                              * (K:2843 * K:2843))
                                         + (3/2
                                              * (phi_tmp___0:2840
                                                   * phi_tmp___0:2840)
                                              * (K:2843 * K:2843))
                                         + (-1/2
                                              * ((phi_tmp___0:2840
                                                    * phi_tmp___0:2840)
                                                   * phi_tmp___0:2840)
                                              * (K:2843 * K:2843))))
         /\ (!(0 <= K:2843)
               \/ -mid___cost:2847 <= ((-1/2
                                          * ((phi_tmp___0:2840
                                                * phi_tmp___0:2840)
                                               * phi_tmp___0:2840) * K:2843)
                                         + (-1/2
                                              * ((phi_tmp___0:2840
                                                    * phi_tmp___0:2840)
                                                   * phi_tmp___0:2840)
                                              * (K:2843 * K:2843))))
         /\ ((K:2843 = 0 /\ m:2849 = mid_m:2848 /\ l:2851 = mid_l:2850
                /\ k:2853 = mid_k:2852 /\ j:2845 = mid_j:2844
                /\ 0 = mid_i:2846 /\ 0 = mid___cost:2847)
               \/ (1 <= K:2843 /\ 0 <= (-1 + phi_tmp___0:2840)
                     /\ 0 <= (-1 + (3 * phi_tmp___0:2840)
                                + (-3 * (phi_tmp___0:2840 * phi_tmp___0:2840))
                                + ((phi_tmp___0:2840 * phi_tmp___0:2840)
                                     * phi_tmp___0:2840))
                     /\ 0 <= (1 + (-2 * phi_tmp___0:2840)
                                + (phi_tmp___0:2840 * phi_tmp___0:2840))
                     /\ 0 <= (-phi_tmp___0:2840
                                + (phi_tmp___0:2840 * phi_tmp___0:2840))
                     /\ 0 <= (-((phi_tmp___0:2840 * phi_tmp___0:2840))
                                + ((phi_tmp___0:2840 * phi_tmp___0:2840)
                                     * phi_tmp___0:2840))
                     /\ 0 <= (-(((phi_tmp___0:2840 * phi_tmp___0:2840)
                                   * phi_tmp___0:2840))
                                + (((phi_tmp___0:2840 * phi_tmp___0:2840)
                                      * phi_tmp___0:2840) * phi_tmp___0:2840))
                     /\ 0 <= (1 + (-4 * phi_tmp___0:2840)
                                + (6 * (phi_tmp___0:2840 * phi_tmp___0:2840))
                                + (-4
                                     * ((phi_tmp___0:2840 * phi_tmp___0:2840)
                                          * phi_tmp___0:2840))
                                + (((phi_tmp___0:2840 * phi_tmp___0:2840)
                                      * phi_tmp___0:2840) * phi_tmp___0:2840))
                     /\ (-phi_tmp___0:2840 + mid_m:2848) = 0
                     /\ (-phi_tmp___0:2840 + mid_l:2850) = 0
                     /\ (-phi_tmp___0:2840 + mid_k:2852) = 0
                     /\ (-phi_tmp___0:2840 + mid_j:2844) = 0
                     /\ 0 <= ((-4 * phi_tmp___0:2840)
                                + (6 * (phi_tmp___0:2840 * phi_tmp___0:2840))
                                + (-4
                                     * ((phi_tmp___0:2840 * phi_tmp___0:2840)
                                          * phi_tmp___0:2840)) + mid_i:2846
                                + (3
                                     * ((phi_tmp___0:2840 * phi_tmp___0:2840)
                                          * (-1 + mid_i:2846)))
                                + (((phi_tmp___0:2840 * phi_tmp___0:2840)
                                      * phi_tmp___0:2840) * phi_tmp___0:2840)
                                + -((((phi_tmp___0:2840 * phi_tmp___0:2840)
                                        * phi_tmp___0:2840)
                                       * (-1 + mid_i:2846)))
                                + (-3
                                     * (phi_tmp___0:2840 * (-1 + mid_i:2846))))
                     /\ 0 <= (1 + (-2 * phi_tmp___0:2840)
                                + (phi_tmp___0:2840 * phi_tmp___0:2840))
                     /\ 0 <= (-phi_tmp___0:2840
                                + (phi_tmp___0:2840 * phi_tmp___0:2840)
                                + -((phi_tmp___0:2840 * (-1 + mid_i:2846))))
                     /\ 0 <= (-((phi_tmp___0:2840 * phi_tmp___0:2840))
                                + ((phi_tmp___0:2840 * phi_tmp___0:2840)
                                     * phi_tmp___0:2840)
                                + -(((phi_tmp___0:2840 * phi_tmp___0:2840)
                                       * (-1 + mid_i:2846))))
                     /\ 0 <= (-(((phi_tmp___0:2840 * phi_tmp___0:2840)
                                   * phi_tmp___0:2840))
                                + (((phi_tmp___0:2840 * phi_tmp___0:2840)
                                      * phi_tmp___0:2840) * phi_tmp___0:2840)
                                + -((((phi_tmp___0:2840 * phi_tmp___0:2840)
                                        * phi_tmp___0:2840)
                                       * (-1 + mid_i:2846))))
                     /\ 0 <= (1 + -mid_i:2846
                                + (-3
                                     * ((phi_tmp___0:2840 * phi_tmp___0:2840)
                                          * (-1 + mid_i:2846)))
                                + (((phi_tmp___0:2840 * phi_tmp___0:2840)
                                      * phi_tmp___0:2840) * (-1 + mid_i:2846))
                                + (3 * (phi_tmp___0:2840 * (-1 + mid_i:2846))))
                     /\ 0 <= (1 + -mid_i:2846
                                + (phi_tmp___0:2840 * (-1 + mid_i:2846)))
                     /\ 0 <= (-((((phi_tmp___0:2840 * phi_tmp___0:2840)
                                    * phi_tmp___0:2840) * phi_tmp___0:2840))
                                + mid___cost:2847) /\ 0 <= (-1 + mid_i:2846)
                     /\ 0 <= (-1 + mid_i:2846
                                + ((phi_tmp___0:2840 * phi_tmp___0:2840)
                                     * (-1 + mid_i:2846))
                                + (-2
                                     * (phi_tmp___0:2840 * (-1 + mid_i:2846))))
                     /\ 0 <= (phi_tmp___0:2840 + -mid_i:2846)
                     /\ 0 <= ((3 * phi_tmp___0:2840)
                                + (-3 * (phi_tmp___0:2840 * phi_tmp___0:2840))
                                + ((phi_tmp___0:2840 * phi_tmp___0:2840)
                                     * phi_tmp___0:2840) + -mid_i:2846
                                + -(((phi_tmp___0:2840 * phi_tmp___0:2840)
                                       * (-1 + mid_i:2846)))
                                + (2 * (phi_tmp___0:2840 * (-1 + mid_i:2846))))))
         /\ K:2854 = 0 /\ mid_m:2848 = m':2855 /\ mid_l:2850 = l':2856
         /\ mid_k:2852 = k':2857 /\ mid_j:2844 = j':2858
         /\ mid_i:2846 = i':2859 /\ mid___cost:2847 = __cost':2860
         /\ 0 = K:2854 /\ (K:2843 + K:2854) = K:2861 /\ 0 <= K:2861
         /\ 0 <= i':2859 /\ phi_tmp___0:2840 <= i':2859)}

------------------------------------------------
Procedure summary for work

Base relation: 
{__cost := __cost':2716
 i := i':2715
 j := j':2714
 k := k':2713
 l := l':2712
 m := m':2711
 n := param0:27
 return := havoc:2718
 return@pos := type_err:2719
 return@width := type_err:2720
 when ((!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_j:2704 = j:66)
         /\ (!(1 <= K:2703) \/ mid_j:2704 = param0:27)
         /\ (!(0 <= K:2703) \/ mid_i:2705 = K:2703)
         /\ (!(0 <= K:2703)
               \/ mid___cost:2706 = (__cost:70
                                       + (((param0:27 * param0:27)
                                             * (param0:27 * param0:27))
                                            * K:2703)))
         /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_m:2707 = m:69)
         /\ (!(1 <= K:2703) \/ mid_m:2707 = param0:27)
         /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_l:2708 = l:68)
         /\ (!(1 <= K:2703) \/ mid_l:2708 = param0:27)
         /\ (!((0 <= K:2703 /\ K:2703 <= 0)) \/ mid_k:2709 = k:67)
         /\ (!(1 <= K:2703) \/ mid_k:2709 = param0:27)
         /\ (!(0 <= K:2703)
               \/ -mid___cost:2706 <= (-__cost:70 + (1/2 * K:2703)
                                         + (-5/2 * param0:27 * K:2703)
                                         + (9/2 * (param0:27 * param0:27)
                                              * K:2703)
                                         + (-7/2
                                              * ((param0:27 * param0:27)
                                                   * param0:27) * K:2703)
                                         + (1/2 * (K:2703 * K:2703))
                                         + (-3/2 * param0:27
                                              * (K:2703 * K:2703))
                                         + (3/2 * (param0:27 * param0:27)
                                              * (K:2703 * K:2703))
                                         + (-1/2
                                              * ((param0:27 * param0:27)
                                                   * param0:27)
                                              * (K:2703 * K:2703))))
         /\ (!(0 <= K:2703)
               \/ -mid___cost:2706 <= (-__cost:70
                                         + (-1/2
                                              * ((param0:27 * param0:27)
                                                   * param0:27) * K:2703)
                                         + (-1/2
                                              * ((param0:27 * param0:27)
                                                   * param0:27)
                                              * (K:2703 * K:2703))))
         /\ ((K:2703 = 0 /\ m:69 = mid_m:2707 /\ l:68 = mid_l:2708
                /\ k:67 = mid_k:2709 /\ j:66 = mid_j:2704 /\ 0 = mid_i:2705
                /\ __cost:70 = mid___cost:2706)
               \/ (1 <= K:2703 /\ 0 <= (-1 + param0:27)
                     /\ 0 <= (-1 + (3 * param0:27)
                                + (-3 * (param0:27 * param0:27))
                                + ((param0:27 * param0:27) * param0:27))
                     /\ 0 <= (1 + (-2 * param0:27) + (param0:27 * param0:27))
                     /\ 0 <= (-param0:27 + (param0:27 * param0:27))
                     /\ 0 <= (-((param0:27 * param0:27))
                                + ((param0:27 * param0:27) * param0:27))
                     /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                + (((param0:27 * param0:27) * param0:27)
                                     * param0:27)) /\ 0 <= __cost:70
                     /\ 0 <= (1 + (-4 * param0:27)
                                + (6 * (param0:27 * param0:27))
                                + (-4 * ((param0:27 * param0:27) * param0:27))
                                + (((param0:27 * param0:27) * param0:27)
                                     * param0:27))
                     /\ (-param0:27 + mid_m:2707) = 0
                     /\ (-param0:27 + mid_l:2708) = 0
                     /\ (-param0:27 + mid_k:2709) = 0
                     /\ (-param0:27 + mid_j:2704) = 0
                     /\ 0 <= ((-4 * param0:27)
                                + (6 * (param0:27 * param0:27))
                                + (-4 * ((param0:27 * param0:27) * param0:27))
                                + mid_i:2705
                                + (3
                                     * ((param0:27 * param0:27)
                                          * (-1 + mid_i:2705)))
                                + (((param0:27 * param0:27) * param0:27)
                                     * param0:27)
                                + -((((param0:27 * param0:27) * param0:27)
                                       * (-1 + mid_i:2705)))
                                + (-3 * (param0:27 * (-1 + mid_i:2705))))
                     /\ 0 <= (1 + (-2 * param0:27) + (param0:27 * param0:27))
                     /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                + -((param0:27 * (-1 + mid_i:2705))))
                     /\ 0 <= (-((param0:27 * param0:27))
                                + ((param0:27 * param0:27) * param0:27)
                                + -(((param0:27 * param0:27)
                                       * (-1 + mid_i:2705))))
                     /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                + (((param0:27 * param0:27) * param0:27)
                                     * param0:27)
                                + -((((param0:27 * param0:27) * param0:27)
                                       * (-1 + mid_i:2705))))
                     /\ 0 <= (1 + -mid_i:2705
                                + (-3
                                     * ((param0:27 * param0:27)
                                          * (-1 + mid_i:2705)))
                                + (((param0:27 * param0:27) * param0:27)
                                     * (-1 + mid_i:2705))
                                + (3 * (param0:27 * (-1 + mid_i:2705))))
                     /\ 0 <= (1 + -mid_i:2705
                                + (param0:27 * (-1 + mid_i:2705)))
                     /\ 0 <= (-((((param0:27 * param0:27) * param0:27)
                                   * param0:27)) + mid___cost:2706)
                     /\ 0 <= (-1 + mid_i:2705)
                     /\ 0 <= (-1 + mid_i:2705
                                + ((param0:27 * param0:27)
                                     * (-1 + mid_i:2705))
                                + (-2 * (param0:27 * (-1 + mid_i:2705))))
                     /\ 0 <= (param0:27 + -mid_i:2705)
                     /\ 0 <= ((3 * param0:27)
                                + (-3 * (param0:27 * param0:27))
                                + ((param0:27 * param0:27) * param0:27)
                                + -mid_i:2705
                                + -(((param0:27 * param0:27)
                                       * (-1 + mid_i:2705)))
                                + (2 * (param0:27 * (-1 + mid_i:2705))))))
         /\ K:2710 = 0 /\ mid_m:2707 = m':2711 /\ mid_l:2708 = l':2712
         /\ mid_k:2709 = k':2713 /\ mid_j:2704 = j':2714
         /\ mid_i:2705 = i':2715 /\ mid___cost:2706 = __cost':2716
         /\ 0 = K:2710 /\ (K:2703 + K:2710) = K:2717 /\ 0 <= K:2717
         /\ 0 <= i':2715 /\ param0:27 <= i':2715)}

================================================
Assertion Checking at Error Points

================================================
Bounds on Variables

Variable bounds at line 15 in work

min(__cost, (((((n * n) * n) * n) * n) + __cost)) <= __cost
__cost is o(1)
__cost <= max(__cost, (((((n * n) * n) * n) * n) + __cost))
__cost is O(n^5)

================================================
Finished!