/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, 49>	Base relation: 
{}	
<Unique State Name, 17> -> <Unique State Name, 72>	Base relation: 
{return := havoc:41
 return@pos := type_err:44
 return@width := type_err:45}	
<Unique State Name, 15> -> <Unique State Name, 70>	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
<Unique State Name, 22> -> <Unique State Name, 75>	Base relation: 
{when 0 <= x:62}	
<Unique State Name, 71> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 69> -> <Unique State Name, 73>	Base relation: 
{return := 0
 return@pos := type_err:19
 return@width := type_err:20
 when ((0 < n:2 /\ n:2 = phi_tmp___0:14) \/ (n:2 <= 0 /\ 0 = phi_tmp___0:14))}	
<Unique State Name, 67> -> <Unique State Name, 66>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
<Unique State Name, 73> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 65> -> <Unique State Name, 17>	Base relation: 
{}	
<Unique State Name, 44> -> <Unique State Name, 45>	Base relation: 
{}	
<Unique State Name, 49> -> <Unique State Name, 45>	Base relation: 
{__cost := (__cost:66 + 1)
 x := (x:62 + 1)
 when (x:62 < n:63 /\ 0 <= __cost:66 /\ 0 <= (__cost:66 + 1))}	
<Unique State Name, 49> -> <Unique State Name, 71>	Base relation: 
{return := havoc:73
 return@pos := type_err:74
 return@width := type_err:75
 when n:63 <= x:62}	
<Unique State Name, 72> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 45> -> <Unique State Name, 74>	Base relation: 
{when 0 <= x:62}	
<Unique State Name, 66> -> <Unique State Name, 63 65>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 63> -> <Unique State Name, 22>	Base relation: 
{x := 0
 n := param0:53}	
<Unique State Name, 75> -> <Unique State Name, 26>	Base relation: 
{}	
<Unique State Name, 70> -> <Unique State Name, 67 69>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 34> -> <Unique State Name, 22>	Base relation: 
{__cost := (__cost:66 + 1)
 x := (x:62 + 1)
 when (tmp:65 = 0 /\ 0 <= __cost:66 /\ 0 <= (__cost:66 + 1))}	
<Unique State Name, 34> -> <Unique State Name, 44>	Base relation: 
{when !(tmp:65 = 0)}	
<Unique State Name, 26> -> <Unique State Name, 34>	Base relation: 
{tmp := havoc:72
 when x:62 < n:63}	
