/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, 66> -> <Unique State Name, 16>	Base relation: 
{__cost := 0
 argc := param0:30
 argv := param1:33
 argv@pos := param1@pos:32
 argv@width := param1@width:31}	
<Unique State Name, 70> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 16> -> <Unique State Name, 26>	Base relation: 
{__retres6 := -1
 when (argc:4 < 1 \/ 1 < argc:4)}	
<Unique State Name, 16> -> <Unique State Name, 56>	Base relation: 
{param0 := tr:34
 param0@pos := type_err:35
 param0@width := type_err:36
 when (1 <= argc:4 /\ argc:4 <= 1)}	
<Unique State Name, 64> -> <Unique State Name, 59>	Base relation: 
{param0 := havoc:22
 param0@pos := type_err:37
 param0@width := type_err:38}	
<Unique State Name, 33> -> <Unique State Name, 29>	Base relation: 
{__cost := (__cost:121 + 1)
 i := (i:119 + 1)
 when (i:119 < m_length:120 /\ 0 <= __cost:121 /\ 0 <= (__cost:121 + 1))}	
<Unique State Name, 33> -> <Unique State Name, 44>	Base relation: 
{when m_length:120 <= i:119}	
<Unique State Name, 9> -> <Unique State Name, 26>	Base relation: 
{__retres6 := -1
 when 99 < tmp:3}	
<Unique State Name, 9> -> <Unique State Name, 65>	Base relation: 
{param0 := tr:39
 param0@pos := type_err:40
 param0@width := type_err:41
 when tmp:3 <= 99}	
<Unique State Name, 69> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 72> -> <Unique State Name, 33>	Base relation: 
{}	
<Unique State Name, 71> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 58> -> <Unique State Name, 61>	Base relation: 
{}	
<Unique State Name, 52> -> <Unique State Name, 68>	Base relation: 
{m_length := (param0:30 * param0:30)
 return := havoc:111
 return@pos := type_err:112
 return@width := type_err:113}	
<Unique State Name, 29> -> <Unique State Name, 72>	Base relation: 
{when 0 <= i:119}	
<Unique State Name, 56> -> <Unique State Name, 71 55>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 68> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 60> -> <Unique State Name, 26>	Base relation: 
{__retres6 := 0}	
<Unique State Name, 59> -> <Unique State Name, 52 58>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 61> -> <Unique State Name, 47 60>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 55> -> <Unique State Name, 9>	Base relation: 
{tmp := havoc:11}	
<Unique State Name, 65> -> <Unique State Name, 71 64>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 47> -> <Unique State Name, 29>	Base relation: 
{i := 0}	
<Unique State Name, 44> -> <Unique State Name, 69>	Base relation: 
{return := havoc:122
 return@pos := type_err:125
 return@width := type_err:126}	
<Unique State Name, 26> -> <Unique State Name, 70>	Base relation: 
{return := __retres6:6
 return@pos := type_err:9
 return@width := type_err:10}	
#################################################################
           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:121 + 1)
 i := (i:119 + 1)
 when (0 <= i:119 /\ i:119 < m_length:120 /\ 0 <= __cost:121
         /\ 0 <= (__cost:121 + 1))}
