/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, 86> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 18> -> <Unique State Name, 92>	Base relation: 
{when 0 <= i:64}	
<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, 83>	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, 49> -> <Unique State Name, 36>	Base relation: 
{k := (k:67 + 1)
 when n:65 <= l:68}	
<Unique State Name, 49> -> <Unique State Name, 45>	Base relation: 
{__cost := (__cost:69 + 1)
 l := (l:68 + 1)
 when (l:68 < n:65 /\ 0 <= __cost:69 /\ 0 <= (__cost:69 + 1))}	
<Unique State Name, 84> -> <Unique State Name, 8>	Base relation: 
{__cost := 0
 argv := param1:30
 argv@pos := param1@pos:29
 argv@width := param1@width:28}	
<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, 72> -> <Unique State Name, 86>	Base relation: 
{return := havoc:70
 return@pos := type_err:73
 return@width := type_err:74}	
<Unique State Name, 78> -> <Unique State Name, 87>	Base relation: 
{return := 0
 return@pos := type_err:35
 return@width := type_err:36}	
<Unique State Name, 79> -> <Unique State Name, 76 78>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 89> -> <Unique State Name, 49>	Base relation: 
{}	
<Unique State Name, 45> -> <Unique State Name, 89>	Base relation: 
{when (1 <= n:65 /\ 0 <= l:68 /\ i:64 < n:65 /\ j:66 < n:65 /\ k:67 < n:65)}	
<Unique State Name, 92> -> <Unique State Name, 22>	Base relation: 
{}	
<Unique State Name, 90> -> <Unique State Name, 40>	Base relation: 
{}	
<Unique State Name, 36> -> <Unique State Name, 90>	Base relation: 
{when (1 <= n:65 /\ 0 <= k:67 /\ i:64 < n:65 /\ j:66 < n:65)}	
<Unique State Name, 87> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 9> -> <Unique State Name, 79>	Base relation: 
{param0 := tmp___0:8
 param0@pos := type_err:37
 param0@width := type_err:38}	
<Unique State Name, 82> -> <Unique State Name, 9>	Base relation: 
{tmp___0 := havoc:19}	
<Unique State Name, 22> -> <Unique State Name, 27>	Base relation: 
{j := 0
 when i:64 < n:65}	
<Unique State Name, 22> -> <Unique State Name, 72>	Base relation: 
{when n:65 <= i:64}	
<Unique State Name, 88> -> <Unique State Name, >	Base relation: 
{}	
<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, 76> -> <Unique State Name, 18>	Base relation: 
{i := 0
 n := param0:27}	
