/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, 55> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 23> -> <Unique State Name, 57>	Base relation: 
{when (0 <= y:62 /\ 0 <= x:63)}	
<Unique State Name, 49> -> <Unique State Name, 46 48>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 56> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 54> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 27> -> <Unique State Name, 34>	Base relation: 
{y := (y:62 + -1)
 when 0 < y:62}	
<Unique State Name, 27> -> <Unique State Name, 54>	Base relation: 
{return := havoc:71
 return@pos := type_err:72
 return@width := type_err:73
 when y:62 <= 0}	
<Unique State Name, 57> -> <Unique State Name, 33>	Base relation: 
{}	
<Unique State Name, 52> -> <Unique State Name, 56>	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, 53> -> <Unique State Name, 50 52>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 46> -> <Unique State Name, 23>	Base relation: 
{x := 0
 y := 0
 n := param0:53}	
<Unique State Name, 48> -> <Unique State Name, 17>	Base relation: 
{}	
<Unique State Name, 33> -> <Unique State Name, 27>	Base relation: 
{when n:64 <= x:63}	
<Unique State Name, 33> -> <Unique State Name, 34>	Base relation: 
{x := (x:63 + 1)
 y := (y:62 + 1)
 when x:63 < n:64}	
<Unique State Name, 50> -> <Unique State Name, 49>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
<Unique State Name, 17> -> <Unique State Name, 55>	Base relation: 
{return := havoc:41
 return@pos := type_err:44
 return@width := type_err:45}	
<Unique State Name, 15> -> <Unique State Name, 53>	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
<Unique State Name, 34> -> <Unique State Name, 23>	Base relation: 
{__cost := (__cost:65 + 1)
 when (0 <= __cost:65 /\ 0 <= (__cost:65 + 1))}	
#################################################################
           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:65 + 1)
 x := phi_x:199
 y := phi_y:200
 when (0 <= y:62 /\ 0 <= x:63
         /\ ((x:63 < n:64 /\ (x:63 + 1) = phi_x:199 /\ (y:62 + 1) = phi_y:200)
               \/ (n:64 <= x:63 /\ 0 < y:62 /\ x:63 = phi_x:199
                     /\ (y:62 + -1) = phi_y:200)) /\ 0 <= __cost:65
         /\ 0 <= (__cost:65 + 1))}