**** alpha hat: 
  {<Split [true
            (i':189) = (1)*(i:119) + 1
           (__cost':188) = (1)*(__cost:121) + 1
           }
          pre:
            [|-i:119+m_length:120-1>=0; __cost:121>=0; i:119>=0|]
          post:
            [|i':189-1>=0; __cost':188-1>=0; m_length:120-i':189>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':188
   i := i':189
   when ((!(0 <= K:198) \/ mid_i:200 = (i:119 + K:198))
           /\ (!(0 <= K:198) \/ mid___cost:201 = (__cost:121 + K:198))
           /\ ((K:198 = 0 /\ i:119 = mid_i:200 /\ __cost:121 = mid___cost:201)
                 \/ (1 <= K:198 /\ 0 <= (-1 + -i:119 + m_length:120)
                       /\ 0 <= __cost:121 /\ 0 <= i:119
                       /\ 0 <= (-1 + mid_i:200) /\ 0 <= (-1 + mid___cost:201)
                       /\ 0 <= (m_length:120 + -mid_i:200))) /\ K:199 = 0
           /\ mid_i:200 = i':189 /\ mid___cost:201 = __cost':188 /\ 0 = K:199
           /\ (K:198 + K:199) = K:197 /\ 0 <= K:197)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
18  20  23  30  


New-style (IRE) regular expression in IREregExpMap for reID=18: 
Dot(
  Plus(
    Plus(
      Weight(Base relation: 
        {__cost := 0
         __retres6 := -1
         argc := param0:30
         argv := param1:33
         argv@pos := param1@pos:32
         argv@width := param1@width:31
         when (param0:30 < 1 \/ 1 < param0:30)}      )
      ,
      Dot(
        Dot(
          Weight(Base relation: 
            {__cost := 0
             argc := param0:30
             argv := param1:33
             param0 := tr:182
             argv@pos := param1@pos:32
             param0@pos := type_err:183
             argv@width := param1@width:31
             param0@width := type_err:184
             when (1 <= param0:30 /\ param0:30 <= 1)}          )
          ,
          Var(20)
        )
        ,
        Weight(Base relation: 
          {tmp := havoc:11
           __retres6 := -1
           when 99 < havoc:11}        )
      )
    )
    ,
    Dot(
      Dot(
        Dot(
          Dot(
            Dot(
              Dot(
                Dot(
                  Weight(Base relation: 
                    {__cost := 0
                     argc := param0:30
                     argv := param1:33
                     param0 := tr:182
                     argv@pos := param1@pos:32
                     param0@pos := type_err:183
                     argv@width := param1@width:31
                     param0@width := type_err:184
                     when (1 <= param0:30 /\ param0:30 <= 1)}                  )
                  ,
                  Var(20)
                )
                ,
                Weight(Base relation: 
                  {tmp := havoc:11
                   param0 := tr:185
                   param0@pos := type_err:186
                   param0@width := type_err:187
                   when havoc:11 <= 99}                )
              )
              ,
              Var(20)
            )
            ,
            Weight(Base relation: 
              {param0 := havoc:22
               param0@pos := type_err:37
               param0@width := type_err:38}            )
          )
          ,
          Var(23)
        )
        ,
        Var(30)
      )
      ,
      Weight(Base relation: 
        {__retres6 := 0}      )
    )
  )
  ,
  Weight(Base relation: 
    {return := __retres6:6
     return@pos := type_err:9
     return@width := type_err:10}  )
)


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


New-style (IRE) regular expression in IREregExpMap for reID=23: 
Weight(Base relation: 
  {m_length := (param0:30 * param0:30)
   return := havoc:111
   return@pos := type_err:112
   return@width := type_err:113})


New-style (IRE) regular expression in IREregExpMap for reID=30: 
Weight(Base relation: 
  {__cost := __cost':207
   i := i':206
   return := havoc:209
   return@pos := type_err:210
   return@width := type_err:211
   when ((!(0 <= K:202) \/ mid_i:203 = K:202)
           /\ (!(0 <= K:202) \/ mid___cost:204 = (__cost:121 + K:202))
           /\ ((K:202 = 0 /\ 0 = mid_i:203 /\ __cost:121 = mid___cost:204)
                 \/ (1 <= K:202 /\ 0 <= (-1 + m_length:120)
                       /\ 0 <= __cost:121 /\ 0 <= (-1 + mid_i:203)
                       /\ 0 <= (-1 + mid___cost:204)
                       /\ 0 <= (m_length:120 + -mid_i:203))) /\ K:205 = 0
           /\ mid_i:203 = i':206 /\ mid___cost:204 = __cost':207 /\ 0 = K:205
           /\ (K:202 + K:205) = K:208 /\ 0 <= K:208 /\ 0 <= i':206
           /\ m_length:120 <= i':206)})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Plus(
      Plus(
        Weight(Base relation: 
          {__cost := 0
           __retres6 := -1
           argc := param0:30
           argv := param1:33
           argv@pos := param1@pos:32
           argv@width := param1@width:31
           when (param0:30 < 1 \/ 1 < param0:30)}        )
        ,
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := 0
               argc := param0:30
               argv := param1:33
               param0 := tr:182
               argv@pos := param1@pos:32
               param0@pos := type_err:183
               argv@width := param1@width:31
               param0@width := type_err:184
               when (1 <= param0:30 /\ param0:30 <= 1)}            )
            ,
            Var(20)
          )
          ,
          Weight(Base relation: 
            {tmp := havoc:11
             __retres6 := -1
             when 99 < havoc:11}          )
        )
      )
      ,
      Dot(
        Dot(
          Dot(
            Dot(
              Dot(
                Dot(
                  Dot(
                    Weight(Base relation: 
                      {__cost := 0
                       argc := param0:30
                       argv := param1:33
                       param0 := tr:182
                       argv@pos := param1@pos:32
                       param0@pos := type_err:183
                       argv@width := param1@width:31
                       param0@width := type_err:184
                       when (1 <= param0:30 /\ param0:30 <= 1)}                    )
                    ,
                    Var(20)
                  )
                  ,
                  Weight(Base relation: 
                    {tmp := havoc:11
                     param0 := tr:185
                     param0@pos := type_err:186
                     param0@width := type_err:187
                     when havoc:11 <= 99}                  )
                )
                ,
                Var(20)
              )
              ,
              Weight(Base relation: 
                {param0 := havoc:22
                 param0@pos := type_err:37
                 param0@width := type_err:38}              )
            )
            ,
            Var(23)
          )
          ,
          Var(30)
        )
        ,
        Weight(Base relation: 
          {__retres6 := 0}        )
      )
    )
    ,
    Weight(Base relation: 
      {return := __retres6:6
       return@pos := type_err:9
       return@width := type_err:10}    )
  )
)



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

