/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, 8> -> <Unique State Name, 9>	Base relation: 
{tmp___0 := 0
 when (0 <= tr:7 /\ tr:6 <= 0)}	
<Unique State Name, 8> -> <Unique State Name, 57>	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, 56> -> <Unique State Name, 9>	Base relation: 
{tmp___0 := havoc:19}	
<Unique State Name, 64> -> <Unique State Name, 22>	Base relation: 
{}	
<Unique State Name, 61> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 31> -> <Unique State Name, 18>	Base relation: 
{i := (i:64 + 1)
 when i:64 <= j:66}	
<Unique State Name, 31> -> <Unique State Name, 27>	Base relation: 
{__cost := (__cost:67 + 1)
 j := (j:66 + 1)
 when (j:66 < i:64 /\ 0 <= __cost:67 /\ 0 <= (__cost:67 + 1))}	
<Unique State Name, 27> -> <Unique State Name, 63>	Base relation: 
{when (0 <= j:66 /\ 0 <= i:64 /\ i:64 < n:65)}	
<Unique State Name, 18> -> <Unique State Name, 64>	Base relation: 
{when 0 <= i:64}	
<Unique State Name, 58> -> <Unique State Name, 8>	Base relation: 
{__cost := 0
 argv := param1:30
 argv@pos := param1@pos:29
 argv@width := param1@width:28}	
<Unique State Name, 53> -> <Unique State Name, 50 52>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 46> -> <Unique State Name, 60>	Base relation: 
{return := havoc:68
 return@pos := type_err:71
 return@width := type_err:72}	
<Unique State Name, 22> -> <Unique State Name, 27>	Base relation: 
{j := 0
 when i:64 < n:65}	
<Unique State Name, 22> -> <Unique State Name, 46>	Base relation: 
{when n:65 <= i:64}	
<Unique State Name, 57> -> <Unique State Name, 62 56>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 63> -> <Unique State Name, 31>	Base relation: 
{}	
<Unique State Name, 62> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 52> -> <Unique State Name, 61>	Base relation: 
{return := 0
 return@pos := type_err:35
 return@width := type_err:36}	
<Unique State Name, 50> -> <Unique State Name, 18>	Base relation: 
{i := 0
 n := param0:27}	
<Unique State Name, 60> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 9> -> <Unique State Name, 53>	Base relation: 
{param0 := tmp___0:8
 param0@pos := type_err:37
 param0@width := type_err:38}	
