/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, 74> -> <Unique State Name, 16>	Base relation: 
{__cost := 0
 argc := param0:29
 argv := param1:32
 argv@pos := param1@pos:31
 argv@width := param1@width:30}	
<Unique State Name, 39> -> <Unique State Name, 79>	Base relation: 
{when (1 <= n:100 /\ 0 <= t:102 /\ 1000 <= __cost:101 /\ i:99 < n:100
         /\ 0 <= __cost:101 /\ 0 <= (__cost:101 + 1000)
         /\ 0 <= (__cost:101 + 1))}	
<Unique State Name, 62> -> <Unique State Name, 27>	Base relation: 
{i := 0
 n := param0:29}	
<Unique State Name, 31> -> <Unique State Name, 39>	Base relation: 
{__cost := (__cost:101 + 1000)
 t := 0
 when (i:99 < n:100 /\ 0 <= __cost:101 /\ 0 <= (__cost:101 + 1000))}	
<Unique State Name, 31> -> <Unique State Name, 58>	Base relation: 
{when n:100 <= i:99}	
<Unique State Name, 66> -> <Unique State Name, 78 65>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 69> -> <Unique State Name, 73>	Base relation: 
{param0 := havoc:16
 param0@pos := type_err:39
 param0@width := type_err:40}	
<Unique State Name, 65> -> <Unique State Name, 9>	Base relation: 
{tmp := havoc:10}	
<Unique State Name, 70> -> <Unique State Name, 78 69>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 43> -> <Unique State Name, 27>	Base relation: 
{i := (i:99 + 1)
 when n:100 <= t:102}	
<Unique State Name, 43> -> <Unique State Name, 39>	Base relation: 
{__cost := (__cost:101 + 1)
 t := (t:102 + 1)
 when (t:102 < n:100 /\ 0 <= __cost:101 /\ 0 <= (__cost:101 + 1))}	
<Unique State Name, 24> -> <Unique State Name, 77>	Base relation: 
{return := __retres5:5
 return@pos := type_err:8
 return@width := type_err:9}	
<Unique State Name, 27> -> <Unique State Name, 80>	Base relation: 
{when 0 <= i:99}	
<Unique State Name, 76> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 77> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 73> -> <Unique State Name, 62 72>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 80> -> <Unique State Name, 31>	Base relation: 
{}	
<Unique State Name, 58> -> <Unique State Name, 76>	Base relation: 
{return := havoc:103
 return@pos := type_err:106
 return@width := type_err:107}	
<Unique State Name, 72> -> <Unique State Name, 24>	Base relation: 
{__retres5 := 0}	
<Unique State Name, 79> -> <Unique State Name, 43>	Base relation: 
{}	
<Unique State Name, 16> -> <Unique State Name, 24>	Base relation: 
{__retres5 := -1
 when (argc:4 < 2 \/ 2 < argc:4)}	
<Unique State Name, 16> -> <Unique State Name, 66>	Base relation: 
{param0 := tr:33
 param0@pos := type_err:34
 param0@width := type_err:35
 when (2 <= argc:4 /\ argc:4 <= 2)}	
<Unique State Name, 78> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 9> -> <Unique State Name, 24>	Base relation: 
{__retres5 := -1
 when 99 < tmp:3}	
<Unique State Name, 9> -> <Unique State Name, 70>	Base relation: 
{param0 := tr:36
 param0@pos := type_err:37
 param0@width := type_err:38
 when tmp:3 <= 99}	
