/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, 72> -> <Unique State Name, 16>	Base relation: 
{__cost := 0
 argc := param0:32
 argv := param1:35
 argv@pos := param1@pos:34
 argv@width := param1@width:33}	
<Unique State Name, 76> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 16> -> <Unique State Name, 26>	Base relation: 
{__retres7 := -1
 when (argc:4 < 1 \/ 1 < argc:4)}	
<Unique State Name, 16> -> <Unique State Name, 60>	Base relation: 
{param0 := tr:36
 param0@pos := type_err:37
 param0@width := type_err:38
 when (1 <= argc:4 /\ argc:4 <= 1)}	
<Unique State Name, 70> -> <Unique State Name, 64>	Base relation: 
{param0 := tr:39
 param1 := havoc:24
 param0@pos := 0
 param1@pos := type_err:40
 param0@width := 1
 param1@width := type_err:41}	
<Unique State Name, 33> -> <Unique State Name, 29>	Base relation: 
{__cost := (__cost:160 + 1)
 i := (i:157 + 1)
 when (i:157 < tr:158 /\ 0 <= __cost:160 /\ 0 <= (__cost:160 + 1))}	
<Unique State Name, 33> -> <Unique State Name, 44>	Base relation: 
{when tr:159 <= i:157}	
<Unique State Name, 9> -> <Unique State Name, 26>	Base relation: 
{__retres7 := -1
 when 99 < tmp:3}	
<Unique State Name, 9> -> <Unique State Name, 71>	Base relation: 
{param0 := tr:42
 param0@pos := type_err:43
 param0@width := type_err:44
 when tmp:3 <= 99}	
<Unique State Name, 75> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 78> -> <Unique State Name, 33>	Base relation: 
{}	
<Unique State Name, 77> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 63> -> <Unique State Name, 67>	Base relation: 
{param0 := tr:23
 param0@pos := 0
 param0@width := 1}	
<Unique State Name, 74> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 29> -> <Unique State Name, 78>	Base relation: 
{when 0 <= i:157}	
<Unique State Name, 60> -> <Unique State Name, 77 59>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 56> -> <Unique State Name, 29>	Base relation: 
{i := 0}	
<Unique State Name, 66> -> <Unique State Name, 26>	Base relation: 
{__retres7 := 0}	
<Unique State Name, 64> -> <Unique State Name, 54 63>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 67> -> <Unique State Name, 56 66>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 59> -> <Unique State Name, 9>	Base relation: 
{tmp := havoc:11}	
<Unique State Name, 71> -> <Unique State Name, 77 70>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 54> -> <Unique State Name, 74>	Base relation: 
{return := havoc:149
 return@pos := type_err:151
 return@width := type_err:153}	
<Unique State Name, 44> -> <Unique State Name, 75>	Base relation: 
{return := havoc:161
 return@pos := type_err:164
 return@width := type_err:165}	
