/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, 33> -> <Unique State Name, 29>	Base relation: 
{__cost := (__cost:102 + 1)
 i := (i:101 + -1)
 when (100 < i:101 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}	
<Unique State Name, 33> -> <Unique State Name, 45>	Base relation: 
{i := ((i:101 + k:103) + 50)
 when i:101 <= 100}	
<Unique State Name, 76> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 67> -> <Unique State Name, 25>	Base relation: 
{}	
<Unique State Name, 74> -> <Unique State Name, 69 73>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 49> -> <Unique State Name, 45>	Base relation: 
{__cost := (__cost:102 + 1)
 i := (i:101 + -1)
 when (0 <= i:101 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}	
<Unique State Name, 49> -> <Unique State Name, 75>	Base relation: 
{return := havoc:109
 return@pos := type_err:110
 return@width := type_err:111
 when i:101 < 0}	
<Unique State Name, 23> -> <Unique State Name, 74>	Base relation: 
{__cost := 0
 i := havoc:21
 k := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}	
<Unique State Name, 75> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 79> -> <Unique State Name, 33>	Base relation: 
{}	
<Unique State Name, 25> -> <Unique State Name, 76>	Base relation: 
{return := havoc:63
 return@pos := type_err:66
 return@width := type_err:67}	
<Unique State Name, 78> -> <Unique State Name, 49>	Base relation: 
{}	
<Unique State Name, 73> -> <Unique State Name, 77>	Base relation: 
{return := 0
 return@pos := type_err:32
 return@width := type_err:33
 when (((-1 < i:4 /\ (i:4 + 1) = phi_tmp___1:23)
          \/ (i:4 <= -1 /\ 0 = phi_tmp___1:23))
         /\ ((0 < k:5 /\ k:5 = phi_tmp___2:31)
               \/ (k:5 <= 0 /\ 0 = phi_tmp___2:31)))}	
<Unique State Name, 29> -> <Unique State Name, 79>	Base relation: 
{}	
<Unique State Name, 45> -> <Unique State Name, 78>	Base relation: 
{}	
<Unique State Name, 69> -> <Unique State Name, 68>	Base relation: 
{param0 := param0:80
 param1 := param1:83
 param0@pos := type_err:88
 param1@pos := type_err:89
 param0@width := type_err:90
 param1@width := type_err:91}	
<Unique State Name, 63> -> <Unique State Name, 29>	Base relation: 
{i := param0:80
 k := param1:83}	
<Unique State Name, 77> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 68> -> <Unique State Name, 63 67>	Base relation: 
{}	MergeFn[Base relation: 
{}]
#################################################################
           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:102 + 1)
 i := (i:101 + -1)
 when (100 < i:101 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':158) = (1)*(__cost:102) + 1
           (i':159) = (1)*(i:101) + (-1)*1
           }
          pre:
            [|__cost:102>=0; i:101-101>=0|]
          post:
            [|i':159-100>=0; __cost':158-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':158
   i := i':159
   when ((!(0 <= K:167) \/ mid___cost:170 = (__cost:102 + K:167))
           /\ (!(0 <= K:167) \/ mid_i:169 = (i:101 + -K:167))
           /\ ((K:167 = 0 /\ i:101 = mid_i:169 /\ __cost:102 = mid___cost:170)
                 \/ (1 <= K:167 /\ 0 <= __cost:102 /\ 0 <= (-101 + i:101)
                       /\ 0 <= (-100 + mid_i:169)
                       /\ 0 <= (-1 + mid___cost:170))) /\ K:168 = 0
           /\ mid_i:169 = i':159 /\ mid___cost:170 = __cost':158 /\ 0 = K:168
           /\ (K:167 + K:168) = K:166 /\ 0 <= K:166)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:102 + 1)
 i := (i:101 + -1)
 when (0 <= i:101 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':158) = (1)*(__cost:102) + 1
           (i':159) = (1)*(i:101) + (-1)*1
           }
          pre:
            [|i:101>=0; __cost:102>=0|]
          post:
            [|i':159+1>=0; __cost':158-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':158
   i := i':159
   when ((!(0 <= K:185) \/ mid___cost:188 = (__cost:102 + K:185))
           /\ (!(0 <= K:185) \/ mid_i:187 = (i:101 + -K:185))
           /\ ((K:185 = 0 /\ i:101 = mid_i:187 /\ __cost:102 = mid___cost:188)
                 \/ (1 <= K:185 /\ 0 <= i:101 /\ 0 <= __cost:102
                       /\ 0 <= (1 + mid_i:187) /\ 0 <= (-1 + mid___cost:188)))
           /\ K:186 = 0 /\ mid_i:187 = i':159 /\ mid___cost:188 = __cost':158
           /\ 0 = K:186 /\ (K:185 + K:186) = K:184 /\ 0 <= K:184)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  22  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       i := havoc:21
       k := havoc:22
       param0 := havoc:21
       param1 := havoc:22
       param0@pos := type_err:27
       param1@pos := type_err:29
       param0@width := type_err:28
       param1@width := type_err:30}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:32
     return@width := type_err:33
     when (((-1 < i:4 /\ (i:4 + 1) = phi_tmp___1:23)
              \/ (i:4 <= -1 /\ 0 = phi_tmp___1:23))
             /\ ((0 < k:5 /\ k:5 = phi_tmp___2:31)
                   \/ (k:5 <= 0 /\ 0 = phi_tmp___2:31)))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:80
       param1 := param1:83
       param0@pos := type_err:88
       param1@pos := type_err:89
       param0@width := type_err:90
       param1@width := type_err:91}    )
    ,
    Var(22)
  )
  ,
  Weight(Base relation: 
    {return := havoc:63
     return@pos := type_err:66
     return@width := type_err:67}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=22: 
Weight(Base relation: 
  {__cost := __cost':194
   i := i':193
   k := param1:83
   return := havoc:196
   return@pos := type_err:197
   return@width := type_err:198
   when ((!(0 <= K:171) \/ mid___cost:172 = (__cost:102 + K:171))
           /\ (!(0 <= K:171) \/ mid_i:173 = (param0:80 + -K:171))
           /\ ((K:171 = 0 /\ param0:80 = mid_i:173
                  /\ __cost:102 = mid___cost:172)
                 \/ (1 <= K:171 /\ 0 <= __cost:102 /\ 0 <= (-101 + param0:80)
                       /\ 0 <= (-100 + mid_i:173)
                       /\ 0 <= (-1 + mid___cost:172))) /\ K:174 = 0
           /\ mid_i:173 = i':175 /\ mid___cost:172 = __cost':176 /\ 0 = K:174
           /\ (K:171 + K:174) = K:177 /\ 0 <= K:177 /\ i':175 <= 100
           /\ (!(0 <= K:189) \/ mid___cost:190 = (__cost':176 + K:189))
           /\ (!(0 <= K:189)
                 \/ mid_i:191 = (((i':175 + param1:83) + 50) + -K:189))
           /\ ((K:189 = 0 /\ ((i':175 + param1:83) + 50) = mid_i:191
                  /\ __cost':176 = mid___cost:190)
                 \/ (1 <= K:189 /\ 0 <= ((i':175 + param1:83) + 50)
                       /\ 0 <= __cost':176 /\ 0 <= (1 + mid_i:191)
                       /\ 0 <= (-1 + mid___cost:190))) /\ K:192 = 0
           /\ mid_i:191 = i':193 /\ mid___cost:190 = __cost':194 /\ 0 = K:192
           /\ (K:189 + K:192) = K:195 /\ 0 <= K:195 /\ i':193 < 0)})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := 0
         i := havoc:21
         k := havoc:22
         param0 := havoc:21
         param1 := havoc:22
         param0@pos := type_err:27
         param1@pos := type_err:29
         param0@width := type_err:28
         param1@width := type_err:30}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:32
       return@width := type_err:33
       when (((-1 < i:4 /\ (i:4 + 1) = phi_tmp___1:23)
                \/ (i:4 <= -1 /\ 0 = phi_tmp___1:23))
               /\ ((0 < k:5 /\ k:5 = phi_tmp___2:31)
                     \/ (k:5 <= 0 /\ 0 = phi_tmp___2:31)))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:80
         param1 := param1:83
         param0@pos := type_err:88
         param1@pos := type_err:89
         param0@width := type_err:90
         param1@width := type_err:91}      )
      ,
      Var(22)
    )
    ,
    Weight(Base relation: 
      {return := havoc:63
       return@pos := type_err:66
       return@width := type_err:67}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':194
   return := havoc:196
   return@pos := type_err:197
   return@width := type_err:198
   when ((!(0 <= K:171) \/ mid___cost:172 = (__cost:102 + K:171))
           /\ (!(0 <= K:171) \/ mid_i:173 = (param0:80 + -K:171))
           /\ ((K:171 = 0 /\ param0:80 = mid_i:173
                  /\ __cost:102 = mid___cost:172)
                 \/ (1 <= K:171 /\ 0 <= __cost:102 /\ 0 <= (-101 + param0:80)
                       /\ 0 <= (-100 + mid_i:173)
                       /\ 0 <= (-1 + mid___cost:172))) /\ K:174 = 0
           /\ mid_i:173 = i':175 /\ mid___cost:172 = __cost':176 /\ 0 = K:174
           /\ (K:171 + K:174) = K:177 /\ 0 <= K:177 /\ i':175 <= 100
           /\ (!(0 <= K:189) \/ mid___cost:190 = (__cost':176 + K:189))
           /\ (!(0 <= K:189)
                 \/ mid_i:191 = (((i':175 + param1:83) + 50) + -K:189))
           /\ ((K:189 = 0 /\ ((i':175 + param1:83) + 50) = mid_i:191
                  /\ __cost':176 = mid___cost:190)
                 \/ (1 <= K:189 /\ 0 <= ((i':175 + param1:83) + 50)
                       /\ 0 <= __cost':176 /\ 0 <= (1 + mid_i:191)
                       /\ 0 <= (-1 + mid___cost:190))) /\ K:192 = 0
           /\ mid_i:191 = i':193 /\ mid___cost:190 = __cost':194 /\ 0 = K:192
           /\ (K:189 + K:192) = K:195 /\ 0 <= K:195 /\ i':193 < 0)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':231
   return := 0
   param0 := havoc:21
   param1 := havoc:22
   return@pos := type_err:242
   param0@pos := type_err:235
   param1@pos := type_err:236
   return@width := type_err:243
   param0@width := type_err:238
   param1@width := type_err:239
   when ((!(0 <= K:219) \/ mid___cost:220 = K:219)
           /\ (!(0 <= K:219) \/ mid_i:221 = (havoc:21 + -K:219))
           /\ ((K:219 = 0 /\ havoc:21 = mid_i:221 /\ 0 = mid___cost:220)
                 \/ (1 <= K:219 /\ 0 <= (-101 + havoc:21)
                       /\ 0 <= (-100 + mid_i:221)
                       /\ 0 <= (-1 + mid___cost:220))) /\ K:222 = 0
           /\ mid_i:221 = i':223 /\ mid___cost:220 = __cost':224 /\ 0 = K:222
           /\ (K:219 + K:222) = K:225 /\ 0 <= K:225 /\ i':223 <= 100
           /\ (!(0 <= K:226) \/ mid___cost:227 = (__cost':224 + K:226))
           /\ (!(0 <= K:226)
                 \/ mid_i:228 = (((i':223 + havoc:22) + 50) + -K:226))
           /\ ((K:226 = 0 /\ ((i':223 + havoc:22) + 50) = mid_i:228
                  /\ __cost':224 = mid___cost:227)
                 \/ (1 <= K:226 /\ 0 <= ((i':223 + havoc:22) + 50)
                       /\ 0 <= __cost':224 /\ 0 <= (1 + mid_i:228)
                       /\ 0 <= (-1 + mid___cost:227))) /\ K:229 = 0
           /\ mid_i:228 = i':230 /\ mid___cost:227 = __cost':231 /\ 0 = K:229
           /\ (K:226 + K:229) = K:232 /\ 0 <= K:232 /\ i':230 < 0
           /\ ((-1 < havoc:21 /\ (havoc:21 + 1) = phi_tmp___1:240)
                 \/ (havoc:21 <= -1 /\ 0 = phi_tmp___1:240))
           /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:241)
                 \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:241)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':256
   return := havoc:261
   param0 := param0:80
   param1 := param1:83
   return@pos := type_err:262
   param0@pos := type_err:88
   param1@pos := type_err:89
   return@width := type_err:263
   param0@width := type_err:90
   param1@width := type_err:91
   when ((!(0 <= K:244) \/ mid___cost:245 = (__cost:102 + K:244))
           /\ (!(0 <= K:244) \/ mid_i:246 = (param0:80 + -K:244))
           /\ ((K:244 = 0 /\ param0:80 = mid_i:246
                  /\ __cost:102 = mid___cost:245)
                 \/ (1 <= K:244 /\ 0 <= __cost:102 /\ 0 <= (-101 + param0:80)
                       /\ 0 <= (-100 + mid_i:246)
                       /\ 0 <= (-1 + mid___cost:245))) /\ K:247 = 0
           /\ mid_i:246 = i':248 /\ mid___cost:245 = __cost':249 /\ 0 = K:247
           /\ (K:244 + K:247) = K:250 /\ 0 <= K:250 /\ i':248 <= 100
           /\ (!(0 <= K:251) \/ mid___cost:252 = (__cost':249 + K:251))
           /\ (!(0 <= K:251)
                 \/ mid_i:253 = (((i':248 + param1:83) + 50) + -K:251))
           /\ ((K:251 = 0 /\ ((i':248 + param1:83) + 50) = mid_i:253
                  /\ __cost':249 = mid___cost:252)
                 \/ (1 <= K:251 /\ 0 <= ((i':248 + param1:83) + 50)
                       /\ 0 <= __cost':249 /\ 0 <= (1 + mid_i:253)
                       /\ 0 <= (-1 + mid___cost:252))) /\ K:254 = 0
           /\ mid_i:253 = i':255 /\ mid___cost:252 = __cost':256 /\ 0 = K:254
           /\ (K:251 + K:254) = K:257 /\ 0 <= K:257 /\ i':255 < 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=22: 
Weight(Base relation: 
  {__cost := __cost':194
   return := havoc:196
   return@pos := type_err:197
   return@width := type_err:198
   when ((!(0 <= K:171) \/ mid___cost:172 = (__cost:102 + K:171))
           /\ (!(0 <= K:171) \/ mid_i:173 = (param0:80 + -K:171))
           /\ ((K:171 = 0 /\ param0:80 = mid_i:173
                  /\ __cost:102 = mid___cost:172)
                 \/ (1 <= K:171 /\ 0 <= __cost:102 /\ 0 <= (-101 + param0:80)
                       /\ 0 <= (-100 + mid_i:173)
                       /\ 0 <= (-1 + mid___cost:172))) /\ K:174 = 0
           /\ mid_i:173 = i':175 /\ mid___cost:172 = __cost':176 /\ 0 = K:174
           /\ (K:171 + K:174) = K:177 /\ 0 <= K:177 /\ i':175 <= 100
           /\ (!(0 <= K:189) \/ mid___cost:190 = (__cost':176 + K:189))
           /\ (!(0 <= K:189)
                 \/ mid_i:191 = (((i':175 + param1:83) + 50) + -K:189))
           /\ ((K:189 = 0 /\ ((i':175 + param1:83) + 50) = mid_i:191
                  /\ __cost':176 = mid___cost:190)
                 \/ (1 <= K:189 /\ 0 <= ((i':175 + param1:83) + 50)
                       /\ 0 <= __cost':176 /\ 0 <= (1 + mid_i:191)
                       /\ 0 <= (-1 + mid___cost:190))) /\ K:192 = 0
           /\ mid_i:191 = i':193 /\ mid___cost:190 = __cost':194 /\ 0 = K:192
           /\ (K:189 + K:192) = K:195 /\ 0 <= K:195 /\ i':193 < 0)})


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

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':231
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:242
 param0@pos := type_err:235
 param1@pos := type_err:236
 return@width := type_err:243
 param0@width := type_err:238
 param1@width := type_err:239
 when ((!(0 <= K:219) \/ mid___cost:220 = K:219)
         /\ (!(0 <= K:219) \/ mid_i:221 = (havoc:21 + -K:219))
         /\ ((K:219 = 0 /\ havoc:21 = mid_i:221 /\ 0 = mid___cost:220)
               \/ (1 <= K:219 /\ 0 <= (-101 + havoc:21)
                     /\ 0 <= (-100 + mid_i:221) /\ 0 <= (-1 + mid___cost:220)))
         /\ K:222 = 0 /\ mid_i:221 = i':223 /\ mid___cost:220 = __cost':224
         /\ 0 = K:222 /\ (K:219 + K:222) = K:225 /\ 0 <= K:225
         /\ i':223 <= 100
         /\ (!(0 <= K:226) \/ mid___cost:227 = (__cost':224 + K:226))
         /\ (!(0 <= K:226)
               \/ mid_i:228 = (((i':223 + havoc:22) + 50) + -K:226))
         /\ ((K:226 = 0 /\ ((i':223 + havoc:22) + 50) = mid_i:228
                /\ __cost':224 = mid___cost:227)
               \/ (1 <= K:226 /\ 0 <= ((i':223 + havoc:22) + 50)
                     /\ 0 <= __cost':224 /\ 0 <= (1 + mid_i:228)
                     /\ 0 <= (-1 + mid___cost:227))) /\ K:229 = 0
         /\ mid_i:228 = i':230 /\ mid___cost:227 = __cost':231 /\ 0 = K:229
         /\ (K:226 + K:229) = K:232 /\ 0 <= K:232 /\ i':230 < 0
         /\ ((-1 < havoc:21 /\ (havoc:21 + 1) = phi_tmp___1:240)
               \/ (havoc:21 <= -1 /\ 0 = phi_tmp___1:240))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:241)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:241)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':256
 return := havoc:261
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:262
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:263
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:244) \/ mid___cost:245 = (__cost:102 + K:244))
         /\ (!(0 <= K:244) \/ mid_i:246 = (param0:80 + -K:244))
         /\ ((K:244 = 0 /\ param0:80 = mid_i:246
                /\ __cost:102 = mid___cost:245)
               \/ (1 <= K:244 /\ 0 <= __cost:102 /\ 0 <= (-101 + param0:80)
                     /\ 0 <= (-100 + mid_i:246) /\ 0 <= (-1 + mid___cost:245)))
         /\ K:247 = 0 /\ mid_i:246 = i':248 /\ mid___cost:245 = __cost':249
         /\ 0 = K:247 /\ (K:244 + K:247) = K:250 /\ 0 <= K:250
         /\ i':248 <= 100
         /\ (!(0 <= K:251) \/ mid___cost:252 = (__cost':249 + K:251))
         /\ (!(0 <= K:251)
               \/ mid_i:253 = (((i':248 + param1:83) + 50) + -K:251))
         /\ ((K:251 = 0 /\ ((i':248 + param1:83) + 50) = mid_i:253
                /\ __cost':249 = mid___cost:252)
               \/ (1 <= K:251 /\ 0 <= ((i':248 + param1:83) + 50)
                     /\ 0 <= __cost':249 /\ 0 <= (1 + mid_i:253)
                     /\ 0 <= (-1 + mid___cost:252))) /\ K:254 = 0
         /\ mid_i:253 = i':255 /\ mid___cost:252 = __cost':256 /\ 0 = K:254
         /\ (K:251 + K:254) = K:257 /\ 0 <= K:257 /\ i':255 < 0)}

Evaluating variable number 22 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':194
 return := havoc:196
 return@pos := type_err:197
 return@width := type_err:198
 when ((!(0 <= K:171) \/ mid___cost:172 = (__cost:102 + K:171))
         /\ (!(0 <= K:171) \/ mid_i:173 = (param0:80 + -K:171))
         /\ ((K:171 = 0 /\ param0:80 = mid_i:173
                /\ __cost:102 = mid___cost:172)
               \/ (1 <= K:171 /\ 0 <= __cost:102 /\ 0 <= (-101 + param0:80)
                     /\ 0 <= (-100 + mid_i:173) /\ 0 <= (-1 + mid___cost:172)))
         /\ K:174 = 0 /\ mid_i:173 = i':175 /\ mid___cost:172 = __cost':176
         /\ 0 = K:174 /\ (K:171 + K:174) = K:177 /\ 0 <= K:177
         /\ i':175 <= 100
         /\ (!(0 <= K:189) \/ mid___cost:190 = (__cost':176 + K:189))
         /\ (!(0 <= K:189)
               \/ mid_i:191 = (((i':175 + param1:83) + 50) + -K:189))
         /\ ((K:189 = 0 /\ ((i':175 + param1:83) + 50) = mid_i:191
                /\ __cost':176 = mid___cost:190)
               \/ (1 <= K:189 /\ 0 <= ((i':175 + param1:83) + 50)
                     /\ 0 <= __cost':176 /\ 0 <= (1 + mid_i:191)
                     /\ 0 <= (-1 + mid___cost:190))) /\ K:192 = 0
         /\ mid_i:191 = i':193 /\ mid___cost:190 = __cost':194 /\ 0 = K:192
         /\ (K:189 + K:192) = K:195 /\ 0 <= K:195 /\ i':193 < 0)}

    (IRE-tc) Checking termination condition.
    (IRE-tc)     >> All star bodies equivalent.

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,69)_g1> -> <__pstate, (Unique State Name,63)_g1>	Base relation: 
{param0 := param0:80
 param1 := param1:83
 param0@pos := type_err:88
 param1@pos := type_err:89
 param0@width := type_err:90
 param1@width := type_err:91}	
<__pstate, accept> -> <__pstate, (Unique State Name,69)_g1>	Base relation: 
{__cost := 0
 i := havoc:21
 k := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x12255b0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x2219d70: 
	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,63)_g1 , __done )	Base relation: 
{__cost := 0
 i := havoc:21
 k := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:309
 param1@pos := type_err:310
 param0@width := type_err:311
 param1@width := type_err:312}
    ( __pstate , (Unique State Name,69)_g1 , __done )	Base relation: 
{__cost := 0
 i := havoc:21
 k := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}

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

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

Base relation: 
{__cost := __cost':276
 i := havoc:21
 k := havoc:22
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:287
 param0@pos := type_err:280
 param1@pos := type_err:281
 return@width := type_err:288
 param0@width := type_err:283
 param1@width := type_err:284
 when ((!(0 <= K:264) \/ mid___cost:265 = K:264)
         /\ (!(0 <= K:264) \/ mid_i:266 = (havoc:21 + -K:264))
         /\ ((K:264 = 0 /\ havoc:21 = mid_i:266 /\ 0 = mid___cost:265)
               \/ (1 <= K:264 /\ 0 <= (-101 + havoc:21)
                     /\ 0 <= (-100 + mid_i:266) /\ 0 <= (-1 + mid___cost:265)))
         /\ K:267 = 0 /\ mid_i:266 = i':268 /\ mid___cost:265 = __cost':269
         /\ 0 = K:267 /\ (K:264 + K:267) = K:270 /\ 0 <= K:270
         /\ i':268 <= 100
         /\ (!(0 <= K:271) \/ mid___cost:272 = (__cost':269 + K:271))
         /\ (!(0 <= K:271)
               \/ mid_i:273 = (((i':268 + havoc:22) + 50) + -K:271))
         /\ ((K:271 = 0 /\ ((i':268 + havoc:22) + 50) = mid_i:273
                /\ __cost':269 = mid___cost:272)
               \/ (1 <= K:271 /\ 0 <= ((i':268 + havoc:22) + 50)
                     /\ 0 <= __cost':269 /\ 0 <= (1 + mid_i:273)
                     /\ 0 <= (-1 + mid___cost:272))) /\ K:274 = 0
         /\ mid_i:273 = i':275 /\ mid___cost:272 = __cost':276 /\ 0 = K:274
         /\ (K:271 + K:274) = K:277 /\ 0 <= K:277 /\ i':275 < 0
         /\ ((-1 < havoc:21 /\ (havoc:21 + 1) = phi_tmp___1:285)
               \/ (havoc:21 <= -1 /\ 0 = phi_tmp___1:285))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:286)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:286)))}

------------------------------------------------
Procedure summary for run

Base relation: 
{__cost := __cost':301
 return := havoc:306
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:307
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:308
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:289) \/ mid___cost:290 = (__cost:102 + K:289))
         /\ (!(0 <= K:289) \/ mid_i:291 = (param0:80 + -K:289))
         /\ ((K:289 = 0 /\ param0:80 = mid_i:291
                /\ __cost:102 = mid___cost:290)
               \/ (1 <= K:289 /\ 0 <= __cost:102 /\ 0 <= (-101 + param0:80)
                     /\ 0 <= (-100 + mid_i:291) /\ 0 <= (-1 + mid___cost:290)))
         /\ K:292 = 0 /\ mid_i:291 = i':293 /\ mid___cost:290 = __cost':294
         /\ 0 = K:292 /\ (K:289 + K:292) = K:295 /\ 0 <= K:295
         /\ i':293 <= 100
         /\ (!(0 <= K:296) \/ mid___cost:297 = (__cost':294 + K:296))
         /\ (!(0 <= K:296)
               \/ mid_i:298 = (((i':293 + param1:83) + 50) + -K:296))
         /\ ((K:296 = 0 /\ ((i':293 + param1:83) + 50) = mid_i:298
                /\ __cost':294 = mid___cost:297)
               \/ (1 <= K:296 /\ 0 <= ((i':293 + param1:83) + 50)
                     /\ 0 <= __cost':294 /\ 0 <= (1 + mid_i:298)
                     /\ 0 <= (-1 + mid___cost:297))) /\ K:299 = 0
         /\ mid_i:298 = i':300 /\ mid___cost:297 = __cost':301 /\ 0 = K:299
         /\ (K:296 + K:299) = K:302 /\ 0 <= K:302 /\ i':300 < 0)}

------------------------------------------------
Procedure summary for start

Base relation: 
{__cost := __cost':194
 i := i':193
 k := param1:83
 return := havoc:196
 return@pos := type_err:197
 return@width := type_err:198
 when ((!(0 <= K:171) \/ mid___cost:172 = (__cost:102 + K:171))
         /\ (!(0 <= K:171) \/ mid_i:173 = (param0:80 + -K:171))
         /\ ((K:171 = 0 /\ param0:80 = mid_i:173
                /\ __cost:102 = mid___cost:172)
               \/ (1 <= K:171 /\ 0 <= __cost:102 /\ 0 <= (-101 + param0:80)
                     /\ 0 <= (-100 + mid_i:173) /\ 0 <= (-1 + mid___cost:172)))
         /\ K:174 = 0 /\ mid_i:173 = i':175 /\ mid___cost:172 = __cost':176
         /\ 0 = K:174 /\ (K:171 + K:174) = K:177 /\ 0 <= K:177
         /\ i':175 <= 100
         /\ (!(0 <= K:189) \/ mid___cost:190 = (__cost':176 + K:189))
         /\ (!(0 <= K:189)
               \/ mid_i:191 = (((i':175 + param1:83) + 50) + -K:189))
         /\ ((K:189 = 0 /\ ((i':175 + param1:83) + 50) = mid_i:191
                /\ __cost':176 = mid___cost:190)
               \/ (1 <= K:189 /\ 0 <= ((i':175 + param1:83) + 50)
                     /\ 0 <= __cost':176 /\ 0 <= (1 + mid_i:191)
                     /\ 0 <= (-1 + mid___cost:190))) /\ K:192 = 0
         /\ mid_i:191 = i':193 /\ mid___cost:190 = __cost':194 /\ 0 = K:192
         /\ (K:189 + K:192) = K:195 /\ 0 <= K:195 /\ i':193 < 0)}

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

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

Variable bounds at line 21 in run

min(min((-100 + __cost + i), __cost),
    max((-99 + __cost + i), (50 + __cost + i + k))) <= __cost
__cost is o(1)
__cost <= max(max((-100 + __cost + i), __cost), (51 + __cost + i + k))
__cost is O(n)

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