#################################################################
           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:101 + 1)
 t := (t:102 + 1)
 when (1 <= n:100 /\ 0 <= t:102 /\ 1000 <= __cost:101 /\ i:99 < n:100
         /\ 0 <= __cost:101 /\ 0 <= (__cost:101 + 1000)
         /\ 0 <= (__cost:101 + 1) /\ t:102 < n:100 /\ 0 <= __cost:101
         /\ 0 <= (__cost:101 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':433) = (1)*(__cost:101) + 1
           (t':434) = (1)*(t:102) + 1
           }
          pre:
            [|__cost:101-1000>=0; t:102>=0; n:100-i:99-1>=0; n:100-t:102-1>=0|]
          post:
            [|t':434-1>=0; __cost':433-1001>=0; n:100-i:99-1>=0;
              n:100-t':434>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':433
   t := t':434
   when ((!(0 <= K:444) \/ mid___cost:447 = (__cost:101 + K:444))
           /\ (!(0 <= K:444) \/ mid_t:446 = (t:102 + K:444))
           /\ ((K:444 = 0 /\ t:102 = mid_t:446 /\ __cost:101 = mid___cost:447)
                 \/ (1 <= K:444 /\ 0 <= (-1000 + __cost:101) /\ 0 <= t:102
                       /\ 0 <= (-1 + n:100 + -i:99)
                       /\ 0 <= (-1 + n:100 + -t:102) /\ 0 <= (-1 + mid_t:446)
                       /\ 0 <= (-1001 + mid___cost:447)
                       /\ 0 <= (-1 + n:100 + -i:99)
                       /\ 0 <= (n:100 + -mid_t:446))) /\ K:445 = 0
           /\ mid_t:446 = t':434 /\ mid___cost:447 = __cost':433 /\ 0 = K:445
           /\ (K:444 + K:445) = K:443 /\ 0 <= K:443)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':460
 i := (i:99 + 1)
 t := t':459
 when (0 <= i:99 /\ i:99 < n:100 /\ 0 <= __cost:101
         /\ 0 <= (__cost:101 + 1000)
         /\ (!(0 <= K:455) \/ mid___cost:456 = ((__cost:101 + 1000) + K:455))
         /\ (!(0 <= K:455) \/ mid_t:457 = K:455)
         /\ ((K:455 = 0 /\ 0 = mid_t:457
                /\ (__cost:101 + 1000) = mid___cost:456)
               \/ (1 <= K:455 /\ 0 <= (-1000 + (__cost:101 + 1000))
                     /\ 0 <= (-1 + n:100 + -i:99) /\ 0 <= (-1 + n:100)
                     /\ 0 <= (-1 + mid_t:457)
                     /\ 0 <= (-1001 + mid___cost:456)
                     /\ 0 <= (-1 + n:100 + -i:99)
                     /\ 0 <= (n:100 + -mid_t:457))) /\ K:458 = 0
         /\ mid_t:457 = t':459 /\ mid___cost:456 = __cost':460 /\ 0 = K:458
         /\ (K:455 + K:458) = K:461 /\ 0 <= K:461 /\ 1 <= n:100
         /\ 0 <= t':459 /\ 1000 <= __cost':460 /\ i:99 < n:100
         /\ 0 <= __cost':460 /\ 0 <= (__cost':460 + 1000)
         /\ 0 <= (__cost':460 + 1) /\ n:100 <= t':459)}
**** alpha hat: 
  {<Split [true
            (t':434) = n:100
           (i':462) = (1)*(i:99) + 1
           (__cost':433) = (1)*(__cost:101) + 1000*1 + n:100
           (-__cost':433) <= (1)*(-__cost:101) + (-1001)*1 + (-1)*i:99
           }
          pre:
            [|-i:99+n:100-1>=0; __cost:101>=0; i:99>=0|]
          post:
            [|-n:100+t':434=0; -n:100+__cost':433-1000>=0; i':462-1>=0;
              n:100-i':462>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':433
   i := i':462
   t := t':434
   when ((!((0 <= K:474 /\ K:474 <= 0)) \/ mid_t:476 = t:102)
           /\ (!(1 <= K:474) \/ mid_t:476 = n:100)
           /\ (!(0 <= K:474) \/ mid_i:477 = (i:99 + K:474))
           /\ (!(0 <= K:474)
                 \/ mid___cost:478 = (__cost:101 + (1000 * K:474)
                                        + (n:100 * K:474)))
           /\ (!(0 <= K:474)
                 \/ -mid___cost:478 <= (-__cost:101 + (-2001/2 * K:474)
                                          + -((i:99 * K:474))
                                          + (-1/2 * (K:474 * K:474))))
           /\ ((K:474 = 0 /\ t:102 = mid_t:476 /\ i:99 = mid_i:477
                  /\ __cost:101 = mid___cost:478)
                 \/ (1 <= K:474 /\ 0 <= (-1 + -i:99 + n:100)
                       /\ 0 <= __cost:101 /\ 0 <= i:99
                       /\ (-n:100 + mid_t:476) = 0
                       /\ 0 <= (-1000 + -n:100 + mid___cost:478)
                       /\ 0 <= (-1 + mid_i:477) /\ 0 <= (n:100 + -mid_i:477)))
           /\ K:475 = 0 /\ mid_t:476 = t':434 /\ mid_i:477 = i':462
           /\ mid___cost:478 = __cost':433 /\ 0 = K:475
           /\ (K:474 + K:475) = K:473 /\ 0 <= K:473)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
15  17  25  


New-style (IRE) regular expression in IREregExpMap for reID=15: 
Dot(
  Plus(
    Plus(
      Weight(Base relation: 
        {__cost := 0
         __retres5 := -1
         argc := param0:29
         argv := param1:32
         argv@pos := param1@pos:31
         argv@width := param1@width:30
         when (param0:29 < 2 \/ 2 < param0:29)}      )
      ,
      Dot(
        Dot(
          Weight(Base relation: 
            {__cost := 0
             argc := param0:29
             argv := param1:32
             param0 := tr:427
             argv@pos := param1@pos:31
             param0@pos := type_err:428
             argv@width := param1@width:30
             param0@width := type_err:429
             when (2 <= param0:29 /\ param0:29 <= 2)}          )
          ,
          Var(17)
        )
        ,
        Weight(Base relation: 
          {tmp := havoc:10
           __retres5 := -1
           when 99 < havoc:10}        )
      )
    )
    ,
    Dot(
      Dot(
        Dot(
          Dot(
            Dot(
              Dot(
                Weight(Base relation: 
                  {__cost := 0
                   argc := param0:29
                   argv := param1:32
                   param0 := tr:427
                   argv@pos := param1@pos:31
                   param0@pos := type_err:428
                   argv@width := param1@width:30
                   param0@width := type_err:429
                   when (2 <= param0:29 /\ param0:29 <= 2)}                )
                ,
                Var(17)
              )
              ,
              Weight(Base relation: 
                {tmp := havoc:10
                 param0 := tr:430
                 param0@pos := type_err:431
                 param0@width := type_err:432
                 when havoc:10 <= 99}              )
            )
            ,
            Var(17)
          )
          ,
          Weight(Base relation: 
            {param0 := havoc:16
             param0@pos := type_err:39
             param0@width := type_err:40}          )
        )
        ,
        Var(25)
      )
      ,
      Weight(Base relation: 
        {__retres5 := 0}      )
    )
  )
  ,
  Weight(Base relation: 
    {return := __retres5:5
     return@pos := type_err:8
     return@width := type_err:9}  )
)


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


New-style (IRE) regular expression in IREregExpMap for reID=25: 
Weight(Base relation: 
  {__cost := __cost':486
   i := i':485
   t := t':484
   n := param0:29
   return := havoc:488
   return@pos := type_err:489
   return@width := type_err:490
   when ((!((0 <= K:479 /\ K:479 <= 0)) \/ mid_t:480 = t:102)
           /\ (!(1 <= K:479) \/ mid_t:480 = param0:29)
           /\ (!(0 <= K:479) \/ mid_i:481 = K:479)
           /\ (!(0 <= K:479)
                 \/ mid___cost:482 = (__cost:101 + (1000 * K:479)
                                        + (param0:29 * K:479)))
           /\ (!(0 <= K:479)
                 \/ -mid___cost:482 <= (-__cost:101 + (-2001/2 * K:479)
                                          + (-1/2 * (K:479 * K:479))))
           /\ ((K:479 = 0 /\ t:102 = mid_t:480 /\ 0 = mid_i:481
                  /\ __cost:101 = mid___cost:482)
                 \/ (1 <= K:479 /\ 0 <= (-1 + param0:29) /\ 0 <= __cost:101
                       /\ (-param0:29 + mid_t:480) = 0
                       /\ 0 <= (-1000 + -param0:29 + mid___cost:482)
                       /\ 0 <= (-1 + mid_i:481)
                       /\ 0 <= (param0:29 + -mid_i:481))) /\ K:483 = 0
           /\ mid_t:480 = t':484 /\ mid_i:481 = i':485
           /\ mid___cost:482 = __cost':486 /\ 0 = K:483
           /\ (K:479 + K:483) = K:487 /\ 0 <= K:487 /\ 0 <= i':485
           /\ param0:29 <= i':485)})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Plus(
      Plus(
        Weight(Base relation: 
          {__cost := 0
           __retres5 := -1
           argc := param0:29
           argv := param1:32
           argv@pos := param1@pos:31
           argv@width := param1@width:30
           when (param0:29 < 2 \/ 2 < param0:29)}        )
        ,
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := 0
               argc := param0:29
               argv := param1:32
               param0 := tr:427
               argv@pos := param1@pos:31
               param0@pos := type_err:428
               argv@width := param1@width:30
               param0@width := type_err:429
               when (2 <= param0:29 /\ param0:29 <= 2)}            )
            ,
            Var(17)
          )
          ,
          Weight(Base relation: 
            {tmp := havoc:10
             __retres5 := -1
             when 99 < havoc:10}          )
        )
      )
      ,
      Dot(
        Dot(
          Dot(
            Dot(
              Dot(
                Dot(
                  Weight(Base relation: 
                    {__cost := 0
                     argc := param0:29
                     argv := param1:32
                     param0 := tr:427
                     argv@pos := param1@pos:31
                     param0@pos := type_err:428
                     argv@width := param1@width:30
                     param0@width := type_err:429
                     when (2 <= param0:29 /\ param0:29 <= 2)}                  )
                  ,
                  Var(17)
                )
                ,
                Weight(Base relation: 
                  {tmp := havoc:10
                   param0 := tr:430
                   param0@pos := type_err:431
                   param0@width := type_err:432
                   when havoc:10 <= 99}                )
              )
              ,
              Var(17)
            )
            ,
            Weight(Base relation: 
              {param0 := havoc:16
               param0@pos := type_err:39
               param0@width := type_err:40}            )
          )
          ,
          Var(25)
        )
        ,
        Weight(Base relation: 
          {__retres5 := 0}        )
      )
    )
    ,
    Weight(Base relation: 
      {return := __retres5:5
       return@pos := type_err:8
       return@width := type_err:9}    )
  )
)



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

One()



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

Weight(Base relation: 
  {__cost := __cost':486
   return := havoc:488
   return@pos := type_err:489
   return@width := type_err:490
   when ((!((0 <= K:479 /\ K:479 <= 0)) \/ mid_t:480 = t:505)
           /\ (!(1 <= K:479) \/ mid_t:480 = param0:29)
           /\ (!(0 <= K:479) \/ mid_i:481 = K:479)
           /\ (!(0 <= K:479)
                 \/ mid___cost:482 = (__cost:101 + (1000 * K:479)
                                        + (param0:29 * K:479)))
           /\ (!(0 <= K:479)
                 \/ -mid___cost:482 <= (-__cost:101 + (-2001/2 * K:479)
                                          + (-1/2 * (K:479 * K:479))))
           /\ ((K:479 = 0 /\ t:505 = mid_t:480 /\ 0 = mid_i:481
                  /\ __cost:101 = mid___cost:482)
                 \/ (1 <= K:479 /\ 0 <= (-1 + param0:29) /\ 0 <= __cost:101
                       /\ (-param0:29 + mid_t:480) = 0
                       /\ 0 <= (-1000 + -param0:29 + mid___cost:482)
                       /\ 0 <= (-1 + mid_i:481)
                       /\ 0 <= (param0:29 + -mid_i:481))) /\ K:483 = 0
           /\ mid_t:480 = t':484 /\ mid_i:481 = i':485
           /\ mid___cost:482 = __cost':486 /\ 0 = K:483
           /\ (K:479 + K:483) = K:487 /\ 0 <= K:487 /\ 0 <= i':485
           /\ param0:29 <= i':485)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=15: 
Weight(Base relation: 
  {__cost := phi___cost:542
   return := phi___retres5:540
   param0 := phi_param0:537
   return@pos := type_err:543
   param0@pos := phi_param0@pos:534
   return@width := type_err:544
   param0@width := phi_param0@width:531
   when (((((param0:29 < 2 \/ 2 < param0:29) /\ tmp:545 = phi_tmp:517
              /\ param0:29 = phi_param0:516
              /\ param0@pos:28 = phi_param0@pos:515
              /\ param0@width:27 = phi_param0@width:514)
             \/ (2 <= param0:29 /\ param0:29 <= 2 /\ 99 < havoc:513
                   /\ havoc:513 = phi_tmp:517 /\ tr:427 = phi_param0:516
                   /\ type_err:428 = phi_param0@pos:515
                   /\ type_err:429 = phi_param0@width:514))
            /\ 0 = phi___cost:542 /\ phi_tmp:517 = phi_tmp:541
            /\ -1 = phi___retres5:540 /\ return:539 = phi_return:538
            /\ phi_param0:516 = phi_param0:537
            /\ return@pos:536 = phi_return@pos:535
            /\ phi_param0@pos:515 = phi_param0@pos:534
            /\ return@width:533 = phi_return@width:532
            /\ phi_param0@width:514 = phi_param0@width:531)
           \/ (2 <= param0:29 /\ param0:29 <= 2 /\ havoc:506 <= 99
                 /\ (!((0 <= K:518 /\ K:518 <= 0)) \/ mid_t:519 = t:520)
                 /\ (!(1 <= K:518) \/ mid_t:519 = havoc:510)
                 /\ (!(0 <= K:518) \/ mid_i:521 = K:518)
                 /\ (!(0 <= K:518)
                       \/ mid___cost:522 = ((1000 * K:518)
                                              + (havoc:510 * K:518)))
                 /\ (!(0 <= K:518)
                       \/ -mid___cost:522 <= ((-2001/2 * K:518)
                                                + (-1/2 * (K:518 * K:518))))
                 /\ ((K:518 = 0 /\ t:520 = mid_t:519 /\ 0 = mid_i:521
                        /\ 0 = mid___cost:522)
                       \/ (1 <= K:518 /\ 0 <= (-1 + havoc:510)
                             /\ (-havoc:510 + mid_t:519) = 0
                             /\ 0 <= (-1000 + -havoc:510 + mid___cost:522)
                             /\ 0 <= (-1 + mid_i:521)
                             /\ 0 <= (havoc:510 + -mid_i:521))) /\ K:523 = 0
                 /\ mid_t:519 = t':524 /\ mid_i:521 = i':525
                 /\ mid___cost:522 = __cost':526 /\ 0 = K:523
                 /\ (K:518 + K:523) = K:527 /\ 0 <= K:527 /\ 0 <= i':525
                 /\ havoc:510 <= i':525 /\ __cost':526 = phi___cost:542
                 /\ havoc:506 = phi_tmp:541 /\ 0 = phi___retres5:540
                 /\ havoc:528 = phi_return:538 /\ havoc:510 = phi_param0:537
                 /\ type_err:529 = phi_return@pos:535
                 /\ type_err:511 = phi_param0@pos:534
                 /\ type_err:530 = phi_return@width:532
                 /\ type_err:512 = phi_param0@width:531))})


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


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=25: 
Weight(Base relation: 
  {__cost := __cost':486
   return := havoc:488
   return@pos := type_err:489
   return@width := type_err:490
   when ((!((0 <= K:479 /\ K:479 <= 0)) \/ mid_t:480 = t:505)
           /\ (!(1 <= K:479) \/ mid_t:480 = param0:29)
           /\ (!(0 <= K:479) \/ mid_i:481 = K:479)
           /\ (!(0 <= K:479)
                 \/ mid___cost:482 = (__cost:101 + (1000 * K:479)
                                        + (param0:29 * K:479)))
           /\ (!(0 <= K:479)
                 \/ -mid___cost:482 <= (-__cost:101 + (-2001/2 * K:479)
                                          + (-1/2 * (K:479 * K:479))))
           /\ ((K:479 = 0 /\ t:505 = mid_t:480 /\ 0 = mid_i:481
                  /\ __cost:101 = mid___cost:482)
                 \/ (1 <= K:479 /\ 0 <= (-1 + param0:29) /\ 0 <= __cost:101
                       /\ (-param0:29 + mid_t:480) = 0
                       /\ 0 <= (-1000 + -param0:29 + mid___cost:482)
                       /\ 0 <= (-1 + mid_i:481)
                       /\ 0 <= (param0:29 + -mid_i:481))) /\ K:483 = 0
           /\ mid_t:480 = t':484 /\ mid_i:481 = i':485
           /\ mid___cost:482 = __cost':486 /\ 0 = K:483
           /\ (K:479 + K:483) = K:487 /\ 0 <= K:487 /\ 0 <= i':485
           /\ param0:29 <= i':485)})


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

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:542
 return := phi___retres5:540
 param0 := phi_param0:537
 return@pos := type_err:543
 param0@pos := phi_param0@pos:534
 return@width := type_err:544
 param0@width := phi_param0@width:531
 when (((((param0:29 < 2 \/ 2 < param0:29) /\ tmp:545 = phi_tmp:517
            /\ param0:29 = phi_param0:516
            /\ param0@pos:28 = phi_param0@pos:515
            /\ param0@width:27 = phi_param0@width:514)
           \/ (2 <= param0:29 /\ param0:29 <= 2 /\ 99 < havoc:513
                 /\ havoc:513 = phi_tmp:517 /\ tr:427 = phi_param0:516
                 /\ type_err:428 = phi_param0@pos:515
                 /\ type_err:429 = phi_param0@width:514))
          /\ 0 = phi___cost:542 /\ phi_tmp:517 = phi_tmp:541
          /\ -1 = phi___retres5:540 /\ return:539 = phi_return:538
          /\ phi_param0:516 = phi_param0:537
          /\ return@pos:536 = phi_return@pos:535
          /\ phi_param0@pos:515 = phi_param0@pos:534
          /\ return@width:533 = phi_return@width:532
          /\ phi_param0@width:514 = phi_param0@width:531)
         \/ (2 <= param0:29 /\ param0:29 <= 2 /\ havoc:506 <= 99
               /\ (!((0 <= K:518 /\ K:518 <= 0)) \/ mid_t:519 = t:520)
               /\ (!(1 <= K:518) \/ mid_t:519 = havoc:510)
               /\ (!(0 <= K:518) \/ mid_i:521 = K:518)
               /\ (!(0 <= K:518)
                     \/ mid___cost:522 = ((1000 * K:518)
                                            + (havoc:510 * K:518)))
               /\ (!(0 <= K:518)
                     \/ -mid___cost:522 <= ((-2001/2 * K:518)
                                              + (-1/2 * (K:518 * K:518))))
               /\ ((K:518 = 0 /\ t:520 = mid_t:519 /\ 0 = mid_i:521
                      /\ 0 = mid___cost:522)
                     \/ (1 <= K:518 /\ 0 <= (-1 + havoc:510)
                           /\ (-havoc:510 + mid_t:519) = 0
                           /\ 0 <= (-1000 + -havoc:510 + mid___cost:522)
                           /\ 0 <= (-1 + mid_i:521)
                           /\ 0 <= (havoc:510 + -mid_i:521))) /\ K:523 = 0
               /\ mid_t:519 = t':524 /\ mid_i:521 = i':525
               /\ mid___cost:522 = __cost':526 /\ 0 = K:523
               /\ (K:518 + K:523) = K:527 /\ 0 <= K:527 /\ 0 <= i':525
               /\ havoc:510 <= i':525 /\ __cost':526 = phi___cost:542
               /\ havoc:506 = phi_tmp:541 /\ 0 = phi___retres5:540
               /\ havoc:528 = phi_return:538 /\ havoc:510 = phi_param0:537
               /\ type_err:529 = phi_return@pos:535
               /\ type_err:511 = phi_param0@pos:534
               /\ type_err:530 = phi_return@width:532
               /\ type_err:512 = phi_param0@width:531))}

Evaluating variable number 17 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

Evaluating variable number 25 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':486
 return := havoc:488
 return@pos := type_err:489
 return@width := type_err:490
 when ((!((0 <= K:479 /\ K:479 <= 0)) \/ mid_t:480 = t:505)
         /\ (!(1 <= K:479) \/ mid_t:480 = param0:29)
         /\ (!(0 <= K:479) \/ mid_i:481 = K:479)
         /\ (!(0 <= K:479)
               \/ mid___cost:482 = (__cost:101 + (1000 * K:479)
                                      + (param0:29 * K:479)))
         /\ (!(0 <= K:479)
               \/ -mid___cost:482 <= (-__cost:101 + (-2001/2 * K:479)
                                        + (-1/2 * (K:479 * K:479))))
         /\ ((K:479 = 0 /\ t:505 = mid_t:480 /\ 0 = mid_i:481
                /\ __cost:101 = mid___cost:482)
               \/ (1 <= K:479 /\ 0 <= (-1 + param0:29) /\ 0 <= __cost:101
                     /\ (-param0:29 + mid_t:480) = 0
                     /\ 0 <= (-1000 + -param0:29 + mid___cost:482)
                     /\ 0 <= (-1 + mid_i:481)
                     /\ 0 <= (param0:29 + -mid_i:481))) /\ K:483 = 0
         /\ mid_t:480 = t':484 /\ mid_i:481 = i':485
         /\ mid___cost:482 = __cost':486 /\ 0 = K:483
         /\ (K:479 + K:483) = K:487 /\ 0 <= K:487 /\ 0 <= i':485
         /\ param0:29 <= i':485)}

    (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,62)_g1>	Base relation: 
{__cost := 0
 tmp := havoc:551
 argc := param0:29
 argv := param1:32
 param0 := havoc:555
 argv@pos := param1@pos:31
 param0@pos := type_err:556
 argv@width := param1@width:30
 param0@width := type_err:557
 when (2 <= param0:29 /\ param0:29 <= 2 /\ havoc:551 <= 99)}	
<__pstate, accept> -> <__pstate, (Unique State Name,78)_g1>	Base relation: 
{__cost := 0
 tmp := phi_tmp:586
 argc := param0:29
 argv := param1:32
 param0 := phi_param0:585
 argv@pos := param1@pos:31
 param0@pos := phi_param0@pos:584
 argv@width := param1@width:30
 param0@width := phi_param0@width:583
 when ((2 <= param0:29 /\ param0:29 <= 2 /\ tmp:3 = phi_tmp:586
          /\ tr:427 = phi_param0:585 /\ type_err:428 = phi_param0@pos:584
          /\ type_err:429 = phi_param0@width:583)
         \/ (2 <= param0:29 /\ param0:29 <= 2 /\ havoc:551 <= 99
               /\ havoc:551 = phi_tmp:586 /\ tr:552 = phi_param0:585
               /\ type_err:553 = phi_param0@pos:584
               /\ type_err:554 = phi_param0@width:583))}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0xcb10d30: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0xcb57570: 
	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,78)_g1 , __done )	Base relation: 
{__cost := 0
 tmp := phi_tmp:586
 argc := param0:29
 argv := param1:32
 param0 := phi_param0:585
 argv@pos := param1@pos:31
 param0@pos := phi_param0@pos:584
 argv@width := param1@width:30
 param0@width := phi_param0@width:583
 when ((2 <= param0:29 /\ param0:29 <= 2 /\ tmp:3 = phi_tmp:586
          /\ tr:427 = phi_param0:585 /\ type_err:428 = phi_param0@pos:584
          /\ type_err:429 = phi_param0@width:583)
         \/ (2 <= param0:29 /\ param0:29 <= 2 /\ havoc:551 <= 99
               /\ havoc:551 = phi_tmp:586 /\ tr:552 = phi_param0:585
               /\ type_err:553 = phi_param0@pos:584
               /\ type_err:554 = phi_param0@width:583))}
    ( __pstate , (Unique State Name,62)_g1 , __done )	Base relation: 
{__cost := 0
 tmp := havoc:551
 argc := param0:29
 argv := param1:32
 param0 := havoc:555
 argv@pos := param1@pos:31
 param0@pos := type_err:556
 argv@width := param1@width:30
 param0@width := type_err:557
 when (2 <= param0:29 /\ param0:29 <= 2 /\ havoc:551 <= 99)}

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

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

Base relation: 
{}

------------------------------------------------
Procedure summary for doProcess

Base relation: 
{__cost := __cost':486
 i := i':485
 t := t':484
 n := param0:29
 return := havoc:488
 return@pos := type_err:489
 return@width := type_err:490
 when ((!((0 <= K:479 /\ K:479 <= 0)) \/ mid_t:480 = t:102)
         /\ (!(1 <= K:479) \/ mid_t:480 = param0:29)
         /\ (!(0 <= K:479) \/ mid_i:481 = K:479)
         /\ (!(0 <= K:479)
               \/ mid___cost:482 = (__cost:101 + (1000 * K:479)
                                      + (param0:29 * K:479)))
         /\ (!(0 <= K:479)
               \/ -mid___cost:482 <= (-__cost:101 + (-2001/2 * K:479)
                                        + (-1/2 * (K:479 * K:479))))
         /\ ((K:479 = 0 /\ t:102 = mid_t:480 /\ 0 = mid_i:481
                /\ __cost:101 = mid___cost:482)
               \/ (1 <= K:479 /\ 0 <= (-1 + param0:29) /\ 0 <= __cost:101
                     /\ (-param0:29 + mid_t:480) = 0
                     /\ 0 <= (-1000 + -param0:29 + mid___cost:482)
                     /\ 0 <= (-1 + mid_i:481)
                     /\ 0 <= (param0:29 + -mid_i:481))) /\ K:483 = 0
         /\ mid_t:480 = t':484 /\ mid_i:481 = i':485
         /\ mid___cost:482 = __cost':486 /\ 0 = K:483
         /\ (K:479 + K:483) = K:487 /\ 0 <= K:487 /\ 0 <= i':485
         /\ param0:29 <= i':485)}

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

Base relation: 
{__cost := phi___cost:579
 tmp := phi_tmp:578
 __retres5 := phi___retres5:577
 argc := param0:29
 argv := param1:32
 return := phi___retres5:577
 param0 := phi_param0:575
 argv@pos := param1@pos:31
 return@pos := type_err:580
 param0@pos := phi_param0@pos:573
 argv@width := param1@width:30
 return@width := type_err:581
 param0@width := phi_param0@width:571
 when (((((param0:29 < 2 \/ 2 < param0:29) /\ tmp:3 = phi_tmp:550
            /\ param0:29 = phi_param0:549
            /\ param0@pos:28 = phi_param0@pos:548
            /\ param0@width:27 = phi_param0@width:547)
           \/ (2 <= param0:29 /\ param0:29 <= 2 /\ 99 < havoc:546
                 /\ havoc:546 = phi_tmp:550 /\ tr:427 = phi_param0:549
                 /\ type_err:428 = phi_param0@pos:548
                 /\ type_err:429 = phi_param0@width:547))
          /\ 0 = phi___cost:579 /\ phi_tmp:550 = phi_tmp:578
          /\ -1 = phi___retres5:577 /\ return:539 = phi_return:576
          /\ phi_param0:549 = phi_param0:575
          /\ return@pos:536 = phi_return@pos:574
          /\ phi_param0@pos:548 = phi_param0@pos:573
          /\ return@width:533 = phi_return@width:572
          /\ phi_param0@width:547 = phi_param0@width:571)
         \/ (2 <= param0:29 /\ param0:29 <= 2 /\ havoc:551 <= 99
               /\ (!((0 <= K:558 /\ K:558 <= 0)) \/ mid_t:559 = t:560)
               /\ (!(1 <= K:558) \/ mid_t:559 = havoc:555)
               /\ (!(0 <= K:558) \/ mid_i:561 = K:558)
               /\ (!(0 <= K:558)
                     \/ mid___cost:562 = ((1000 * K:558)
                                            + (havoc:555 * K:558)))
               /\ (!(0 <= K:558)
                     \/ -mid___cost:562 <= ((-2001/2 * K:558)
                                              + (-1/2 * (K:558 * K:558))))
               /\ ((K:558 = 0 /\ t:560 = mid_t:559 /\ 0 = mid_i:561
                      /\ 0 = mid___cost:562)
                     \/ (1 <= K:558 /\ 0 <= (-1 + havoc:555)
                           /\ (-havoc:555 + mid_t:559) = 0
                           /\ 0 <= (-1000 + -havoc:555 + mid___cost:562)
                           /\ 0 <= (-1 + mid_i:561)
                           /\ 0 <= (havoc:555 + -mid_i:561))) /\ K:563 = 0
               /\ mid_t:559 = t':564 /\ mid_i:561 = i':565
               /\ mid___cost:562 = __cost':566 /\ 0 = K:563
               /\ (K:558 + K:563) = K:567 /\ 0 <= K:567 /\ 0 <= i':565
               /\ havoc:555 <= i':565 /\ __cost':566 = phi___cost:579
               /\ havoc:551 = phi_tmp:578 /\ 0 = phi___retres5:577
               /\ havoc:568 = phi_return:576 /\ havoc:555 = phi_param0:575
               /\ type_err:569 = phi_return@pos:574
               /\ type_err:556 = phi_param0@pos:573
               /\ type_err:570 = phi_return@width:572
               /\ type_err:557 = phi_param0@width:571))}

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

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

Variable bounds at line 10 in doProcess

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

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