<Unique State Name, 26> -> <Unique State Name, 76>	Base relation: 
{return := __retres7: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:160 + 1)
 i := (i:157 + 1)
 when (0 <= i:157 /\ i:157 < tr:219 /\ 0 <= __cost:160
         /\ 0 <= (__cost:160 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':220) = (1)*(__cost:160) + 1
           (i':221) = (1)*(i:157) + 1
           }
          pre:
            [|i:157>=0; __cost:160>=0|]
          post:
            [|i':221-1>=0; __cost':220-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':220
   i := i':221
   when ((!(0 <= K:229) \/ mid___cost:232 = (__cost:160 + K:229))
           /\ (!(0 <= K:229) \/ mid_i:231 = (i:157 + K:229))
           /\ ((K:229 = 0 /\ i:157 = mid_i:231 /\ __cost:160 = mid___cost:232)
                 \/ (1 <= K:229 /\ 0 <= i:157 /\ 0 <= __cost:160
                       /\ 0 <= (-1 + mid_i:231) /\ 0 <= (-1 + mid___cost:232)))
           /\ K:230 = 0 /\ mid_i:231 = i':221 /\ mid___cost:232 = __cost':220
           /\ 0 = K:230 /\ (K:229 + K:230) = K:228 /\ 0 <= K:228)}
}
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
         __retres7 := -1
         argc := param0:32
         argv := param1:35
         argv@pos := param1@pos:34
         argv@width := param1@width:33
         when (param0:32 < 1 \/ 1 < param0:32)}      )
      ,
      Dot(
        Dot(
          Weight(Base relation: 
            {__cost := 0
             argc := param0:32
             argv := param1:35
             param0 := tr:213
             argv@pos := param1@pos:34
             param0@pos := type_err:214
             argv@width := param1@width:33
             param0@width := type_err:215
             when (1 <= param0:32 /\ param0:32 <= 1)}          )
          ,
          Var(20)
        )
        ,
        Weight(Base relation: 
          {tmp := havoc:11
           __retres7 := -1
           when 99 < havoc:11}        )
      )
    )
    ,
    Dot(
      Dot(
        Dot(
          Dot(
            Dot(
              Dot(
                Dot(
                  Dot(
                    Weight(Base relation: 
                      {__cost := 0
                       argc := param0:32
                       argv := param1:35
                       param0 := tr:213
                       argv@pos := param1@pos:34
                       param0@pos := type_err:214
                       argv@width := param1@width:33
                       param0@width := type_err:215
                       when (1 <= param0:32 /\ param0:32 <= 1)}                    )
                    ,
                    Var(20)
                  )
                  ,
                  Weight(Base relation: 
                    {tmp := havoc:11
                     param0 := tr:216
                     param0@pos := type_err:217
                     param0@width := type_err:218
                     when havoc:11 <= 99}                  )
                )
                ,
                Var(20)
              )
              ,
              Weight(Base relation: 
                {param0 := tr:39
                 param1 := havoc:24
                 param0@pos := 0
                 param1@pos := type_err:40
                 param0@width := 1
                 param1@width := type_err:41}              )
            )
            ,
            Var(23)
          )
          ,
          Weight(Base relation: 
            {param0 := tr:23
             param0@pos := 0
             param0@width := 1}          )
        )
        ,
        Var(30)
      )
      ,
      Weight(Base relation: 
        {__retres7 := 0}      )
    )
  )
  ,
  Weight(Base relation: 
    {return := __retres7: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: 
  {return := havoc:149
   return@pos := type_err:151
   return@width := type_err:153})


New-style (IRE) regular expression in IREregExpMap for reID=30: 
Weight(Base relation: 
  {__cost := __cost':238
   i := i':237
   return := havoc:241
   return@pos := type_err:242
   return@width := type_err:243
   when ((!(0 <= K:233) \/ mid___cost:234 = (__cost:160 + K:233))
           /\ (!(0 <= K:233) \/ mid_i:235 = K:233)
           /\ ((K:233 = 0 /\ 0 = mid_i:235 /\ __cost:160 = mid___cost:234)
                 \/ (1 <= K:233 /\ 0 <= __cost:160 /\ 0 <= (-1 + mid_i:235)
                       /\ 0 <= (-1 + mid___cost:234))) /\ K:236 = 0
           /\ mid_i:235 = i':237 /\ mid___cost:234 = __cost':238 /\ 0 = K:236
           /\ (K:233 + K:236) = K:239 /\ 0 <= K:239 /\ 0 <= i':237
           /\ tr:240 <= i':237)})



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
           __retres7 := -1
           argc := param0:32
           argv := param1:35
           argv@pos := param1@pos:34
           argv@width := param1@width:33
           when (param0:32 < 1 \/ 1 < param0:32)}        )
        ,
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := 0
               argc := param0:32
               argv := param1:35
               param0 := tr:213
               argv@pos := param1@pos:34
               param0@pos := type_err:214
               argv@width := param1@width:33
               param0@width := type_err:215
               when (1 <= param0:32 /\ param0:32 <= 1)}            )
            ,
            Var(20)
          )
          ,
          Weight(Base relation: 
            {tmp := havoc:11
             __retres7 := -1
             when 99 < havoc:11}          )
        )
      )
      ,
      Dot(
        Dot(
          Dot(
            Dot(
              Dot(
                Dot(
                  Dot(
                    Dot(
                      Weight(Base relation: 
                        {__cost := 0
                         argc := param0:32
                         argv := param1:35
                         param0 := tr:213
                         argv@pos := param1@pos:34
                         param0@pos := type_err:214
                         argv@width := param1@width:33
                         param0@width := type_err:215
                         when (1 <= param0:32 /\ param0:32 <= 1)}                      )
                      ,
                      Var(20)
                    )
                    ,
                    Weight(Base relation: 
                      {tmp := havoc:11
                       param0 := tr:216
                       param0@pos := type_err:217
                       param0@width := type_err:218
                       when havoc:11 <= 99}                    )
                  )
                  ,
                  Var(20)
                )
                ,
                Weight(Base relation: 
                  {param0 := tr:39
                   param1 := havoc:24
                   param0@pos := 0
                   param1@pos := type_err:40
                   param0@width := 1
                   param1@width := type_err:41}                )
              )
              ,
              Var(23)
            )
            ,
            Weight(Base relation: 
              {param0 := tr:23
               param0@pos := 0
               param0@width := 1}            )
          )
          ,
          Var(30)
        )
        ,
        Weight(Base relation: 
          {__retres7 := 0}        )
      )
    )
    ,
    Weight(Base relation: 
      {return := __retres7: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: 
  {return := havoc:149
   return@pos := type_err:151
   return@width := type_err:153})



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

Weight(Base relation: 
  {__cost := __cost':238
   return := havoc:241
   return@pos := type_err:242
   return@width := type_err:243
   when ((!(0 <= K:233) \/ mid___cost:234 = (__cost:160 + K:233))
           /\ (!(0 <= K:233) \/ mid_i:235 = K:233)
           /\ ((K:233 = 0 /\ 0 = mid_i:235 /\ __cost:160 = mid___cost:234)
                 \/ (1 <= K:233 /\ 0 <= __cost:160 /\ 0 <= (-1 + mid_i:235)
                       /\ 0 <= (-1 + mid___cost:234))) /\ K:236 = 0
           /\ mid_i:235 = i':237 /\ mid___cost:234 = __cost':238 /\ 0 = K:236
           /\ (K:233 + K:236) = K:239 /\ 0 <= K:239 /\ 0 <= i':237
           /\ tr:240 <= i':237)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=18: 
Weight(Base relation: 
  {__cost := phi___cost:286
   return := phi___retres7:284
   param0 := phi_param0:281
   param1 := phi_param1:280
   return@pos := type_err:287
   param0@pos := phi_param0@pos:277
   param1@pos := phi_param1@pos:276
   return@width := type_err:288
   param0@width := phi_param0@width:273
   param1@width := phi_param1@width:272
   when (((((param0:32 < 1 \/ 1 < param0:32) /\ tmp:289 = phi_tmp:256
              /\ param0:32 = phi_param0:255
              /\ param0@pos:31 = phi_param0@pos:254
              /\ param0@width:30 = phi_param0@width:253)
             \/ (1 <= param0:32 /\ param0:32 <= 1 /\ 99 < havoc:252
                   /\ havoc:252 = phi_tmp:256 /\ tr:213 = phi_param0:255
                   /\ type_err:214 = phi_param0@pos:254
                   /\ type_err:215 = phi_param0@width:253))
            /\ 0 = phi___cost:286 /\ phi_tmp:256 = phi_tmp:285
            /\ -1 = phi___retres7:284 /\ return:283 = phi_return:282
            /\ phi_param0:255 = phi_param0:281 /\ param1:35 = phi_param1:280
            /\ return@pos:279 = phi_return@pos:278
            /\ phi_param0@pos:254 = phi_param0@pos:277
            /\ param1@pos:34 = phi_param1@pos:276
            /\ return@width:275 = phi_return@width:274
            /\ phi_param0@width:253 = phi_param0@width:273
            /\ param1@width:33 = phi_param1@width:272)
           \/ (1 <= param0:32 /\ param0:32 <= 1 /\ havoc:244 <= 99
                 /\ (!(0 <= K:261) \/ mid___cost:262 = K:261)
                 /\ (!(0 <= K:261) \/ mid_i:263 = K:261)
                 /\ ((K:261 = 0 /\ 0 = mid_i:263 /\ 0 = mid___cost:262)
                       \/ (1 <= K:261 /\ 0 <= (-1 + mid_i:263)
                             /\ 0 <= (-1 + mid___cost:262))) /\ K:264 = 0
                 /\ mid_i:263 = i':265 /\ mid___cost:262 = __cost':266
                 /\ 0 = K:264 /\ (K:261 + K:264) = K:267 /\ 0 <= K:267
                 /\ 0 <= i':265 /\ tr:268 <= i':265
                 /\ __cost':266 = phi___cost:286 /\ havoc:244 = phi_tmp:285
                 /\ 0 = phi___retres7:284 /\ havoc:269 = phi_return:282
                 /\ tr:260 = phi_param0:281 /\ havoc:249 = phi_param1:280
                 /\ type_err:270 = phi_return@pos:278
                 /\ 0 = phi_param0@pos:277
                 /\ type_err:250 = phi_param1@pos:276
                 /\ type_err:271 = phi_return@width:274
                 /\ 1 = phi_param0@width:273
                 /\ type_err:251 = phi_param1@width:272))})


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


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=23: 
Weight(Base relation: 
  {return := havoc:149
   return@pos := type_err:151
   return@width := type_err:153})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=30: 
Weight(Base relation: 
  {__cost := __cost':238
   return := havoc:241
   return@pos := type_err:242
   return@width := type_err:243
   when ((!(0 <= K:233) \/ mid___cost:234 = (__cost:160 + K:233))
           /\ (!(0 <= K:233) \/ mid_i:235 = K:233)
           /\ ((K:233 = 0 /\ 0 = mid_i:235 /\ __cost:160 = mid___cost:234)
                 \/ (1 <= K:233 /\ 0 <= __cost:160 /\ 0 <= (-1 + mid_i:235)
                       /\ 0 <= (-1 + mid___cost:234))) /\ K:236 = 0
           /\ mid_i:235 = i':237 /\ mid___cost:234 = __cost':238 /\ 0 = K:236
           /\ (K:233 + K:236) = K:239 /\ 0 <= K:239 /\ 0 <= i':237
           /\ tr:240 <= i':237)})


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

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:286
 return := phi___retres7:284
 param0 := phi_param0:281
 param1 := phi_param1:280
 return@pos := type_err:287
 param0@pos := phi_param0@pos:277
 param1@pos := phi_param1@pos:276
 return@width := type_err:288
 param0@width := phi_param0@width:273
 param1@width := phi_param1@width:272
 when (((((param0:32 < 1 \/ 1 < param0:32) /\ tmp:289 = phi_tmp:256
            /\ param0:32 = phi_param0:255
            /\ param0@pos:31 = phi_param0@pos:254
            /\ param0@width:30 = phi_param0@width:253)
           \/ (1 <= param0:32 /\ param0:32 <= 1 /\ 99 < havoc:252
                 /\ havoc:252 = phi_tmp:256 /\ tr:213 = phi_param0:255
                 /\ type_err:214 = phi_param0@pos:254
                 /\ type_err:215 = phi_param0@width:253))
          /\ 0 = phi___cost:286 /\ phi_tmp:256 = phi_tmp:285
          /\ -1 = phi___retres7:284 /\ return:283 = phi_return:282
          /\ phi_param0:255 = phi_param0:281 /\ param1:35 = phi_param1:280
          /\ return@pos:279 = phi_return@pos:278
          /\ phi_param0@pos:254 = phi_param0@pos:277
          /\ param1@pos:34 = phi_param1@pos:276
          /\ return@width:275 = phi_return@width:274
          /\ phi_param0@width:253 = phi_param0@width:273
          /\ param1@width:33 = phi_param1@width:272)
         \/ (1 <= param0:32 /\ param0:32 <= 1 /\ havoc:244 <= 99
               /\ (!(0 <= K:261) \/ mid___cost:262 = K:261)
               /\ (!(0 <= K:261) \/ mid_i:263 = K:261)
               /\ ((K:261 = 0 /\ 0 = mid_i:263 /\ 0 = mid___cost:262)
                     \/ (1 <= K:261 /\ 0 <= (-1 + mid_i:263)
                           /\ 0 <= (-1 + mid___cost:262))) /\ K:264 = 0
               /\ mid_i:263 = i':265 /\ mid___cost:262 = __cost':266
               /\ 0 = K:264 /\ (K:261 + K:264) = K:267 /\ 0 <= K:267
               /\ 0 <= i':265 /\ tr:268 <= i':265
               /\ __cost':266 = phi___cost:286 /\ havoc:244 = phi_tmp:285
               /\ 0 = phi___retres7:284 /\ havoc:269 = phi_return:282
               /\ tr:260 = phi_param0:281 /\ havoc:249 = phi_param1:280
               /\ type_err:270 = phi_return@pos:278 /\ 0 = phi_param0@pos:277
               /\ type_err:250 = phi_param1@pos:276
               /\ type_err:271 = phi_return@width:274
               /\ 1 = phi_param0@width:273
               /\ type_err:251 = phi_param1@width:272))}

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: 
{return := havoc:149
 return@pos := type_err:151
 return@width := type_err:153}

Evaluating variable number 30 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':238
 return := havoc:241
 return@pos := type_err:242
 return@width := type_err:243
 when ((!(0 <= K:233) \/ mid___cost:234 = (__cost:160 + K:233))
         /\ (!(0 <= K:233) \/ mid_i:235 = K:233)
         /\ ((K:233 = 0 /\ 0 = mid_i:235 /\ __cost:160 = mid___cost:234)
               \/ (1 <= K:233 /\ 0 <= __cost:160 /\ 0 <= (-1 + mid_i:235)
                     /\ 0 <= (-1 + mid___cost:234))) /\ K:236 = 0
         /\ mid_i:235 = i':237 /\ mid___cost:234 = __cost':238 /\ 0 = K:236
         /\ (K:233 + K:236) = K:239 /\ 0 <= K:239 /\ 0 <= i':237
         /\ tr:240 <= i':237)}

    (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,56)_g1>	Base relation: 
{__cost := 0
 tmp := havoc:295
 argc := param0:32
 argv := param1:35
 return := havoc:303
 param0 := tr:306
 param1 := havoc:300
 argv@pos := param1@pos:34
 return@pos := type_err:304
 param0@pos := 0
 param1@pos := type_err:301
 argv@width := param1@width:33
 return@width := type_err:305
 param0@width := 1
 param1@width := type_err:302
 when (1 <= param0:32 /\ param0:32 <= 1 /\ havoc:295 <= 99)}	
<__pstate, accept> -> <__pstate, (Unique State Name,77)_g1>	Base relation: 
{__cost := 0
 tmp := phi_tmp:336
 argc := param0:32
 argv := param1:35
 param0 := phi_param0:335
 argv@pos := param1@pos:34
 param0@pos := phi_param0@pos:334
 argv@width := param1@width:33
 param0@width := phi_param0@width:333
 when ((1 <= param0:32 /\ param0:32 <= 1 /\ tmp:3 = phi_tmp:336
          /\ tr:213 = phi_param0:335 /\ type_err:214 = phi_param0@pos:334
          /\ type_err:215 = phi_param0@width:333)
         \/ (1 <= param0:32 /\ param0:32 <= 1 /\ havoc:295 <= 99
               /\ havoc:295 = phi_tmp:336 /\ tr:296 = phi_param0:335
               /\ type_err:297 = phi_param0@pos:334
               /\ type_err:298 = phi_param0@width:333))}	
<__pstate, accept> -> <__pstate, (Unique State Name,54)_g1>	Base relation: 
{__cost := 0
 tmp := havoc:295
 argc := param0:32
 argv := param1:35
 param0 := tr:299
 param1 := havoc:300
 argv@pos := param1@pos:34
 param0@pos := 0
 param1@pos := type_err:301
 argv@width := param1@width:33
 param0@width := 1
 param1@width := type_err:302
 when (1 <= param0:32 /\ param0:32 <= 1 /\ havoc:295 <= 99)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x6c65d90: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x6c65b00: 
	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,56)_g1 , __done )	Base relation: 
{__cost := 0
 tmp := havoc:295
 argc := param0:32
 argv := param1:35
 return := havoc:303
 param0 := tr:306
 param1 := havoc:300
 argv@pos := param1@pos:34
 return@pos := type_err:304
 param0@pos := 0
 param1@pos := type_err:301
 argv@width := param1@width:33
 return@width := type_err:305
 param0@width := 1
 param1@width := type_err:302
 when (1 <= param0:32 /\ param0:32 <= 1 /\ havoc:295 <= 99)}
    ( __pstate , (Unique State Name,54)_g1 , __done )	Base relation: 
{__cost := 0
 tmp := havoc:295
 argc := param0:32
 argv := param1:35
 param0 := tr:299
 param1 := havoc:300
 argv@pos := param1@pos:34
 param0@pos := 0
 param1@pos := type_err:301
 argv@width := param1@width:33
 param0@width := 1
 param1@width := type_err:302
 when (1 <= param0:32 /\ param0:32 <= 1 /\ havoc:295 <= 99)}
    ( __pstate , (Unique State Name,77)_g1 , __done )	Base relation: 
{__cost := 0
 tmp := phi_tmp:336
 argc := param0:32
 argv := param1:35
 param0 := phi_param0:335
 argv@pos := param1@pos:34
 param0@pos := phi_param0@pos:334
 argv@width := param1@width:33
 param0@width := phi_param0@width:333
 when ((1 <= param0:32 /\ param0:32 <= 1 /\ tmp:3 = phi_tmp:336
          /\ tr:213 = phi_param0:335 /\ type_err:214 = phi_param0@pos:334
          /\ type_err:215 = phi_param0@width:333)
         \/ (1 <= param0:32 /\ param0:32 <= 1 /\ havoc:295 <= 99
               /\ havoc:295 = phi_tmp:336 /\ tr:296 = phi_param0:335
               /\ type_err:297 = phi_param0@pos:334
               /\ type_err:298 = phi_param0@width:333))}

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

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

Base relation: 
{}

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

Base relation: 
{__cost := __cost':238
 i := i':237
 return := havoc:241
 return@pos := type_err:242
 return@width := type_err:243
 when ((!(0 <= K:233) \/ mid___cost:234 = (__cost:160 + K:233))
         /\ (!(0 <= K:233) \/ mid_i:235 = K:233)
         /\ ((K:233 = 0 /\ 0 = mid_i:235 /\ __cost:160 = mid___cost:234)
               \/ (1 <= K:233 /\ 0 <= __cost:160 /\ 0 <= (-1 + mid_i:235)
                     /\ 0 <= (-1 + mid___cost:234))) /\ K:236 = 0
         /\ mid_i:235 = i':237 /\ mid___cost:234 = __cost':238 /\ 0 = K:236
         /\ (K:233 + K:236) = K:239 /\ 0 <= K:239 /\ 0 <= i':237
         /\ tr:240 <= i':237)}

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

Base relation: 
{return := havoc:149
 return@pos := type_err:151
 return@width := type_err:153}

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

Base relation: 
{__cost := phi___cost:329
 tmp := phi_tmp:328
 __retres7 := phi___retres7:327
 argc := param0:32
 argv := param1:35
 return := phi___retres7:327
 param0 := phi_param0:325
 param1 := phi_param1:324
 argv@pos := param1@pos:34
 return@pos := type_err:330
 param0@pos := phi_param0@pos:322
 param1@pos := phi_param1@pos:321
 argv@width := param1@width:33
 return@width := type_err:331
 param0@width := phi_param0@width:319
 param1@width := phi_param1@width:318
 when (((((param0:32 < 1 \/ 1 < param0:32) /\ tmp:3 = phi_tmp:294
            /\ param0:32 = phi_param0:293
            /\ param0@pos:31 = phi_param0@pos:292
            /\ param0@width:30 = phi_param0@width:291)
           \/ (1 <= param0:32 /\ param0:32 <= 1 /\ 99 < havoc:290
                 /\ havoc:290 = phi_tmp:294 /\ tr:213 = phi_param0:293
                 /\ type_err:214 = phi_param0@pos:292
                 /\ type_err:215 = phi_param0@width:291))
          /\ 0 = phi___cost:329 /\ phi_tmp:294 = phi_tmp:328
          /\ -1 = phi___retres7:327 /\ return:283 = phi_return:326
          /\ phi_param0:293 = phi_param0:325 /\ param1:35 = phi_param1:324
          /\ return@pos:279 = phi_return@pos:323
          /\ phi_param0@pos:292 = phi_param0@pos:322
          /\ param1@pos:34 = phi_param1@pos:321
          /\ return@width:275 = phi_return@width:320
          /\ phi_param0@width:291 = phi_param0@width:319
          /\ param1@width:33 = phi_param1@width:318)
         \/ (1 <= param0:32 /\ param0:32 <= 1 /\ havoc:295 <= 99
               /\ (!(0 <= K:307) \/ mid___cost:308 = K:307)
               /\ (!(0 <= K:307) \/ mid_i:309 = K:307)
               /\ ((K:307 = 0 /\ 0 = mid_i:309 /\ 0 = mid___cost:308)
                     \/ (1 <= K:307 /\ 0 <= (-1 + mid_i:309)
                           /\ 0 <= (-1 + mid___cost:308))) /\ K:310 = 0
               /\ mid_i:309 = i':311 /\ mid___cost:308 = __cost':312
               /\ 0 = K:310 /\ (K:307 + K:310) = K:313 /\ 0 <= K:313
               /\ 0 <= i':311 /\ tr:314 <= i':311
               /\ __cost':312 = phi___cost:329 /\ havoc:295 = phi_tmp:328
               /\ 0 = phi___retres7:327 /\ havoc:315 = phi_return:326
               /\ tr:306 = phi_param0:325 /\ havoc:300 = phi_param1:324
               /\ type_err:316 = phi_return@pos:323 /\ 0 = phi_param0@pos:322
               /\ type_err:301 = phi_param1@pos:321
               /\ type_err:317 = phi_return@width:320
               /\ 1 = phi_param0@width:319
               /\ type_err:302 = phi_param1@width:318))}

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

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

Variable bounds at line 17 in bar

min((1 + __cost), __cost) <= __cost
__cost is o(1)

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