#################################################################
           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:67 + 1)
 j := (j:66 + 1)
 when (0 <= j:66 /\ 0 <= i:64 /\ i:64 < n:65 /\ j:66 < i:64 /\ 0 <= __cost:67
         /\ 0 <= (__cost:67 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':360) = (1)*(__cost:67) + 1
           (j':361) = (1)*(j:66) + 1
           }
          pre:
            [|-i:64+n:65-1>=0; __cost:67>=0; j:66>=0; i:64-j:66-1>=0|]
          post:
            [|-i:64+n:65-1>=0; j':361-1>=0; __cost':360-1>=0; i:64-j':361>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':360
   j := j':361
   when ((!(0 <= K:371) \/ mid___cost:374 = (__cost:67 + K:371))
           /\ (!(0 <= K:371) \/ mid_j:373 = (j:66 + K:371))
           /\ ((K:371 = 0 /\ j:66 = mid_j:373 /\ __cost:67 = mid___cost:374)
                 \/ (1 <= K:371 /\ 0 <= (-1 + -i:64 + n:65) /\ 0 <= __cost:67
                       /\ 0 <= j:66 /\ 0 <= (-1 + i:64 + -j:66)
                       /\ 0 <= (-1 + -i:64 + n:65) /\ 0 <= (-1 + mid_j:373)
                       /\ 0 <= (-1 + mid___cost:374)
                       /\ 0 <= (i:64 + -mid_j:373))) /\ K:372 = 0
           /\ mid_j:373 = j':361 /\ mid___cost:374 = __cost':360 /\ 0 = K:372
           /\ (K:371 + K:372) = K:370 /\ 0 <= K:370)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':387
 i := (i:64 + 1)
 j := j':386
 when (0 <= i:64 /\ i:64 < n:65
         /\ (!(0 <= K:382) \/ mid___cost:383 = (__cost:67 + K:382))
         /\ (!(0 <= K:382) \/ mid_j:384 = K:382)
         /\ ((K:382 = 0 /\ 0 = mid_j:384 /\ __cost:67 = mid___cost:383)
               \/ (1 <= K:382 /\ 0 <= (-1 + -i:64 + n:65) /\ 0 <= __cost:67
                     /\ 0 <= (-1 + i:64) /\ 0 <= (-1 + -i:64 + n:65)
                     /\ 0 <= (-1 + mid_j:384) /\ 0 <= (-1 + mid___cost:383)
                     /\ 0 <= (i:64 + -mid_j:384))) /\ K:385 = 0
         /\ mid_j:384 = j':386 /\ mid___cost:383 = __cost':387 /\ 0 = K:385
         /\ (K:382 + K:385) = K:388 /\ 0 <= K:388 /\ 0 <= j':386 /\ 0 <= i:64
         /\ i:64 < n:65 /\ i:64 <= j':386)}
**** alpha hat: 
  {<Split [!(-__cost:67 <= 0)
            (__cost':360) = (1)*(__cost:67) + 0
           (j':361) = 0
           (i':389) = 1
           }
          pre:
            [|i:64=0; -__cost:67-1>=0; n:65-1>=0|]
          post:
            [|i':389-1=0; j':361=0; -__cost':360-1>=0; n:65-1>=0|]
           ((-__cost':360 + i':389)) = (-1)*(__cost:67) + 1
          (__cost':360) = (1)*((-__cost:67 + i:64)) + (2)*(__cost:67) + 0
          ((-__cost':360 + j':361)) = (-1)*(__cost:67) + 0
          (__cost':360) <= (1)*(__cost:67) + (-1)*1 + n:65
          (-__cost':360) <= (1)*(-__cost:67) + (-1)*(-__cost:67 + i:64)
          (-__cost':360) <= (1)*(-__cost:67) + 0
          }
  pre:
    [|-i:64+n:65-1>=0; i:64>=0; __cost:67>=0|]
  post:
    [|-i':389+j':361+1=0; -i':389+n:65>=0; i':389-1>=0;
      __cost':360-i':389+1>=0|]],
[!((1 + -i:64) <= 0)
  (j':361) = 0
 (__cost':360) = (1)*(__cost:67) + 0
 (i':389) = 1
 } pre:   [|i:64=0; n:65-1>=0|] post:   [|i':389-1=0; j':361=0; n:65-1>=0|]
 (__cost':360) = (1)*(__cost:67) + (1)*(i:64) + 0 (j':361) = (1)*(i:64) + 0
(i':389) = (1)*(i:64) + 1 (__cost':360) <= (1)*(__cost:67) + (-1)*1 + n:65
(-__cost':360) <= (1)*(-__cost:67) + (-1)*1 } pre:
  [|-i:64+n:65-1>=0; __cost:67>=0; i:64-1>=0|] post:
  [|-j':361+i':389-1=0; j':361-1>=0; __cost':360-j':361>=0; n:65-j':361-1>=0|]]>}
**** star transition: 
  {__cost := __cost':360
   i := i':389
   j := j':361
   when ((!(0 <= K:419) \/ mid___cost:423 = __cost:67)
           /\ (!((0 <= K:419 /\ K:419 <= 0)) \/ mid_j:421 = j:66)
           /\ (!(1 <= K:419) \/ mid_j:421 = 0)
           /\ (!((0 <= K:419 /\ K:419 <= 0)) \/ mid_i:422 = i:64)
           /\ (!(1 <= K:419) \/ mid_i:422 = 1)
           /\ ((K:419 = 0 /\ j:66 = mid_j:421 /\ i:64 = mid_i:422
                  /\ __cost:67 = mid___cost:423)
                 \/ (1 <= K:419 /\ i:64 = 0 /\ 0 <= (-1 + -__cost:67)
                       /\ 0 <= (-1 + n:65) /\ (-1 + mid_i:422) = 0
                       /\ mid_j:421 = 0 /\ 0 <= (-1 + -mid___cost:423)
                       /\ 0 <= (-1 + n:65)))
           /\ (0 = K:419 \/ !(-__cost:67 <= 0))
           /\ (!(0 <= K:420)
                 \/ (-__cost':360 + i':389) = ((-mid___cost:423 + mid_i:422)
                                                 + (3/2 * K:420)
                                                 + -(((-mid___cost:423
                                                         + mid_i:422) * K:420))
                                                 + -((mid___cost:423 * K:420))
                                                 + (-1/2 * (K:420 * K:420))))
           /\ (!(0 <= K:420)
                 \/ __cost':360 = (mid___cost:423 + (-1/2 * K:420)
                                     + ((-mid___cost:423 + mid_i:422) * K:420)
                                     + (mid___cost:423 * K:420)
                                     + (1/2 * (K:420 * K:420))))
           /\ (!((0 <= K:420 /\ K:420 <= 0))
                 \/ (-__cost':360 + j':361) = ((-mid___cost:423 + mid_j:421)
                                                 + (3/2 * K:420)
                                                 + -(((-mid___cost:423
                                                         + mid_i:422) * K:420))
                                                 + -((mid___cost:423 * K:420))
                                                 + (-1/2 * (K:420 * K:420))))
           /\ (!(1 <= K:420)
                 \/ (-__cost':360 + j':361) = (-1
                                                 + (-mid___cost:423
                                                      + mid_i:422)
                                                 + (3/2 * K:420)
                                                 + -(((-mid___cost:423
                                                         + mid_i:422) * K:420))
                                                 + -((mid___cost:423 * K:420))
                                                 + (-1/2 * (K:420 * K:420))))
           /\ (!(0 <= K:420)
                 \/ __cost':360 <= (mid___cost:423 + -K:420 + (n:65 * K:420)))
           /\ (!(0 <= K:420)
                 \/ -__cost':360 <= (-mid___cost:423 + (5/6 * K:420)
                                       + (-3/2
                                            * (-mid___cost:423 + mid_i:422)
                                            * K:420)
                                       + (-1/2 * mid___cost:423 * K:420)
                                       + -((K:420 * K:420))
                                       + (1/2 * (-mid___cost:423 + mid_i:422)
                                            * (K:420 * K:420))
                                       + (1/2 * mid___cost:423
                                            * (K:420 * K:420))
                                       + (1/6 * (K:420 * (K:420 * K:420)))))
           /\ (!(0 <= K:420) \/ -__cost':360 <= -mid___cost:423)
           /\ ((K:420 = 0 /\ mid_j:421 = j':361 /\ mid_i:422 = i':389
                  /\ mid___cost:423 = __cost':360)
                 \/ (1 <= K:420 /\ 0 <= (-1 + -mid_i:422 + n:65)
                       /\ 0 <= mid_i:422 /\ 0 <= mid___cost:423
                       /\ (1 + -i':389 + j':361) = 0 /\ 0 <= (-i':389 + n:65)
                       /\ 0 <= (-1 + i':389)
                       /\ 0 <= (1 + __cost':360 + -i':389)))
           /\ (0 = K:420 \/ -mid___cost:423 <= 0) /\ (K:419 + K:420) = K:418
           /\ (!((0 <= K:424 /\ K:424 <= 0)) \/ mid_j:426 = j:66)
           /\ (!(1 <= K:424) \/ mid_j:426 = 0)
           /\ (!(0 <= K:424) \/ mid___cost:428 = __cost:67)
           /\ (!((0 <= K:424 /\ K:424 <= 0)) \/ mid_i:427 = i:64)
           /\ (!(1 <= K:424) \/ mid_i:427 = 1)
           /\ ((K:424 = 0 /\ j:66 = mid_j:426 /\ i:64 = mid_i:427
                  /\ __cost:67 = mid___cost:428)
                 \/ (1 <= K:424 /\ i:64 = 0 /\ 0 <= (-1 + n:65)
                       /\ (-1 + mid_i:427) = 0 /\ mid_j:426 = 0
                       /\ 0 <= (-1 + n:65)))
           /\ (0 = K:424 \/ !((1 + -i:64) <= 0))
           /\ (!(0 <= K:425)
                 \/ __cost':360 = (mid___cost:428 + (-1/2 * K:425)
                                     + (mid_i:427 * K:425)
                                     + (1/2 * (K:425 * K:425))))
           /\ (!((0 <= K:425 /\ K:425 <= 0)) \/ j':361 = (mid_j:426 + K:425))
           /\ (!(1 <= K:425)
                 \/ j':361 = (-1 + mid_j:426 + mid_i:427 + -mid_j:426 + K:425))
           /\ (!(0 <= K:425) \/ i':389 = (mid_i:427 + K:425))
           /\ (!(0 <= K:425)
                 \/ __cost':360 <= (mid___cost:428 + -K:425 + (n:65 * K:425)))
           /\ (!(0 <= K:425) \/ -__cost':360 <= (-mid___cost:428 + -K:425))
           /\ ((K:425 = 0 /\ mid_j:426 = j':361 /\ mid_i:427 = i':389
                  /\ mid___cost:428 = __cost':360)
                 \/ (1 <= K:425 /\ 0 <= (-1 + -mid_i:427 + n:65)
                       /\ 0 <= mid___cost:428 /\ 0 <= (-1 + mid_i:427)
                       /\ (-1 + -j':361 + i':389) = 0 /\ 0 <= (-1 + j':361)
                       /\ 0 <= (__cost':360 + -j':361)
                       /\ 0 <= (-1 + n:65 + -j':361)))
           /\ (0 = K:425 \/ (1 + -mid_i:427) <= 0) /\ (K:424 + K:425) = K:418
           /\ 0 <= K:418)}
}
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:358 /\ tr:359 <= 0)}        )
        ,
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := 0
               argv := param1:30
               param0 := tr:355
               argv@pos := param1@pos:29
               param0@pos := type_err:356
               argv@width := param1@width:28
               param0@width := type_err:357
               when (tr:353 < 0 \/ 0 < tr:354)}            )
            ,
            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':434
   i := i':435
   j := j':436
   n := param0:27
   return := havoc:443
   return@pos := type_err:444
   return@width := type_err:445
   when ((!(0 <= K:429) \/ mid___cost:430 = __cost:67)
           /\ (!((0 <= K:429 /\ K:429 <= 0)) \/ mid_j:431 = j:66)
           /\ (!(1 <= K:429) \/ mid_j:431 = 0)
           /\ (!((0 <= K:429 /\ K:429 <= 0)) \/ mid_i:432 = 0)
           /\ (!(1 <= K:429) \/ mid_i:432 = 1)
           /\ ((K:429 = 0 /\ j:66 = mid_j:431 /\ 0 = mid_i:432
                  /\ __cost:67 = mid___cost:430)
                 \/ (1 <= K:429 /\ 0 <= (-1 + -__cost:67)
                       /\ 0 <= (-1 + param0:27) /\ (-1 + mid_i:432) = 0
                       /\ mid_j:431 = 0 /\ 0 <= (-1 + -mid___cost:430)
                       /\ 0 <= (-1 + param0:27)))
           /\ (0 = K:429 \/ !(-__cost:67 <= 0))
           /\ (!(0 <= K:433)
                 \/ (-__cost':434 + i':435) = ((-mid___cost:430 + mid_i:432)
                                                 + (3/2 * K:433)
                                                 + -(((-mid___cost:430
                                                         + mid_i:432) * K:433))
                                                 + -((mid___cost:430 * K:433))
                                                 + (-1/2 * (K:433 * K:433))))
           /\ (!(0 <= K:433)
                 \/ __cost':434 = (mid___cost:430 + (-1/2 * K:433)
                                     + ((-mid___cost:430 + mid_i:432) * K:433)
                                     + (mid___cost:430 * K:433)
                                     + (1/2 * (K:433 * K:433))))
           /\ (!((0 <= K:433 /\ K:433 <= 0))
                 \/ (-__cost':434 + j':436) = ((-mid___cost:430 + mid_j:431)
                                                 + (3/2 * K:433)
                                                 + -(((-mid___cost:430
                                                         + mid_i:432) * K:433))
                                                 + -((mid___cost:430 * K:433))
                                                 + (-1/2 * (K:433 * K:433))))
           /\ (!(1 <= K:433)
                 \/ (-__cost':434 + j':436) = (-1
                                                 + (-mid___cost:430
                                                      + mid_i:432)
                                                 + (3/2 * K:433)
                                                 + -(((-mid___cost:430
                                                         + mid_i:432) * K:433))
                                                 + -((mid___cost:430 * K:433))
                                                 + (-1/2 * (K:433 * K:433))))
           /\ (!(0 <= K:433)
                 \/ __cost':434 <= (mid___cost:430 + -K:433
                                      + (param0:27 * K:433)))
           /\ (!(0 <= K:433)
                 \/ -__cost':434 <= (-mid___cost:430 + (5/6 * K:433)
                                       + (-3/2
                                            * (-mid___cost:430 + mid_i:432)
                                            * K:433)
                                       + (-1/2 * mid___cost:430 * K:433)
                                       + -((K:433 * K:433))
                                       + (1/2 * (-mid___cost:430 + mid_i:432)
                                            * (K:433 * K:433))
                                       + (1/2 * mid___cost:430
                                            * (K:433 * K:433))
                                       + (1/6 * (K:433 * (K:433 * K:433)))))
           /\ (!(0 <= K:433) \/ -__cost':434 <= -mid___cost:430)
           /\ ((K:433 = 0 /\ mid_j:431 = j':436 /\ mid_i:432 = i':435
                  /\ mid___cost:430 = __cost':434)
                 \/ (1 <= K:433 /\ 0 <= (-1 + -mid_i:432 + param0:27)
                       /\ 0 <= mid_i:432 /\ 0 <= mid___cost:430
                       /\ (1 + -i':435 + j':436) = 0
                       /\ 0 <= (-i':435 + param0:27) /\ 0 <= (-1 + i':435)
                       /\ 0 <= (1 + __cost':434 + -i':435)))
           /\ (0 = K:433 \/ -mid___cost:430 <= 0) /\ (K:429 + K:433) = K:437
           /\ (!((0 <= K:438 /\ K:438 <= 0)) \/ mid_j:439 = j:66)
           /\ (!(1 <= K:438) \/ mid_j:439 = 0)
           /\ (!(0 <= K:438) \/ mid___cost:440 = __cost:67)
           /\ (!((0 <= K:438 /\ K:438 <= 0)) \/ mid_i:441 = 0)
           /\ (!(1 <= K:438) \/ mid_i:441 = 1)
           /\ ((K:438 = 0 /\ j:66 = mid_j:439 /\ 0 = mid_i:441
                  /\ __cost:67 = mid___cost:440)
                 \/ (1 <= K:438 /\ 0 <= (-1 + param0:27)
                       /\ (-1 + mid_i:441) = 0 /\ mid_j:439 = 0
                       /\ 0 <= (-1 + param0:27)))
           /\ (!(0 <= K:442)
                 \/ __cost':434 = (mid___cost:440 + (-1/2 * K:442)
                                     + (mid_i:441 * K:442)
                                     + (1/2 * (K:442 * K:442))))
           /\ (!((0 <= K:442 /\ K:442 <= 0)) \/ j':436 = (mid_j:439 + K:442))
           /\ (!(1 <= K:442)
                 \/ j':436 = (-1 + mid_j:439 + mid_i:441 + -mid_j:439 + K:442))
           /\ (!(0 <= K:442) \/ i':435 = (mid_i:441 + K:442))
           /\ (!(0 <= K:442)
                 \/ __cost':434 <= (mid___cost:440 + -K:442
                                      + (param0:27 * K:442)))
           /\ (!(0 <= K:442) \/ -__cost':434 <= (-mid___cost:440 + -K:442))
           /\ ((K:442 = 0 /\ mid_j:439 = j':436 /\ mid_i:441 = i':435
                  /\ mid___cost:440 = __cost':434)
                 \/ (1 <= K:442 /\ 0 <= (-1 + -mid_i:441 + param0:27)
                       /\ 0 <= mid___cost:440 /\ 0 <= (-1 + mid_i:441)
                       /\ (-1 + -j':436 + i':435) = 0 /\ 0 <= (-1 + j':436)
                       /\ 0 <= (__cost':434 + -j':436)
                       /\ 0 <= (-1 + param0:27 + -j':436)))
           /\ (0 = K:442 \/ (1 + -mid_i:441) <= 0) /\ (K:438 + K:442) = K:437
           /\ 0 <= K:437 /\ 0 <= i':435 /\ param0:27 <= i':435)})



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:358 /\ tr:359 <= 0)}          )
          ,
          Dot(
            Dot(
              Weight(Base relation: 
                {__cost := 0
                 argv := param1:30
                 param0 := tr:355
                 argv@pos := param1@pos:29
                 param0@pos := type_err:356
                 argv@width := param1@width:28
                 param0@width := type_err:357
                 when (tr:353 < 0 \/ 0 < tr:354)}              )
              ,
              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':434
   return := havoc:443
   return@pos := type_err:444
   return@width := type_err:445
   when ((!(0 <= K:429) \/ mid___cost:430 = __cost:67)
           /\ (!((0 <= K:429 /\ K:429 <= 0)) \/ mid_j:431 = j:460)
           /\ (!(1 <= K:429) \/ mid_j:431 = 0)
           /\ (!((0 <= K:429 /\ K:429 <= 0)) \/ mid_i:432 = 0)
           /\ (!(1 <= K:429) \/ mid_i:432 = 1)
           /\ ((K:429 = 0 /\ j:460 = mid_j:431 /\ 0 = mid_i:432
                  /\ __cost:67 = mid___cost:430)
                 \/ (1 <= K:429 /\ 0 <= (-1 + -__cost:67)
                       /\ 0 <= (-1 + param0:27) /\ (-1 + mid_i:432) = 0
                       /\ mid_j:431 = 0 /\ 0 <= (-1 + -mid___cost:430)
                       /\ 0 <= (-1 + param0:27)))
           /\ (0 = K:429 \/ !(-__cost:67 <= 0))
           /\ (!(0 <= K:433)
                 \/ (-__cost':434 + i':435) = ((-mid___cost:430 + mid_i:432)
                                                 + (3/2 * K:433)
                                                 + -(((-mid___cost:430
                                                         + mid_i:432) * K:433))
                                                 + -((mid___cost:430 * K:433))
                                                 + (-1/2 * (K:433 * K:433))))
           /\ (!(0 <= K:433)
                 \/ __cost':434 = (mid___cost:430 + (-1/2 * K:433)
                                     + ((-mid___cost:430 + mid_i:432) * K:433)
                                     + (mid___cost:430 * K:433)
                                     + (1/2 * (K:433 * K:433))))
           /\ (!((0 <= K:433 /\ K:433 <= 0))
                 \/ (-__cost':434 + j':436) = ((-mid___cost:430 + mid_j:431)
                                                 + (3/2 * K:433)
                                                 + -(((-mid___cost:430
                                                         + mid_i:432) * K:433))
                                                 + -((mid___cost:430 * K:433))
                                                 + (-1/2 * (K:433 * K:433))))
           /\ (!(1 <= K:433)
                 \/ (-__cost':434 + j':436) = (-1
                                                 + (-mid___cost:430
                                                      + mid_i:432)
                                                 + (3/2 * K:433)
                                                 + -(((-mid___cost:430
                                                         + mid_i:432) * K:433))
                                                 + -((mid___cost:430 * K:433))
                                                 + (-1/2 * (K:433 * K:433))))
           /\ (!(0 <= K:433)
                 \/ __cost':434 <= (mid___cost:430 + -K:433
                                      + (param0:27 * K:433)))
           /\ (!(0 <= K:433)
                 \/ -__cost':434 <= (-mid___cost:430 + (5/6 * K:433)
                                       + (-3/2
                                            * (-mid___cost:430 + mid_i:432)
                                            * K:433)
                                       + (-1/2 * mid___cost:430 * K:433)
                                       + -((K:433 * K:433))
                                       + (1/2 * (-mid___cost:430 + mid_i:432)
                                            * (K:433 * K:433))
                                       + (1/2 * mid___cost:430
                                            * (K:433 * K:433))
                                       + (1/6 * (K:433 * (K:433 * K:433)))))
           /\ (!(0 <= K:433) \/ -__cost':434 <= -mid___cost:430)
           /\ ((K:433 = 0 /\ mid_j:431 = j':436 /\ mid_i:432 = i':435
                  /\ mid___cost:430 = __cost':434)
                 \/ (1 <= K:433 /\ 0 <= (-1 + -mid_i:432 + param0:27)
                       /\ 0 <= mid_i:432 /\ 0 <= mid___cost:430
                       /\ (1 + -i':435 + j':436) = 0
                       /\ 0 <= (-i':435 + param0:27) /\ 0 <= (-1 + i':435)
                       /\ 0 <= (1 + __cost':434 + -i':435)))
           /\ (0 = K:433 \/ -mid___cost:430 <= 0) /\ (K:429 + K:433) = K:437
           /\ (!((0 <= K:438 /\ K:438 <= 0)) \/ mid_j:439 = j:460)
           /\ (!(1 <= K:438) \/ mid_j:439 = 0)
           /\ (!(0 <= K:438) \/ mid___cost:440 = __cost:67)
           /\ (!((0 <= K:438 /\ K:438 <= 0)) \/ mid_i:441 = 0)
           /\ (!(1 <= K:438) \/ mid_i:441 = 1)
           /\ ((K:438 = 0 /\ j:460 = mid_j:439 /\ 0 = mid_i:441
                  /\ __cost:67 = mid___cost:440)
                 \/ (1 <= K:438 /\ 0 <= (-1 + param0:27)
                       /\ (-1 + mid_i:441) = 0 /\ mid_j:439 = 0
                       /\ 0 <= (-1 + param0:27)))
           /\ (!(0 <= K:442)
                 \/ __cost':434 = (mid___cost:440 + (-1/2 * K:442)
                                     + (mid_i:441 * K:442)
                                     + (1/2 * (K:442 * K:442))))
           /\ (!((0 <= K:442 /\ K:442 <= 0)) \/ j':436 = (mid_j:439 + K:442))
           /\ (!(1 <= K:442)
                 \/ j':436 = (-1 + mid_j:439 + mid_i:441 + -mid_j:439 + K:442))
           /\ (!(0 <= K:442) \/ i':435 = (mid_i:441 + K:442))
           /\ (!(0 <= K:442)
                 \/ __cost':434 <= (mid___cost:440 + -K:442
                                      + (param0:27 * K:442)))
           /\ (!(0 <= K:442) \/ -__cost':434 <= (-mid___cost:440 + -K:442))
           /\ ((K:442 = 0 /\ mid_j:439 = j':436 /\ mid_i:441 = i':435
                  /\ mid___cost:440 = __cost':434)
                 \/ (1 <= K:442 /\ 0 <= (-1 + -mid_i:441 + param0:27)
                       /\ 0 <= mid___cost:440 /\ 0 <= (-1 + mid_i:441)
                       /\ (-1 + -j':436 + i':435) = 0 /\ 0 <= (-1 + j':436)
                       /\ 0 <= (__cost':434 + -j':436)
                       /\ 0 <= (-1 + param0:27 + -j':436)))
           /\ (0 = K:442 \/ (1 + -mid_i:441) <= 0) /\ (K:438 + K:442) = K:437
           /\ 0 <= K:437 /\ 0 <= i':435 /\ param0:27 <= i':435)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=11: 
Weight(Base relation: 
  {__cost := __cost':474
   return := 0
   param0 := phi_tmp___0:465
   return@pos := type_err:486
   param0@pos := type_err:466
   return@width := type_err:487
   param0@width := type_err:467
   when (((0 <= tr:358 /\ tr:359 <= 0 /\ 0 = phi_tmp___0:465
             /\ param0:27 = phi_param0:464
             /\ param0@pos:26 = phi_param0@pos:463
             /\ param0@width:25 = phi_param0@width:462)
            \/ ((tr:353 < 0 \/ 0 < tr:354) /\ havoc:461 = phi_tmp___0:465
                  /\ tr:355 = phi_param0:464
                  /\ type_err:356 = phi_param0@pos:463
                  /\ type_err:357 = phi_param0@width:462))
           /\ (!(0 <= K:468) \/ mid___cost:469 = 0)
           /\ (!((0 <= K:468 /\ K:468 <= 0)) \/ mid_j:470 = j:471)
           /\ (!(1 <= K:468) \/ mid_j:470 = 0)
           /\ (!((0 <= K:468 /\ K:468 <= 0)) \/ mid_i:472 = 0)
           /\ (!(1 <= K:468) \/ mid_i:472 = 1) /\ K:468 = 0
           /\ j:471 = mid_j:470 /\ 0 = mid_i:472 /\ 0 = mid___cost:469
           /\ 0 = K:468
           /\ (!(0 <= K:473)
                 \/ (-__cost':474 + i':475) = ((-mid___cost:469 + mid_i:472)
                                                 + (3/2 * K:473)
                                                 + -(((-mid___cost:469
                                                         + mid_i:472) * K:473))
                                                 + -((mid___cost:469 * K:473))
                                                 + (-1/2 * (K:473 * K:473))))
           /\ (!(0 <= K:473)
                 \/ __cost':474 = (mid___cost:469 + (-1/2 * K:473)
                                     + ((-mid___cost:469 + mid_i:472) * K:473)
                                     + (mid___cost:469 * K:473)
                                     + (1/2 * (K:473 * K:473))))
           /\ (!((0 <= K:473 /\ K:473 <= 0))
                 \/ (-__cost':474 + j':476) = ((-mid___cost:469 + mid_j:470)
                                                 + (3/2 * K:473)
                                                 + -(((-mid___cost:469
                                                         + mid_i:472) * K:473))
                                                 + -((mid___cost:469 * K:473))
                                                 + (-1/2 * (K:473 * K:473))))
           /\ (!(1 <= K:473)
                 \/ (-__cost':474 + j':476) = (-1
                                                 + (-mid___cost:469
                                                      + mid_i:472)
                                                 + (3/2 * K:473)
                                                 + -(((-mid___cost:469
                                                         + mid_i:472) * K:473))
                                                 + -((mid___cost:469 * K:473))
                                                 + (-1/2 * (K:473 * K:473))))
           /\ (!(0 <= K:473)
                 \/ __cost':474 <= (mid___cost:469 + -K:473
                                      + (phi_tmp___0:465 * K:473)))
           /\ (!(0 <= K:473)
                 \/ -__cost':474 <= (-mid___cost:469 + (5/6 * K:473)
                                       + (-3/2
                                            * (-mid___cost:469 + mid_i:472)
                                            * K:473)
                                       + (-1/2 * mid___cost:469 * K:473)
                                       + -((K:473 * K:473))
                                       + (1/2 * (-mid___cost:469 + mid_i:472)
                                            * (K:473 * K:473))
                                       + (1/2 * mid___cost:469
                                            * (K:473 * K:473))
                                       + (1/6 * (K:473 * (K:473 * K:473)))))
           /\ (!(0 <= K:473) \/ -__cost':474 <= -mid___cost:469)
           /\ ((K:473 = 0 /\ mid_j:470 = j':476 /\ mid_i:472 = i':475
                  /\ mid___cost:469 = __cost':474)
                 \/ (1 <= K:473 /\ 0 <= (-1 + -mid_i:472 + phi_tmp___0:465)
                       /\ 0 <= mid_i:472 /\ 0 <= mid___cost:469
                       /\ (1 + -i':475 + j':476) = 0
                       /\ 0 <= (-i':475 + phi_tmp___0:465)
                       /\ 0 <= (-1 + i':475)
                       /\ 0 <= (1 + __cost':474 + -i':475)))
           /\ (0 = K:473 \/ -mid___cost:469 <= 0) /\ (K:468 + K:473) = K:477
           /\ (!((0 <= K:478 /\ K:478 <= 0)) \/ mid_j:479 = j:471)
           /\ (!(1 <= K:478) \/ mid_j:479 = 0)
           /\ (!(0 <= K:478) \/ mid___cost:480 = 0)
           /\ (!((0 <= K:478 /\ K:478 <= 0)) \/ mid_i:481 = 0)
           /\ (!(1 <= K:478) \/ mid_i:481 = 1)
           /\ ((K:478 = 0 /\ j:471 = mid_j:479 /\ 0 = mid_i:481
                  /\ 0 = mid___cost:480)
                 \/ (1 <= K:478 /\ 0 <= (-1 + phi_tmp___0:465)
                       /\ (-1 + mid_i:481) = 0 /\ mid_j:479 = 0
                       /\ 0 <= (-1 + phi_tmp___0:465)))
           /\ (!(0 <= K:482)
                 \/ __cost':474 = (mid___cost:480 + (-1/2 * K:482)
                                     + (mid_i:481 * K:482)
                                     + (1/2 * (K:482 * K:482))))
           /\ (!((0 <= K:482 /\ K:482 <= 0)) \/ j':476 = (mid_j:479 + K:482))
           /\ (!(1 <= K:482)
                 \/ j':476 = (-1 + mid_j:479 + mid_i:481 + -mid_j:479 + K:482))
           /\ (!(0 <= K:482) \/ i':475 = (mid_i:481 + K:482))
           /\ (!(0 <= K:482)
                 \/ __cost':474 <= (mid___cost:480 + -K:482
                                      + (phi_tmp___0:465 * K:482)))
           /\ (!(0 <= K:482) \/ -__cost':474 <= (-mid___cost:480 + -K:482))
           /\ ((K:482 = 0 /\ mid_j:479 = j':476 /\ mid_i:481 = i':475
                  /\ mid___cost:480 = __cost':474)
                 \/ (1 <= K:482 /\ 0 <= (-1 + -mid_i:481 + phi_tmp___0:465)
                       /\ 0 <= mid___cost:480 /\ 0 <= (-1 + mid_i:481)
                       /\ (-1 + -j':476 + i':475) = 0 /\ 0 <= (-1 + j':476)
                       /\ 0 <= (__cost':474 + -j':476)
                       /\ 0 <= (-1 + phi_tmp___0:465 + -j':476)))
           /\ (0 = K:482 \/ (1 + -mid_i:481) <= 0) /\ (K:478 + K:482) = K:477
           /\ 0 <= K:477 /\ 0 <= i':475 /\ phi_tmp___0:465 <= i':475)})


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':434
   return := havoc:443
   return@pos := type_err:444
   return@width := type_err:445
   when ((!(0 <= K:429) \/ mid___cost:430 = __cost:67)
           /\ (!((0 <= K:429 /\ K:429 <= 0)) \/ mid_j:431 = j:460)
           /\ (!(1 <= K:429) \/ mid_j:431 = 0)
           /\ (!((0 <= K:429 /\ K:429 <= 0)) \/ mid_i:432 = 0)
           /\ (!(1 <= K:429) \/ mid_i:432 = 1)
           /\ ((K:429 = 0 /\ j:460 = mid_j:431 /\ 0 = mid_i:432
                  /\ __cost:67 = mid___cost:430)
                 \/ (1 <= K:429 /\ 0 <= (-1 + -__cost:67)
                       /\ 0 <= (-1 + param0:27) /\ (-1 + mid_i:432) = 0
                       /\ mid_j:431 = 0 /\ 0 <= (-1 + -mid___cost:430)
                       /\ 0 <= (-1 + param0:27)))
           /\ (0 = K:429 \/ !(-__cost:67 <= 0))
           /\ (!(0 <= K:433)
                 \/ (-__cost':434 + i':435) = ((-mid___cost:430 + mid_i:432)
                                                 + (3/2 * K:433)
                                                 + -(((-mid___cost:430
                                                         + mid_i:432) * K:433))
                                                 + -((mid___cost:430 * K:433))
                                                 + (-1/2 * (K:433 * K:433))))
           /\ (!(0 <= K:433)
                 \/ __cost':434 = (mid___cost:430 + (-1/2 * K:433)
                                     + ((-mid___cost:430 + mid_i:432) * K:433)
                                     + (mid___cost:430 * K:433)
                                     + (1/2 * (K:433 * K:433))))
           /\ (!((0 <= K:433 /\ K:433 <= 0))
                 \/ (-__cost':434 + j':436) = ((-mid___cost:430 + mid_j:431)
                                                 + (3/2 * K:433)
                                                 + -(((-mid___cost:430
                                                         + mid_i:432) * K:433))
                                                 + -((mid___cost:430 * K:433))
                                                 + (-1/2 * (K:433 * K:433))))
           /\ (!(1 <= K:433)
                 \/ (-__cost':434 + j':436) = (-1
                                                 + (-mid___cost:430
                                                      + mid_i:432)
                                                 + (3/2 * K:433)
                                                 + -(((-mid___cost:430
                                                         + mid_i:432) * K:433))
                                                 + -((mid___cost:430 * K:433))
                                                 + (-1/2 * (K:433 * K:433))))
           /\ (!(0 <= K:433)
                 \/ __cost':434 <= (mid___cost:430 + -K:433
                                      + (param0:27 * K:433)))
           /\ (!(0 <= K:433)
                 \/ -__cost':434 <= (-mid___cost:430 + (5/6 * K:433)
                                       + (-3/2
                                            * (-mid___cost:430 + mid_i:432)
                                            * K:433)
                                       + (-1/2 * mid___cost:430 * K:433)
                                       + -((K:433 * K:433))
                                       + (1/2 * (-mid___cost:430 + mid_i:432)
                                            * (K:433 * K:433))
                                       + (1/2 * mid___cost:430
                                            * (K:433 * K:433))
                                       + (1/6 * (K:433 * (K:433 * K:433)))))
           /\ (!(0 <= K:433) \/ -__cost':434 <= -mid___cost:430)
           /\ ((K:433 = 0 /\ mid_j:431 = j':436 /\ mid_i:432 = i':435
                  /\ mid___cost:430 = __cost':434)
                 \/ (1 <= K:433 /\ 0 <= (-1 + -mid_i:432 + param0:27)
                       /\ 0 <= mid_i:432 /\ 0 <= mid___cost:430
                       /\ (1 + -i':435 + j':436) = 0
                       /\ 0 <= (-i':435 + param0:27) /\ 0 <= (-1 + i':435)
                       /\ 0 <= (1 + __cost':434 + -i':435)))
           /\ (0 = K:433 \/ -mid___cost:430 <= 0) /\ (K:429 + K:433) = K:437
           /\ (!((0 <= K:438 /\ K:438 <= 0)) \/ mid_j:439 = j:460)
           /\ (!(1 <= K:438) \/ mid_j:439 = 0)
           /\ (!(0 <= K:438) \/ mid___cost:440 = __cost:67)
           /\ (!((0 <= K:438 /\ K:438 <= 0)) \/ mid_i:441 = 0)
           /\ (!(1 <= K:438) \/ mid_i:441 = 1)
           /\ ((K:438 = 0 /\ j:460 = mid_j:439 /\ 0 = mid_i:441
                  /\ __cost:67 = mid___cost:440)
                 \/ (1 <= K:438 /\ 0 <= (-1 + param0:27)
                       /\ (-1 + mid_i:441) = 0 /\ mid_j:439 = 0
                       /\ 0 <= (-1 + param0:27)))
           /\ (!(0 <= K:442)
                 \/ __cost':434 = (mid___cost:440 + (-1/2 * K:442)
                                     + (mid_i:441 * K:442)
                                     + (1/2 * (K:442 * K:442))))
           /\ (!((0 <= K:442 /\ K:442 <= 0)) \/ j':436 = (mid_j:439 + K:442))
           /\ (!(1 <= K:442)
                 \/ j':436 = (-1 + mid_j:439 + mid_i:441 + -mid_j:439 + K:442))
           /\ (!(0 <= K:442) \/ i':435 = (mid_i:441 + K:442))
           /\ (!(0 <= K:442)
                 \/ __cost':434 <= (mid___cost:440 + -K:442
                                      + (param0:27 * K:442)))
           /\ (!(0 <= K:442) \/ -__cost':434 <= (-mid___cost:440 + -K:442))
           /\ ((K:442 = 0 /\ mid_j:439 = j':436 /\ mid_i:441 = i':435
                  /\ mid___cost:440 = __cost':434)
                 \/ (1 <= K:442 /\ 0 <= (-1 + -mid_i:441 + param0:27)
                       /\ 0 <= mid___cost:440 /\ 0 <= (-1 + mid_i:441)
                       /\ (-1 + -j':436 + i':435) = 0 /\ 0 <= (-1 + j':436)
                       /\ 0 <= (__cost':434 + -j':436)
                       /\ 0 <= (-1 + param0:27 + -j':436)))
           /\ (0 = K:442 \/ (1 + -mid_i:441) <= 0) /\ (K:438 + K:442) = K:437
           /\ 0 <= K:437 /\ 0 <= i':435 /\ param0:27 <= i':435)})


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':474
 return := 0
 param0 := phi_tmp___0:465
 return@pos := type_err:486
 param0@pos := type_err:466
 return@width := type_err:487
 param0@width := type_err:467
 when (((0 <= tr:358 /\ tr:359 <= 0 /\ 0 = phi_tmp___0:465
           /\ param0:27 = phi_param0:464
           /\ param0@pos:26 = phi_param0@pos:463
           /\ param0@width:25 = phi_param0@width:462)
          \/ ((tr:353 < 0 \/ 0 < tr:354) /\ havoc:461 = phi_tmp___0:465
                /\ tr:355 = phi_param0:464
                /\ type_err:356 = phi_param0@pos:463
                /\ type_err:357 = phi_param0@width:462))
         /\ (!(0 <= K:468) \/ mid___cost:469 = 0)
         /\ (!((0 <= K:468 /\ K:468 <= 0)) \/ mid_j:470 = j:471)
         /\ (!(1 <= K:468) \/ mid_j:470 = 0)
         /\ (!((0 <= K:468 /\ K:468 <= 0)) \/ mid_i:472 = 0)
         /\ (!(1 <= K:468) \/ mid_i:472 = 1) /\ K:468 = 0
         /\ j:471 = mid_j:470 /\ 0 = mid_i:472 /\ 0 = mid___cost:469
         /\ 0 = K:468
         /\ (!(0 <= K:473)
               \/ (-__cost':474 + i':475) = ((-mid___cost:469 + mid_i:472)
                                               + (3/2 * K:473)
                                               + -(((-mid___cost:469
                                                       + mid_i:472) * K:473))
                                               + -((mid___cost:469 * K:473))
                                               + (-1/2 * (K:473 * K:473))))
         /\ (!(0 <= K:473)
               \/ __cost':474 = (mid___cost:469 + (-1/2 * K:473)
                                   + ((-mid___cost:469 + mid_i:472) * K:473)
                                   + (mid___cost:469 * K:473)
                                   + (1/2 * (K:473 * K:473))))
         /\ (!((0 <= K:473 /\ K:473 <= 0))
               \/ (-__cost':474 + j':476) = ((-mid___cost:469 + mid_j:470)
                                               + (3/2 * K:473)
                                               + -(((-mid___cost:469
                                                       + mid_i:472) * K:473))
                                               + -((mid___cost:469 * K:473))
                                               + (-1/2 * (K:473 * K:473))))
         /\ (!(1 <= K:473)
               \/ (-__cost':474 + j':476) = (-1
                                               + (-mid___cost:469 + mid_i:472)
                                               + (3/2 * K:473)
                                               + -(((-mid___cost:469
                                                       + mid_i:472) * K:473))
                                               + -((mid___cost:469 * K:473))
                                               + (-1/2 * (K:473 * K:473))))
         /\ (!(0 <= K:473)
               \/ __cost':474 <= (mid___cost:469 + -K:473
                                    + (phi_tmp___0:465 * K:473)))
         /\ (!(0 <= K:473)
               \/ -__cost':474 <= (-mid___cost:469 + (5/6 * K:473)
                                     + (-3/2 * (-mid___cost:469 + mid_i:472)
                                          * K:473)
                                     + (-1/2 * mid___cost:469 * K:473)
                                     + -((K:473 * K:473))
                                     + (1/2 * (-mid___cost:469 + mid_i:472)
                                          * (K:473 * K:473))
                                     + (1/2 * mid___cost:469
                                          * (K:473 * K:473))
                                     + (1/6 * (K:473 * (K:473 * K:473)))))
         /\ (!(0 <= K:473) \/ -__cost':474 <= -mid___cost:469)
         /\ ((K:473 = 0 /\ mid_j:470 = j':476 /\ mid_i:472 = i':475
                /\ mid___cost:469 = __cost':474)
               \/ (1 <= K:473 /\ 0 <= (-1 + -mid_i:472 + phi_tmp___0:465)
                     /\ 0 <= mid_i:472 /\ 0 <= mid___cost:469
                     /\ (1 + -i':475 + j':476) = 0
                     /\ 0 <= (-i':475 + phi_tmp___0:465)
                     /\ 0 <= (-1 + i':475)
                     /\ 0 <= (1 + __cost':474 + -i':475)))
         /\ (0 = K:473 \/ -mid___cost:469 <= 0) /\ (K:468 + K:473) = K:477
         /\ (!((0 <= K:478 /\ K:478 <= 0)) \/ mid_j:479 = j:471)
         /\ (!(1 <= K:478) \/ mid_j:479 = 0)
         /\ (!(0 <= K:478) \/ mid___cost:480 = 0)
         /\ (!((0 <= K:478 /\ K:478 <= 0)) \/ mid_i:481 = 0)
         /\ (!(1 <= K:478) \/ mid_i:481 = 1)
         /\ ((K:478 = 0 /\ j:471 = mid_j:479 /\ 0 = mid_i:481
                /\ 0 = mid___cost:480)
               \/ (1 <= K:478 /\ 0 <= (-1 + phi_tmp___0:465)
                     /\ (-1 + mid_i:481) = 0 /\ mid_j:479 = 0
                     /\ 0 <= (-1 + phi_tmp___0:465)))
         /\ (!(0 <= K:482)
               \/ __cost':474 = (mid___cost:480 + (-1/2 * K:482)
                                   + (mid_i:481 * K:482)
                                   + (1/2 * (K:482 * K:482))))
         /\ (!((0 <= K:482 /\ K:482 <= 0)) \/ j':476 = (mid_j:479 + K:482))
         /\ (!(1 <= K:482)
               \/ j':476 = (-1 + mid_j:479 + mid_i:481 + -mid_j:479 + K:482))
         /\ (!(0 <= K:482) \/ i':475 = (mid_i:481 + K:482))
         /\ (!(0 <= K:482)
               \/ __cost':474 <= (mid___cost:480 + -K:482
                                    + (phi_tmp___0:465 * K:482)))
         /\ (!(0 <= K:482) \/ -__cost':474 <= (-mid___cost:480 + -K:482))
         /\ ((K:482 = 0 /\ mid_j:479 = j':476 /\ mid_i:481 = i':475
                /\ mid___cost:480 = __cost':474)
               \/ (1 <= K:482 /\ 0 <= (-1 + -mid_i:481 + phi_tmp___0:465)
                     /\ 0 <= mid___cost:480 /\ 0 <= (-1 + mid_i:481)
                     /\ (-1 + -j':476 + i':475) = 0 /\ 0 <= (-1 + j':476)
                     /\ 0 <= (__cost':474 + -j':476)
                     /\ 0 <= (-1 + phi_tmp___0:465 + -j':476)))
         /\ (0 = K:482 \/ (1 + -mid_i:481) <= 0) /\ (K:478 + K:482) = K:477
         /\ 0 <= K:477 /\ 0 <= i':475 /\ phi_tmp___0:465 <= i':475)}

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':434
 return := havoc:443
 return@pos := type_err:444
 return@width := type_err:445
 when ((!(0 <= K:429) \/ mid___cost:430 = __cost:67)
         /\ (!((0 <= K:429 /\ K:429 <= 0)) \/ mid_j:431 = j:460)
         /\ (!(1 <= K:429) \/ mid_j:431 = 0)
         /\ (!((0 <= K:429 /\ K:429 <= 0)) \/ mid_i:432 = 0)
         /\ (!(1 <= K:429) \/ mid_i:432 = 1)
         /\ ((K:429 = 0 /\ j:460 = mid_j:431 /\ 0 = mid_i:432
                /\ __cost:67 = mid___cost:430)
               \/ (1 <= K:429 /\ 0 <= (-1 + -__cost:67)
                     /\ 0 <= (-1 + param0:27) /\ (-1 + mid_i:432) = 0
                     /\ mid_j:431 = 0 /\ 0 <= (-1 + -mid___cost:430)
                     /\ 0 <= (-1 + param0:27)))
         /\ (0 = K:429 \/ !(-__cost:67 <= 0))
         /\ (!(0 <= K:433)
               \/ (-__cost':434 + i':435) = ((-mid___cost:430 + mid_i:432)
                                               + (3/2 * K:433)
                                               + -(((-mid___cost:430
                                                       + mid_i:432) * K:433))
                                               + -((mid___cost:430 * K:433))
                                               + (-1/2 * (K:433 * K:433))))
         /\ (!(0 <= K:433)
               \/ __cost':434 = (mid___cost:430 + (-1/2 * K:433)
                                   + ((-mid___cost:430 + mid_i:432) * K:433)
                                   + (mid___cost:430 * K:433)
                                   + (1/2 * (K:433 * K:433))))
         /\ (!((0 <= K:433 /\ K:433 <= 0))
               \/ (-__cost':434 + j':436) = ((-mid___cost:430 + mid_j:431)
                                               + (3/2 * K:433)
                                               + -(((-mid___cost:430
                                                       + mid_i:432) * K:433))
                                               + -((mid___cost:430 * K:433))
                                               + (-1/2 * (K:433 * K:433))))
         /\ (!(1 <= K:433)
               \/ (-__cost':434 + j':436) = (-1
                                               + (-mid___cost:430 + mid_i:432)
                                               + (3/2 * K:433)
                                               + -(((-mid___cost:430
                                                       + mid_i:432) * K:433))
                                               + -((mid___cost:430 * K:433))
                                               + (-1/2 * (K:433 * K:433))))
         /\ (!(0 <= K:433)
               \/ __cost':434 <= (mid___cost:430 + -K:433
                                    + (param0:27 * K:433)))
         /\ (!(0 <= K:433)
               \/ -__cost':434 <= (-mid___cost:430 + (5/6 * K:433)
                                     + (-3/2 * (-mid___cost:430 + mid_i:432)
                                          * K:433)
                                     + (-1/2 * mid___cost:430 * K:433)
                                     + -((K:433 * K:433))
                                     + (1/2 * (-mid___cost:430 + mid_i:432)
                                          * (K:433 * K:433))
                                     + (1/2 * mid___cost:430
                                          * (K:433 * K:433))
                                     + (1/6 * (K:433 * (K:433 * K:433)))))
         /\ (!(0 <= K:433) \/ -__cost':434 <= -mid___cost:430)
         /\ ((K:433 = 0 /\ mid_j:431 = j':436 /\ mid_i:432 = i':435
                /\ mid___cost:430 = __cost':434)
               \/ (1 <= K:433 /\ 0 <= (-1 + -mid_i:432 + param0:27)
                     /\ 0 <= mid_i:432 /\ 0 <= mid___cost:430
                     /\ (1 + -i':435 + j':436) = 0
                     /\ 0 <= (-i':435 + param0:27) /\ 0 <= (-1 + i':435)
                     /\ 0 <= (1 + __cost':434 + -i':435)))
         /\ (0 = K:433 \/ -mid___cost:430 <= 0) /\ (K:429 + K:433) = K:437
         /\ (!((0 <= K:438 /\ K:438 <= 0)) \/ mid_j:439 = j:460)
         /\ (!(1 <= K:438) \/ mid_j:439 = 0)
         /\ (!(0 <= K:438) \/ mid___cost:440 = __cost:67)
         /\ (!((0 <= K:438 /\ K:438 <= 0)) \/ mid_i:441 = 0)
         /\ (!(1 <= K:438) \/ mid_i:441 = 1)
         /\ ((K:438 = 0 /\ j:460 = mid_j:439 /\ 0 = mid_i:441
                /\ __cost:67 = mid___cost:440)
               \/ (1 <= K:438 /\ 0 <= (-1 + param0:27)
                     /\ (-1 + mid_i:441) = 0 /\ mid_j:439 = 0
                     /\ 0 <= (-1 + param0:27)))
         /\ (!(0 <= K:442)
               \/ __cost':434 = (mid___cost:440 + (-1/2 * K:442)
                                   + (mid_i:441 * K:442)
                                   + (1/2 * (K:442 * K:442))))
         /\ (!((0 <= K:442 /\ K:442 <= 0)) \/ j':436 = (mid_j:439 + K:442))
         /\ (!(1 <= K:442)
               \/ j':436 = (-1 + mid_j:439 + mid_i:441 + -mid_j:439 + K:442))
         /\ (!(0 <= K:442) \/ i':435 = (mid_i:441 + K:442))
         /\ (!(0 <= K:442)
               \/ __cost':434 <= (mid___cost:440 + -K:442
                                    + (param0:27 * K:442)))
         /\ (!(0 <= K:442) \/ -__cost':434 <= (-mid___cost:440 + -K:442))
         /\ ((K:442 = 0 /\ mid_j:439 = j':436 /\ mid_i:441 = i':435
                /\ mid___cost:440 = __cost':434)
               \/ (1 <= K:442 /\ 0 <= (-1 + -mid_i:441 + param0:27)
                     /\ 0 <= mid___cost:440 /\ 0 <= (-1 + mid_i:441)
                     /\ (-1 + -j':436 + i':435) = 0 /\ 0 <= (-1 + j':436)
                     /\ 0 <= (__cost':434 + -j':436)
                     /\ 0 <= (-1 + param0:27 + -j':436)))
         /\ (0 = K:442 \/ (1 + -mid_i:441) <= 0) /\ (K:438 + K:442) = K:437
         /\ 0 <= K:437 /\ 0 <= i':435 /\ param0:27 <= i':435)}

    (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,50)_g1>	Base relation: 
{__cost := 0
 tmp___0 := phi_tmp___0:492
 argv := param1:30
 param0 := phi_tmp___0:492
 argv@pos := param1@pos:29
 param0@pos := type_err:493
 argv@width := param1@width:28
 param0@width := type_err:494
 when ((0 <= tr:358 /\ tr:359 <= 0 /\ 0 = phi_tmp___0:492
          /\ param0:27 = phi_param0:491 /\ param0@pos:26 = phi_param0@pos:490
          /\ param0@width:25 = phi_param0@width:489)
         \/ ((tr:353 < 0 \/ 0 < tr:354) /\ havoc:488 = phi_tmp___0:492
               /\ tr:355 = phi_param0:491
               /\ type_err:356 = phi_param0@pos:490
               /\ type_err:357 = phi_param0@width:489))}	
<__pstate, accept> -> <__pstate, (Unique State Name,62)_g1>	Base relation: 
{__cost := 0
 argv := param1:30
 param0 := tr:355
 argv@pos := param1@pos:29
 param0@pos := type_err:356
 argv@width := param1@width:28
 param0@width := type_err:357
 when (tr:353 < 0 \/ 0 < tr:354)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0xcb86e50: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0xc301f70: 
	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,50)_g1 , __done )	Base relation: 
{__cost := 0
 tmp___0 := phi_tmp___0:492
 argv := param1:30
 param0 := phi_tmp___0:492
 argv@pos := param1@pos:29
 param0@pos := type_err:493
 argv@width := param1@width:28
 param0@width := type_err:494
 when ((0 <= tr:358 /\ tr:359 <= 0 /\ 0 = phi_tmp___0:492
          /\ param0:27 = phi_param0:491 /\ param0@pos:26 = phi_param0@pos:490
          /\ param0@width:25 = phi_param0@width:489)
         \/ ((tr:353 < 0 \/ 0 < tr:354) /\ havoc:488 = phi_tmp___0:492
               /\ tr:355 = phi_param0:491
               /\ type_err:356 = phi_param0@pos:490
               /\ type_err:357 = phi_param0@width:489))}
    ( __pstate , (Unique State Name,62)_g1 , __done )	Base relation: 
{__cost := 0
 argv := param1:30
 param0 := tr:355
 argv@pos := param1@pos:29
 param0@pos := type_err:356
 argv@width := param1@width:28
 param0@width := type_err:357
 when (tr:353 < 0 \/ 0 < tr:354)}

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

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

Base relation: 
{}

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

Base relation: 
{__cost := __cost':501
 tmp___0 := phi_tmp___0:492
 argv := param1:30
 return := 0
 param0 := phi_tmp___0:492
 argv@pos := param1@pos:29
 return@pos := type_err:513
 param0@pos := type_err:493
 argv@width := param1@width:28
 return@width := type_err:514
 param0@width := type_err:494
 when (((0 <= tr:358 /\ tr:359 <= 0 /\ 0 = phi_tmp___0:492
           /\ param0:27 = phi_param0:491
           /\ param0@pos:26 = phi_param0@pos:490
           /\ param0@width:25 = phi_param0@width:489)
          \/ ((tr:353 < 0 \/ 0 < tr:354) /\ havoc:488 = phi_tmp___0:492
                /\ tr:355 = phi_param0:491
                /\ type_err:356 = phi_param0@pos:490
                /\ type_err:357 = phi_param0@width:489))
         /\ (!(0 <= K:495) \/ mid___cost:496 = 0)
         /\ (!((0 <= K:495 /\ K:495 <= 0)) \/ mid_j:497 = j:498)
         /\ (!(1 <= K:495) \/ mid_j:497 = 0)
         /\ (!((0 <= K:495 /\ K:495 <= 0)) \/ mid_i:499 = 0)
         /\ (!(1 <= K:495) \/ mid_i:499 = 1) /\ K:495 = 0
         /\ j:498 = mid_j:497 /\ 0 = mid_i:499 /\ 0 = mid___cost:496
         /\ 0 = K:495
         /\ (!(0 <= K:500)
               \/ (-__cost':501 + i':502) = ((-mid___cost:496 + mid_i:499)
                                               + (3/2 * K:500)
                                               + -(((-mid___cost:496
                                                       + mid_i:499) * K:500))
                                               + -((mid___cost:496 * K:500))
                                               + (-1/2 * (K:500 * K:500))))
         /\ (!(0 <= K:500)
               \/ __cost':501 = (mid___cost:496 + (-1/2 * K:500)
                                   + ((-mid___cost:496 + mid_i:499) * K:500)
                                   + (mid___cost:496 * K:500)
                                   + (1/2 * (K:500 * K:500))))
         /\ (!((0 <= K:500 /\ K:500 <= 0))
               \/ (-__cost':501 + j':503) = ((-mid___cost:496 + mid_j:497)
                                               + (3/2 * K:500)
                                               + -(((-mid___cost:496
                                                       + mid_i:499) * K:500))
                                               + -((mid___cost:496 * K:500))
                                               + (-1/2 * (K:500 * K:500))))
         /\ (!(1 <= K:500)
               \/ (-__cost':501 + j':503) = (-1
                                               + (-mid___cost:496 + mid_i:499)
                                               + (3/2 * K:500)
                                               + -(((-mid___cost:496
                                                       + mid_i:499) * K:500))
                                               + -((mid___cost:496 * K:500))
                                               + (-1/2 * (K:500 * K:500))))
         /\ (!(0 <= K:500)
               \/ __cost':501 <= (mid___cost:496 + -K:500
                                    + (phi_tmp___0:492 * K:500)))
         /\ (!(0 <= K:500)
               \/ -__cost':501 <= (-mid___cost:496 + (5/6 * K:500)
                                     + (-3/2 * (-mid___cost:496 + mid_i:499)
                                          * K:500)
                                     + (-1/2 * mid___cost:496 * K:500)
                                     + -((K:500 * K:500))
                                     + (1/2 * (-mid___cost:496 + mid_i:499)
                                          * (K:500 * K:500))
                                     + (1/2 * mid___cost:496
                                          * (K:500 * K:500))
                                     + (1/6 * (K:500 * (K:500 * K:500)))))
         /\ (!(0 <= K:500) \/ -__cost':501 <= -mid___cost:496)
         /\ ((K:500 = 0 /\ mid_j:497 = j':503 /\ mid_i:499 = i':502
                /\ mid___cost:496 = __cost':501)
               \/ (1 <= K:500 /\ 0 <= (-1 + -mid_i:499 + phi_tmp___0:492)
                     /\ 0 <= mid_i:499 /\ 0 <= mid___cost:496
                     /\ (1 + -i':502 + j':503) = 0
                     /\ 0 <= (-i':502 + phi_tmp___0:492)
                     /\ 0 <= (-1 + i':502)
                     /\ 0 <= (1 + __cost':501 + -i':502)))
         /\ (0 = K:500 \/ -mid___cost:496 <= 0) /\ (K:495 + K:500) = K:504
         /\ (!((0 <= K:505 /\ K:505 <= 0)) \/ mid_j:506 = j:498)
         /\ (!(1 <= K:505) \/ mid_j:506 = 0)
         /\ (!(0 <= K:505) \/ mid___cost:507 = 0)
         /\ (!((0 <= K:505 /\ K:505 <= 0)) \/ mid_i:508 = 0)
         /\ (!(1 <= K:505) \/ mid_i:508 = 1)
         /\ ((K:505 = 0 /\ j:498 = mid_j:506 /\ 0 = mid_i:508
                /\ 0 = mid___cost:507)
               \/ (1 <= K:505 /\ 0 <= (-1 + phi_tmp___0:492)
                     /\ (-1 + mid_i:508) = 0 /\ mid_j:506 = 0
                     /\ 0 <= (-1 + phi_tmp___0:492)))
         /\ (!(0 <= K:509)
               \/ __cost':501 = (mid___cost:507 + (-1/2 * K:509)
                                   + (mid_i:508 * K:509)
                                   + (1/2 * (K:509 * K:509))))
         /\ (!((0 <= K:509 /\ K:509 <= 0)) \/ j':503 = (mid_j:506 + K:509))
         /\ (!(1 <= K:509)
               \/ j':503 = (-1 + mid_j:506 + mid_i:508 + -mid_j:506 + K:509))
         /\ (!(0 <= K:509) \/ i':502 = (mid_i:508 + K:509))
         /\ (!(0 <= K:509)
               \/ __cost':501 <= (mid___cost:507 + -K:509
                                    + (phi_tmp___0:492 * K:509)))
         /\ (!(0 <= K:509) \/ -__cost':501 <= (-mid___cost:507 + -K:509))
         /\ ((K:509 = 0 /\ mid_j:506 = j':503 /\ mid_i:508 = i':502
                /\ mid___cost:507 = __cost':501)
               \/ (1 <= K:509 /\ 0 <= (-1 + -mid_i:508 + phi_tmp___0:492)
                     /\ 0 <= mid___cost:507 /\ 0 <= (-1 + mid_i:508)
                     /\ (-1 + -j':503 + i':502) = 0 /\ 0 <= (-1 + j':503)
                     /\ 0 <= (__cost':501 + -j':503)
                     /\ 0 <= (-1 + phi_tmp___0:492 + -j':503)))
         /\ (0 = K:509 \/ (1 + -mid_i:508) <= 0) /\ (K:505 + K:509) = K:504
         /\ 0 <= K:504 /\ 0 <= i':502 /\ phi_tmp___0:492 <= i':502)}

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

Base relation: 
{__cost := __cost':434
 i := i':435
 j := j':436
 n := param0:27
 return := havoc:443
 return@pos := type_err:444
 return@width := type_err:445
 when ((!(0 <= K:429) \/ mid___cost:430 = __cost:67)
         /\ (!((0 <= K:429 /\ K:429 <= 0)) \/ mid_j:431 = j:66)
         /\ (!(1 <= K:429) \/ mid_j:431 = 0)
         /\ (!((0 <= K:429 /\ K:429 <= 0)) \/ mid_i:432 = 0)
         /\ (!(1 <= K:429) \/ mid_i:432 = 1)
         /\ ((K:429 = 0 /\ j:66 = mid_j:431 /\ 0 = mid_i:432
                /\ __cost:67 = mid___cost:430)
               \/ (1 <= K:429 /\ 0 <= (-1 + -__cost:67)
                     /\ 0 <= (-1 + param0:27) /\ (-1 + mid_i:432) = 0
                     /\ mid_j:431 = 0 /\ 0 <= (-1 + -mid___cost:430)
                     /\ 0 <= (-1 + param0:27)))
         /\ (0 = K:429 \/ !(-__cost:67 <= 0))
         /\ (!(0 <= K:433)
               \/ (-__cost':434 + i':435) = ((-mid___cost:430 + mid_i:432)
                                               + (3/2 * K:433)
                                               + -(((-mid___cost:430
                                                       + mid_i:432) * K:433))
                                               + -((mid___cost:430 * K:433))
                                               + (-1/2 * (K:433 * K:433))))
         /\ (!(0 <= K:433)
               \/ __cost':434 = (mid___cost:430 + (-1/2 * K:433)
                                   + ((-mid___cost:430 + mid_i:432) * K:433)
                                   + (mid___cost:430 * K:433)
                                   + (1/2 * (K:433 * K:433))))
         /\ (!((0 <= K:433 /\ K:433 <= 0))
               \/ (-__cost':434 + j':436) = ((-mid___cost:430 + mid_j:431)
                                               + (3/2 * K:433)
                                               + -(((-mid___cost:430
                                                       + mid_i:432) * K:433))
                                               + -((mid___cost:430 * K:433))
                                               + (-1/2 * (K:433 * K:433))))
         /\ (!(1 <= K:433)
               \/ (-__cost':434 + j':436) = (-1
                                               + (-mid___cost:430 + mid_i:432)
                                               + (3/2 * K:433)
                                               + -(((-mid___cost:430
                                                       + mid_i:432) * K:433))
                                               + -((mid___cost:430 * K:433))
                                               + (-1/2 * (K:433 * K:433))))
         /\ (!(0 <= K:433)
               \/ __cost':434 <= (mid___cost:430 + -K:433
                                    + (param0:27 * K:433)))
         /\ (!(0 <= K:433)
               \/ -__cost':434 <= (-mid___cost:430 + (5/6 * K:433)
                                     + (-3/2 * (-mid___cost:430 + mid_i:432)
                                          * K:433)
                                     + (-1/2 * mid___cost:430 * K:433)
                                     + -((K:433 * K:433))
                                     + (1/2 * (-mid___cost:430 + mid_i:432)
                                          * (K:433 * K:433))
                                     + (1/2 * mid___cost:430
                                          * (K:433 * K:433))
                                     + (1/6 * (K:433 * (K:433 * K:433)))))
         /\ (!(0 <= K:433) \/ -__cost':434 <= -mid___cost:430)
         /\ ((K:433 = 0 /\ mid_j:431 = j':436 /\ mid_i:432 = i':435
                /\ mid___cost:430 = __cost':434)
               \/ (1 <= K:433 /\ 0 <= (-1 + -mid_i:432 + param0:27)
                     /\ 0 <= mid_i:432 /\ 0 <= mid___cost:430
                     /\ (1 + -i':435 + j':436) = 0
                     /\ 0 <= (-i':435 + param0:27) /\ 0 <= (-1 + i':435)
                     /\ 0 <= (1 + __cost':434 + -i':435)))
         /\ (0 = K:433 \/ -mid___cost:430 <= 0) /\ (K:429 + K:433) = K:437
         /\ (!((0 <= K:438 /\ K:438 <= 0)) \/ mid_j:439 = j:66)
         /\ (!(1 <= K:438) \/ mid_j:439 = 0)
         /\ (!(0 <= K:438) \/ mid___cost:440 = __cost:67)
         /\ (!((0 <= K:438 /\ K:438 <= 0)) \/ mid_i:441 = 0)
         /\ (!(1 <= K:438) \/ mid_i:441 = 1)
         /\ ((K:438 = 0 /\ j:66 = mid_j:439 /\ 0 = mid_i:441
                /\ __cost:67 = mid___cost:440)
               \/ (1 <= K:438 /\ 0 <= (-1 + param0:27)
                     /\ (-1 + mid_i:441) = 0 /\ mid_j:439 = 0
                     /\ 0 <= (-1 + param0:27)))
         /\ (!(0 <= K:442)
               \/ __cost':434 = (mid___cost:440 + (-1/2 * K:442)
                                   + (mid_i:441 * K:442)
                                   + (1/2 * (K:442 * K:442))))
         /\ (!((0 <= K:442 /\ K:442 <= 0)) \/ j':436 = (mid_j:439 + K:442))
         /\ (!(1 <= K:442)
               \/ j':436 = (-1 + mid_j:439 + mid_i:441 + -mid_j:439 + K:442))
         /\ (!(0 <= K:442) \/ i':435 = (mid_i:441 + K:442))
         /\ (!(0 <= K:442)
               \/ __cost':434 <= (mid___cost:440 + -K:442
                                    + (param0:27 * K:442)))
         /\ (!(0 <= K:442) \/ -__cost':434 <= (-mid___cost:440 + -K:442))
         /\ ((K:442 = 0 /\ mid_j:439 = j':436 /\ mid_i:441 = i':435
                /\ mid___cost:440 = __cost':434)
               \/ (1 <= K:442 /\ 0 <= (-1 + -mid_i:441 + param0:27)
                     /\ 0 <= mid___cost:440 /\ 0 <= (-1 + mid_i:441)
                     /\ (-1 + -j':436 + i':435) = 0 /\ 0 <= (-1 + j':436)
                     /\ 0 <= (__cost':434 + -j':436)
                     /\ 0 <= (-1 + param0:27 + -j':436)))
         /\ (0 = K:442 \/ (1 + -mid_i:441) <= 0) /\ (K:438 + K:442) = K:437
         /\ 0 <= K:437 /\ 0 <= i':435 /\ param0:27 <= i':435)}

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

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

Variable bounds at line 9 in work

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

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