<Unique State Name, 27> -> <Unique State Name, 91>	Base relation: 
{when (1 <= n:65 /\ 0 <= j:66 /\ i:64 < n:65)}	
<Unique State Name, 83> -> <Unique State Name, 88 82>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 91> -> <Unique State Name, 31>	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:69 + 1)
 l := (l:68 + 1)
 when (1 <= n:65 /\ 0 <= l:68 /\ i:64 < n:65 /\ j:66 < n:65 /\ k:67 < n:65
         /\ l:68 < n:65 /\ 0 <= __cost:69 /\ 0 <= (__cost:69 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':1416) = (1)*(__cost:69) + 1
           (l':1417) = (1)*(l:68) + 1
           }
          pre:
            [|__cost:69>=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:
            [|l':1417-1>=0; __cost':1416-1>=0; n:65-k:67-1>=0;
              n:65-j:66-1>=0; n:65-i:64-1>=0; n:65-l':1417>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':1416
   l := l':1417
   when ((!(0 <= K:1429) \/ mid___cost:1432 = (__cost:69 + K:1429))
           /\ (!(0 <= K:1429) \/ mid_l:1431 = (l:68 + K:1429))
           /\ ((K:1429 = 0 /\ l:68 = mid_l:1431
                  /\ __cost:69 = mid___cost:1432)
                 \/ (1 <= K:1429 /\ 0 <= __cost:69 /\ 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) /\ 0 <= (-1 + mid_l:1431)
                       /\ 0 <= (-1 + mid___cost:1432)
                       /\ 0 <= (-1 + n:65 + -k:67)
                       /\ 0 <= (-1 + n:65 + -j:66)
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (n:65 + -mid_l:1431))) /\ K:1430 = 0
           /\ mid_l:1431 = l':1417 /\ mid___cost:1432 = __cost':1416
           /\ 0 = K:1430 /\ (K:1429 + K:1430) = K:1428 /\ 0 <= K:1428)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':1445
 k := (k:67 + 1)
 l := l':1444
 when (1 <= n:65 /\ 0 <= k:67 /\ i:64 < n:65 /\ j:66 < n:65 /\ k:67 < n:65
         /\ (!(0 <= K:1440) \/ mid___cost:1441 = (__cost:69 + K:1440))
         /\ (!(0 <= K:1440) \/ mid_l:1442 = K:1440)
         /\ ((K:1440 = 0 /\ 0 = mid_l:1442 /\ __cost:69 = mid___cost:1441)
               \/ (1 <= K:1440 /\ 0 <= __cost:69 /\ 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_l:1442)
                     /\ 0 <= (-1 + mid___cost:1441)
                     /\ 0 <= (-1 + n:65 + -k:67) /\ 0 <= (-1 + n:65 + -j:66)
                     /\ 0 <= (-1 + n:65 + -i:64) /\ 0 <= (n:65 + -mid_l:1442)))
         /\ K:1443 = 0 /\ mid_l:1442 = l':1444
         /\ mid___cost:1441 = __cost':1445 /\ 0 = K:1443
         /\ (K:1440 + K:1443) = K:1446 /\ 0 <= K:1446 /\ 1 <= n:65
         /\ 0 <= l':1444 /\ i:64 < n:65 /\ j:66 < n:65 /\ k:67 < n:65
         /\ n:65 <= l':1444)}
**** alpha hat: 
  {<Split [true
            (__cost':1416) = (1)*(__cost:69) + n:65
           (l':1417) = n:65
           (k':1447) = (1)*(k:67) + 1
           (-__cost':1416) <= (1)*(-__cost:69) + (-1)*1 + (-1)*j:66
           (-__cost':1416) <= (1)*(-__cost:69) + (-1)*1 + (-1)*i:64
           (-__cost':1416) <= (1)*(-__cost:69) + (-1)*1 + (-1)*k:67
           }
          pre:
            [|__cost:69>=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+l':1417=0; -n:65+__cost':1416>=0; k':1447-1>=0;
              n:65-j:66-1>=0; n:65-i:64-1>=0; n:65-k':1447>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':1416
   k := k':1447
   l := l':1417
   when ((!(0 <= K:1461) \/ mid___cost:1465 = (__cost:69 + (n:65 * K:1461)))
           /\ (!((0 <= K:1461 /\ K:1461 <= 0)) \/ mid_l:1463 = l:68)
           /\ (!(1 <= K:1461) \/ mid_l:1463 = n:65)
           /\ (!(0 <= K:1461) \/ mid_k:1464 = (k:67 + K:1461))
           /\ (!(0 <= K:1461)
                 \/ -mid___cost:1465 <= (-__cost:69 + -K:1461
                                           + -((j:66 * K:1461))))
           /\ (!(0 <= K:1461)
                 \/ -mid___cost:1465 <= (-__cost:69 + -K:1461
                                           + -((i:64 * K:1461))))
           /\ (!(0 <= K:1461)
                 \/ -mid___cost:1465 <= (-__cost:69 + (-1/2 * K:1461)
                                           + -((k:67 * K:1461))
                                           + (-1/2 * (K:1461 * K:1461))))
           /\ ((K:1461 = 0 /\ l:68 = mid_l:1463 /\ k:67 = mid_k:1464
                  /\ __cost:69 = mid___cost:1465)
                 \/ (1 <= K:1461 /\ 0 <= __cost:69 /\ 0 <= k:67
                       /\ 0 <= (-1 + n:65 + -j:66)
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (-1 + n:65 + -k:67)
                       /\ (-n:65 + mid_l:1463) = 0
                       /\ 0 <= (-n:65 + mid___cost:1465)
                       /\ 0 <= (-1 + mid_k:1464) /\ 0 <= (-1 + n:65 + -j:66)
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (n:65 + -mid_k:1464))) /\ K:1462 = 0
           /\ mid_l:1463 = l':1417 /\ mid_k:1464 = k':1447
           /\ mid___cost:1465 = __cost':1416 /\ 0 = K:1462
           /\ (K:1461 + K:1462) = K:1460 /\ 0 <= K:1460)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':1482
 j := (j:66 + 1)
 k := k':1481
 l := l':1480
 when (1 <= n:65 /\ 0 <= j:66 /\ i:64 < n:65 /\ j:66 < n:65
         /\ (!(0 <= K:1475)
               \/ mid___cost:1476 = (__cost:69 + (n:65 * K:1475)))
         /\ (!((0 <= K:1475 /\ K:1475 <= 0)) \/ mid_l:1477 = l:68)
         /\ (!(1 <= K:1475) \/ mid_l:1477 = n:65)
         /\ (!(0 <= K:1475) \/ mid_k:1478 = K:1475)
         /\ (!(0 <= K:1475)
               \/ -mid___cost:1476 <= (-__cost:69 + -K:1475
                                         + -((j:66 * K:1475))))
         /\ (!(0 <= K:1475)
               \/ -mid___cost:1476 <= (-__cost:69 + -K:1475
                                         + -((i:64 * K:1475))))
         /\ (!(0 <= K:1475)
               \/ -mid___cost:1476 <= (-__cost:69 + (-1/2 * K:1475)
                                         + (-1/2 * (K:1475 * K:1475))))
         /\ ((K:1475 = 0 /\ l:68 = mid_l:1477 /\ 0 = mid_k:1478
                /\ __cost:69 = mid___cost:1476)
               \/ (1 <= K:1475 /\ 0 <= __cost:69 /\ 0 <= (-1 + n:65 + -j:66)
                     /\ 0 <= (-1 + n:65 + -i:64) /\ 0 <= (-1 + n:65)
                     /\ (-n:65 + mid_l:1477) = 0
                     /\ 0 <= (-n:65 + mid___cost:1476)
                     /\ 0 <= (-1 + mid_k:1478) /\ 0 <= (-1 + n:65 + -j:66)
                     /\ 0 <= (-1 + n:65 + -i:64) /\ 0 <= (n:65 + -mid_k:1478)))
         /\ K:1479 = 0 /\ mid_l:1477 = l':1480 /\ mid_k:1478 = k':1481
         /\ mid___cost:1476 = __cost':1482 /\ 0 = K:1479
         /\ (K:1475 + K:1479) = K:1483 /\ 0 <= K:1483 /\ 1 <= n:65
         /\ 0 <= k':1481 /\ i:64 < n:65 /\ j:66 < n:65 /\ n:65 <= k':1481)}
**** alpha hat: 
  {<Split [true
            (j':1484) = (1)*(j:66) + 1
           (l':1417) = n:65
           (k':1447) = n:65
           (__cost':1416) = (1)*(__cost:69) + n:65^2
           (-__cost':1416) <= (1)*(-__cost:69) + (-1)*n:65
                               + (-1)*(n:65 * i:64)
           (-__cost':1416) <= (1)*(-__cost:69) + (-1)*n:65 + (-1)*n:65*j:66
           }
          pre:
            [|-n:65+(n:65 * n:65)-(n:65 * i:64)>=0;
              -n:65+(n:65 * n:65)-(n:65 * j:66)>=0; -j:66+(n:65 * j:66)>=0;
              __cost:69>=0; j:66>=0; n:65-i:64-1>=0; n:65-j:66-1>=0|]
          post:
            [|-n:65+l':1417=0; -n:65+k':1447=0;
              -n:65+(n:65 * n:65)-(n:65 * i:64)>=0;
              -n:65+(n:65 * n:65)-(n:65 * (-1 + j':1484))>=0;
              -(n:65 * n:65)+__cost':1416>=0;
              -j':1484+(n:65 * (-1 + j':1484))+1>=0; j':1484-1>=0;
              n:65-i:64-1>=0; n:65-j':1484>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':1416
   j := j':1484
   k := k':1447
   l := l':1417
   when ((!(0 <= K:1506) \/ mid_j:1510 = (j:66 + K:1506))
           /\ (!((0 <= K:1506 /\ K:1506 <= 0)) \/ mid_l:1508 = l:68)
           /\ (!(1 <= K:1506) \/ mid_l:1508 = n:65)
           /\ (!((0 <= K:1506 /\ K:1506 <= 0)) \/ mid_k:1509 = k:67)
           /\ (!(1 <= K:1506) \/ mid_k:1509 = n:65)
           /\ (!(0 <= K:1506)
                 \/ mid___cost:1511 = (__cost:69 + ((n:65 * n:65) * K:1506)))
           /\ (!(0 <= K:1506)
                 \/ -mid___cost:1511 <= (-__cost:69 + -((n:65 * K:1506))
                                           + -(((n:65 * i:64) * K:1506))))
           /\ (!(0 <= K:1506)
                 \/ -mid___cost:1511 <= (-__cost:69 + (-1/2 * n:65 * K:1506)
                                           + -((n:65 * j:66 * K:1506))
                                           + (-1/2 * n:65 * (K:1506 * K:1506))))
           /\ ((K:1506 = 0 /\ l:68 = mid_l:1508 /\ k:67 = mid_k:1509
                  /\ j:66 = mid_j:1510 /\ __cost:69 = mid___cost:1511)
                 \/ (1 <= K:1506
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * j:66)))
                       /\ 0 <= (-j:66 + (n:65 * j:66)) /\ 0 <= __cost:69
                       /\ 0 <= j:66 /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (-1 + n:65 + -j:66)
                       /\ (-n:65 + mid_l:1508) = 0
                       /\ (-n:65 + mid_k:1509) = 0
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                       /\ 0 <= (-n:65 + (n:65 * n:65)
                                  + -((n:65 * (-1 + mid_j:1510))))
                       /\ 0 <= (-((n:65 * n:65)) + mid___cost:1511)
                       /\ 0 <= (1 + -mid_j:1510 + (n:65 * (-1 + mid_j:1510)))
                       /\ 0 <= (-1 + mid_j:1510) /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (n:65 + -mid_j:1510))) /\ K:1507 = 0
           /\ mid_l:1508 = l':1417 /\ mid_k:1509 = k':1447
           /\ mid_j:1510 = j':1484 /\ mid___cost:1511 = __cost':1416
           /\ 0 = K:1507 /\ (K:1506 + K:1507) = K:1505 /\ 0 <= K:1505)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':1532
 i := (i:64 + 1)
 j := j':1531
 k := k':1530
 l := l':1529
 when (0 <= i:64 /\ i:64 < n:65 /\ (!(0 <= K:1523) \/ mid_j:1524 = K:1523)
         /\ (!((0 <= K:1523 /\ K:1523 <= 0)) \/ mid_l:1525 = l:68)
         /\ (!(1 <= K:1523) \/ mid_l:1525 = n:65)
         /\ (!((0 <= K:1523 /\ K:1523 <= 0)) \/ mid_k:1526 = k:67)
         /\ (!(1 <= K:1523) \/ mid_k:1526 = n:65)
         /\ (!(0 <= K:1523)
               \/ mid___cost:1527 = (__cost:69 + ((n:65 * n:65) * K:1523)))
         /\ (!(0 <= K:1523)
               \/ -mid___cost:1527 <= (-__cost:69 + -((n:65 * K:1523))
                                         + -(((n:65 * i:64) * K:1523))))
         /\ (!(0 <= K:1523)
               \/ -mid___cost:1527 <= (-__cost:69 + (-1/2 * n:65 * K:1523)
                                         + (-1/2 * n:65 * (K:1523 * K:1523))))
         /\ ((K:1523 = 0 /\ l:68 = mid_l:1525 /\ k:67 = mid_k:1526
                /\ 0 = mid_j:1524 /\ __cost:69 = mid___cost:1527)
               \/ (1 <= K:1523
                     /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                     /\ 0 <= (-n:65 + (n:65 * n:65)) /\ 0 <= __cost:69
                     /\ 0 <= (-1 + n:65 + -i:64) /\ 0 <= (-1 + n:65)
                     /\ (-n:65 + mid_l:1525) = 0 /\ (-n:65 + mid_k:1526) = 0
                     /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                     /\ 0 <= (-n:65 + (n:65 * n:65)
                                + -((n:65 * (-1 + mid_j:1524))))
                     /\ 0 <= (-((n:65 * n:65)) + mid___cost:1527)
                     /\ 0 <= (1 + -mid_j:1524 + (n:65 * (-1 + mid_j:1524)))
                     /\ 0 <= (-1 + mid_j:1524) /\ 0 <= (-1 + n:65 + -i:64)
                     /\ 0 <= (n:65 + -mid_j:1524))) /\ K:1528 = 0
         /\ mid_l:1525 = l':1529 /\ mid_k:1526 = k':1530
         /\ mid_j:1524 = j':1531 /\ mid___cost:1527 = __cost':1532
         /\ 0 = K:1528 /\ (K:1523 + K:1528) = K:1533 /\ 0 <= K:1533
         /\ 1 <= n:65 /\ 0 <= j':1531 /\ i:64 < n:65 /\ n:65 <= j':1531)}
**** alpha hat: 
  {<Split [true
            (l':1417) = n:65
           (k':1447) = n:65
           (i':1534) = (1)*(i:64) + 1
           (__cost':1416) = (1)*(__cost:69) + n:65^3
           (j':1484) = n:65
           (-__cost':1416) <= (1)*(-__cost:69) + (-1)*(n:65 * n:65)
                               + (-1)*(n:65 * n:65)*i:64
           (-__cost':1416) <= (1)*(-__cost:69) + (-1)*1 + 3*n:65
                               + 2*n:65*i:64 + (-3)*(n:65 * n:65)
                               + (-1)*(n:65 * n:65)*i:64 + (-1)*i:64
           }
          pre:
            [|-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;
              __cost:69>=0; i:64>=0;
              i:64+((n:65 * n:65) * i:64)-2(n:65 * i:64)>=0|]
          post:
            [|-n:65+l':1417=0; -n:65+k':1447=0; -n:65+j':1484=0;
              -2n:65+(n:65 * n:65)+1>=0;
              -n:65+(n:65 * n:65)-(n:65 * (-1 + i':1534))>=0;
              -(n:65 * n:65)+((n:65 * n:65) * n:65)
              -((n:65 * n:65) * (-1 + i':1534))>=0;
              -((n:65 * n:65) * n:65)+__cost':1416>=0;
              -i':1534+(n:65 * (-1 + i':1534))+1>=0; i':1534-1>=0;
              i':1534+((n:65 * n:65) * (-1 + i':1534))
              -2(n:65 * (-1 + i':1534))-1>=0; n:65-i':1534>=0;
              3n:65-3(n:65 * n:65)+((n:65 * n:65) * n:65)-i':1534
              -((n:65 * n:65) * (-1 + i':1534))+2(n:65 * (-1 + i':1534))>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':1416
   i := i':1534
   j := j':1484
   k := k':1447
   l := l':1417
   when ((!((0 <= K:1562 /\ K:1562 <= 0)) \/ mid_l:1564 = l:68)
           /\ (!(1 <= K:1562) \/ mid_l:1564 = n:65)
           /\ (!((0 <= K:1562 /\ K:1562 <= 0)) \/ mid_k:1565 = k:67)
           /\ (!(1 <= K:1562) \/ mid_k:1565 = n:65)
           /\ (!(0 <= K:1562) \/ mid_i:1567 = (i:64 + K:1562))
           /\ (!(0 <= K:1562)
                 \/ mid___cost:1568 = (__cost:69
                                         + ((n:65 * (n:65 * n:65)) * K:1562)))
           /\ (!((0 <= K:1562 /\ K:1562 <= 0)) \/ mid_j:1566 = j:66)
           /\ (!(1 <= K:1562) \/ mid_j:1566 = n:65)
           /\ (!(0 <= K:1562)
                 \/ -mid___cost:1568 <= (-__cost:69
                                           + (-1/2 * (n:65 * n:65) * K:1562)
                                           + -(((n:65 * n:65) * i:64 * K:1562))
                                           + (-1/2 * (n:65 * n:65)
                                                * (K:1562 * K:1562))))
           /\ (!(0 <= K:1562)
                 \/ -mid___cost:1568 <= (-__cost:69 + (-1/2 * K:1562)
                                           + (2 * n:65 * K:1562)
                                           + (-5/2 * (n:65 * n:65) * K:1562)
                                           + -((i:64 * K:1562))
                                           + (2 * n:65 * i:64 * K:1562)
                                           + -(((n:65 * n:65) * i:64 * K:1562))
                                           + (-1/2 * (K:1562 * K:1562))
                                           + (n:65 * (K:1562 * K:1562))
                                           + (-1/2 * (n:65 * n:65)
                                                * (K:1562 * K:1562))))
           /\ ((K:1562 = 0 /\ l:68 = mid_l:1564 /\ k:67 = mid_k:1565
                  /\ j:66 = mid_j:1566 /\ i:64 = mid_i:1567
                  /\ __cost:69 = mid___cost:1568)
                 \/ (1 <= K:1562 /\ 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 <= __cost:69 /\ 0 <= i:64
                       /\ 0 <= (i:64 + ((n:65 * n:65) * i:64)
                                  + (-2 * (n:65 * i:64)))
                       /\ (-n:65 + mid_l:1564) = 0
                       /\ (-n:65 + mid_k:1565) = 0
                       /\ (-n:65 + mid_j:1566) = 0
                       /\ 0 <= (1 + (-2 * n:65) + (n:65 * n:65))
                       /\ 0 <= (-n:65 + (n:65 * n:65)
                                  + -((n:65 * (-1 + mid_i:1567))))
                       /\ 0 <= (-((n:65 * n:65)) + ((n:65 * n:65) * n:65)
                                  + -(((n:65 * n:65) * (-1 + mid_i:1567))))
                       /\ 0 <= (-(((n:65 * n:65) * n:65)) + mid___cost:1568)
                       /\ 0 <= (1 + -mid_i:1567 + (n:65 * (-1 + mid_i:1567)))
                       /\ 0 <= (-1 + mid_i:1567)
                       /\ 0 <= (-1 + mid_i:1567
                                  + ((n:65 * n:65) * (-1 + mid_i:1567))
                                  + (-2 * (n:65 * (-1 + mid_i:1567))))
                       /\ 0 <= (n:65 + -mid_i:1567)
                       /\ 0 <= ((3 * n:65) + (-3 * (n:65 * n:65))
                                  + ((n:65 * n:65) * n:65) + -mid_i:1567
                                  + -(((n:65 * n:65) * (-1 + mid_i:1567)))
                                  + (2 * (n:65 * (-1 + mid_i:1567))))))
           /\ K:1563 = 0 /\ mid_l:1564 = l':1417 /\ mid_k:1565 = k':1447
           /\ mid_j:1566 = j':1484 /\ mid_i:1567 = i':1534
           /\ mid___cost:1568 = __cost':1416 /\ 0 = K:1563
           /\ (K:1562 + K:1563) = K:1561 /\ 0 <= K:1561)}
}
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:1409 /\ tr:1410 <= 0)}        )
        ,
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := 0
               argv := param1:30
               param0 := tr:1413
               argv@pos := param1@pos:29
               param0@pos := type_err:1414
               argv@width := param1@width:28
               param0@width := type_err:1415
               when (tr:1411 < 0 \/ 0 < tr:1412)}            )
            ,
            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':1580
   i := i':1579
   j := j':1578
   k := k':1577
   l := l':1576
   n := param0:27
   return := havoc:1582
   return@pos := type_err:1583
   return@width := type_err:1584
   when ((!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_l:1570 = l:68)
           /\ (!(1 <= K:1569) \/ mid_l:1570 = param0:27)
           /\ (!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_k:1571 = k:67)
           /\ (!(1 <= K:1569) \/ mid_k:1571 = param0:27)
           /\ (!(0 <= K:1569) \/ mid_i:1572 = K:1569)
           /\ (!(0 <= K:1569)
                 \/ mid___cost:1573 = (__cost:69
                                         + ((param0:27
                                               * (param0:27 * param0:27))
                                              * K:1569)))
           /\ (!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_j:1574 = j:66)
           /\ (!(1 <= K:1569) \/ mid_j:1574 = param0:27)
           /\ (!(0 <= K:1569)
                 \/ -mid___cost:1573 <= (-__cost:69
                                           + (-1/2 * (param0:27 * param0:27)
                                                * K:1569)
                                           + (-1/2 * (param0:27 * param0:27)
                                                * (K:1569 * K:1569))))
           /\ (!(0 <= K:1569)
                 \/ -mid___cost:1573 <= (-__cost:69 + (-1/2 * K:1569)
                                           + (2 * param0:27 * K:1569)
                                           + (-5/2 * (param0:27 * param0:27)
                                                * K:1569)
                                           + (-1/2 * (K:1569 * K:1569))
                                           + (param0:27 * (K:1569 * K:1569))
                                           + (-1/2 * (param0:27 * param0:27)
                                                * (K:1569 * K:1569))))
           /\ ((K:1569 = 0 /\ l:68 = mid_l:1570 /\ k:67 = mid_k:1571
                  /\ j:66 = mid_j:1574 /\ 0 = mid_i:1572
                  /\ __cost:69 = mid___cost:1573)
                 \/ (1 <= K:1569 /\ 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 <= __cost:69 /\ (-param0:27 + mid_l:1570) = 0
                       /\ (-param0:27 + mid_k:1571) = 0
                       /\ (-param0:27 + mid_j:1574) = 0
                       /\ 0 <= (1 + (-2 * param0:27)
                                  + (param0:27 * param0:27))
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                  + -((param0:27 * (-1 + mid_i:1572))))
                       /\ 0 <= (-((param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27)
                                  + -(((param0:27 * param0:27)
                                         * (-1 + mid_i:1572))))
                       /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                  + mid___cost:1573)
                       /\ 0 <= (1 + -mid_i:1572
                                  + (param0:27 * (-1 + mid_i:1572)))
                       /\ 0 <= (-1 + mid_i:1572)
                       /\ 0 <= (-1 + mid_i:1572
                                  + ((param0:27 * param0:27)
                                       * (-1 + mid_i:1572))
                                  + (-2 * (param0:27 * (-1 + mid_i:1572))))
                       /\ 0 <= (param0:27 + -mid_i:1572)
                       /\ 0 <= ((3 * param0:27)
                                  + (-3 * (param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27)
                                  + -mid_i:1572
                                  + -(((param0:27 * param0:27)
                                         * (-1 + mid_i:1572)))
                                  + (2 * (param0:27 * (-1 + mid_i:1572))))))
           /\ K:1575 = 0 /\ mid_l:1570 = l':1576 /\ mid_k:1571 = k':1577
           /\ mid_j:1574 = j':1578 /\ mid_i:1572 = i':1579
           /\ mid___cost:1573 = __cost':1580 /\ 0 = K:1575
           /\ (K:1569 + K:1575) = K:1581 /\ 0 <= K:1581 /\ 0 <= i':1579
           /\ param0:27 <= i':1579)})



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:1409 /\ tr:1410 <= 0)}          )
          ,
          Dot(
            Dot(
              Weight(Base relation: 
                {__cost := 0
                 argv := param1:30
                 param0 := tr:1413
                 argv@pos := param1@pos:29
                 param0@pos := type_err:1414
                 argv@width := param1@width:28
                 param0@width := type_err:1415
                 when (tr:1411 < 0 \/ 0 < tr:1412)}              )
              ,
              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':1580
   return := havoc:1582
   return@pos := type_err:1583
   return@width := type_err:1584
   when ((!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_l:1570 = l:1639)
           /\ (!(1 <= K:1569) \/ mid_l:1570 = param0:27)
           /\ (!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_k:1571 = k:1640)
           /\ (!(1 <= K:1569) \/ mid_k:1571 = param0:27)
           /\ (!(0 <= K:1569) \/ mid_i:1572 = K:1569)
           /\ (!(0 <= K:1569)
                 \/ mid___cost:1573 = (__cost:69
                                         + ((param0:27
                                               * (param0:27 * param0:27))
                                              * K:1569)))
           /\ (!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_j:1574 = j:1641)
           /\ (!(1 <= K:1569) \/ mid_j:1574 = param0:27)
           /\ (!(0 <= K:1569)
                 \/ -mid___cost:1573 <= (-__cost:69
                                           + (-1/2 * (param0:27 * param0:27)
                                                * K:1569)
                                           + (-1/2 * (param0:27 * param0:27)
                                                * (K:1569 * K:1569))))
           /\ (!(0 <= K:1569)
                 \/ -mid___cost:1573 <= (-__cost:69 + (-1/2 * K:1569)
                                           + (2 * param0:27 * K:1569)
                                           + (-5/2 * (param0:27 * param0:27)
                                                * K:1569)
                                           + (-1/2 * (K:1569 * K:1569))
                                           + (param0:27 * (K:1569 * K:1569))
                                           + (-1/2 * (param0:27 * param0:27)
                                                * (K:1569 * K:1569))))
           /\ ((K:1569 = 0 /\ l:1639 = mid_l:1570 /\ k:1640 = mid_k:1571
                  /\ j:1641 = mid_j:1574 /\ 0 = mid_i:1572
                  /\ __cost:69 = mid___cost:1573)
                 \/ (1 <= K:1569 /\ 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 <= __cost:69 /\ (-param0:27 + mid_l:1570) = 0
                       /\ (-param0:27 + mid_k:1571) = 0
                       /\ (-param0:27 + mid_j:1574) = 0
                       /\ 0 <= (1 + (-2 * param0:27)
                                  + (param0:27 * param0:27))
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                  + -((param0:27 * (-1 + mid_i:1572))))
                       /\ 0 <= (-((param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27)
                                  + -(((param0:27 * param0:27)
                                         * (-1 + mid_i:1572))))
                       /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                  + mid___cost:1573)
                       /\ 0 <= (1 + -mid_i:1572
                                  + (param0:27 * (-1 + mid_i:1572)))
                       /\ 0 <= (-1 + mid_i:1572)
                       /\ 0 <= (-1 + mid_i:1572
                                  + ((param0:27 * param0:27)
                                       * (-1 + mid_i:1572))
                                  + (-2 * (param0:27 * (-1 + mid_i:1572))))
                       /\ 0 <= (param0:27 + -mid_i:1572)
                       /\ 0 <= ((3 * param0:27)
                                  + (-3 * (param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27)
                                  + -mid_i:1572
                                  + -(((param0:27 * param0:27)
                                         * (-1 + mid_i:1572)))
                                  + (2 * (param0:27 * (-1 + mid_i:1572))))))
           /\ K:1575 = 0 /\ mid_l:1570 = l':1576 /\ mid_k:1571 = k':1577
           /\ mid_j:1574 = j':1578 /\ mid_i:1572 = i':1579
           /\ mid___cost:1573 = __cost':1580 /\ 0 = K:1575
           /\ (K:1569 + K:1575) = K:1581 /\ 0 <= K:1581 /\ 0 <= i':1579
           /\ param0:27 <= i':1579)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=11: 
Weight(Base relation: 
  {__cost := __cost':1663
   return := 0
   param0 := phi_tmp___0:1646
   return@pos := type_err:1668
   param0@pos := type_err:1647
   return@width := type_err:1669
   param0@width := type_err:1648
   when (((0 <= tr:1409 /\ tr:1410 <= 0 /\ 0 = phi_tmp___0:1646
             /\ param0:27 = phi_param0:1645
             /\ param0@pos:26 = phi_param0@pos:1644
             /\ param0@width:25 = phi_param0@width:1643)
            \/ ((tr:1411 < 0 \/ 0 < tr:1412) /\ havoc:1642 = phi_tmp___0:1646
                  /\ tr:1413 = phi_param0:1645
                  /\ type_err:1414 = phi_param0@pos:1644
                  /\ type_err:1415 = phi_param0@width:1643))
           /\ (!((0 <= K:1649 /\ K:1649 <= 0)) \/ mid_l:1650 = l:1651)
           /\ (!(1 <= K:1649) \/ mid_l:1650 = phi_tmp___0:1646)
           /\ (!((0 <= K:1649 /\ K:1649 <= 0)) \/ mid_k:1652 = k:1653)
           /\ (!(1 <= K:1649) \/ mid_k:1652 = phi_tmp___0:1646)
           /\ (!(0 <= K:1649) \/ mid_i:1654 = K:1649)
           /\ (!(0 <= K:1649)
                 \/ mid___cost:1655 = ((phi_tmp___0:1646
                                          * (phi_tmp___0:1646
                                               * phi_tmp___0:1646)) * K:1649))
           /\ (!((0 <= K:1649 /\ K:1649 <= 0)) \/ mid_j:1656 = j:1657)
           /\ (!(1 <= K:1649) \/ mid_j:1656 = phi_tmp___0:1646)
           /\ (!(0 <= K:1649)
                 \/ -mid___cost:1655 <= ((-1/2
                                            * (phi_tmp___0:1646
                                                 * phi_tmp___0:1646) * K:1649)
                                           + (-1/2
                                                * (phi_tmp___0:1646
                                                     * phi_tmp___0:1646)
                                                * (K:1649 * K:1649))))
           /\ (!(0 <= K:1649)
                 \/ -mid___cost:1655 <= ((-1/2 * K:1649)
                                           + (2 * phi_tmp___0:1646 * K:1649)
                                           + (-5/2
                                                * (phi_tmp___0:1646
                                                     * phi_tmp___0:1646)
                                                * K:1649)
                                           + (-1/2 * (K:1649 * K:1649))
                                           + (phi_tmp___0:1646
                                                * (K:1649 * K:1649))
                                           + (-1/2
                                                * (phi_tmp___0:1646
                                                     * phi_tmp___0:1646)
                                                * (K:1649 * K:1649))))
           /\ ((K:1649 = 0 /\ l:1651 = mid_l:1650 /\ k:1653 = mid_k:1652
                  /\ j:1657 = mid_j:1656 /\ 0 = mid_i:1654
                  /\ 0 = mid___cost:1655)
                 \/ (1 <= K:1649 /\ 0 <= (-1 + phi_tmp___0:1646)
                       /\ 0 <= (-1 + (3 * phi_tmp___0:1646)
                                  + (-3
                                       * (phi_tmp___0:1646 * phi_tmp___0:1646))
                                  + ((phi_tmp___0:1646 * phi_tmp___0:1646)
                                       * phi_tmp___0:1646))
                       /\ 0 <= (1 + (-2 * phi_tmp___0:1646)
                                  + (phi_tmp___0:1646 * phi_tmp___0:1646))
                       /\ 0 <= (-phi_tmp___0:1646
                                  + (phi_tmp___0:1646 * phi_tmp___0:1646))
                       /\ 0 <= (-((phi_tmp___0:1646 * phi_tmp___0:1646))
                                  + ((phi_tmp___0:1646 * phi_tmp___0:1646)
                                       * phi_tmp___0:1646))
                       /\ (-phi_tmp___0:1646 + mid_l:1650) = 0
                       /\ (-phi_tmp___0:1646 + mid_k:1652) = 0
                       /\ (-phi_tmp___0:1646 + mid_j:1656) = 0
                       /\ 0 <= (1 + (-2 * phi_tmp___0:1646)
                                  + (phi_tmp___0:1646 * phi_tmp___0:1646))
                       /\ 0 <= (-phi_tmp___0:1646
                                  + (phi_tmp___0:1646 * phi_tmp___0:1646)
                                  + -((phi_tmp___0:1646 * (-1 + mid_i:1654))))
                       /\ 0 <= (-((phi_tmp___0:1646 * phi_tmp___0:1646))
                                  + ((phi_tmp___0:1646 * phi_tmp___0:1646)
                                       * phi_tmp___0:1646)
                                  + -(((phi_tmp___0:1646 * phi_tmp___0:1646)
                                         * (-1 + mid_i:1654))))
                       /\ 0 <= (-(((phi_tmp___0:1646 * phi_tmp___0:1646)
                                     * phi_tmp___0:1646)) + mid___cost:1655)
                       /\ 0 <= (1 + -mid_i:1654
                                  + (phi_tmp___0:1646 * (-1 + mid_i:1654)))
                       /\ 0 <= (-1 + mid_i:1654)
                       /\ 0 <= (-1 + mid_i:1654
                                  + ((phi_tmp___0:1646 * phi_tmp___0:1646)
                                       * (-1 + mid_i:1654))
                                  + (-2
                                       * (phi_tmp___0:1646
                                            * (-1 + mid_i:1654))))
                       /\ 0 <= (phi_tmp___0:1646 + -mid_i:1654)
                       /\ 0 <= ((3 * phi_tmp___0:1646)
                                  + (-3
                                       * (phi_tmp___0:1646 * phi_tmp___0:1646))
                                  + ((phi_tmp___0:1646 * phi_tmp___0:1646)
                                       * phi_tmp___0:1646) + -mid_i:1654
                                  + -(((phi_tmp___0:1646 * phi_tmp___0:1646)
                                         * (-1 + mid_i:1654)))
                                  + (2
                                       * (phi_tmp___0:1646
                                            * (-1 + mid_i:1654))))))
           /\ K:1658 = 0 /\ mid_l:1650 = l':1659 /\ mid_k:1652 = k':1660
           /\ mid_j:1656 = j':1661 /\ mid_i:1654 = i':1662
           /\ mid___cost:1655 = __cost':1663 /\ 0 = K:1658
           /\ (K:1649 + K:1658) = K:1664 /\ 0 <= K:1664 /\ 0 <= i':1662
           /\ phi_tmp___0:1646 <= i':1662)})


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':1580
   return := havoc:1582
   return@pos := type_err:1583
   return@width := type_err:1584
   when ((!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_l:1570 = l:1639)
           /\ (!(1 <= K:1569) \/ mid_l:1570 = param0:27)
           /\ (!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_k:1571 = k:1640)
           /\ (!(1 <= K:1569) \/ mid_k:1571 = param0:27)
           /\ (!(0 <= K:1569) \/ mid_i:1572 = K:1569)
           /\ (!(0 <= K:1569)
                 \/ mid___cost:1573 = (__cost:69
                                         + ((param0:27
                                               * (param0:27 * param0:27))
                                              * K:1569)))
           /\ (!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_j:1574 = j:1641)
           /\ (!(1 <= K:1569) \/ mid_j:1574 = param0:27)
           /\ (!(0 <= K:1569)
                 \/ -mid___cost:1573 <= (-__cost:69
                                           + (-1/2 * (param0:27 * param0:27)
                                                * K:1569)
                                           + (-1/2 * (param0:27 * param0:27)
                                                * (K:1569 * K:1569))))
           /\ (!(0 <= K:1569)
                 \/ -mid___cost:1573 <= (-__cost:69 + (-1/2 * K:1569)
                                           + (2 * param0:27 * K:1569)
                                           + (-5/2 * (param0:27 * param0:27)
                                                * K:1569)
                                           + (-1/2 * (K:1569 * K:1569))
                                           + (param0:27 * (K:1569 * K:1569))
                                           + (-1/2 * (param0:27 * param0:27)
                                                * (K:1569 * K:1569))))
           /\ ((K:1569 = 0 /\ l:1639 = mid_l:1570 /\ k:1640 = mid_k:1571
                  /\ j:1641 = mid_j:1574 /\ 0 = mid_i:1572
                  /\ __cost:69 = mid___cost:1573)
                 \/ (1 <= K:1569 /\ 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 <= __cost:69 /\ (-param0:27 + mid_l:1570) = 0
                       /\ (-param0:27 + mid_k:1571) = 0
                       /\ (-param0:27 + mid_j:1574) = 0
                       /\ 0 <= (1 + (-2 * param0:27)
                                  + (param0:27 * param0:27))
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                  + -((param0:27 * (-1 + mid_i:1572))))
                       /\ 0 <= (-((param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27)
                                  + -(((param0:27 * param0:27)
                                         * (-1 + mid_i:1572))))
                       /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                  + mid___cost:1573)
                       /\ 0 <= (1 + -mid_i:1572
                                  + (param0:27 * (-1 + mid_i:1572)))
                       /\ 0 <= (-1 + mid_i:1572)
                       /\ 0 <= (-1 + mid_i:1572
                                  + ((param0:27 * param0:27)
                                       * (-1 + mid_i:1572))
                                  + (-2 * (param0:27 * (-1 + mid_i:1572))))
                       /\ 0 <= (param0:27 + -mid_i:1572)
                       /\ 0 <= ((3 * param0:27)
                                  + (-3 * (param0:27 * param0:27))
                                  + ((param0:27 * param0:27) * param0:27)
                                  + -mid_i:1572
                                  + -(((param0:27 * param0:27)
                                         * (-1 + mid_i:1572)))
                                  + (2 * (param0:27 * (-1 + mid_i:1572))))))
           /\ K:1575 = 0 /\ mid_l:1570 = l':1576 /\ mid_k:1571 = k':1577
           /\ mid_j:1574 = j':1578 /\ mid_i:1572 = i':1579
           /\ mid___cost:1573 = __cost':1580 /\ 0 = K:1575
           /\ (K:1569 + K:1575) = K:1581 /\ 0 <= K:1581 /\ 0 <= i':1579
           /\ param0:27 <= i':1579)})


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':1663
 return := 0
 param0 := phi_tmp___0:1646
 return@pos := type_err:1668
 param0@pos := type_err:1647
 return@width := type_err:1669
 param0@width := type_err:1648
 when (((0 <= tr:1409 /\ tr:1410 <= 0 /\ 0 = phi_tmp___0:1646
           /\ param0:27 = phi_param0:1645
           /\ param0@pos:26 = phi_param0@pos:1644
           /\ param0@width:25 = phi_param0@width:1643)
          \/ ((tr:1411 < 0 \/ 0 < tr:1412) /\ havoc:1642 = phi_tmp___0:1646
                /\ tr:1413 = phi_param0:1645
                /\ type_err:1414 = phi_param0@pos:1644
                /\ type_err:1415 = phi_param0@width:1643))
         /\ (!((0 <= K:1649 /\ K:1649 <= 0)) \/ mid_l:1650 = l:1651)
         /\ (!(1 <= K:1649) \/ mid_l:1650 = phi_tmp___0:1646)
         /\ (!((0 <= K:1649 /\ K:1649 <= 0)) \/ mid_k:1652 = k:1653)
         /\ (!(1 <= K:1649) \/ mid_k:1652 = phi_tmp___0:1646)
         /\ (!(0 <= K:1649) \/ mid_i:1654 = K:1649)
         /\ (!(0 <= K:1649)
               \/ mid___cost:1655 = ((phi_tmp___0:1646
                                        * (phi_tmp___0:1646
                                             * phi_tmp___0:1646)) * K:1649))
         /\ (!((0 <= K:1649 /\ K:1649 <= 0)) \/ mid_j:1656 = j:1657)
         /\ (!(1 <= K:1649) \/ mid_j:1656 = phi_tmp___0:1646)
         /\ (!(0 <= K:1649)
               \/ -mid___cost:1655 <= ((-1/2
                                          * (phi_tmp___0:1646
                                               * phi_tmp___0:1646) * K:1649)
                                         + (-1/2
                                              * (phi_tmp___0:1646
                                                   * phi_tmp___0:1646)
                                              * (K:1649 * K:1649))))
         /\ (!(0 <= K:1649)
               \/ -mid___cost:1655 <= ((-1/2 * K:1649)
                                         + (2 * phi_tmp___0:1646 * K:1649)
                                         + (-5/2
                                              * (phi_tmp___0:1646
                                                   * phi_tmp___0:1646)
                                              * K:1649)
                                         + (-1/2 * (K:1649 * K:1649))
                                         + (phi_tmp___0:1646
                                              * (K:1649 * K:1649))
                                         + (-1/2
                                              * (phi_tmp___0:1646
                                                   * phi_tmp___0:1646)
                                              * (K:1649 * K:1649))))
         /\ ((K:1649 = 0 /\ l:1651 = mid_l:1650 /\ k:1653 = mid_k:1652
                /\ j:1657 = mid_j:1656 /\ 0 = mid_i:1654
                /\ 0 = mid___cost:1655)
               \/ (1 <= K:1649 /\ 0 <= (-1 + phi_tmp___0:1646)
                     /\ 0 <= (-1 + (3 * phi_tmp___0:1646)
                                + (-3 * (phi_tmp___0:1646 * phi_tmp___0:1646))
                                + ((phi_tmp___0:1646 * phi_tmp___0:1646)
                                     * phi_tmp___0:1646))
                     /\ 0 <= (1 + (-2 * phi_tmp___0:1646)
                                + (phi_tmp___0:1646 * phi_tmp___0:1646))
                     /\ 0 <= (-phi_tmp___0:1646
                                + (phi_tmp___0:1646 * phi_tmp___0:1646))
                     /\ 0 <= (-((phi_tmp___0:1646 * phi_tmp___0:1646))
                                + ((phi_tmp___0:1646 * phi_tmp___0:1646)
                                     * phi_tmp___0:1646))
                     /\ (-phi_tmp___0:1646 + mid_l:1650) = 0
                     /\ (-phi_tmp___0:1646 + mid_k:1652) = 0
                     /\ (-phi_tmp___0:1646 + mid_j:1656) = 0
                     /\ 0 <= (1 + (-2 * phi_tmp___0:1646)
                                + (phi_tmp___0:1646 * phi_tmp___0:1646))
                     /\ 0 <= (-phi_tmp___0:1646
                                + (phi_tmp___0:1646 * phi_tmp___0:1646)
                                + -((phi_tmp___0:1646 * (-1 + mid_i:1654))))
                     /\ 0 <= (-((phi_tmp___0:1646 * phi_tmp___0:1646))
                                + ((phi_tmp___0:1646 * phi_tmp___0:1646)
                                     * phi_tmp___0:1646)
                                + -(((phi_tmp___0:1646 * phi_tmp___0:1646)
                                       * (-1 + mid_i:1654))))
                     /\ 0 <= (-(((phi_tmp___0:1646 * phi_tmp___0:1646)
                                   * phi_tmp___0:1646)) + mid___cost:1655)
                     /\ 0 <= (1 + -mid_i:1654
                                + (phi_tmp___0:1646 * (-1 + mid_i:1654)))
                     /\ 0 <= (-1 + mid_i:1654)
                     /\ 0 <= (-1 + mid_i:1654
                                + ((phi_tmp___0:1646 * phi_tmp___0:1646)
                                     * (-1 + mid_i:1654))
                                + (-2
                                     * (phi_tmp___0:1646 * (-1 + mid_i:1654))))
                     /\ 0 <= (phi_tmp___0:1646 + -mid_i:1654)
                     /\ 0 <= ((3 * phi_tmp___0:1646)
                                + (-3 * (phi_tmp___0:1646 * phi_tmp___0:1646))
                                + ((phi_tmp___0:1646 * phi_tmp___0:1646)
                                     * phi_tmp___0:1646) + -mid_i:1654
                                + -(((phi_tmp___0:1646 * phi_tmp___0:1646)
                                       * (-1 + mid_i:1654)))
                                + (2 * (phi_tmp___0:1646 * (-1 + mid_i:1654))))))
         /\ K:1658 = 0 /\ mid_l:1650 = l':1659 /\ mid_k:1652 = k':1660
         /\ mid_j:1656 = j':1661 /\ mid_i:1654 = i':1662
         /\ mid___cost:1655 = __cost':1663 /\ 0 = K:1658
         /\ (K:1649 + K:1658) = K:1664 /\ 0 <= K:1664 /\ 0 <= i':1662
         /\ phi_tmp___0:1646 <= i':1662)}

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':1580
 return := havoc:1582
 return@pos := type_err:1583
 return@width := type_err:1584
 when ((!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_l:1570 = l:1639)
         /\ (!(1 <= K:1569) \/ mid_l:1570 = param0:27)
         /\ (!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_k:1571 = k:1640)
         /\ (!(1 <= K:1569) \/ mid_k:1571 = param0:27)
         /\ (!(0 <= K:1569) \/ mid_i:1572 = K:1569)
         /\ (!(0 <= K:1569)
               \/ mid___cost:1573 = (__cost:69
                                       + ((param0:27
                                             * (param0:27 * param0:27))
                                            * K:1569)))
         /\ (!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_j:1574 = j:1641)
         /\ (!(1 <= K:1569) \/ mid_j:1574 = param0:27)
         /\ (!(0 <= K:1569)
               \/ -mid___cost:1573 <= (-__cost:69
                                         + (-1/2 * (param0:27 * param0:27)
                                              * K:1569)
                                         + (-1/2 * (param0:27 * param0:27)
                                              * (K:1569 * K:1569))))
         /\ (!(0 <= K:1569)
               \/ -mid___cost:1573 <= (-__cost:69 + (-1/2 * K:1569)
                                         + (2 * param0:27 * K:1569)
                                         + (-5/2 * (param0:27 * param0:27)
                                              * K:1569)
                                         + (-1/2 * (K:1569 * K:1569))
                                         + (param0:27 * (K:1569 * K:1569))
                                         + (-1/2 * (param0:27 * param0:27)
                                              * (K:1569 * K:1569))))
         /\ ((K:1569 = 0 /\ l:1639 = mid_l:1570 /\ k:1640 = mid_k:1571
                /\ j:1641 = mid_j:1574 /\ 0 = mid_i:1572
                /\ __cost:69 = mid___cost:1573)
               \/ (1 <= K:1569 /\ 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 <= __cost:69 /\ (-param0:27 + mid_l:1570) = 0
                     /\ (-param0:27 + mid_k:1571) = 0
                     /\ (-param0:27 + mid_j:1574) = 0
                     /\ 0 <= (1 + (-2 * param0:27) + (param0:27 * param0:27))
                     /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                + -((param0:27 * (-1 + mid_i:1572))))
                     /\ 0 <= (-((param0:27 * param0:27))
                                + ((param0:27 * param0:27) * param0:27)
                                + -(((param0:27 * param0:27)
                                       * (-1 + mid_i:1572))))
                     /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                + mid___cost:1573)
                     /\ 0 <= (1 + -mid_i:1572
                                + (param0:27 * (-1 + mid_i:1572)))
                     /\ 0 <= (-1 + mid_i:1572)
                     /\ 0 <= (-1 + mid_i:1572
                                + ((param0:27 * param0:27)
                                     * (-1 + mid_i:1572))
                                + (-2 * (param0:27 * (-1 + mid_i:1572))))
                     /\ 0 <= (param0:27 + -mid_i:1572)
                     /\ 0 <= ((3 * param0:27)
                                + (-3 * (param0:27 * param0:27))
                                + ((param0:27 * param0:27) * param0:27)
                                + -mid_i:1572
                                + -(((param0:27 * param0:27)
                                       * (-1 + mid_i:1572)))
                                + (2 * (param0:27 * (-1 + mid_i:1572))))))
         /\ K:1575 = 0 /\ mid_l:1570 = l':1576 /\ mid_k:1571 = k':1577
         /\ mid_j:1574 = j':1578 /\ mid_i:1572 = i':1579
         /\ mid___cost:1573 = __cost':1580 /\ 0 = K:1575
         /\ (K:1569 + K:1575) = K:1581 /\ 0 <= K:1581 /\ 0 <= i':1579
         /\ param0:27 <= i':1579)}

    (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,76)_g1>	Base relation: 
{__cost := 0
 tmp___0 := phi_tmp___0:1674
 argv := param1:30
 param0 := phi_tmp___0:1674
 argv@pos := param1@pos:29
 param0@pos := type_err:1675
 argv@width := param1@width:28
 param0@width := type_err:1676
 when ((0 <= tr:1409 /\ tr:1410 <= 0 /\ 0 = phi_tmp___0:1674
          /\ param0:27 = phi_param0:1673
          /\ param0@pos:26 = phi_param0@pos:1672
          /\ param0@width:25 = phi_param0@width:1671)
         \/ ((tr:1411 < 0 \/ 0 < tr:1412) /\ havoc:1670 = phi_tmp___0:1674
               /\ tr:1413 = phi_param0:1673
               /\ type_err:1414 = phi_param0@pos:1672
               /\ type_err:1415 = phi_param0@width:1671))}	
<__pstate, accept> -> <__pstate, (Unique State Name,88)_g1>	Base relation: 
{__cost := 0
 argv := param1:30
 param0 := tr:1413
 argv@pos := param1@pos:29
 param0@pos := type_err:1414
 argv@width := param1@width:28
 param0@width := type_err:1415
 when (tr:1411 < 0 \/ 0 < tr:1412)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x21f96710: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x21c93d50: 
	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,88)_g1 , __done )	Base relation: 
{__cost := 0
 argv := param1:30
 param0 := tr:1413
 argv@pos := param1@pos:29
 param0@pos := type_err:1414
 argv@width := param1@width:28
 param0@width := type_err:1415
 when (tr:1411 < 0 \/ 0 < tr:1412)}
    ( __pstate , (Unique State Name,76)_g1 , __done )	Base relation: 
{__cost := 0
 tmp___0 := phi_tmp___0:1674
 argv := param1:30
 param0 := phi_tmp___0:1674
 argv@pos := param1@pos:29
 param0@pos := type_err:1675
 argv@width := param1@width:28
 param0@width := type_err:1676
 when ((0 <= tr:1409 /\ tr:1410 <= 0 /\ 0 = phi_tmp___0:1674
          /\ param0:27 = phi_param0:1673
          /\ param0@pos:26 = phi_param0@pos:1672
          /\ param0@width:25 = phi_param0@width:1671)
         \/ ((tr:1411 < 0 \/ 0 < tr:1412) /\ havoc:1670 = phi_tmp___0:1674
               /\ tr:1413 = phi_param0:1673
               /\ type_err:1414 = phi_param0@pos:1672
               /\ type_err:1415 = phi_param0@width:1671))}

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

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

Base relation: 
{}

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

Base relation: 
{__cost := __cost':1691
 tmp___0 := phi_tmp___0:1674
 argv := param1:30
 return := 0
 param0 := phi_tmp___0:1674
 argv@pos := param1@pos:29
 return@pos := type_err:1696
 param0@pos := type_err:1675
 argv@width := param1@width:28
 return@width := type_err:1697
 param0@width := type_err:1676
 when (((0 <= tr:1409 /\ tr:1410 <= 0 /\ 0 = phi_tmp___0:1674
           /\ param0:27 = phi_param0:1673
           /\ param0@pos:26 = phi_param0@pos:1672
           /\ param0@width:25 = phi_param0@width:1671)
          \/ ((tr:1411 < 0 \/ 0 < tr:1412) /\ havoc:1670 = phi_tmp___0:1674
                /\ tr:1413 = phi_param0:1673
                /\ type_err:1414 = phi_param0@pos:1672
                /\ type_err:1415 = phi_param0@width:1671))
         /\ (!((0 <= K:1677 /\ K:1677 <= 0)) \/ mid_l:1678 = l:1679)
         /\ (!(1 <= K:1677) \/ mid_l:1678 = phi_tmp___0:1674)
         /\ (!((0 <= K:1677 /\ K:1677 <= 0)) \/ mid_k:1680 = k:1681)
         /\ (!(1 <= K:1677) \/ mid_k:1680 = phi_tmp___0:1674)
         /\ (!(0 <= K:1677) \/ mid_i:1682 = K:1677)
         /\ (!(0 <= K:1677)
               \/ mid___cost:1683 = ((phi_tmp___0:1674
                                        * (phi_tmp___0:1674
                                             * phi_tmp___0:1674)) * K:1677))
         /\ (!((0 <= K:1677 /\ K:1677 <= 0)) \/ mid_j:1684 = j:1685)
         /\ (!(1 <= K:1677) \/ mid_j:1684 = phi_tmp___0:1674)
         /\ (!(0 <= K:1677)
               \/ -mid___cost:1683 <= ((-1/2
                                          * (phi_tmp___0:1674
                                               * phi_tmp___0:1674) * K:1677)
                                         + (-1/2
                                              * (phi_tmp___0:1674
                                                   * phi_tmp___0:1674)
                                              * (K:1677 * K:1677))))
         /\ (!(0 <= K:1677)
               \/ -mid___cost:1683 <= ((-1/2 * K:1677)
                                         + (2 * phi_tmp___0:1674 * K:1677)
                                         + (-5/2
                                              * (phi_tmp___0:1674
                                                   * phi_tmp___0:1674)
                                              * K:1677)
                                         + (-1/2 * (K:1677 * K:1677))
                                         + (phi_tmp___0:1674
                                              * (K:1677 * K:1677))
                                         + (-1/2
                                              * (phi_tmp___0:1674
                                                   * phi_tmp___0:1674)
                                              * (K:1677 * K:1677))))
         /\ ((K:1677 = 0 /\ l:1679 = mid_l:1678 /\ k:1681 = mid_k:1680
                /\ j:1685 = mid_j:1684 /\ 0 = mid_i:1682
                /\ 0 = mid___cost:1683)
               \/ (1 <= K:1677 /\ 0 <= (-1 + phi_tmp___0:1674)
                     /\ 0 <= (-1 + (3 * phi_tmp___0:1674)
                                + (-3 * (phi_tmp___0:1674 * phi_tmp___0:1674))
                                + ((phi_tmp___0:1674 * phi_tmp___0:1674)
                                     * phi_tmp___0:1674))
                     /\ 0 <= (1 + (-2 * phi_tmp___0:1674)
                                + (phi_tmp___0:1674 * phi_tmp___0:1674))
                     /\ 0 <= (-phi_tmp___0:1674
                                + (phi_tmp___0:1674 * phi_tmp___0:1674))
                     /\ 0 <= (-((phi_tmp___0:1674 * phi_tmp___0:1674))
                                + ((phi_tmp___0:1674 * phi_tmp___0:1674)
                                     * phi_tmp___0:1674))
                     /\ (-phi_tmp___0:1674 + mid_l:1678) = 0
                     /\ (-phi_tmp___0:1674 + mid_k:1680) = 0
                     /\ (-phi_tmp___0:1674 + mid_j:1684) = 0
                     /\ 0 <= (1 + (-2 * phi_tmp___0:1674)
                                + (phi_tmp___0:1674 * phi_tmp___0:1674))
                     /\ 0 <= (-phi_tmp___0:1674
                                + (phi_tmp___0:1674 * phi_tmp___0:1674)
                                + -((phi_tmp___0:1674 * (-1 + mid_i:1682))))
                     /\ 0 <= (-((phi_tmp___0:1674 * phi_tmp___0:1674))
                                + ((phi_tmp___0:1674 * phi_tmp___0:1674)
                                     * phi_tmp___0:1674)
                                + -(((phi_tmp___0:1674 * phi_tmp___0:1674)
                                       * (-1 + mid_i:1682))))
                     /\ 0 <= (-(((phi_tmp___0:1674 * phi_tmp___0:1674)
                                   * phi_tmp___0:1674)) + mid___cost:1683)
                     /\ 0 <= (1 + -mid_i:1682
                                + (phi_tmp___0:1674 * (-1 + mid_i:1682)))
                     /\ 0 <= (-1 + mid_i:1682)
                     /\ 0 <= (-1 + mid_i:1682
                                + ((phi_tmp___0:1674 * phi_tmp___0:1674)
                                     * (-1 + mid_i:1682))
                                + (-2
                                     * (phi_tmp___0:1674 * (-1 + mid_i:1682))))
                     /\ 0 <= (phi_tmp___0:1674 + -mid_i:1682)
                     /\ 0 <= ((3 * phi_tmp___0:1674)
                                + (-3 * (phi_tmp___0:1674 * phi_tmp___0:1674))
                                + ((phi_tmp___0:1674 * phi_tmp___0:1674)
                                     * phi_tmp___0:1674) + -mid_i:1682
                                + -(((phi_tmp___0:1674 * phi_tmp___0:1674)
                                       * (-1 + mid_i:1682)))
                                + (2 * (phi_tmp___0:1674 * (-1 + mid_i:1682))))))
         /\ K:1686 = 0 /\ mid_l:1678 = l':1687 /\ mid_k:1680 = k':1688
         /\ mid_j:1684 = j':1689 /\ mid_i:1682 = i':1690
         /\ mid___cost:1683 = __cost':1691 /\ 0 = K:1686
         /\ (K:1677 + K:1686) = K:1692 /\ 0 <= K:1692 /\ 0 <= i':1690
         /\ phi_tmp___0:1674 <= i':1690)}

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

Base relation: 
{__cost := __cost':1580
 i := i':1579
 j := j':1578
 k := k':1577
 l := l':1576
 n := param0:27
 return := havoc:1582
 return@pos := type_err:1583
 return@width := type_err:1584
 when ((!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_l:1570 = l:68)
         /\ (!(1 <= K:1569) \/ mid_l:1570 = param0:27)
         /\ (!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_k:1571 = k:67)
         /\ (!(1 <= K:1569) \/ mid_k:1571 = param0:27)
         /\ (!(0 <= K:1569) \/ mid_i:1572 = K:1569)
         /\ (!(0 <= K:1569)
               \/ mid___cost:1573 = (__cost:69
                                       + ((param0:27
                                             * (param0:27 * param0:27))
                                            * K:1569)))
         /\ (!((0 <= K:1569 /\ K:1569 <= 0)) \/ mid_j:1574 = j:66)
         /\ (!(1 <= K:1569) \/ mid_j:1574 = param0:27)
         /\ (!(0 <= K:1569)
               \/ -mid___cost:1573 <= (-__cost:69
                                         + (-1/2 * (param0:27 * param0:27)
                                              * K:1569)
                                         + (-1/2 * (param0:27 * param0:27)
                                              * (K:1569 * K:1569))))
         /\ (!(0 <= K:1569)
               \/ -mid___cost:1573 <= (-__cost:69 + (-1/2 * K:1569)
                                         + (2 * param0:27 * K:1569)
                                         + (-5/2 * (param0:27 * param0:27)
                                              * K:1569)
                                         + (-1/2 * (K:1569 * K:1569))
                                         + (param0:27 * (K:1569 * K:1569))
                                         + (-1/2 * (param0:27 * param0:27)
                                              * (K:1569 * K:1569))))
         /\ ((K:1569 = 0 /\ l:68 = mid_l:1570 /\ k:67 = mid_k:1571
                /\ j:66 = mid_j:1574 /\ 0 = mid_i:1572
                /\ __cost:69 = mid___cost:1573)
               \/ (1 <= K:1569 /\ 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 <= __cost:69 /\ (-param0:27 + mid_l:1570) = 0
                     /\ (-param0:27 + mid_k:1571) = 0
                     /\ (-param0:27 + mid_j:1574) = 0
                     /\ 0 <= (1 + (-2 * param0:27) + (param0:27 * param0:27))
                     /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                + -((param0:27 * (-1 + mid_i:1572))))
                     /\ 0 <= (-((param0:27 * param0:27))
                                + ((param0:27 * param0:27) * param0:27)
                                + -(((param0:27 * param0:27)
                                       * (-1 + mid_i:1572))))
                     /\ 0 <= (-(((param0:27 * param0:27) * param0:27))
                                + mid___cost:1573)
                     /\ 0 <= (1 + -mid_i:1572
                                + (param0:27 * (-1 + mid_i:1572)))
                     /\ 0 <= (-1 + mid_i:1572)
                     /\ 0 <= (-1 + mid_i:1572
                                + ((param0:27 * param0:27)
                                     * (-1 + mid_i:1572))
                                + (-2 * (param0:27 * (-1 + mid_i:1572))))
                     /\ 0 <= (param0:27 + -mid_i:1572)
                     /\ 0 <= ((3 * param0:27)
                                + (-3 * (param0:27 * param0:27))
                                + ((param0:27 * param0:27) * param0:27)
                                + -mid_i:1572
                                + -(((param0:27 * param0:27)
                                       * (-1 + mid_i:1572)))
                                + (2 * (param0:27 * (-1 + mid_i:1572))))))
         /\ K:1575 = 0 /\ mid_l:1570 = l':1576 /\ mid_k:1571 = k':1577
         /\ mid_j:1574 = j':1578 /\ mid_i:1572 = i':1579
         /\ mid___cost:1573 = __cost':1580 /\ 0 = K:1575
         /\ (K:1569 + K:1575) = K:1581 /\ 0 <= K:1581 /\ 0 <= i':1579
         /\ param0:27 <= i':1579)}

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

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

Variable bounds at line 13 in work

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

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