**** alpha hat: 
  {<Split [(x:63 + -n:64) < 0
            (y':203) = (1)*(y:62) + 1
           (x':202) = (1)*(x:63) + 1
           (__cost':201) = (1)*(__cost:65) + 1
           }
          pre:
            [|-x:63+n:64-1>=0; y:62>=0; __cost:65>=0; x:63>=0|]
          post:
            [|y':203-1>=0; x':202-1>=0; __cost':201-1>=0; n:64-x':202>=0|]
           (y':203) = (1)*(y:62) + (-1)*1
          (__cost':201) = (1)*(__cost:65) + 1
          (x':202) = (1)*(x:63) + 0
          }
  pre:
    [|x:63-n:64>=0; x:63>=0; __cost:65>=0; y:62-1>=0|]
  post:
    [|-n:64+x':202>=0; y':203>=0; __cost':201-1>=0; x':202>=0|]],
[!((-x:63 + n:64) <= 0)
  (y':203) = (1)*(y:62) + 1
 (x':202) = (1)*(x:63) + 1
 (__cost':201) = (1)*(__cost:65) + 1
 } pre:   [|-x:63+n:64-1>=0; y:62>=0; __cost:65>=0; x:63>=0|] post:
  [|y':203-1>=0; x':202-1>=0; __cost':201-1>=0; n:64-x':202>=0|]
 (y':203) = (1)*(y:62) + (-1)*1 (__cost':201) = (1)*(__cost:65) + 1
(x':202) = (1)*(x:63) + 0 } pre:
  [|x:63-n:64>=0; x:63>=0; __cost:65>=0; y:62-1>=0|] post:
  [|-n:64+x':202>=0; y':203>=0; __cost':201-1>=0; x':202>=0|]]>}
**** star transition: 
  {__cost := __cost':201
   x := x':202
   y := y':203
   when ((!(0 <= K:233) \/ mid_y:235 = (y:62 + K:233))
           /\ (!(0 <= K:233) \/ mid_x:236 = (x:63 + K:233))
           /\ (!(0 <= K:233) \/ mid___cost:237 = (__cost:65 + K:233))
           /\ ((K:233 = 0 /\ y:62 = mid_y:235 /\ x:63 = mid_x:236
                  /\ __cost:65 = mid___cost:237)
                 \/ (1 <= K:233 /\ 0 <= (-1 + -x:63 + n:64) /\ 0 <= y:62
                       /\ 0 <= __cost:65 /\ 0 <= x:63
                       /\ 0 <= (-1 + mid_y:235) /\ 0 <= (-1 + mid_x:236)
                       /\ 0 <= (-1 + mid___cost:237)
                       /\ 0 <= (n:64 + -mid_x:236)))
           /\ (0 = K:233 \/ (x:63 + -n:64) < 0)
           /\ (!(0 <= K:234) \/ y':203 = (mid_y:235 + -K:234))
           /\ (!(0 <= K:234) \/ __cost':201 = (mid___cost:237 + K:234))
           /\ (!(0 <= K:234) \/ x':202 = mid_x:236)
           /\ ((K:234 = 0 /\ mid_y:235 = y':203 /\ mid_x:236 = x':202
                  /\ mid___cost:237 = __cost':201)
                 \/ (1 <= K:234 /\ 0 <= (mid_x:236 + -n:64) /\ 0 <= mid_x:236
                       /\ 0 <= mid___cost:237 /\ 0 <= (-1 + mid_y:235)
                       /\ 0 <= (-n:64 + x':202) /\ 0 <= y':203
                       /\ 0 <= (-1 + __cost':201) /\ 0 <= x':202))
           /\ (0 = K:234 \/ !((mid_x:236 + -n:64) < 0))
           /\ (K:233 + K:234) = K:232
           /\ (!(0 <= K:238) \/ mid_y:240 = (y:62 + K:238))
           /\ (!(0 <= K:238) \/ mid_x:241 = (x:63 + K:238))
           /\ (!(0 <= K:238) \/ mid___cost:242 = (__cost:65 + K:238))
           /\ ((K:238 = 0 /\ y:62 = mid_y:240 /\ x:63 = mid_x:241
                  /\ __cost:65 = mid___cost:242)
                 \/ (1 <= K:238 /\ 0 <= (-1 + -x:63 + n:64) /\ 0 <= y:62
                       /\ 0 <= __cost:65 /\ 0 <= x:63
                       /\ 0 <= (-1 + mid_y:240) /\ 0 <= (-1 + mid_x:241)
                       /\ 0 <= (-1 + mid___cost:242)
                       /\ 0 <= (n:64 + -mid_x:241)))
           /\ (0 = K:238 \/ !((-x:63 + n:64) <= 0))
           /\ (!(0 <= K:239) \/ y':203 = (mid_y:240 + -K:239))
           /\ (!(0 <= K:239) \/ __cost':201 = (mid___cost:242 + K:239))
           /\ (!(0 <= K:239) \/ x':202 = mid_x:241)
           /\ ((K:239 = 0 /\ mid_y:240 = y':203 /\ mid_x:241 = x':202
                  /\ mid___cost:242 = __cost':201)
                 \/ (1 <= K:239 /\ 0 <= (mid_x:241 + -n:64) /\ 0 <= mid_x:241
                       /\ 0 <= mid___cost:242 /\ 0 <= (-1 + mid_y:240)
                       /\ 0 <= (-n:64 + x':202) /\ 0 <= y':203
                       /\ 0 <= (-1 + __cost':201) /\ 0 <= x':202))
           /\ (0 = K:239 \/ (-mid_x:241 + n:64) <= 0)
           /\ (K:238 + K:239) = K:232 /\ 0 <= K:232)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  21  


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(21)
  )
  ,
  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=21: 
Weight(Base relation: 
  {__cost := __cost':249
   x := x':250
   y := y':248
   n := param0:53
   return := havoc:257
   return@pos := type_err:258
   return@width := type_err:259
   when ((!(0 <= K:243) \/ mid_y:244 = K:243)
           /\ (!(0 <= K:243) \/ mid_x:245 = K:243)
           /\ (!(0 <= K:243) \/ mid___cost:246 = (__cost:65 + K:243))
           /\ ((K:243 = 0 /\ 0 = mid_y:244 /\ 0 = mid_x:245
                  /\ __cost:65 = mid___cost:246)
                 \/ (1 <= K:243 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                       /\ 0 <= (-1 + mid_y:244) /\ 0 <= (-1 + mid_x:245)
                       /\ 0 <= (-1 + mid___cost:246)
                       /\ 0 <= (param0:53 + -mid_x:245)))
           /\ (0 = K:243 \/ -param0:53 < 0)
           /\ (!(0 <= K:247) \/ y':248 = (mid_y:244 + -K:247))
           /\ (!(0 <= K:247) \/ __cost':249 = (mid___cost:246 + K:247))
           /\ (!(0 <= K:247) \/ x':250 = mid_x:245)
           /\ ((K:247 = 0 /\ mid_y:244 = y':248 /\ mid_x:245 = x':250
                  /\ mid___cost:246 = __cost':249)
                 \/ (1 <= K:247 /\ 0 <= (mid_x:245 + -param0:53)
                       /\ 0 <= mid_x:245 /\ 0 <= mid___cost:246
                       /\ 0 <= (-1 + mid_y:244) /\ 0 <= (-param0:53 + x':250)
                       /\ 0 <= y':248 /\ 0 <= (-1 + __cost':249)
                       /\ 0 <= x':250))
           /\ (0 = K:247 \/ !((mid_x:245 + -param0:53) < 0))
           /\ (K:243 + K:247) = K:251 /\ (!(0 <= K:252) \/ mid_y:253 = K:252)
           /\ (!(0 <= K:252) \/ mid_x:254 = K:252)
           /\ (!(0 <= K:252) \/ mid___cost:255 = (__cost:65 + K:252))
           /\ ((K:252 = 0 /\ 0 = mid_y:253 /\ 0 = mid_x:254
                  /\ __cost:65 = mid___cost:255)
                 \/ (1 <= K:252 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                       /\ 0 <= (-1 + mid_y:253) /\ 0 <= (-1 + mid_x:254)
                       /\ 0 <= (-1 + mid___cost:255)
                       /\ 0 <= (param0:53 + -mid_x:254)))
           /\ (0 = K:252 \/ !(param0:53 <= 0))
           /\ (!(0 <= K:256) \/ y':248 = (mid_y:253 + -K:256))
           /\ (!(0 <= K:256) \/ __cost':249 = (mid___cost:255 + K:256))
           /\ (!(0 <= K:256) \/ x':250 = mid_x:254)
           /\ ((K:256 = 0 /\ mid_y:253 = y':248 /\ mid_x:254 = x':250
                  /\ mid___cost:255 = __cost':249)
                 \/ (1 <= K:256 /\ 0 <= (mid_x:254 + -param0:53)
                       /\ 0 <= mid_x:254 /\ 0 <= mid___cost:255
                       /\ 0 <= (-1 + mid_y:253) /\ 0 <= (-param0:53 + x':250)
                       /\ 0 <= y':248 /\ 0 <= (-1 + __cost':249)
                       /\ 0 <= x':250))
           /\ (0 = K:256 \/ (-mid_x:254 + param0:53) <= 0)
           /\ (K:252 + K:256) = K:251 /\ 0 <= K:251 /\ 0 <= y':248
           /\ 0 <= x':250 /\ param0:53 <= x':250 /\ y':248 <= 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
         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(21)
    )
    ,
    Weight(Base relation: 
      {return := havoc:41
       return@pos := type_err:44
       return@width := type_err:45}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':249
   return := havoc:257
   return@pos := type_err:258
   return@width := type_err:259
   when ((!(0 <= K:243) \/ mid_y:244 = K:243)
           /\ (!(0 <= K:243) \/ mid_x:245 = K:243)
           /\ (!(0 <= K:243) \/ mid___cost:246 = (__cost:65 + K:243))
           /\ ((K:243 = 0 /\ 0 = mid_y:244 /\ 0 = mid_x:245
                  /\ __cost:65 = mid___cost:246)
                 \/ (1 <= K:243 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                       /\ 0 <= (-1 + mid_y:244) /\ 0 <= (-1 + mid_x:245)
                       /\ 0 <= (-1 + mid___cost:246)
                       /\ 0 <= (param0:53 + -mid_x:245)))
           /\ (0 = K:243 \/ -param0:53 < 0)
           /\ (!(0 <= K:247) \/ y':248 = (mid_y:244 + -K:247))
           /\ (!(0 <= K:247) \/ __cost':249 = (mid___cost:246 + K:247))
           /\ (!(0 <= K:247) \/ x':250 = mid_x:245)
           /\ ((K:247 = 0 /\ mid_y:244 = y':248 /\ mid_x:245 = x':250
                  /\ mid___cost:246 = __cost':249)
                 \/ (1 <= K:247 /\ 0 <= (mid_x:245 + -param0:53)
                       /\ 0 <= mid_x:245 /\ 0 <= mid___cost:246
                       /\ 0 <= (-1 + mid_y:244) /\ 0 <= (-param0:53 + x':250)
                       /\ 0 <= y':248 /\ 0 <= (-1 + __cost':249)
                       /\ 0 <= x':250))
           /\ (0 = K:247 \/ !((mid_x:245 + -param0:53) < 0))
           /\ (K:243 + K:247) = K:251 /\ (!(0 <= K:252) \/ mid_y:253 = K:252)
           /\ (!(0 <= K:252) \/ mid_x:254 = K:252)
           /\ (!(0 <= K:252) \/ mid___cost:255 = (__cost:65 + K:252))
           /\ ((K:252 = 0 /\ 0 = mid_y:253 /\ 0 = mid_x:254
                  /\ __cost:65 = mid___cost:255)
                 \/ (1 <= K:252 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                       /\ 0 <= (-1 + mid_y:253) /\ 0 <= (-1 + mid_x:254)
                       /\ 0 <= (-1 + mid___cost:255)
                       /\ 0 <= (param0:53 + -mid_x:254)))
           /\ (0 = K:252 \/ !(param0:53 <= 0))
           /\ (!(0 <= K:256) \/ y':248 = (mid_y:253 + -K:256))
           /\ (!(0 <= K:256) \/ __cost':249 = (mid___cost:255 + K:256))
           /\ (!(0 <= K:256) \/ x':250 = mid_x:254)
           /\ ((K:256 = 0 /\ mid_y:253 = y':248 /\ mid_x:254 = x':250
                  /\ mid___cost:255 = __cost':249)
                 \/ (1 <= K:256 /\ 0 <= (mid_x:254 + -param0:53)
                       /\ 0 <= mid_x:254 /\ 0 <= mid___cost:255
                       /\ 0 <= (-1 + mid_y:253) /\ 0 <= (-param0:53 + x':250)
                       /\ 0 <= y':248 /\ 0 <= (-1 + __cost':249)
                       /\ 0 <= x':250))
           /\ (0 = K:256 \/ (-mid_x:254 + param0:53) <= 0)
           /\ (K:252 + K:256) = K:251 /\ 0 <= K:251 /\ 0 <= y':248
           /\ 0 <= x':250 /\ param0:53 <= x':250 /\ y':248 <= 0)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':288
   return := 0
   param0 := havoc:13
   return@pos := type_err:302
   param0@pos := type_err:298
   return@width := type_err:303
   param0@width := type_err:300
   when ((!(0 <= K:282) \/ mid_y:283 = K:282)
           /\ (!(0 <= K:282) \/ mid_x:284 = K:282)
           /\ (!(0 <= K:282) \/ mid___cost:285 = K:282)
           /\ ((K:282 = 0 /\ 0 = mid_y:283 /\ 0 = mid_x:284
                  /\ 0 = mid___cost:285)
                 \/ (1 <= K:282 /\ 0 <= (-1 + havoc:13)
                       /\ 0 <= (-1 + mid_y:283) /\ 0 <= (-1 + mid_x:284)
                       /\ 0 <= (-1 + mid___cost:285)
                       /\ 0 <= (havoc:13 + -mid_x:284)))
           /\ (0 = K:282 \/ -havoc:13 < 0)
           /\ (!(0 <= K:286) \/ y':287 = (mid_y:283 + -K:286))
           /\ (!(0 <= K:286) \/ __cost':288 = (mid___cost:285 + K:286))
           /\ (!(0 <= K:286) \/ x':289 = mid_x:284)
           /\ ((K:286 = 0 /\ mid_y:283 = y':287 /\ mid_x:284 = x':289
                  /\ mid___cost:285 = __cost':288)
                 \/ (1 <= K:286 /\ 0 <= (mid_x:284 + -havoc:13)
                       /\ 0 <= mid_x:284 /\ 0 <= mid___cost:285
                       /\ 0 <= (-1 + mid_y:283) /\ 0 <= (-havoc:13 + x':289)
                       /\ 0 <= y':287 /\ 0 <= (-1 + __cost':288)
                       /\ 0 <= x':289))
           /\ (0 = K:286 \/ !((mid_x:284 + -havoc:13) < 0))
           /\ (K:282 + K:286) = K:290 /\ (!(0 <= K:291) \/ mid_y:292 = K:291)
           /\ (!(0 <= K:291) \/ mid_x:293 = K:291)
           /\ (!(0 <= K:291) \/ mid___cost:294 = K:291)
           /\ ((K:291 = 0 /\ 0 = mid_y:292 /\ 0 = mid_x:293
                  /\ 0 = mid___cost:294)
                 \/ (1 <= K:291 /\ 0 <= (-1 + havoc:13)
                       /\ 0 <= (-1 + mid_y:292) /\ 0 <= (-1 + mid_x:293)
                       /\ 0 <= (-1 + mid___cost:294)
                       /\ 0 <= (havoc:13 + -mid_x:293)))
           /\ (0 = K:291 \/ !(havoc:13 <= 0))
           /\ (!(0 <= K:295) \/ y':287 = (mid_y:292 + -K:295))
           /\ (!(0 <= K:295) \/ __cost':288 = (mid___cost:294 + K:295))
           /\ (!(0 <= K:295) \/ x':289 = mid_x:293)
           /\ ((K:295 = 0 /\ mid_y:292 = y':287 /\ mid_x:293 = x':289
                  /\ mid___cost:294 = __cost':288)
                 \/ (1 <= K:295 /\ 0 <= (mid_x:293 + -havoc:13)
                       /\ 0 <= mid_x:293 /\ 0 <= mid___cost:294
                       /\ 0 <= (-1 + mid_y:292) /\ 0 <= (-havoc:13 + x':289)
                       /\ 0 <= y':287 /\ 0 <= (-1 + __cost':288)
                       /\ 0 <= x':289))
           /\ (0 = K:295 \/ (-mid_x:293 + havoc:13) <= 0)
           /\ (K:291 + K:295) = K:290 /\ 0 <= K:290 /\ 0 <= y':287
           /\ 0 <= x':289 /\ havoc:13 <= x':289 /\ y':287 <= 0
           /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:301)
                 \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:301)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':310
   return := havoc:321
   param0 := param0:53
   return@pos := type_err:322
   param0@pos := type_err:54
   return@width := type_err:323
   param0@width := type_err:55
   when ((!(0 <= K:304) \/ mid_y:305 = K:304)
           /\ (!(0 <= K:304) \/ mid_x:306 = K:304)
           /\ (!(0 <= K:304) \/ mid___cost:307 = (__cost:65 + K:304))
           /\ ((K:304 = 0 /\ 0 = mid_y:305 /\ 0 = mid_x:306
                  /\ __cost:65 = mid___cost:307)
                 \/ (1 <= K:304 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                       /\ 0 <= (-1 + mid_y:305) /\ 0 <= (-1 + mid_x:306)
                       /\ 0 <= (-1 + mid___cost:307)
                       /\ 0 <= (param0:53 + -mid_x:306)))
           /\ (0 = K:304 \/ -param0:53 < 0)
           /\ (!(0 <= K:308) \/ y':309 = (mid_y:305 + -K:308))
           /\ (!(0 <= K:308) \/ __cost':310 = (mid___cost:307 + K:308))
           /\ (!(0 <= K:308) \/ x':311 = mid_x:306)
           /\ ((K:308 = 0 /\ mid_y:305 = y':309 /\ mid_x:306 = x':311
                  /\ mid___cost:307 = __cost':310)
                 \/ (1 <= K:308 /\ 0 <= (mid_x:306 + -param0:53)
                       /\ 0 <= mid_x:306 /\ 0 <= mid___cost:307
                       /\ 0 <= (-1 + mid_y:305) /\ 0 <= (-param0:53 + x':311)
                       /\ 0 <= y':309 /\ 0 <= (-1 + __cost':310)
                       /\ 0 <= x':311))
           /\ (0 = K:308 \/ !((mid_x:306 + -param0:53) < 0))
           /\ (K:304 + K:308) = K:312 /\ (!(0 <= K:313) \/ mid_y:314 = K:313)
           /\ (!(0 <= K:313) \/ mid_x:315 = K:313)
           /\ (!(0 <= K:313) \/ mid___cost:316 = (__cost:65 + K:313))
           /\ ((K:313 = 0 /\ 0 = mid_y:314 /\ 0 = mid_x:315
                  /\ __cost:65 = mid___cost:316)
                 \/ (1 <= K:313 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                       /\ 0 <= (-1 + mid_y:314) /\ 0 <= (-1 + mid_x:315)
                       /\ 0 <= (-1 + mid___cost:316)
                       /\ 0 <= (param0:53 + -mid_x:315)))
           /\ (0 = K:313 \/ !(param0:53 <= 0))
           /\ (!(0 <= K:317) \/ y':309 = (mid_y:314 + -K:317))
           /\ (!(0 <= K:317) \/ __cost':310 = (mid___cost:316 + K:317))
           /\ (!(0 <= K:317) \/ x':311 = mid_x:315)
           /\ ((K:317 = 0 /\ mid_y:314 = y':309 /\ mid_x:315 = x':311
                  /\ mid___cost:316 = __cost':310)
                 \/ (1 <= K:317 /\ 0 <= (mid_x:315 + -param0:53)
                       /\ 0 <= mid_x:315 /\ 0 <= mid___cost:316
                       /\ 0 <= (-1 + mid_y:314) /\ 0 <= (-param0:53 + x':311)
                       /\ 0 <= y':309 /\ 0 <= (-1 + __cost':310)
                       /\ 0 <= x':311))
           /\ (0 = K:317 \/ (-mid_x:315 + param0:53) <= 0)
           /\ (K:313 + K:317) = K:312 /\ 0 <= K:312 /\ 0 <= y':309
           /\ 0 <= x':311 /\ param0:53 <= x':311 /\ y':309 <= 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=21: 
Weight(Base relation: 
  {__cost := __cost':249
   return := havoc:257
   return@pos := type_err:258
   return@width := type_err:259
   when ((!(0 <= K:243) \/ mid_y:244 = K:243)
           /\ (!(0 <= K:243) \/ mid_x:245 = K:243)
           /\ (!(0 <= K:243) \/ mid___cost:246 = (__cost:65 + K:243))
           /\ ((K:243 = 0 /\ 0 = mid_y:244 /\ 0 = mid_x:245
                  /\ __cost:65 = mid___cost:246)
                 \/ (1 <= K:243 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                       /\ 0 <= (-1 + mid_y:244) /\ 0 <= (-1 + mid_x:245)
                       /\ 0 <= (-1 + mid___cost:246)
                       /\ 0 <= (param0:53 + -mid_x:245)))
           /\ (0 = K:243 \/ -param0:53 < 0)
           /\ (!(0 <= K:247) \/ y':248 = (mid_y:244 + -K:247))
           /\ (!(0 <= K:247) \/ __cost':249 = (mid___cost:246 + K:247))
           /\ (!(0 <= K:247) \/ x':250 = mid_x:245)
           /\ ((K:247 = 0 /\ mid_y:244 = y':248 /\ mid_x:245 = x':250
                  /\ mid___cost:246 = __cost':249)
                 \/ (1 <= K:247 /\ 0 <= (mid_x:245 + -param0:53)
                       /\ 0 <= mid_x:245 /\ 0 <= mid___cost:246
                       /\ 0 <= (-1 + mid_y:244) /\ 0 <= (-param0:53 + x':250)
                       /\ 0 <= y':248 /\ 0 <= (-1 + __cost':249)
                       /\ 0 <= x':250))
           /\ (0 = K:247 \/ !((mid_x:245 + -param0:53) < 0))
           /\ (K:243 + K:247) = K:251 /\ (!(0 <= K:252) \/ mid_y:253 = K:252)
           /\ (!(0 <= K:252) \/ mid_x:254 = K:252)
           /\ (!(0 <= K:252) \/ mid___cost:255 = (__cost:65 + K:252))
           /\ ((K:252 = 0 /\ 0 = mid_y:253 /\ 0 = mid_x:254
                  /\ __cost:65 = mid___cost:255)
                 \/ (1 <= K:252 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                       /\ 0 <= (-1 + mid_y:253) /\ 0 <= (-1 + mid_x:254)
                       /\ 0 <= (-1 + mid___cost:255)
                       /\ 0 <= (param0:53 + -mid_x:254)))
           /\ (0 = K:252 \/ !(param0:53 <= 0))
           /\ (!(0 <= K:256) \/ y':248 = (mid_y:253 + -K:256))
           /\ (!(0 <= K:256) \/ __cost':249 = (mid___cost:255 + K:256))
           /\ (!(0 <= K:256) \/ x':250 = mid_x:254)
           /\ ((K:256 = 0 /\ mid_y:253 = y':248 /\ mid_x:254 = x':250
                  /\ mid___cost:255 = __cost':249)
                 \/ (1 <= K:256 /\ 0 <= (mid_x:254 + -param0:53)
                       /\ 0 <= mid_x:254 /\ 0 <= mid___cost:255
                       /\ 0 <= (-1 + mid_y:253) /\ 0 <= (-param0:53 + x':250)
                       /\ 0 <= y':248 /\ 0 <= (-1 + __cost':249)
                       /\ 0 <= x':250))
           /\ (0 = K:256 \/ (-mid_x:254 + param0:53) <= 0)
           /\ (K:252 + K:256) = K:251 /\ 0 <= K:251 /\ 0 <= y':248
           /\ 0 <= x':250 /\ param0:53 <= x':250 /\ y':248 <= 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':288
 return := 0
 param0 := havoc:13
 return@pos := type_err:302
 param0@pos := type_err:298
 return@width := type_err:303
 param0@width := type_err:300
 when ((!(0 <= K:282) \/ mid_y:283 = K:282)
         /\ (!(0 <= K:282) \/ mid_x:284 = K:282)
         /\ (!(0 <= K:282) \/ mid___cost:285 = K:282)
         /\ ((K:282 = 0 /\ 0 = mid_y:283 /\ 0 = mid_x:284
                /\ 0 = mid___cost:285)
               \/ (1 <= K:282 /\ 0 <= (-1 + havoc:13)
                     /\ 0 <= (-1 + mid_y:283) /\ 0 <= (-1 + mid_x:284)
                     /\ 0 <= (-1 + mid___cost:285)
                     /\ 0 <= (havoc:13 + -mid_x:284)))
         /\ (0 = K:282 \/ -havoc:13 < 0)
         /\ (!(0 <= K:286) \/ y':287 = (mid_y:283 + -K:286))
         /\ (!(0 <= K:286) \/ __cost':288 = (mid___cost:285 + K:286))
         /\ (!(0 <= K:286) \/ x':289 = mid_x:284)
         /\ ((K:286 = 0 /\ mid_y:283 = y':287 /\ mid_x:284 = x':289
                /\ mid___cost:285 = __cost':288)
               \/ (1 <= K:286 /\ 0 <= (mid_x:284 + -havoc:13)
                     /\ 0 <= mid_x:284 /\ 0 <= mid___cost:285
                     /\ 0 <= (-1 + mid_y:283) /\ 0 <= (-havoc:13 + x':289)
                     /\ 0 <= y':287 /\ 0 <= (-1 + __cost':288) /\ 0 <= x':289))
         /\ (0 = K:286 \/ !((mid_x:284 + -havoc:13) < 0))
         /\ (K:282 + K:286) = K:290 /\ (!(0 <= K:291) \/ mid_y:292 = K:291)
         /\ (!(0 <= K:291) \/ mid_x:293 = K:291)
         /\ (!(0 <= K:291) \/ mid___cost:294 = K:291)
         /\ ((K:291 = 0 /\ 0 = mid_y:292 /\ 0 = mid_x:293
                /\ 0 = mid___cost:294)
               \/ (1 <= K:291 /\ 0 <= (-1 + havoc:13)
                     /\ 0 <= (-1 + mid_y:292) /\ 0 <= (-1 + mid_x:293)
                     /\ 0 <= (-1 + mid___cost:294)
                     /\ 0 <= (havoc:13 + -mid_x:293)))
         /\ (0 = K:291 \/ !(havoc:13 <= 0))
         /\ (!(0 <= K:295) \/ y':287 = (mid_y:292 + -K:295))
         /\ (!(0 <= K:295) \/ __cost':288 = (mid___cost:294 + K:295))
         /\ (!(0 <= K:295) \/ x':289 = mid_x:293)
         /\ ((K:295 = 0 /\ mid_y:292 = y':287 /\ mid_x:293 = x':289
                /\ mid___cost:294 = __cost':288)
               \/ (1 <= K:295 /\ 0 <= (mid_x:293 + -havoc:13)
                     /\ 0 <= mid_x:293 /\ 0 <= mid___cost:294
                     /\ 0 <= (-1 + mid_y:292) /\ 0 <= (-havoc:13 + x':289)
                     /\ 0 <= y':287 /\ 0 <= (-1 + __cost':288) /\ 0 <= x':289))
         /\ (0 = K:295 \/ (-mid_x:293 + havoc:13) <= 0)
         /\ (K:291 + K:295) = K:290 /\ 0 <= K:290 /\ 0 <= y':287
         /\ 0 <= x':289 /\ havoc:13 <= x':289 /\ y':287 <= 0
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:301)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:301)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':310
 return := havoc:321
 param0 := param0:53
 return@pos := type_err:322
 param0@pos := type_err:54
 return@width := type_err:323
 param0@width := type_err:55
 when ((!(0 <= K:304) \/ mid_y:305 = K:304)
         /\ (!(0 <= K:304) \/ mid_x:306 = K:304)
         /\ (!(0 <= K:304) \/ mid___cost:307 = (__cost:65 + K:304))
         /\ ((K:304 = 0 /\ 0 = mid_y:305 /\ 0 = mid_x:306
                /\ __cost:65 = mid___cost:307)
               \/ (1 <= K:304 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                     /\ 0 <= (-1 + mid_y:305) /\ 0 <= (-1 + mid_x:306)
                     /\ 0 <= (-1 + mid___cost:307)
                     /\ 0 <= (param0:53 + -mid_x:306)))
         /\ (0 = K:304 \/ -param0:53 < 0)
         /\ (!(0 <= K:308) \/ y':309 = (mid_y:305 + -K:308))
         /\ (!(0 <= K:308) \/ __cost':310 = (mid___cost:307 + K:308))
         /\ (!(0 <= K:308) \/ x':311 = mid_x:306)
         /\ ((K:308 = 0 /\ mid_y:305 = y':309 /\ mid_x:306 = x':311
                /\ mid___cost:307 = __cost':310)
               \/ (1 <= K:308 /\ 0 <= (mid_x:306 + -param0:53)
                     /\ 0 <= mid_x:306 /\ 0 <= mid___cost:307
                     /\ 0 <= (-1 + mid_y:305) /\ 0 <= (-param0:53 + x':311)
                     /\ 0 <= y':309 /\ 0 <= (-1 + __cost':310) /\ 0 <= x':311))
         /\ (0 = K:308 \/ !((mid_x:306 + -param0:53) < 0))
         /\ (K:304 + K:308) = K:312 /\ (!(0 <= K:313) \/ mid_y:314 = K:313)
         /\ (!(0 <= K:313) \/ mid_x:315 = K:313)
         /\ (!(0 <= K:313) \/ mid___cost:316 = (__cost:65 + K:313))
         /\ ((K:313 = 0 /\ 0 = mid_y:314 /\ 0 = mid_x:315
                /\ __cost:65 = mid___cost:316)
               \/ (1 <= K:313 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                     /\ 0 <= (-1 + mid_y:314) /\ 0 <= (-1 + mid_x:315)
                     /\ 0 <= (-1 + mid___cost:316)
                     /\ 0 <= (param0:53 + -mid_x:315)))
         /\ (0 = K:313 \/ !(param0:53 <= 0))
         /\ (!(0 <= K:317) \/ y':309 = (mid_y:314 + -K:317))
         /\ (!(0 <= K:317) \/ __cost':310 = (mid___cost:316 + K:317))
         /\ (!(0 <= K:317) \/ x':311 = mid_x:315)
         /\ ((K:317 = 0 /\ mid_y:314 = y':309 /\ mid_x:315 = x':311
                /\ mid___cost:316 = __cost':310)
               \/ (1 <= K:317 /\ 0 <= (mid_x:315 + -param0:53)
                     /\ 0 <= mid_x:315 /\ 0 <= mid___cost:316
                     /\ 0 <= (-1 + mid_y:314) /\ 0 <= (-param0:53 + x':311)
                     /\ 0 <= y':309 /\ 0 <= (-1 + __cost':310) /\ 0 <= x':311))
         /\ (0 = K:317 \/ (-mid_x:315 + param0:53) <= 0)
         /\ (K:313 + K:317) = K:312 /\ 0 <= K:312 /\ 0 <= y':309
         /\ 0 <= x':311 /\ param0:53 <= x':311 /\ y':309 <= 0)}

Evaluating variable number 21 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':249
 return := havoc:257
 return@pos := type_err:258
 return@width := type_err:259
 when ((!(0 <= K:243) \/ mid_y:244 = K:243)
         /\ (!(0 <= K:243) \/ mid_x:245 = K:243)
         /\ (!(0 <= K:243) \/ mid___cost:246 = (__cost:65 + K:243))
         /\ ((K:243 = 0 /\ 0 = mid_y:244 /\ 0 = mid_x:245
                /\ __cost:65 = mid___cost:246)
               \/ (1 <= K:243 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                     /\ 0 <= (-1 + mid_y:244) /\ 0 <= (-1 + mid_x:245)
                     /\ 0 <= (-1 + mid___cost:246)
                     /\ 0 <= (param0:53 + -mid_x:245)))
         /\ (0 = K:243 \/ -param0:53 < 0)
         /\ (!(0 <= K:247) \/ y':248 = (mid_y:244 + -K:247))
         /\ (!(0 <= K:247) \/ __cost':249 = (mid___cost:246 + K:247))
         /\ (!(0 <= K:247) \/ x':250 = mid_x:245)
         /\ ((K:247 = 0 /\ mid_y:244 = y':248 /\ mid_x:245 = x':250
                /\ mid___cost:246 = __cost':249)
               \/ (1 <= K:247 /\ 0 <= (mid_x:245 + -param0:53)
                     /\ 0 <= mid_x:245 /\ 0 <= mid___cost:246
                     /\ 0 <= (-1 + mid_y:244) /\ 0 <= (-param0:53 + x':250)
                     /\ 0 <= y':248 /\ 0 <= (-1 + __cost':249) /\ 0 <= x':250))
         /\ (0 = K:247 \/ !((mid_x:245 + -param0:53) < 0))
         /\ (K:243 + K:247) = K:251 /\ (!(0 <= K:252) \/ mid_y:253 = K:252)
         /\ (!(0 <= K:252) \/ mid_x:254 = K:252)
         /\ (!(0 <= K:252) \/ mid___cost:255 = (__cost:65 + K:252))
         /\ ((K:252 = 0 /\ 0 = mid_y:253 /\ 0 = mid_x:254
                /\ __cost:65 = mid___cost:255)
               \/ (1 <= K:252 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                     /\ 0 <= (-1 + mid_y:253) /\ 0 <= (-1 + mid_x:254)
                     /\ 0 <= (-1 + mid___cost:255)
                     /\ 0 <= (param0:53 + -mid_x:254)))
         /\ (0 = K:252 \/ !(param0:53 <= 0))
         /\ (!(0 <= K:256) \/ y':248 = (mid_y:253 + -K:256))
         /\ (!(0 <= K:256) \/ __cost':249 = (mid___cost:255 + K:256))
         /\ (!(0 <= K:256) \/ x':250 = mid_x:254)
         /\ ((K:256 = 0 /\ mid_y:253 = y':248 /\ mid_x:254 = x':250
                /\ mid___cost:255 = __cost':249)
               \/ (1 <= K:256 /\ 0 <= (mid_x:254 + -param0:53)
                     /\ 0 <= mid_x:254 /\ 0 <= mid___cost:255
                     /\ 0 <= (-1 + mid_y:253) /\ 0 <= (-param0:53 + x':250)
                     /\ 0 <= y':248 /\ 0 <= (-1 + __cost':249) /\ 0 <= x':250))
         /\ (0 = K:256 \/ (-mid_x:254 + param0:53) <= 0)
         /\ (K:252 + K:256) = K:251 /\ 0 <= K:251 /\ 0 <= y':248
         /\ 0 <= x':250 /\ param0:53 <= x':250 /\ y':248 <= 0)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,50)_g1> -> <__pstate, (Unique State Name,46)_g1>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
<__pstate, accept> -> <__pstate, (Unique State Name,50)_g1>	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x779c5a0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x78ab7e0: 
	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,46)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:366
 param0@width := type_err:367}
    ( __pstate , (Unique State Name,50)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}

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

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

Base relation: 
{__cost := __cost':330
 n := havoc:13
 return := 0
 param0 := havoc:13
 return@pos := type_err:344
 param0@pos := type_err:340
 return@width := type_err:345
 param0@width := type_err:342
 when ((!(0 <= K:324) \/ mid_y:325 = K:324)
         /\ (!(0 <= K:324) \/ mid_x:326 = K:324)
         /\ (!(0 <= K:324) \/ mid___cost:327 = K:324)
         /\ ((K:324 = 0 /\ 0 = mid_y:325 /\ 0 = mid_x:326
                /\ 0 = mid___cost:327)
               \/ (1 <= K:324 /\ 0 <= (-1 + havoc:13)
                     /\ 0 <= (-1 + mid_y:325) /\ 0 <= (-1 + mid_x:326)
                     /\ 0 <= (-1 + mid___cost:327)
                     /\ 0 <= (havoc:13 + -mid_x:326)))
         /\ (0 = K:324 \/ -havoc:13 < 0)
         /\ (!(0 <= K:328) \/ y':329 = (mid_y:325 + -K:328))
         /\ (!(0 <= K:328) \/ __cost':330 = (mid___cost:327 + K:328))
         /\ (!(0 <= K:328) \/ x':331 = mid_x:326)
         /\ ((K:328 = 0 /\ mid_y:325 = y':329 /\ mid_x:326 = x':331
                /\ mid___cost:327 = __cost':330)
               \/ (1 <= K:328 /\ 0 <= (mid_x:326 + -havoc:13)
                     /\ 0 <= mid_x:326 /\ 0 <= mid___cost:327
                     /\ 0 <= (-1 + mid_y:325) /\ 0 <= (-havoc:13 + x':331)
                     /\ 0 <= y':329 /\ 0 <= (-1 + __cost':330) /\ 0 <= x':331))
         /\ (0 = K:328 \/ !((mid_x:326 + -havoc:13) < 0))
         /\ (K:324 + K:328) = K:332 /\ (!(0 <= K:333) \/ mid_y:334 = K:333)
         /\ (!(0 <= K:333) \/ mid_x:335 = K:333)
         /\ (!(0 <= K:333) \/ mid___cost:336 = K:333)
         /\ ((K:333 = 0 /\ 0 = mid_y:334 /\ 0 = mid_x:335
                /\ 0 = mid___cost:336)
               \/ (1 <= K:333 /\ 0 <= (-1 + havoc:13)
                     /\ 0 <= (-1 + mid_y:334) /\ 0 <= (-1 + mid_x:335)
                     /\ 0 <= (-1 + mid___cost:336)
                     /\ 0 <= (havoc:13 + -mid_x:335)))
         /\ (0 = K:333 \/ !(havoc:13 <= 0))
         /\ (!(0 <= K:337) \/ y':329 = (mid_y:334 + -K:337))
         /\ (!(0 <= K:337) \/ __cost':330 = (mid___cost:336 + K:337))
         /\ (!(0 <= K:337) \/ x':331 = mid_x:335)
         /\ ((K:337 = 0 /\ mid_y:334 = y':329 /\ mid_x:335 = x':331
                /\ mid___cost:336 = __cost':330)
               \/ (1 <= K:337 /\ 0 <= (mid_x:335 + -havoc:13)
                     /\ 0 <= mid_x:335 /\ 0 <= mid___cost:336
                     /\ 0 <= (-1 + mid_y:334) /\ 0 <= (-havoc:13 + x':331)
                     /\ 0 <= y':329 /\ 0 <= (-1 + __cost':330) /\ 0 <= x':331))
         /\ (0 = K:337 \/ (-mid_x:335 + havoc:13) <= 0)
         /\ (K:333 + K:337) = K:332 /\ 0 <= K:332 /\ 0 <= y':329
         /\ 0 <= x':331 /\ havoc:13 <= x':331 /\ y':329 <= 0
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:343)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:343)))}

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

Base relation: 
{__cost := __cost':352
 return := havoc:363
 param0 := param0:53
 return@pos := type_err:364
 param0@pos := type_err:54
 return@width := type_err:365
 param0@width := type_err:55
 when ((!(0 <= K:346) \/ mid_y:347 = K:346)
         /\ (!(0 <= K:346) \/ mid_x:348 = K:346)
         /\ (!(0 <= K:346) \/ mid___cost:349 = (__cost:65 + K:346))
         /\ ((K:346 = 0 /\ 0 = mid_y:347 /\ 0 = mid_x:348
                /\ __cost:65 = mid___cost:349)
               \/ (1 <= K:346 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                     /\ 0 <= (-1 + mid_y:347) /\ 0 <= (-1 + mid_x:348)
                     /\ 0 <= (-1 + mid___cost:349)
                     /\ 0 <= (param0:53 + -mid_x:348)))
         /\ (0 = K:346 \/ -param0:53 < 0)
         /\ (!(0 <= K:350) \/ y':351 = (mid_y:347 + -K:350))
         /\ (!(0 <= K:350) \/ __cost':352 = (mid___cost:349 + K:350))
         /\ (!(0 <= K:350) \/ x':353 = mid_x:348)
         /\ ((K:350 = 0 /\ mid_y:347 = y':351 /\ mid_x:348 = x':353
                /\ mid___cost:349 = __cost':352)
               \/ (1 <= K:350 /\ 0 <= (mid_x:348 + -param0:53)
                     /\ 0 <= mid_x:348 /\ 0 <= mid___cost:349
                     /\ 0 <= (-1 + mid_y:347) /\ 0 <= (-param0:53 + x':353)
                     /\ 0 <= y':351 /\ 0 <= (-1 + __cost':352) /\ 0 <= x':353))
         /\ (0 = K:350 \/ !((mid_x:348 + -param0:53) < 0))
         /\ (K:346 + K:350) = K:354 /\ (!(0 <= K:355) \/ mid_y:356 = K:355)
         /\ (!(0 <= K:355) \/ mid_x:357 = K:355)
         /\ (!(0 <= K:355) \/ mid___cost:358 = (__cost:65 + K:355))
         /\ ((K:355 = 0 /\ 0 = mid_y:356 /\ 0 = mid_x:357
                /\ __cost:65 = mid___cost:358)
               \/ (1 <= K:355 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                     /\ 0 <= (-1 + mid_y:356) /\ 0 <= (-1 + mid_x:357)
                     /\ 0 <= (-1 + mid___cost:358)
                     /\ 0 <= (param0:53 + -mid_x:357)))
         /\ (0 = K:355 \/ !(param0:53 <= 0))
         /\ (!(0 <= K:359) \/ y':351 = (mid_y:356 + -K:359))
         /\ (!(0 <= K:359) \/ __cost':352 = (mid___cost:358 + K:359))
         /\ (!(0 <= K:359) \/ x':353 = mid_x:357)
         /\ ((K:359 = 0 /\ mid_y:356 = y':351 /\ mid_x:357 = x':353
                /\ mid___cost:358 = __cost':352)
               \/ (1 <= K:359 /\ 0 <= (mid_x:357 + -param0:53)
                     /\ 0 <= mid_x:357 /\ 0 <= mid___cost:358
                     /\ 0 <= (-1 + mid_y:356) /\ 0 <= (-param0:53 + x':353)
                     /\ 0 <= y':351 /\ 0 <= (-1 + __cost':352) /\ 0 <= x':353))
         /\ (0 = K:359 \/ (-mid_x:357 + param0:53) <= 0)
         /\ (K:355 + K:359) = K:354 /\ 0 <= K:354 /\ 0 <= y':351
         /\ 0 <= x':353 /\ param0:53 <= x':353 /\ y':351 <= 0)}

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

Base relation: 
{__cost := __cost':249
 x := x':250
 y := y':248
 n := param0:53
 return := havoc:257
 return@pos := type_err:258
 return@width := type_err:259
 when ((!(0 <= K:243) \/ mid_y:244 = K:243)
         /\ (!(0 <= K:243) \/ mid_x:245 = K:243)
         /\ (!(0 <= K:243) \/ mid___cost:246 = (__cost:65 + K:243))
         /\ ((K:243 = 0 /\ 0 = mid_y:244 /\ 0 = mid_x:245
                /\ __cost:65 = mid___cost:246)
               \/ (1 <= K:243 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                     /\ 0 <= (-1 + mid_y:244) /\ 0 <= (-1 + mid_x:245)
                     /\ 0 <= (-1 + mid___cost:246)
                     /\ 0 <= (param0:53 + -mid_x:245)))
         /\ (0 = K:243 \/ -param0:53 < 0)
         /\ (!(0 <= K:247) \/ y':248 = (mid_y:244 + -K:247))
         /\ (!(0 <= K:247) \/ __cost':249 = (mid___cost:246 + K:247))
         /\ (!(0 <= K:247) \/ x':250 = mid_x:245)
         /\ ((K:247 = 0 /\ mid_y:244 = y':248 /\ mid_x:245 = x':250
                /\ mid___cost:246 = __cost':249)
               \/ (1 <= K:247 /\ 0 <= (mid_x:245 + -param0:53)
                     /\ 0 <= mid_x:245 /\ 0 <= mid___cost:246
                     /\ 0 <= (-1 + mid_y:244) /\ 0 <= (-param0:53 + x':250)
                     /\ 0 <= y':248 /\ 0 <= (-1 + __cost':249) /\ 0 <= x':250))
         /\ (0 = K:247 \/ !((mid_x:245 + -param0:53) < 0))
         /\ (K:243 + K:247) = K:251 /\ (!(0 <= K:252) \/ mid_y:253 = K:252)
         /\ (!(0 <= K:252) \/ mid_x:254 = K:252)
         /\ (!(0 <= K:252) \/ mid___cost:255 = (__cost:65 + K:252))
         /\ ((K:252 = 0 /\ 0 = mid_y:253 /\ 0 = mid_x:254
                /\ __cost:65 = mid___cost:255)
               \/ (1 <= K:252 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:65
                     /\ 0 <= (-1 + mid_y:253) /\ 0 <= (-1 + mid_x:254)
                     /\ 0 <= (-1 + mid___cost:255)
                     /\ 0 <= (param0:53 + -mid_x:254)))
         /\ (0 = K:252 \/ !(param0:53 <= 0))
         /\ (!(0 <= K:256) \/ y':248 = (mid_y:253 + -K:256))
         /\ (!(0 <= K:256) \/ __cost':249 = (mid___cost:255 + K:256))
         /\ (!(0 <= K:256) \/ x':250 = mid_x:254)
         /\ ((K:256 = 0 /\ mid_y:253 = y':248 /\ mid_x:254 = x':250
                /\ mid___cost:255 = __cost':249)
               \/ (1 <= K:256 /\ 0 <= (mid_x:254 + -param0:53)
                     /\ 0 <= mid_x:254 /\ 0 <= mid___cost:255
                     /\ 0 <= (-1 + mid_y:253) /\ 0 <= (-param0:53 + x':250)
                     /\ 0 <= y':248 /\ 0 <= (-1 + __cost':249) /\ 0 <= x':250))
         /\ (0 = K:256 \/ (-mid_x:254 + param0:53) <= 0)
         /\ (K:252 + K:256) = K:251 /\ 0 <= K:251 /\ 0 <= y':248
         /\ 0 <= x':250 /\ param0:53 <= x':250 /\ y':248 <= 0)}

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

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

Variable bounds at line 26 in run

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

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