/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 n:65 <= j:66}	
<Unique State Name, 31> -> <Unique State Name, 27>	Base relation: 
{__cost := (__cost:67 + 1)
 j := (j:66 + 1)
 when (j:66 < n:65 /\ 0 <= __cost:67 /\ 0 <= (__cost:67 + 1))}	
<Unique State Name, 27> -> <Unique State Name, 63>	Base relation: 
{when (1 <= n:65 /\ 0 <= j:66 /\ 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 (1 <= n:65 /\ 0 <= j:66 /\ i:64 < n:65 /\ j:66 < n:65 /\ 0 <= __cost:67
         /\ 0 <= (__cost:67 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':334) = (1)*(__cost:67) + 1
           (j':335) = (1)*(j:66) + 1
           }
          pre:
            [|__cost:67>=0; j:66>=0; n:65-i:64-1>=0; n:65-j:66-1>=0|]
          post:
            [|j':335-1>=0; __cost':334-1>=0; n:65-i:64-1>=0; n:65-j':335>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':334
   j := j':335
   when ((!(0 <= K:345) \/ mid___cost:348 = (__cost:67 + K:345))
           /\ (!(0 <= K:345) \/ mid_j:347 = (j:66 + K:345))
           /\ ((K:345 = 0 /\ j:66 = mid_j:347 /\ __cost:67 = mid___cost:348)
                 \/ (1 <= K:345 /\ 0 <= __cost:67 /\ 0 <= j:66
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (-1 + n:65 + -j:66) /\ 0 <= (-1 + mid_j:347)
                       /\ 0 <= (-1 + mid___cost:348)
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (n:65 + -mid_j:347))) /\ K:346 = 0
           /\ mid_j:347 = j':335 /\ mid___cost:348 = __cost':334 /\ 0 = K:346
           /\ (K:345 + K:346) = K:344 /\ 0 <= K:344)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':361
 i := (i:64 + 1)
 j := j':360
 when (0 <= i:64 /\ i:64 < n:65
         /\ (!(0 <= K:356) \/ mid___cost:357 = (__cost:67 + K:356))
         /\ (!(0 <= K:356) \/ mid_j:358 = K:356)
         /\ ((K:356 = 0 /\ 0 = mid_j:358 /\ __cost:67 = mid___cost:357)
               \/ (1 <= K:356 /\ 0 <= __cost:67 /\ 0 <= (-1 + n:65 + -i:64)
                     /\ 0 <= (-1 + n:65) /\ 0 <= (-1 + mid_j:358)
                     /\ 0 <= (-1 + mid___cost:357)
                     /\ 0 <= (-1 + n:65 + -i:64) /\ 0 <= (n:65 + -mid_j:358)))
         /\ K:359 = 0 /\ mid_j:358 = j':360 /\ mid___cost:357 = __cost':361
         /\ 0 = K:359 /\ (K:356 + K:359) = K:362 /\ 0 <= K:362 /\ 1 <= n:65
         /\ 0 <= j':360 /\ i:64 < n:65 /\ n:65 <= j':360)}
**** alpha hat: 
  {<Split [true
            (i':363) = (1)*(i:64) + 1
           (__cost':334) = (1)*(__cost:67) + n:65
           (j':335) = n:65
           (-__cost':334) <= (1)*(-__cost:67) + (-1)*1 + (-1)*i:64
           }
          pre:
            [|-i:64+n:65-1>=0; __cost:67>=0; i:64>=0|]
          post:
            [|-n:65+j':335=0; -n:65+__cost':334>=0; i':363-1>=0;
              n:65-i':363>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':334
   i := i':363
   j := j':335
   when ((!(0 <= K:375) \/ mid_i:378 = (i:64 + K:375))
           /\ (!(0 <= K:375) \/ mid___cost:379 = (__cost:67 + (n:65 * K:375)))
           /\ (!((0 <= K:375 /\ K:375 <= 0)) \/ mid_j:377 = j:66)
           /\ (!(1 <= K:375) \/ mid_j:377 = n:65)
           /\ (!(0 <= K:375)
                 \/ -mid___cost:379 <= (-__cost:67 + (-1/2 * K:375)
                                          + -((i:64 * K:375))
                                          + (-1/2 * (K:375 * K:375))))
           /\ ((K:375 = 0 /\ j:66 = mid_j:377 /\ i:64 = mid_i:378
                  /\ __cost:67 = mid___cost:379)
                 \/ (1 <= K:375 /\ 0 <= (-1 + -i:64 + n:65) /\ 0 <= __cost:67
                       /\ 0 <= i:64 /\ (-n:65 + mid_j:377) = 0
                       /\ 0 <= (-n:65 + mid___cost:379)
                       /\ 0 <= (-1 + mid_i:378) /\ 0 <= (n:65 + -mid_i:378)))
           /\ K:376 = 0 /\ mid_j:377 = j':335 /\ mid_i:378 = i':363
           /\ mid___cost:379 = __cost':334 /\ 0 = K:376
           /\ (K:375 + K:376) = K:374 /\ 0 <= K:374)}
}
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:332 /\ tr:333 <= 0)}        )
        ,
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := 0
               argv := param1:30
               param0 := tr:329
               argv@pos := param1@pos:29
               param0@pos := type_err:330
               argv@width := param1@width:28
               param0@width := type_err:331
               when (tr:327 < 0 \/ 0 < tr:328)}            )
            ,
            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':387
   i := i':386
   j := j':385
   n := param0:27
   return := havoc:389
   return@pos := type_err:390
   return@width := type_err:391
   when ((!(0 <= K:380) \/ mid_i:381 = K:380)
           /\ (!(0 <= K:380)
                 \/ mid___cost:382 = (__cost:67 + (param0:27 * K:380)))
           /\ (!((0 <= K:380 /\ K:380 <= 0)) \/ mid_j:383 = j:66)
           /\ (!(1 <= K:380) \/ mid_j:383 = param0:27)
           /\ (!(0 <= K:380)
                 \/ -mid___cost:382 <= (-__cost:67 + (-1/2 * K:380)
                                          + (-1/2 * (K:380 * K:380))))
           /\ ((K:380 = 0 /\ j:66 = mid_j:383 /\ 0 = mid_i:381
                  /\ __cost:67 = mid___cost:382)
                 \/ (1 <= K:380 /\ 0 <= (-1 + param0:27) /\ 0 <= __cost:67
                       /\ (-param0:27 + mid_j:383) = 0
                       /\ 0 <= (-param0:27 + mid___cost:382)
                       /\ 0 <= (-1 + mid_i:381)
                       /\ 0 <= (param0:27 + -mid_i:381))) /\ K:384 = 0
           /\ mid_j:383 = j':385 /\ mid_i:381 = i':386
           /\ mid___cost:382 = __cost':387 /\ 0 = K:384
           /\ (K:380 + K:384) = K:388 /\ 0 <= K:388 /\ 0 <= i':386
           /\ param0:27 <= i':386)})



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:332 /\ tr:333 <= 0)}          )
          ,
          Dot(
            Dot(
              Weight(Base relation: 
                {__cost := 0
                 argv := param1:30
                 param0 := tr:329
                 argv@pos := param1@pos:29
                 param0@pos := type_err:330
                 argv@width := param1@width:28
                 param0@width := type_err:331
                 when (tr:327 < 0 \/ 0 < tr:328)}              )
              ,
              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':387
   return := havoc:389
   return@pos := type_err:390
   return@width := type_err:391
   when ((!(0 <= K:380) \/ mid_i:381 = K:380)
           /\ (!(0 <= K:380)
                 \/ mid___cost:382 = (__cost:67 + (param0:27 * K:380)))
           /\ (!((0 <= K:380 /\ K:380 <= 0)) \/ mid_j:383 = j:406)
           /\ (!(1 <= K:380) \/ mid_j:383 = param0:27)
           /\ (!(0 <= K:380)
                 \/ -mid___cost:382 <= (-__cost:67 + (-1/2 * K:380)
                                          + (-1/2 * (K:380 * K:380))))
           /\ ((K:380 = 0 /\ j:406 = mid_j:383 /\ 0 = mid_i:381
                  /\ __cost:67 = mid___cost:382)
                 \/ (1 <= K:380 /\ 0 <= (-1 + param0:27) /\ 0 <= __cost:67
                       /\ (-param0:27 + mid_j:383) = 0
                       /\ 0 <= (-param0:27 + mid___cost:382)
                       /\ 0 <= (-1 + mid_i:381)
                       /\ 0 <= (param0:27 + -mid_i:381))) /\ K:384 = 0
           /\ mid_j:383 = j':385 /\ mid_i:381 = i':386
           /\ mid___cost:382 = __cost':387 /\ 0 = K:384
           /\ (K:380 + K:384) = K:388 /\ 0 <= K:388 /\ 0 <= i':386
           /\ param0:27 <= i':386)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=11: 
Weight(Base relation: 
  {__cost := __cost':422
   return := 0
   param0 := phi_tmp___0:411
   return@pos := type_err:427
   param0@pos := type_err:412
   return@width := type_err:428
   param0@width := type_err:413
   when (((0 <= tr:332 /\ tr:333 <= 0 /\ 0 = phi_tmp___0:411
             /\ param0:27 = phi_param0:410
             /\ param0@pos:26 = phi_param0@pos:409
             /\ param0@width:25 = phi_param0@width:408)
            \/ ((tr:327 < 0 \/ 0 < tr:328) /\ havoc:407 = phi_tmp___0:411
                  /\ tr:329 = phi_param0:410
                  /\ type_err:330 = phi_param0@pos:409
                  /\ type_err:331 = phi_param0@width:408))
           /\ (!(0 <= K:414) \/ mid_i:415 = K:414)
           /\ (!(0 <= K:414) \/ mid___cost:416 = (phi_tmp___0:411 * K:414))
           /\ (!((0 <= K:414 /\ K:414 <= 0)) \/ mid_j:417 = j:418)
           /\ (!(1 <= K:414) \/ mid_j:417 = phi_tmp___0:411)
           /\ (!(0 <= K:414)
                 \/ -mid___cost:416 <= ((-1/2 * K:414)
                                          + (-1/2 * (K:414 * K:414))))
           /\ ((K:414 = 0 /\ j:418 = mid_j:417 /\ 0 = mid_i:415
                  /\ 0 = mid___cost:416)
                 \/ (1 <= K:414 /\ 0 <= (-1 + phi_tmp___0:411)
                       /\ (-phi_tmp___0:411 + mid_j:417) = 0
                       /\ 0 <= (-phi_tmp___0:411 + mid___cost:416)
                       /\ 0 <= (-1 + mid_i:415)
                       /\ 0 <= (phi_tmp___0:411 + -mid_i:415))) /\ K:419 = 0
           /\ mid_j:417 = j':420 /\ mid_i:415 = i':421
           /\ mid___cost:416 = __cost':422 /\ 0 = K:419
           /\ (K:414 + K:419) = K:423 /\ 0 <= K:423 /\ 0 <= i':421
           /\ phi_tmp___0:411 <= i':421)})


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':387
   return := havoc:389
   return@pos := type_err:390
   return@width := type_err:391
   when ((!(0 <= K:380) \/ mid_i:381 = K:380)
           /\ (!(0 <= K:380)
                 \/ mid___cost:382 = (__cost:67 + (param0:27 * K:380)))
           /\ (!((0 <= K:380 /\ K:380 <= 0)) \/ mid_j:383 = j:406)
           /\ (!(1 <= K:380) \/ mid_j:383 = param0:27)
           /\ (!(0 <= K:380)
                 \/ -mid___cost:382 <= (-__cost:67 + (-1/2 * K:380)
                                          + (-1/2 * (K:380 * K:380))))
           /\ ((K:380 = 0 /\ j:406 = mid_j:383 /\ 0 = mid_i:381
                  /\ __cost:67 = mid___cost:382)
                 \/ (1 <= K:380 /\ 0 <= (-1 + param0:27) /\ 0 <= __cost:67
                       /\ (-param0:27 + mid_j:383) = 0
                       /\ 0 <= (-param0:27 + mid___cost:382)
                       /\ 0 <= (-1 + mid_i:381)
                       /\ 0 <= (param0:27 + -mid_i:381))) /\ K:384 = 0
           /\ mid_j:383 = j':385 /\ mid_i:381 = i':386
           /\ mid___cost:382 = __cost':387 /\ 0 = K:384
           /\ (K:380 + K:384) = K:388 /\ 0 <= K:388 /\ 0 <= i':386
           /\ param0:27 <= i':386)})


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':422
 return := 0
 param0 := phi_tmp___0:411
 return@pos := type_err:427
 param0@pos := type_err:412
 return@width := type_err:428
 param0@width := type_err:413
 when (((0 <= tr:332 /\ tr:333 <= 0 /\ 0 = phi_tmp___0:411
           /\ param0:27 = phi_param0:410
           /\ param0@pos:26 = phi_param0@pos:409
           /\ param0@width:25 = phi_param0@width:408)
          \/ ((tr:327 < 0 \/ 0 < tr:328) /\ havoc:407 = phi_tmp___0:411
                /\ tr:329 = phi_param0:410
                /\ type_err:330 = phi_param0@pos:409
                /\ type_err:331 = phi_param0@width:408))
         /\ (!(0 <= K:414) \/ mid_i:415 = K:414)
         /\ (!(0 <= K:414) \/ mid___cost:416 = (phi_tmp___0:411 * K:414))
         /\ (!((0 <= K:414 /\ K:414 <= 0)) \/ mid_j:417 = j:418)
         /\ (!(1 <= K:414) \/ mid_j:417 = phi_tmp___0:411)
         /\ (!(0 <= K:414)
               \/ -mid___cost:416 <= ((-1/2 * K:414)
                                        + (-1/2 * (K:414 * K:414))))
         /\ ((K:414 = 0 /\ j:418 = mid_j:417 /\ 0 = mid_i:415
                /\ 0 = mid___cost:416)
               \/ (1 <= K:414 /\ 0 <= (-1 + phi_tmp___0:411)
                     /\ (-phi_tmp___0:411 + mid_j:417) = 0
                     /\ 0 <= (-phi_tmp___0:411 + mid___cost:416)
                     /\ 0 <= (-1 + mid_i:415)
                     /\ 0 <= (phi_tmp___0:411 + -mid_i:415))) /\ K:419 = 0
         /\ mid_j:417 = j':420 /\ mid_i:415 = i':421
         /\ mid___cost:416 = __cost':422 /\ 0 = K:419
         /\ (K:414 + K:419) = K:423 /\ 0 <= K:423 /\ 0 <= i':421
         /\ phi_tmp___0:411 <= i':421)}

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':387
 return := havoc:389
 return@pos := type_err:390
 return@width := type_err:391
 when ((!(0 <= K:380) \/ mid_i:381 = K:380)
         /\ (!(0 <= K:380)
               \/ mid___cost:382 = (__cost:67 + (param0:27 * K:380)))
         /\ (!((0 <= K:380 /\ K:380 <= 0)) \/ mid_j:383 = j:406)
         /\ (!(1 <= K:380) \/ mid_j:383 = param0:27)
         /\ (!(0 <= K:380)
               \/ -mid___cost:382 <= (-__cost:67 + (-1/2 * K:380)
                                        + (-1/2 * (K:380 * K:380))))
         /\ ((K:380 = 0 /\ j:406 = mid_j:383 /\ 0 = mid_i:381
                /\ __cost:67 = mid___cost:382)
               \/ (1 <= K:380 /\ 0 <= (-1 + param0:27) /\ 0 <= __cost:67
                     /\ (-param0:27 + mid_j:383) = 0
                     /\ 0 <= (-param0:27 + mid___cost:382)
                     /\ 0 <= (-1 + mid_i:381)
                     /\ 0 <= (param0:27 + -mid_i:381))) /\ K:384 = 0
         /\ mid_j:383 = j':385 /\ mid_i:381 = i':386
         /\ mid___cost:382 = __cost':387 /\ 0 = K:384
         /\ (K:380 + K:384) = K:388 /\ 0 <= K:388 /\ 0 <= i':386
         /\ param0:27 <= i':386)}

    (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:433
 argv := param1:30
 param0 := phi_tmp___0:433
 argv@pos := param1@pos:29
 param0@pos := type_err:434
 argv@width := param1@width:28
 param0@width := type_err:435
 when ((0 <= tr:332 /\ tr:333 <= 0 /\ 0 = phi_tmp___0:433
          /\ param0:27 = phi_param0:432 /\ param0@pos:26 = phi_param0@pos:431
          /\ param0@width:25 = phi_param0@width:430)
         \/ ((tr:327 < 0 \/ 0 < tr:328) /\ havoc:429 = phi_tmp___0:433
               /\ tr:329 = phi_param0:432
               /\ type_err:330 = phi_param0@pos:431
               /\ type_err:331 = phi_param0@width:430))}	
<__pstate, accept> -> <__pstate, (Unique State Name,62)_g1>	Base relation: 
{__cost := 0
 argv := param1:30
 param0 := tr:329
 argv@pos := param1@pos:29
 param0@pos := type_err:330
 argv@width := param1@width:28
 param0@width := type_err:331
 when (tr:327 < 0 \/ 0 < tr:328)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0xcdbb450: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0xcde97d0: 
	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:433
 argv := param1:30
 param0 := phi_tmp___0:433
 argv@pos := param1@pos:29
 param0@pos := type_err:434
 argv@width := param1@width:28
 param0@width := type_err:435
 when ((0 <= tr:332 /\ tr:333 <= 0 /\ 0 = phi_tmp___0:433
          /\ param0:27 = phi_param0:432 /\ param0@pos:26 = phi_param0@pos:431
          /\ param0@width:25 = phi_param0@width:430)
         \/ ((tr:327 < 0 \/ 0 < tr:328) /\ havoc:429 = phi_tmp___0:433
               /\ tr:329 = phi_param0:432
               /\ type_err:330 = phi_param0@pos:431
               /\ type_err:331 = phi_param0@width:430))}
    ( __pstate , (Unique State Name,62)_g1 , __done )	Base relation: 
{__cost := 0
 argv := param1:30
 param0 := tr:329
 argv@pos := param1@pos:29
 param0@pos := type_err:330
 argv@width := param1@width:28
 param0@width := type_err:331
 when (tr:327 < 0 \/ 0 < tr:328)}

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

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

Base relation: 
{}

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

Base relation: 
{__cost := __cost':444
 tmp___0 := phi_tmp___0:433
 argv := param1:30
 return := 0
 param0 := phi_tmp___0:433
 argv@pos := param1@pos:29
 return@pos := type_err:449
 param0@pos := type_err:434
 argv@width := param1@width:28
 return@width := type_err:450
 param0@width := type_err:435
 when (((0 <= tr:332 /\ tr:333 <= 0 /\ 0 = phi_tmp___0:433
           /\ param0:27 = phi_param0:432
           /\ param0@pos:26 = phi_param0@pos:431
           /\ param0@width:25 = phi_param0@width:430)
          \/ ((tr:327 < 0 \/ 0 < tr:328) /\ havoc:429 = phi_tmp___0:433
                /\ tr:329 = phi_param0:432
                /\ type_err:330 = phi_param0@pos:431
                /\ type_err:331 = phi_param0@width:430))
         /\ (!(0 <= K:436) \/ mid_i:437 = K:436)
         /\ (!(0 <= K:436) \/ mid___cost:438 = (phi_tmp___0:433 * K:436))
         /\ (!((0 <= K:436 /\ K:436 <= 0)) \/ mid_j:439 = j:440)
         /\ (!(1 <= K:436) \/ mid_j:439 = phi_tmp___0:433)
         /\ (!(0 <= K:436)
               \/ -mid___cost:438 <= ((-1/2 * K:436)
                                        + (-1/2 * (K:436 * K:436))))
         /\ ((K:436 = 0 /\ j:440 = mid_j:439 /\ 0 = mid_i:437
                /\ 0 = mid___cost:438)
               \/ (1 <= K:436 /\ 0 <= (-1 + phi_tmp___0:433)
                     /\ (-phi_tmp___0:433 + mid_j:439) = 0
                     /\ 0 <= (-phi_tmp___0:433 + mid___cost:438)
                     /\ 0 <= (-1 + mid_i:437)
                     /\ 0 <= (phi_tmp___0:433 + -mid_i:437))) /\ K:441 = 0
         /\ mid_j:439 = j':442 /\ mid_i:437 = i':443
         /\ mid___cost:438 = __cost':444 /\ 0 = K:441
         /\ (K:436 + K:441) = K:445 /\ 0 <= K:445 /\ 0 <= i':443
         /\ phi_tmp___0:433 <= i':443)}

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

Base relation: 
{__cost := __cost':387
 i := i':386
 j := j':385
 n := param0:27
 return := havoc:389
 return@pos := type_err:390
 return@width := type_err:391
 when ((!(0 <= K:380) \/ mid_i:381 = K:380)
         /\ (!(0 <= K:380)
               \/ mid___cost:382 = (__cost:67 + (param0:27 * K:380)))
         /\ (!((0 <= K:380 /\ K:380 <= 0)) \/ mid_j:383 = j:66)
         /\ (!(1 <= K:380) \/ mid_j:383 = param0:27)
         /\ (!(0 <= K:380)
               \/ -mid___cost:382 <= (-__cost:67 + (-1/2 * K:380)
                                        + (-1/2 * (K:380 * K:380))))
         /\ ((K:380 = 0 /\ j:66 = mid_j:383 /\ 0 = mid_i:381
                /\ __cost:67 = mid___cost:382)
               \/ (1 <= K:380 /\ 0 <= (-1 + param0:27) /\ 0 <= __cost:67
                     /\ (-param0:27 + mid_j:383) = 0
                     /\ 0 <= (-param0:27 + mid___cost:382)
                     /\ 0 <= (-1 + mid_i:381)
                     /\ 0 <= (param0:27 + -mid_i:381))) /\ K:384 = 0
         /\ mid_j:383 = j':385 /\ mid_i:381 = i':386
         /\ mid___cost:382 = __cost':387 /\ 0 = K:384
         /\ (K:380 + K:384) = K:388 /\ 0 <= K:388 /\ 0 <= i':386
         /\ param0:27 <= i':386)}

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

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

Variable bounds at line 9 in work

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

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