<Unique State Name, 26> -> <Unique State Name, 44>	Base relation: 
{when n:63 <= x:62}	
#################################################################
           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:66 + 1)
 x := (x:62 + 1)
 tmp := havoc:187
 when (0 <= x:62 /\ x:62 < n:63 /\ havoc:187 = 0 /\ 0 <= __cost:66
         /\ 0 <= (__cost:66 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':188) = (1)*(__cost:66) + 1
           (tmp':190) = 0
           (x':189) = (1)*(x:62) + 1
           }
          pre:
            [|-x:62+n:63-1>=0; __cost:66>=0; x:62>=0|]
          post:
            [|tmp':190=0; x':189-1>=0; __cost':188-1>=0; n:63-x':189>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':188
   x := x':189
   tmp := tmp':190
   when ((!(0 <= K:202) \/ mid___cost:206 = (__cost:66 + K:202))
           /\ (!((0 <= K:202 /\ K:202 <= 0)) \/ mid_tmp:204 = tmp:65)
           /\ (!(1 <= K:202) \/ mid_tmp:204 = 0)
           /\ (!(0 <= K:202) \/ mid_x:205 = (x:62 + K:202))
           /\ ((K:202 = 0 /\ tmp:65 = mid_tmp:204 /\ x:62 = mid_x:205
                  /\ __cost:66 = mid___cost:206)
                 \/ (1 <= K:202 /\ 0 <= (-1 + -x:62 + n:63) /\ 0 <= __cost:66
                       /\ 0 <= x:62 /\ mid_tmp:204 = 0
                       /\ 0 <= (-1 + mid_x:205) /\ 0 <= (-1 + mid___cost:206)
                       /\ 0 <= (n:63 + -mid_x:205))) /\ K:203 = 0
           /\ mid_tmp:204 = tmp':190 /\ mid_x:205 = x':189
           /\ mid___cost:206 = __cost':188 /\ 0 = K:203
           /\ (K:202 + K:203) = K:201 /\ 0 <= K:201)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:66 + 1)
 x := (x:62 + 1)
 when (0 <= x:62 /\ x:62 < n:63 /\ 0 <= __cost:66 /\ 0 <= (__cost:66 + 1))}
**** alpha hat: 
  {<Split [true
            (x':189) = (1)*(x:62) + 1
           (__cost':188) = (1)*(__cost:66) + 1
           }
          pre:
            [|-x:62+n:63-1>=0; __cost:66>=0; x:62>=0|]
          post:
            [|x':189-1>=0; __cost':188-1>=0; n:63-x':189>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':188
   x := x':189
   when ((!(0 <= K:226) \/ mid_x:228 = (x:62 + K:226))
           /\ (!(0 <= K:226) \/ mid___cost:229 = (__cost:66 + K:226))
           /\ ((K:226 = 0 /\ x:62 = mid_x:228 /\ __cost:66 = mid___cost:229)
                 \/ (1 <= K:226 /\ 0 <= (-1 + -x:62 + n:63) /\ 0 <= __cost:66
                       /\ 0 <= x:62 /\ 0 <= (-1 + mid_x:228)
                       /\ 0 <= (-1 + mid___cost:229)
                       /\ 0 <= (n:63 + -mid_x:228))) /\ K:227 = 0
           /\ mid_x:228 = x':189 /\ mid___cost:229 = __cost':188 /\ 0 = K:227
           /\ (K:226 + K:227) = K:225 /\ 0 <= K:225)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  24  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       n := havoc:13
       param0 := havoc:13
       param0@pos := type_err:17
       param0@width := type_err:18}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:19
     return@width := type_err:20
     when ((0 < n:2 /\ n:2 = phi_tmp___0:14)
             \/ (n:2 <= 0 /\ 0 = phi_tmp___0:14))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:53
       param0@pos := type_err:54
       param0@width := type_err:55}    )
    ,
    Var(24)
  )
  ,
  Weight(Base relation: 
    {return := havoc:41
     return@pos := type_err:44
     return@width := type_err:45}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=24: 
Weight(Base relation: 
  {__cost := __cost':235
   x := x':234
   tmp := phi_tmp:217
   n := param0:53
   return := havoc:237
   return@pos := type_err:238
   return@width := type_err:239
   when ((((!(0 <= K:207) \/ mid___cost:208 = (__cost:66 + K:207))
             /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:65)
             /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
             /\ (!(0 <= K:207) \/ mid_x:210 = K:207)
             /\ ((K:207 = 0 /\ tmp:65 = mid_tmp:209 /\ 0 = mid_x:210
                    /\ __cost:66 = mid___cost:208)
                   \/ (1 <= K:207 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:66
                         /\ mid_tmp:209 = 0 /\ 0 <= (-1 + mid_x:210)
                         /\ 0 <= (-1 + mid___cost:208)
                         /\ 0 <= (param0:53 + -mid_x:210))) /\ K:211 = 0
             /\ mid_tmp:209 = tmp':212 /\ mid_x:210 = x':213
             /\ mid___cost:208 = __cost':214 /\ 0 = K:211
             /\ (K:207 + K:211) = K:215 /\ 0 <= K:215 /\ 0 <= x':213
             /\ param0:53 <= x':213 /\ tmp':212 = phi_tmp:217)
            \/ ((!(0 <= K:207) \/ mid___cost:208 = (__cost:66 + K:207))
                  /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:65)
                  /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
                  /\ (!(0 <= K:207) \/ mid_x:210 = K:207)
                  /\ ((K:207 = 0 /\ tmp:65 = mid_tmp:209 /\ 0 = mid_x:210
                         /\ __cost:66 = mid___cost:208)
                        \/ (1 <= K:207 /\ 0 <= (-1 + param0:53)
                              /\ 0 <= __cost:66 /\ mid_tmp:209 = 0
                              /\ 0 <= (-1 + mid_x:210)
                              /\ 0 <= (-1 + mid___cost:208)
                              /\ 0 <= (param0:53 + -mid_x:210))) /\ K:211 = 0
                  /\ mid_tmp:209 = tmp':212 /\ mid_x:210 = x':213
                  /\ mid___cost:208 = __cost':214 /\ 0 = K:211
                  /\ (K:207 + K:211) = K:215 /\ 0 <= K:215 /\ 0 <= x':213
                  /\ x':213 < param0:53 /\ !(havoc:216 = 0)
                  /\ havoc:216 = phi_tmp:217))
           /\ (!(0 <= K:230) \/ mid_x:231 = (x':213 + K:230))
           /\ (!(0 <= K:230) \/ mid___cost:232 = (__cost':214 + K:230))
           /\ ((K:230 = 0 /\ x':213 = mid_x:231
                  /\ __cost':214 = mid___cost:232)
                 \/ (1 <= K:230 /\ 0 <= (-1 + -x':213 + param0:53)
                       /\ 0 <= __cost':214 /\ 0 <= x':213
                       /\ 0 <= (-1 + mid_x:231) /\ 0 <= (-1 + mid___cost:232)
                       /\ 0 <= (param0:53 + -mid_x:231))) /\ K:233 = 0
           /\ mid_x:231 = x':234 /\ mid___cost:232 = __cost':235 /\ 0 = K:233
           /\ (K:230 + K:233) = K:236 /\ 0 <= K:236 /\ 0 <= x':234
           /\ param0:53 <= x':234)})



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
         n := havoc:13
         param0 := havoc:13
         param0@pos := type_err:17
         param0@width := type_err:18}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:19
       return@width := type_err:20
       when ((0 < n:2 /\ n:2 = phi_tmp___0:14)
               \/ (n:2 <= 0 /\ 0 = phi_tmp___0:14))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:53
         param0@pos := type_err:54
         param0@width := type_err:55}      )
      ,
      Var(24)
    )
    ,
    Weight(Base relation: 
      {return := havoc:41
       return@pos := type_err:44
       return@width := type_err:45}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':235
   return := havoc:237
   return@pos := type_err:238
   return@width := type_err:239
   when ((((!(0 <= K:207) \/ mid___cost:208 = (__cost:66 + K:207))
             /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:240)
             /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
             /\ (!(0 <= K:207) \/ mid_x:210 = K:207)
             /\ ((K:207 = 0 /\ tmp:240 = mid_tmp:209 /\ 0 = mid_x:210
                    /\ __cost:66 = mid___cost:208)
                   \/ (1 <= K:207 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:66
                         /\ mid_tmp:209 = 0 /\ 0 <= (-1 + mid_x:210)
                         /\ 0 <= (-1 + mid___cost:208)
                         /\ 0 <= (param0:53 + -mid_x:210))) /\ K:211 = 0
             /\ mid_tmp:209 = tmp':212 /\ mid_x:210 = x':213
             /\ mid___cost:208 = __cost':214 /\ 0 = K:211
             /\ (K:207 + K:211) = K:215 /\ 0 <= K:215 /\ 0 <= x':213
             /\ param0:53 <= x':213 /\ tmp':212 = phi_tmp:217)
            \/ ((!(0 <= K:207) \/ mid___cost:208 = (__cost:66 + K:207))
                  /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:240)
                  /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
                  /\ (!(0 <= K:207) \/ mid_x:210 = K:207)
                  /\ ((K:207 = 0 /\ tmp:240 = mid_tmp:209 /\ 0 = mid_x:210
                         /\ __cost:66 = mid___cost:208)
                        \/ (1 <= K:207 /\ 0 <= (-1 + param0:53)
                              /\ 0 <= __cost:66 /\ mid_tmp:209 = 0
                              /\ 0 <= (-1 + mid_x:210)
                              /\ 0 <= (-1 + mid___cost:208)
                              /\ 0 <= (param0:53 + -mid_x:210))) /\ K:211 = 0
                  /\ mid_tmp:209 = tmp':212 /\ mid_x:210 = x':213
                  /\ mid___cost:208 = __cost':214 /\ 0 = K:211
                  /\ (K:207 + K:211) = K:215 /\ 0 <= K:215 /\ 0 <= x':213
                  /\ x':213 < param0:53 /\ !(havoc:216 = 0)
                  /\ havoc:216 = phi_tmp:217))
           /\ (!(0 <= K:230) \/ mid_x:231 = (x':213 + K:230))
           /\ (!(0 <= K:230) \/ mid___cost:232 = (__cost':214 + K:230))
           /\ ((K:230 = 0 /\ x':213 = mid_x:231
                  /\ __cost':214 = mid___cost:232)
                 \/ (1 <= K:230 /\ 0 <= (-1 + -x':213 + param0:53)
                       /\ 0 <= __cost':214 /\ 0 <= x':213
                       /\ 0 <= (-1 + mid_x:231) /\ 0 <= (-1 + mid___cost:232)
                       /\ 0 <= (param0:53 + -mid_x:231))) /\ K:233 = 0
           /\ mid_x:231 = x':234 /\ mid___cost:232 = __cost':235 /\ 0 = K:233
           /\ (K:230 + K:233) = K:236 /\ 0 <= K:236 /\ 0 <= x':234
           /\ param0:53 <= x':234)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':283
   return := 0
   param0 := havoc:13
   return@pos := type_err:291
   param0@pos := type_err:287
   return@width := type_err:292
   param0@width := type_err:289
   when ((((!(0 <= K:266) \/ mid___cost:267 = K:266)
             /\ (!((0 <= K:266 /\ K:266 <= 0)) \/ mid_tmp:268 = tmp:269)
             /\ (!(1 <= K:266) \/ mid_tmp:268 = 0)
             /\ (!(0 <= K:266) \/ mid_x:270 = K:266)
             /\ ((K:266 = 0 /\ tmp:269 = mid_tmp:268 /\ 0 = mid_x:270
                    /\ 0 = mid___cost:267)
                   \/ (1 <= K:266 /\ 0 <= (-1 + havoc:13) /\ mid_tmp:268 = 0
                         /\ 0 <= (-1 + mid_x:270)
                         /\ 0 <= (-1 + mid___cost:267)
                         /\ 0 <= (havoc:13 + -mid_x:270))) /\ K:271 = 0
             /\ mid_tmp:268 = tmp':272 /\ mid_x:270 = x':273
             /\ mid___cost:267 = __cost':274 /\ 0 = K:271
             /\ (K:266 + K:271) = K:275 /\ 0 <= K:275 /\ 0 <= x':273
             /\ havoc:13 <= x':273 /\ tmp':272 = phi_tmp:276)
            \/ ((!(0 <= K:266) \/ mid___cost:267 = K:266)
                  /\ (!((0 <= K:266 /\ K:266 <= 0)) \/ mid_tmp:268 = tmp:269)
                  /\ (!(1 <= K:266) \/ mid_tmp:268 = 0)
                  /\ (!(0 <= K:266) \/ mid_x:270 = K:266)
                  /\ ((K:266 = 0 /\ tmp:269 = mid_tmp:268 /\ 0 = mid_x:270
                         /\ 0 = mid___cost:267)
                        \/ (1 <= K:266 /\ 0 <= (-1 + havoc:13)
                              /\ mid_tmp:268 = 0 /\ 0 <= (-1 + mid_x:270)
                              /\ 0 <= (-1 + mid___cost:267)
                              /\ 0 <= (havoc:13 + -mid_x:270))) /\ K:271 = 0
                  /\ mid_tmp:268 = tmp':272 /\ mid_x:270 = x':273
                  /\ mid___cost:267 = __cost':274 /\ 0 = K:271
                  /\ (K:266 + K:271) = K:275 /\ 0 <= K:275 /\ 0 <= x':273
                  /\ x':273 < havoc:13 /\ !(havoc:277 = 0)
                  /\ havoc:277 = phi_tmp:276))
           /\ (!(0 <= K:278) \/ mid_x:279 = (x':273 + K:278))
           /\ (!(0 <= K:278) \/ mid___cost:280 = (__cost':274 + K:278))
           /\ ((K:278 = 0 /\ x':273 = mid_x:279
                  /\ __cost':274 = mid___cost:280)
                 \/ (1 <= K:278 /\ 0 <= (-1 + -x':273 + havoc:13)
                       /\ 0 <= __cost':274 /\ 0 <= x':273
                       /\ 0 <= (-1 + mid_x:279) /\ 0 <= (-1 + mid___cost:280)
                       /\ 0 <= (havoc:13 + -mid_x:279))) /\ K:281 = 0
           /\ mid_x:279 = x':282 /\ mid___cost:280 = __cost':283 /\ 0 = K:281
           /\ (K:278 + K:281) = K:284 /\ 0 <= K:284 /\ 0 <= x':282
           /\ havoc:13 <= x':282
           /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:290)
                 \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:290)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':310
   return := havoc:315
   param0 := param0:53
   return@pos := type_err:316
   param0@pos := type_err:54
   return@width := type_err:317
   param0@width := type_err:55
   when ((((!(0 <= K:293) \/ mid___cost:294 = (__cost:66 + K:293))
             /\ (!((0 <= K:293 /\ K:293 <= 0)) \/ mid_tmp:295 = tmp:296)
             /\ (!(1 <= K:293) \/ mid_tmp:295 = 0)
             /\ (!(0 <= K:293) \/ mid_x:297 = K:293)
             /\ ((K:293 = 0 /\ tmp:296 = mid_tmp:295 /\ 0 = mid_x:297
                    /\ __cost:66 = mid___cost:294)
                   \/ (1 <= K:293 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:66
                         /\ mid_tmp:295 = 0 /\ 0 <= (-1 + mid_x:297)
                         /\ 0 <= (-1 + mid___cost:294)
                         /\ 0 <= (param0:53 + -mid_x:297))) /\ K:298 = 0
             /\ mid_tmp:295 = tmp':299 /\ mid_x:297 = x':300
             /\ mid___cost:294 = __cost':301 /\ 0 = K:298
             /\ (K:293 + K:298) = K:302 /\ 0 <= K:302 /\ 0 <= x':300
             /\ param0:53 <= x':300 /\ tmp':299 = phi_tmp:303)
            \/ ((!(0 <= K:293) \/ mid___cost:294 = (__cost:66 + K:293))
                  /\ (!((0 <= K:293 /\ K:293 <= 0)) \/ mid_tmp:295 = tmp:296)
                  /\ (!(1 <= K:293) \/ mid_tmp:295 = 0)
                  /\ (!(0 <= K:293) \/ mid_x:297 = K:293)
                  /\ ((K:293 = 0 /\ tmp:296 = mid_tmp:295 /\ 0 = mid_x:297
                         /\ __cost:66 = mid___cost:294)
                        \/ (1 <= K:293 /\ 0 <= (-1 + param0:53)
                              /\ 0 <= __cost:66 /\ mid_tmp:295 = 0
                              /\ 0 <= (-1 + mid_x:297)
                              /\ 0 <= (-1 + mid___cost:294)
                              /\ 0 <= (param0:53 + -mid_x:297))) /\ K:298 = 0
                  /\ mid_tmp:295 = tmp':299 /\ mid_x:297 = x':300
                  /\ mid___cost:294 = __cost':301 /\ 0 = K:298
                  /\ (K:293 + K:298) = K:302 /\ 0 <= K:302 /\ 0 <= x':300
                  /\ x':300 < param0:53 /\ !(havoc:304 = 0)
                  /\ havoc:304 = phi_tmp:303))
           /\ (!(0 <= K:305) \/ mid_x:306 = (x':300 + K:305))
           /\ (!(0 <= K:305) \/ mid___cost:307 = (__cost':301 + K:305))
           /\ ((K:305 = 0 /\ x':300 = mid_x:306
                  /\ __cost':301 = mid___cost:307)
                 \/ (1 <= K:305 /\ 0 <= (-1 + -x':300 + param0:53)
                       /\ 0 <= __cost':301 /\ 0 <= x':300
                       /\ 0 <= (-1 + mid_x:306) /\ 0 <= (-1 + mid___cost:307)
                       /\ 0 <= (param0:53 + -mid_x:306))) /\ K:308 = 0
           /\ mid_x:306 = x':309 /\ mid___cost:307 = __cost':310 /\ 0 = K:308
           /\ (K:305 + K:308) = K:311 /\ 0 <= K:311 /\ 0 <= x':309
           /\ param0:53 <= x':309)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=24: 
Weight(Base relation: 
  {__cost := __cost':235
   return := havoc:237
   return@pos := type_err:238
   return@width := type_err:239
   when ((((!(0 <= K:207) \/ mid___cost:208 = (__cost:66 + K:207))
             /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:240)
             /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
             /\ (!(0 <= K:207) \/ mid_x:210 = K:207)
             /\ ((K:207 = 0 /\ tmp:240 = mid_tmp:209 /\ 0 = mid_x:210
                    /\ __cost:66 = mid___cost:208)
                   \/ (1 <= K:207 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:66
                         /\ mid_tmp:209 = 0 /\ 0 <= (-1 + mid_x:210)
                         /\ 0 <= (-1 + mid___cost:208)
                         /\ 0 <= (param0:53 + -mid_x:210))) /\ K:211 = 0
             /\ mid_tmp:209 = tmp':212 /\ mid_x:210 = x':213
             /\ mid___cost:208 = __cost':214 /\ 0 = K:211
             /\ (K:207 + K:211) = K:215 /\ 0 <= K:215 /\ 0 <= x':213
             /\ param0:53 <= x':213 /\ tmp':212 = phi_tmp:217)
            \/ ((!(0 <= K:207) \/ mid___cost:208 = (__cost:66 + K:207))
                  /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:240)
                  /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
                  /\ (!(0 <= K:207) \/ mid_x:210 = K:207)
                  /\ ((K:207 = 0 /\ tmp:240 = mid_tmp:209 /\ 0 = mid_x:210
                         /\ __cost:66 = mid___cost:208)
                        \/ (1 <= K:207 /\ 0 <= (-1 + param0:53)
                              /\ 0 <= __cost:66 /\ mid_tmp:209 = 0
                              /\ 0 <= (-1 + mid_x:210)
                              /\ 0 <= (-1 + mid___cost:208)
                              /\ 0 <= (param0:53 + -mid_x:210))) /\ K:211 = 0
                  /\ mid_tmp:209 = tmp':212 /\ mid_x:210 = x':213
                  /\ mid___cost:208 = __cost':214 /\ 0 = K:211
                  /\ (K:207 + K:211) = K:215 /\ 0 <= K:215 /\ 0 <= x':213
                  /\ x':213 < param0:53 /\ !(havoc:216 = 0)
                  /\ havoc:216 = phi_tmp:217))
           /\ (!(0 <= K:230) \/ mid_x:231 = (x':213 + K:230))
           /\ (!(0 <= K:230) \/ mid___cost:232 = (__cost':214 + K:230))
           /\ ((K:230 = 0 /\ x':213 = mid_x:231
                  /\ __cost':214 = mid___cost:232)
                 \/ (1 <= K:230 /\ 0 <= (-1 + -x':213 + param0:53)
                       /\ 0 <= __cost':214 /\ 0 <= x':213
                       /\ 0 <= (-1 + mid_x:231) /\ 0 <= (-1 + mid___cost:232)
                       /\ 0 <= (param0:53 + -mid_x:231))) /\ K:233 = 0
           /\ mid_x:231 = x':234 /\ mid___cost:232 = __cost':235 /\ 0 = K:233
           /\ (K:230 + K:233) = K:236 /\ 0 <= K:236 /\ 0 <= x':234
           /\ param0:53 <= x':234)})


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':283
 return := 0
 param0 := havoc:13
 return@pos := type_err:291
 param0@pos := type_err:287
 return@width := type_err:292
 param0@width := type_err:289
 when ((((!(0 <= K:266) \/ mid___cost:267 = K:266)
           /\ (!((0 <= K:266 /\ K:266 <= 0)) \/ mid_tmp:268 = tmp:269)
           /\ (!(1 <= K:266) \/ mid_tmp:268 = 0)
           /\ (!(0 <= K:266) \/ mid_x:270 = K:266)
           /\ ((K:266 = 0 /\ tmp:269 = mid_tmp:268 /\ 0 = mid_x:270
                  /\ 0 = mid___cost:267)
                 \/ (1 <= K:266 /\ 0 <= (-1 + havoc:13) /\ mid_tmp:268 = 0
                       /\ 0 <= (-1 + mid_x:270) /\ 0 <= (-1 + mid___cost:267)
                       /\ 0 <= (havoc:13 + -mid_x:270))) /\ K:271 = 0
           /\ mid_tmp:268 = tmp':272 /\ mid_x:270 = x':273
           /\ mid___cost:267 = __cost':274 /\ 0 = K:271
           /\ (K:266 + K:271) = K:275 /\ 0 <= K:275 /\ 0 <= x':273
           /\ havoc:13 <= x':273 /\ tmp':272 = phi_tmp:276)
          \/ ((!(0 <= K:266) \/ mid___cost:267 = K:266)
                /\ (!((0 <= K:266 /\ K:266 <= 0)) \/ mid_tmp:268 = tmp:269)
                /\ (!(1 <= K:266) \/ mid_tmp:268 = 0)
                /\ (!(0 <= K:266) \/ mid_x:270 = K:266)
                /\ ((K:266 = 0 /\ tmp:269 = mid_tmp:268 /\ 0 = mid_x:270
                       /\ 0 = mid___cost:267)
                      \/ (1 <= K:266 /\ 0 <= (-1 + havoc:13)
                            /\ mid_tmp:268 = 0 /\ 0 <= (-1 + mid_x:270)
                            /\ 0 <= (-1 + mid___cost:267)
                            /\ 0 <= (havoc:13 + -mid_x:270))) /\ K:271 = 0
                /\ mid_tmp:268 = tmp':272 /\ mid_x:270 = x':273
                /\ mid___cost:267 = __cost':274 /\ 0 = K:271
                /\ (K:266 + K:271) = K:275 /\ 0 <= K:275 /\ 0 <= x':273
                /\ x':273 < havoc:13 /\ !(havoc:277 = 0)
                /\ havoc:277 = phi_tmp:276))
         /\ (!(0 <= K:278) \/ mid_x:279 = (x':273 + K:278))
         /\ (!(0 <= K:278) \/ mid___cost:280 = (__cost':274 + K:278))
         /\ ((K:278 = 0 /\ x':273 = mid_x:279 /\ __cost':274 = mid___cost:280)
               \/ (1 <= K:278 /\ 0 <= (-1 + -x':273 + havoc:13)
                     /\ 0 <= __cost':274 /\ 0 <= x':273
                     /\ 0 <= (-1 + mid_x:279) /\ 0 <= (-1 + mid___cost:280)
                     /\ 0 <= (havoc:13 + -mid_x:279))) /\ K:281 = 0
         /\ mid_x:279 = x':282 /\ mid___cost:280 = __cost':283 /\ 0 = K:281
         /\ (K:278 + K:281) = K:284 /\ 0 <= K:284 /\ 0 <= x':282
         /\ havoc:13 <= x':282
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:290)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:290)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':310
 return := havoc:315
 param0 := param0:53
 return@pos := type_err:316
 param0@pos := type_err:54
 return@width := type_err:317
 param0@width := type_err:55
 when ((((!(0 <= K:293) \/ mid___cost:294 = (__cost:66 + K:293))
           /\ (!((0 <= K:293 /\ K:293 <= 0)) \/ mid_tmp:295 = tmp:296)
           /\ (!(1 <= K:293) \/ mid_tmp:295 = 0)
           /\ (!(0 <= K:293) \/ mid_x:297 = K:293)
           /\ ((K:293 = 0 /\ tmp:296 = mid_tmp:295 /\ 0 = mid_x:297
                  /\ __cost:66 = mid___cost:294)
                 \/ (1 <= K:293 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:66
                       /\ mid_tmp:295 = 0 /\ 0 <= (-1 + mid_x:297)
                       /\ 0 <= (-1 + mid___cost:294)
                       /\ 0 <= (param0:53 + -mid_x:297))) /\ K:298 = 0
           /\ mid_tmp:295 = tmp':299 /\ mid_x:297 = x':300
           /\ mid___cost:294 = __cost':301 /\ 0 = K:298
           /\ (K:293 + K:298) = K:302 /\ 0 <= K:302 /\ 0 <= x':300
           /\ param0:53 <= x':300 /\ tmp':299 = phi_tmp:303)
          \/ ((!(0 <= K:293) \/ mid___cost:294 = (__cost:66 + K:293))
                /\ (!((0 <= K:293 /\ K:293 <= 0)) \/ mid_tmp:295 = tmp:296)
                /\ (!(1 <= K:293) \/ mid_tmp:295 = 0)
                /\ (!(0 <= K:293) \/ mid_x:297 = K:293)
                /\ ((K:293 = 0 /\ tmp:296 = mid_tmp:295 /\ 0 = mid_x:297
                       /\ __cost:66 = mid___cost:294)
                      \/ (1 <= K:293 /\ 0 <= (-1 + param0:53)
                            /\ 0 <= __cost:66 /\ mid_tmp:295 = 0
                            /\ 0 <= (-1 + mid_x:297)
                            /\ 0 <= (-1 + mid___cost:294)
                            /\ 0 <= (param0:53 + -mid_x:297))) /\ K:298 = 0
                /\ mid_tmp:295 = tmp':299 /\ mid_x:297 = x':300
                /\ mid___cost:294 = __cost':301 /\ 0 = K:298
                /\ (K:293 + K:298) = K:302 /\ 0 <= K:302 /\ 0 <= x':300
                /\ x':300 < param0:53 /\ !(havoc:304 = 0)
                /\ havoc:304 = phi_tmp:303))
         /\ (!(0 <= K:305) \/ mid_x:306 = (x':300 + K:305))
         /\ (!(0 <= K:305) \/ mid___cost:307 = (__cost':301 + K:305))
         /\ ((K:305 = 0 /\ x':300 = mid_x:306 /\ __cost':301 = mid___cost:307)
               \/ (1 <= K:305 /\ 0 <= (-1 + -x':300 + param0:53)
                     /\ 0 <= __cost':301 /\ 0 <= x':300
                     /\ 0 <= (-1 + mid_x:306) /\ 0 <= (-1 + mid___cost:307)
                     /\ 0 <= (param0:53 + -mid_x:306))) /\ K:308 = 0
         /\ mid_x:306 = x':309 /\ mid___cost:307 = __cost':310 /\ 0 = K:308
         /\ (K:305 + K:308) = K:311 /\ 0 <= K:311 /\ 0 <= x':309
         /\ param0:53 <= x':309)}

Evaluating variable number 24 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':235
 return := havoc:237
 return@pos := type_err:238
 return@width := type_err:239
 when ((((!(0 <= K:207) \/ mid___cost:208 = (__cost:66 + K:207))
           /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:240)
           /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
           /\ (!(0 <= K:207) \/ mid_x:210 = K:207)
           /\ ((K:207 = 0 /\ tmp:240 = mid_tmp:209 /\ 0 = mid_x:210
                  /\ __cost:66 = mid___cost:208)
                 \/ (1 <= K:207 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:66
                       /\ mid_tmp:209 = 0 /\ 0 <= (-1 + mid_x:210)
                       /\ 0 <= (-1 + mid___cost:208)
                       /\ 0 <= (param0:53 + -mid_x:210))) /\ K:211 = 0
           /\ mid_tmp:209 = tmp':212 /\ mid_x:210 = x':213
           /\ mid___cost:208 = __cost':214 /\ 0 = K:211
           /\ (K:207 + K:211) = K:215 /\ 0 <= K:215 /\ 0 <= x':213
           /\ param0:53 <= x':213 /\ tmp':212 = phi_tmp:217)
          \/ ((!(0 <= K:207) \/ mid___cost:208 = (__cost:66 + K:207))
                /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:240)
                /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
                /\ (!(0 <= K:207) \/ mid_x:210 = K:207)
                /\ ((K:207 = 0 /\ tmp:240 = mid_tmp:209 /\ 0 = mid_x:210
                       /\ __cost:66 = mid___cost:208)
                      \/ (1 <= K:207 /\ 0 <= (-1 + param0:53)
                            /\ 0 <= __cost:66 /\ mid_tmp:209 = 0
                            /\ 0 <= (-1 + mid_x:210)
                            /\ 0 <= (-1 + mid___cost:208)
                            /\ 0 <= (param0:53 + -mid_x:210))) /\ K:211 = 0
                /\ mid_tmp:209 = tmp':212 /\ mid_x:210 = x':213
                /\ mid___cost:208 = __cost':214 /\ 0 = K:211
                /\ (K:207 + K:211) = K:215 /\ 0 <= K:215 /\ 0 <= x':213
                /\ x':213 < param0:53 /\ !(havoc:216 = 0)
                /\ havoc:216 = phi_tmp:217))
         /\ (!(0 <= K:230) \/ mid_x:231 = (x':213 + K:230))
         /\ (!(0 <= K:230) \/ mid___cost:232 = (__cost':214 + K:230))
         /\ ((K:230 = 0 /\ x':213 = mid_x:231 /\ __cost':214 = mid___cost:232)
               \/ (1 <= K:230 /\ 0 <= (-1 + -x':213 + param0:53)
                     /\ 0 <= __cost':214 /\ 0 <= x':213
                     /\ 0 <= (-1 + mid_x:231) /\ 0 <= (-1 + mid___cost:232)
                     /\ 0 <= (param0:53 + -mid_x:231))) /\ K:233 = 0
         /\ mid_x:231 = x':234 /\ mid___cost:232 = __cost':235 /\ 0 = K:233
         /\ (K:230 + K:233) = K:236 /\ 0 <= K:236 /\ 0 <= x':234
         /\ param0:53 <= x':234)}

    (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,67)_g1>	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
<__pstate, (Unique State Name,67)_g1> -> <__pstate, (Unique State Name,63)_g1>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x8b88a30: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x8b71fb0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
##### ANS
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}
    ( __pstate , (Unique State Name,67)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}
    ( __pstate , (Unique State Name,63)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:370
 param0@width := type_err:371}

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

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

Base relation: 
{__cost := __cost':335
 n := havoc:13
 return := 0
 param0 := havoc:13
 return@pos := type_err:343
 param0@pos := type_err:339
 return@width := type_err:344
 param0@width := type_err:341
 when ((((!(0 <= K:318) \/ mid___cost:319 = K:318)
           /\ (!((0 <= K:318 /\ K:318 <= 0)) \/ mid_tmp:320 = tmp:321)
           /\ (!(1 <= K:318) \/ mid_tmp:320 = 0)
           /\ (!(0 <= K:318) \/ mid_x:322 = K:318)
           /\ ((K:318 = 0 /\ tmp:321 = mid_tmp:320 /\ 0 = mid_x:322
                  /\ 0 = mid___cost:319)
                 \/ (1 <= K:318 /\ 0 <= (-1 + havoc:13) /\ mid_tmp:320 = 0
                       /\ 0 <= (-1 + mid_x:322) /\ 0 <= (-1 + mid___cost:319)
                       /\ 0 <= (havoc:13 + -mid_x:322))) /\ K:323 = 0
           /\ mid_tmp:320 = tmp':324 /\ mid_x:322 = x':325
           /\ mid___cost:319 = __cost':326 /\ 0 = K:323
           /\ (K:318 + K:323) = K:327 /\ 0 <= K:327 /\ 0 <= x':325
           /\ havoc:13 <= x':325 /\ tmp':324 = phi_tmp:328)
          \/ ((!(0 <= K:318) \/ mid___cost:319 = K:318)
                /\ (!((0 <= K:318 /\ K:318 <= 0)) \/ mid_tmp:320 = tmp:321)
                /\ (!(1 <= K:318) \/ mid_tmp:320 = 0)
                /\ (!(0 <= K:318) \/ mid_x:322 = K:318)
                /\ ((K:318 = 0 /\ tmp:321 = mid_tmp:320 /\ 0 = mid_x:322
                       /\ 0 = mid___cost:319)
                      \/ (1 <= K:318 /\ 0 <= (-1 + havoc:13)
                            /\ mid_tmp:320 = 0 /\ 0 <= (-1 + mid_x:322)
                            /\ 0 <= (-1 + mid___cost:319)
                            /\ 0 <= (havoc:13 + -mid_x:322))) /\ K:323 = 0
                /\ mid_tmp:320 = tmp':324 /\ mid_x:322 = x':325
                /\ mid___cost:319 = __cost':326 /\ 0 = K:323
                /\ (K:318 + K:323) = K:327 /\ 0 <= K:327 /\ 0 <= x':325
                /\ x':325 < havoc:13 /\ !(havoc:329 = 0)
                /\ havoc:329 = phi_tmp:328))
         /\ (!(0 <= K:330) \/ mid_x:331 = (x':325 + K:330))
         /\ (!(0 <= K:330) \/ mid___cost:332 = (__cost':326 + K:330))
         /\ ((K:330 = 0 /\ x':325 = mid_x:331 /\ __cost':326 = mid___cost:332)
               \/ (1 <= K:330 /\ 0 <= (-1 + -x':325 + havoc:13)
                     /\ 0 <= __cost':326 /\ 0 <= x':325
                     /\ 0 <= (-1 + mid_x:331) /\ 0 <= (-1 + mid___cost:332)
                     /\ 0 <= (havoc:13 + -mid_x:331))) /\ K:333 = 0
         /\ mid_x:331 = x':334 /\ mid___cost:332 = __cost':335 /\ 0 = K:333
         /\ (K:330 + K:333) = K:336 /\ 0 <= K:336 /\ 0 <= x':334
         /\ havoc:13 <= x':334
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:342)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:342)))}

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

Base relation: 
{__cost := __cost':362
 return := havoc:367
 param0 := param0:53
 return@pos := type_err:368
 param0@pos := type_err:54
 return@width := type_err:369
 param0@width := type_err:55
 when ((((!(0 <= K:345) \/ mid___cost:346 = (__cost:66 + K:345))
           /\ (!((0 <= K:345 /\ K:345 <= 0)) \/ mid_tmp:347 = tmp:348)
           /\ (!(1 <= K:345) \/ mid_tmp:347 = 0)
           /\ (!(0 <= K:345) \/ mid_x:349 = K:345)
           /\ ((K:345 = 0 /\ tmp:348 = mid_tmp:347 /\ 0 = mid_x:349
                  /\ __cost:66 = mid___cost:346)
                 \/ (1 <= K:345 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:66
                       /\ mid_tmp:347 = 0 /\ 0 <= (-1 + mid_x:349)
                       /\ 0 <= (-1 + mid___cost:346)
                       /\ 0 <= (param0:53 + -mid_x:349))) /\ K:350 = 0
           /\ mid_tmp:347 = tmp':351 /\ mid_x:349 = x':352
           /\ mid___cost:346 = __cost':353 /\ 0 = K:350
           /\ (K:345 + K:350) = K:354 /\ 0 <= K:354 /\ 0 <= x':352
           /\ param0:53 <= x':352 /\ tmp':351 = phi_tmp:355)
          \/ ((!(0 <= K:345) \/ mid___cost:346 = (__cost:66 + K:345))
                /\ (!((0 <= K:345 /\ K:345 <= 0)) \/ mid_tmp:347 = tmp:348)
                /\ (!(1 <= K:345) \/ mid_tmp:347 = 0)
                /\ (!(0 <= K:345) \/ mid_x:349 = K:345)
                /\ ((K:345 = 0 /\ tmp:348 = mid_tmp:347 /\ 0 = mid_x:349
                       /\ __cost:66 = mid___cost:346)
                      \/ (1 <= K:345 /\ 0 <= (-1 + param0:53)
                            /\ 0 <= __cost:66 /\ mid_tmp:347 = 0
                            /\ 0 <= (-1 + mid_x:349)
                            /\ 0 <= (-1 + mid___cost:346)
                            /\ 0 <= (param0:53 + -mid_x:349))) /\ K:350 = 0
                /\ mid_tmp:347 = tmp':351 /\ mid_x:349 = x':352
                /\ mid___cost:346 = __cost':353 /\ 0 = K:350
                /\ (K:345 + K:350) = K:354 /\ 0 <= K:354 /\ 0 <= x':352
                /\ x':352 < param0:53 /\ !(havoc:356 = 0)
                /\ havoc:356 = phi_tmp:355))
         /\ (!(0 <= K:357) \/ mid_x:358 = (x':352 + K:357))
         /\ (!(0 <= K:357) \/ mid___cost:359 = (__cost':353 + K:357))
         /\ ((K:357 = 0 /\ x':352 = mid_x:358 /\ __cost':353 = mid___cost:359)
               \/ (1 <= K:357 /\ 0 <= (-1 + -x':352 + param0:53)
                     /\ 0 <= __cost':353 /\ 0 <= x':352
                     /\ 0 <= (-1 + mid_x:358) /\ 0 <= (-1 + mid___cost:359)
                     /\ 0 <= (param0:53 + -mid_x:358))) /\ K:360 = 0
         /\ mid_x:358 = x':361 /\ mid___cost:359 = __cost':362 /\ 0 = K:360
         /\ (K:357 + K:360) = K:363 /\ 0 <= K:363 /\ 0 <= x':361
         /\ param0:53 <= x':361)}

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

Base relation: 
{__cost := __cost':235
 x := x':234
 tmp := phi_tmp:217
 n := param0:53
 return := havoc:237
 return@pos := type_err:238
 return@width := type_err:239
 when ((((!(0 <= K:207) \/ mid___cost:208 = (__cost:66 + K:207))
           /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:65)
           /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
           /\ (!(0 <= K:207) \/ mid_x:210 = K:207)
           /\ ((K:207 = 0 /\ tmp:65 = mid_tmp:209 /\ 0 = mid_x:210
                  /\ __cost:66 = mid___cost:208)
                 \/ (1 <= K:207 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:66
                       /\ mid_tmp:209 = 0 /\ 0 <= (-1 + mid_x:210)
                       /\ 0 <= (-1 + mid___cost:208)
                       /\ 0 <= (param0:53 + -mid_x:210))) /\ K:211 = 0
           /\ mid_tmp:209 = tmp':212 /\ mid_x:210 = x':213
           /\ mid___cost:208 = __cost':214 /\ 0 = K:211
           /\ (K:207 + K:211) = K:215 /\ 0 <= K:215 /\ 0 <= x':213
           /\ param0:53 <= x':213 /\ tmp':212 = phi_tmp:217)
          \/ ((!(0 <= K:207) \/ mid___cost:208 = (__cost:66 + K:207))
                /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:65)
                /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
                /\ (!(0 <= K:207) \/ mid_x:210 = K:207)
                /\ ((K:207 = 0 /\ tmp:65 = mid_tmp:209 /\ 0 = mid_x:210
                       /\ __cost:66 = mid___cost:208)
                      \/ (1 <= K:207 /\ 0 <= (-1 + param0:53)
                            /\ 0 <= __cost:66 /\ mid_tmp:209 = 0
                            /\ 0 <= (-1 + mid_x:210)
                            /\ 0 <= (-1 + mid___cost:208)
                            /\ 0 <= (param0:53 + -mid_x:210))) /\ K:211 = 0
                /\ mid_tmp:209 = tmp':212 /\ mid_x:210 = x':213
                /\ mid___cost:208 = __cost':214 /\ 0 = K:211
                /\ (K:207 + K:211) = K:215 /\ 0 <= K:215 /\ 0 <= x':213
                /\ x':213 < param0:53 /\ !(havoc:216 = 0)
                /\ havoc:216 = phi_tmp:217))
         /\ (!(0 <= K:230) \/ mid_x:231 = (x':213 + K:230))
         /\ (!(0 <= K:230) \/ mid___cost:232 = (__cost':214 + K:230))
         /\ ((K:230 = 0 /\ x':213 = mid_x:231 /\ __cost':214 = mid___cost:232)
               \/ (1 <= K:230 /\ 0 <= (-1 + -x':213 + param0:53)
                     /\ 0 <= __cost':214 /\ 0 <= x':213
                     /\ 0 <= (-1 + mid_x:231) /\ 0 <= (-1 + mid___cost:232)
                     /\ 0 <= (param0:53 + -mid_x:231))) /\ K:233 = 0
         /\ mid_x:231 = x':234 /\ mid___cost:232 = __cost':235 /\ 0 = K:233
         /\ (K:230 + K:233) = K:236 /\ 0 <= K:236 /\ 0 <= x':234
         /\ param0:53 <= x':234)}

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

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

Variable bounds at line 23 in run

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

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