One()



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

Weight(Base relation: 
  {m_length := (param0:30 * param0:30)
   return := havoc:111
   return@pos := type_err:112
   return@width := type_err:113})



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

Weight(Base relation: 
  {__cost := __cost':207
   return := havoc:209
   return@pos := type_err:210
   return@width := type_err:211
   when ((!(0 <= K:202) \/ mid_i:203 = K:202)
           /\ (!(0 <= K:202) \/ mid___cost:204 = (__cost:121 + K:202))
           /\ ((K:202 = 0 /\ 0 = mid_i:203 /\ __cost:121 = mid___cost:204)
                 \/ (1 <= K:202 /\ 0 <= (-1 + m_length:120)
                       /\ 0 <= __cost:121 /\ 0 <= (-1 + mid_i:203)
                       /\ 0 <= (-1 + mid___cost:204)
                       /\ 0 <= (m_length:120 + -mid_i:203))) /\ K:205 = 0
           /\ mid_i:203 = i':206 /\ mid___cost:204 = __cost':207 /\ 0 = K:205
           /\ (K:202 + K:205) = K:208 /\ 0 <= K:208 /\ 0 <= i':206
           /\ m_length:120 <= i':206)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=18: 
Weight(Base relation: 
  {m_length := phi_m_length:249
   __cost := phi___cost:248
   return := phi___retres6:246
   param0 := phi_param0:243
   return@pos := type_err:250
   param0@pos := phi_param0@pos:240
   return@width := type_err:251
   param0@width := phi_param0@width:237
   when (((((param0:30 < 1 \/ 1 < param0:30) /\ tmp:252 = phi_tmp:223
              /\ param0:30 = phi_param0:222
              /\ param0@pos:29 = phi_param0@pos:221
              /\ param0@width:28 = phi_param0@width:220)
             \/ (1 <= param0:30 /\ param0:30 <= 1 /\ 99 < havoc:219
                   /\ havoc:219 = phi_tmp:223 /\ tr:182 = phi_param0:222
                   /\ type_err:183 = phi_param0@pos:221
                   /\ type_err:184 = phi_param0@width:220))
            /\ m_length:120 = phi_m_length:249 /\ 0 = phi___cost:248
            /\ phi_tmp:223 = phi_tmp:247 /\ -1 = phi___retres6:246
            /\ return:245 = phi_return:244 /\ phi_param0:222 = phi_param0:243
            /\ return@pos:242 = phi_return@pos:241
            /\ phi_param0@pos:221 = phi_param0@pos:240
            /\ return@width:239 = phi_return@width:238
            /\ phi_param0@width:220 = phi_param0@width:237)
           \/ (1 <= param0:30 /\ param0:30 <= 1 /\ havoc:212 <= 99
                 /\ (!(0 <= K:227) \/ mid_i:228 = K:227)
                 /\ (!(0 <= K:227) \/ mid___cost:229 = K:227)
                 /\ ((K:227 = 0 /\ 0 = mid_i:228 /\ 0 = mid___cost:229)
                       \/ (1 <= K:227 /\ 0 <= (-1 + (havoc:216 * havoc:216))
                             /\ 0 <= (-1 + mid_i:228)
                             /\ 0 <= (-1 + mid___cost:229)
                             /\ 0 <= ((havoc:216 * havoc:216) + -mid_i:228)))
                 /\ K:230 = 0 /\ mid_i:228 = i':231
                 /\ mid___cost:229 = __cost':232 /\ 0 = K:230
                 /\ (K:227 + K:230) = K:233 /\ 0 <= K:233 /\ 0 <= i':231
                 /\ (havoc:216 * havoc:216) <= i':231
                 /\ (havoc:216 * havoc:216) = phi_m_length:249
                 /\ __cost':232 = phi___cost:248 /\ havoc:212 = phi_tmp:247
                 /\ 0 = phi___retres6:246 /\ havoc:234 = phi_return:244
                 /\ havoc:216 = phi_param0:243
                 /\ type_err:235 = phi_return@pos:241
                 /\ type_err:217 = phi_param0@pos:240
                 /\ type_err:236 = phi_return@width:238
                 /\ type_err:218 = phi_param0@width:237))})


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


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=23: 
Weight(Base relation: 
  {m_length := (param0:30 * param0:30)
   return := havoc:111
   return@pos := type_err:112
   return@width := type_err:113})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=30: 
Weight(Base relation: 
  {__cost := __cost':207
   return := havoc:209
   return@pos := type_err:210
   return@width := type_err:211
   when ((!(0 <= K:202) \/ mid_i:203 = K:202)
           /\ (!(0 <= K:202) \/ mid___cost:204 = (__cost:121 + K:202))
           /\ ((K:202 = 0 /\ 0 = mid_i:203 /\ __cost:121 = mid___cost:204)
                 \/ (1 <= K:202 /\ 0 <= (-1 + m_length:120)
                       /\ 0 <= __cost:121 /\ 0 <= (-1 + mid_i:203)
                       /\ 0 <= (-1 + mid___cost:204)
                       /\ 0 <= (m_length:120 + -mid_i:203))) /\ K:205 = 0
           /\ mid_i:203 = i':206 /\ mid___cost:204 = __cost':207 /\ 0 = K:205
           /\ (K:202 + K:205) = K:208 /\ 0 <= K:208 /\ 0 <= i':206
           /\ m_length:120 <= i':206)})


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

  The IRE-evaluated value on this round is: 

Base relation: 
{m_length := phi_m_length:249
 __cost := phi___cost:248
 return := phi___retres6:246
 param0 := phi_param0:243
 return@pos := type_err:250
 param0@pos := phi_param0@pos:240
 return@width := type_err:251
 param0@width := phi_param0@width:237
 when (((((param0:30 < 1 \/ 1 < param0:30) /\ tmp:252 = phi_tmp:223
            /\ param0:30 = phi_param0:222
            /\ param0@pos:29 = phi_param0@pos:221
            /\ param0@width:28 = phi_param0@width:220)
           \/ (1 <= param0:30 /\ param0:30 <= 1 /\ 99 < havoc:219
                 /\ havoc:219 = phi_tmp:223 /\ tr:182 = phi_param0:222
                 /\ type_err:183 = phi_param0@pos:221
                 /\ type_err:184 = phi_param0@width:220))
          /\ m_length:120 = phi_m_length:249 /\ 0 = phi___cost:248
          /\ phi_tmp:223 = phi_tmp:247 /\ -1 = phi___retres6:246
          /\ return:245 = phi_return:244 /\ phi_param0:222 = phi_param0:243
          /\ return@pos:242 = phi_return@pos:241
          /\ phi_param0@pos:221 = phi_param0@pos:240
          /\ return@width:239 = phi_return@width:238
          /\ phi_param0@width:220 = phi_param0@width:237)
         \/ (1 <= param0:30 /\ param0:30 <= 1 /\ havoc:212 <= 99
               /\ (!(0 <= K:227) \/ mid_i:228 = K:227)
               /\ (!(0 <= K:227) \/ mid___cost:229 = K:227)
               /\ ((K:227 = 0 /\ 0 = mid_i:228 /\ 0 = mid___cost:229)
                     \/ (1 <= K:227 /\ 0 <= (-1 + (havoc:216 * havoc:216))
                           /\ 0 <= (-1 + mid_i:228)
                           /\ 0 <= (-1 + mid___cost:229)
                           /\ 0 <= ((havoc:216 * havoc:216) + -mid_i:228)))
               /\ K:230 = 0 /\ mid_i:228 = i':231
               /\ mid___cost:229 = __cost':232 /\ 0 = K:230
               /\ (K:227 + K:230) = K:233 /\ 0 <= K:233 /\ 0 <= i':231
               /\ (havoc:216 * havoc:216) <= i':231
               /\ (havoc:216 * havoc:216) = phi_m_length:249
               /\ __cost':232 = phi___cost:248 /\ havoc:212 = phi_tmp:247
               /\ 0 = phi___retres6:246 /\ havoc:234 = phi_return:244
               /\ havoc:216 = phi_param0:243
               /\ type_err:235 = phi_return@pos:241
               /\ type_err:217 = phi_param0@pos:240
               /\ type_err:236 = phi_return@width:238
               /\ type_err:218 = phi_param0@width:237))}

Evaluating variable number 20 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

Evaluating variable number 23 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{m_length := (param0:30 * param0:30)
 return := havoc:111
 return@pos := type_err:112
 return@width := type_err:113}

Evaluating variable number 30 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':207
 return := havoc:209
 return@pos := type_err:210
 return@width := type_err:211
 when ((!(0 <= K:202) \/ mid_i:203 = K:202)
         /\ (!(0 <= K:202) \/ mid___cost:204 = (__cost:121 + K:202))
         /\ ((K:202 = 0 /\ 0 = mid_i:203 /\ __cost:121 = mid___cost:204)
               \/ (1 <= K:202 /\ 0 <= (-1 + m_length:120) /\ 0 <= __cost:121
                     /\ 0 <= (-1 + mid_i:203) /\ 0 <= (-1 + mid___cost:204)
                     /\ 0 <= (m_length:120 + -mid_i:203))) /\ K:205 = 0
         /\ mid_i:203 = i':206 /\ mid___cost:204 = __cost':207 /\ 0 = K:205
         /\ (K:202 + K:205) = K:208 /\ 0 <= K:208 /\ 0 <= i':206
         /\ m_length:120 <= i':206)}

    (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,47)_g1>	Base relation: 
{m_length := (havoc:262 * havoc:262)
 __cost := 0
 tmp := havoc:258
 argc := param0:30
 argv := param1:33
 return := havoc:265
 param0 := havoc:262
 argv@pos := param1@pos:32
 return@pos := type_err:266
 param0@pos := type_err:263
 argv@width := param1@width:31
 return@width := type_err:267
 param0@width := type_err:264
 when (1 <= param0:30 /\ param0:30 <= 1 /\ havoc:258 <= 99)}	
<__pstate, accept> -> <__pstate, (Unique State Name,71)_g1>	Base relation: 
{__cost := 0
 tmp := phi_tmp:294
 argc := param0:30
 argv := param1:33
 param0 := phi_param0:293
 argv@pos := param1@pos:32
 param0@pos := phi_param0@pos:292
 argv@width := param1@width:31
 param0@width := phi_param0@width:291
 when ((1 <= param0:30 /\ param0:30 <= 1 /\ tmp:3 = phi_tmp:294
          /\ tr:182 = phi_param0:293 /\ type_err:183 = phi_param0@pos:292
          /\ type_err:184 = phi_param0@width:291)
         \/ (1 <= param0:30 /\ param0:30 <= 1 /\ havoc:258 <= 99
               /\ havoc:258 = phi_tmp:294 /\ tr:259 = phi_param0:293
               /\ type_err:260 = phi_param0@pos:292
               /\ type_err:261 = phi_param0@width:291))}	
<__pstate, accept> -> <__pstate, (Unique State Name,52)_g1>	Base relation: 
{__cost := 0
 tmp := havoc:258
 argc := param0:30
 argv := param1:33
 param0 := havoc:262
 argv@pos := param1@pos:32
 param0@pos := type_err:263
 argv@width := param1@width:31
 param0@width := type_err:264
 when (1 <= param0:30 /\ param0:30 <= 1 /\ havoc:258 <= 99)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x6e14ea0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x6e14fd0: 
	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,47)_g1 , __done )	Base relation: 
{m_length := (havoc:262 * havoc:262)
 __cost := 0
 tmp := havoc:258
 argc := param0:30
 argv := param1:33
 return := havoc:265
 param0 := havoc:262
 argv@pos := param1@pos:32
 return@pos := type_err:266
 param0@pos := type_err:263
 argv@width := param1@width:31
 return@width := type_err:267
 param0@width := type_err:264
 when (1 <= param0:30 /\ param0:30 <= 1 /\ havoc:258 <= 99)}
    ( __pstate , (Unique State Name,52)_g1 , __done )	Base relation: 
{__cost := 0
 tmp := havoc:258
 argc := param0:30
 argv := param1:33
 param0 := havoc:262
 argv@pos := param1@pos:32
 param0@pos := type_err:263
 argv@width := param1@width:31
 param0@width := type_err:264
 when (1 <= param0:30 /\ param0:30 <= 1 /\ havoc:258 <= 99)}
    ( __pstate , (Unique State Name,71)_g1 , __done )	Base relation: 
{__cost := 0
 tmp := phi_tmp:294
 argc := param0:30
 argv := param1:33
 param0 := phi_param0:293
 argv@pos := param1@pos:32
 param0@pos := phi_param0@pos:292
 argv@width := param1@width:31
 param0@width := phi_param0@width:291
 when ((1 <= param0:30 /\ param0:30 <= 1 /\ tmp:3 = phi_tmp:294
          /\ tr:182 = phi_param0:293 /\ type_err:183 = phi_param0@pos:292
          /\ type_err:184 = phi_param0@width:291)
         \/ (1 <= param0:30 /\ param0:30 <= 1 /\ havoc:258 <= 99
               /\ havoc:258 = phi_tmp:294 /\ tr:259 = phi_param0:293
               /\ type_err:260 = phi_param0@pos:292
               /\ type_err:261 = phi_param0@width:291))}

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

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

Base relation: 
{}

------------------------------------------------
Procedure summary for bar

Base relation: 
{__cost := __cost':207
 i := i':206
 return := havoc:209
 return@pos := type_err:210
 return@width := type_err:211
 when ((!(0 <= K:202) \/ mid_i:203 = K:202)
         /\ (!(0 <= K:202) \/ mid___cost:204 = (__cost:121 + K:202))
         /\ ((K:202 = 0 /\ 0 = mid_i:203 /\ __cost:121 = mid___cost:204)
               \/ (1 <= K:202 /\ 0 <= (-1 + m_length:120) /\ 0 <= __cost:121
                     /\ 0 <= (-1 + mid_i:203) /\ 0 <= (-1 + mid___cost:204)
                     /\ 0 <= (m_length:120 + -mid_i:203))) /\ K:205 = 0
         /\ mid_i:203 = i':206 /\ mid___cost:204 = __cost':207 /\ 0 = K:205
         /\ (K:202 + K:205) = K:208 /\ 0 <= K:208 /\ 0 <= i':206
         /\ m_length:120 <= i':206)}

------------------------------------------------
Procedure summary for foo

Base relation: 
{m_length := (param0:30 * param0:30)
 return := havoc:111
 return@pos := type_err:112
 return@width := type_err:113}

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

Base relation: 
{m_length := phi_m_length:287
 __cost := phi___cost:286
 tmp := phi_tmp:285
 __retres6 := phi___retres6:284
 argc := param0:30
 argv := param1:33
 return := phi___retres6:284
 param0 := phi_param0:282
 argv@pos := param1@pos:32
 return@pos := type_err:288
 param0@pos := phi_param0@pos:280
 argv@width := param1@width:31
 return@width := type_err:289
 param0@width := phi_param0@width:278
 when (((((param0:30 < 1 \/ 1 < param0:30) /\ tmp:3 = phi_tmp:257
            /\ param0:30 = phi_param0:256
            /\ param0@pos:29 = phi_param0@pos:255
            /\ param0@width:28 = phi_param0@width:254)
           \/ (1 <= param0:30 /\ param0:30 <= 1 /\ 99 < havoc:253
                 /\ havoc:253 = phi_tmp:257 /\ tr:182 = phi_param0:256
                 /\ type_err:183 = phi_param0@pos:255
                 /\ type_err:184 = phi_param0@width:254))
          /\ m_length:120 = phi_m_length:287 /\ 0 = phi___cost:286
          /\ phi_tmp:257 = phi_tmp:285 /\ -1 = phi___retres6:284
          /\ return:245 = phi_return:283 /\ phi_param0:256 = phi_param0:282
          /\ return@pos:242 = phi_return@pos:281
          /\ phi_param0@pos:255 = phi_param0@pos:280
          /\ return@width:239 = phi_return@width:279
          /\ phi_param0@width:254 = phi_param0@width:278)
         \/ (1 <= param0:30 /\ param0:30 <= 1 /\ havoc:258 <= 99
               /\ (!(0 <= K:268) \/ mid_i:269 = K:268)
               /\ (!(0 <= K:268) \/ mid___cost:270 = K:268)
               /\ ((K:268 = 0 /\ 0 = mid_i:269 /\ 0 = mid___cost:270)
                     \/ (1 <= K:268 /\ 0 <= (-1 + (havoc:262 * havoc:262))
                           /\ 0 <= (-1 + mid_i:269)
                           /\ 0 <= (-1 + mid___cost:270)
                           /\ 0 <= ((havoc:262 * havoc:262) + -mid_i:269)))
               /\ K:271 = 0 /\ mid_i:269 = i':272
               /\ mid___cost:270 = __cost':273 /\ 0 = K:271
               /\ (K:268 + K:271) = K:274 /\ 0 <= K:274 /\ 0 <= i':272
               /\ (havoc:262 * havoc:262) <= i':272
               /\ (havoc:262 * havoc:262) = phi_m_length:287
               /\ __cost':273 = phi___cost:286 /\ havoc:258 = phi_tmp:285
               /\ 0 = phi___retres6:284 /\ havoc:275 = phi_return:283
               /\ havoc:262 = phi_param0:282
               /\ type_err:276 = phi_return@pos:281
               /\ type_err:263 = phi_param0@pos:280
               /\ type_err:277 = phi_return@width:279
               /\ type_err:264 = phi_param0@width:278))}

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

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

Variable bounds at line 18 in bar

min(__cost, (__cost + m_length)) <= __cost
__cost is o(1)
__cost <= max(__cost, (__cost + m_length))
__cost is O(n)

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