/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, 68> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 31> -> <Unique State Name, 70>	Base relation: 
{when (0 <= y:102 /\ 0 <= x:101)}	
<Unique State Name, 60> -> <Unique State Name, 55 59>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 69> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 67> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 36> -> <Unique State Name, 43>	Base relation: 
{x := (x:101 + 1)
 y := (y:102 + 1)
 when y:102 < m:103}	
<Unique State Name, 36> -> <Unique State Name, 67>	Base relation: 
{return := havoc:111
 return@pos := type_err:112
 return@width := type_err:113
 when m:103 <= y:102}	
<Unique State Name, 70> -> <Unique State Name, 42>	Base relation: 
{}	
<Unique State Name, 65> -> <Unique State Name, 69>	Base relation: 
{return := 0
 return@pos := type_err:32
 return@width := type_err:33
 when (((0 < n:4 /\ n:4 = phi_tmp___1:23) \/ (n:4 <= 0 /\ 0 = phi_tmp___1:23))
         /\ ((0 < m:5 /\ m:5 = phi_tmp___2:31)
               \/ (m:5 <= 0 /\ 0 = phi_tmp___2:31)))}	
<Unique State Name, 66> -> <Unique State Name, 61 65>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 55> -> <Unique State Name, 31>	Base relation: 
{x := 0
 y := 0
 n := param0:80
 m := param1:83}	
<Unique State Name, 59> -> <Unique State Name, 25>	Base relation: 
{}	
<Unique State Name, 42> -> <Unique State Name, 36>	Base relation: 
{when n:104 <= x:101}	
<Unique State Name, 42> -> <Unique State Name, 43>	Base relation: 
{x := (x:101 + 1)
 y := (y:102 + 1)
 when x:101 < n:104}	
<Unique State Name, 61> -> <Unique State Name, 60>	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, 25> -> <Unique State Name, 68>	Base relation: 
{return := havoc:63
 return@pos := type_err:66
 return@width := type_err:67}	
<Unique State Name, 23> -> <Unique State Name, 66>	Base relation: 
{__cost := 0
 n := havoc:21
 m := 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, 43> -> <Unique State Name, 31>	Base relation: 
{__cost := (__cost:105 + 1)
 when (0 <= __cost:105 /\ 0 <= (__cost:105 + 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:105 + 1)
 x := (x:101 + 1)
 y := (y:102 + 1)
 when (0 <= y:102 /\ 0 <= x:101
         /\ (x:101 < n:104 \/ (n:104 <= x:101 /\ y:102 < m:103))
         /\ 0 <= __cost:105 /\ 0 <= (__cost:105 + 1))}
**** alpha hat: 
  {<Split [(x:101 + -n:104) < 0
            (y':256) = (1)*(y:102) + 1
           (x':255) = (1)*(x:101) + 1
           (__cost':254) = (1)*(__cost:105) + 1
           }
          pre:
            [|-x:101+n:104-1>=0; y:102>=0; __cost:105>=0; x:101>=0|]
          post:
            [|y':256-1>=0; x':255-1>=0; __cost':254-1>=0; n:104-x':255>=0|]
           (x':255) = (1)*(x:101) + 1
          (y':256) = (1)*(y:102) + 1
          (__cost':254) = (1)*(__cost:105) + 1
          }
  pre:
    [|-y:102+m:103-1>=0; x:101-n:104>=0; x:101>=0; __cost:105>=0; y:102>=0|]
  post:
    [|-n:104+x':255-1>=0; y':256-1>=0; x':255-1>=0; __cost':254-1>=0;
      m:103-y':256>=0|]],
[(y:102 + -m:103) < 0
  (__cost':254) = (1)*(__cost:105) + 1
 (y':256) = (1)*(y:102) + 1
 (x':255) = (1)*(x:101) + 1
 } pre:   [|-y:102+m:103-1>=0; x:101>=0; __cost:105>=0; y:102>=0|] post:
  [|-y':256+m:103>=0; x':255-1>=0; __cost':254-1>=0; y':256-1>=0|]
 (x':255) = (1)*(x:101) + 1 (__cost':254) = (1)*(__cost:105) + 1
(y':256) = (1)*(y:102) + 1 } pre:
  [|-x:101+n:104-1>=0; y:102-m:103>=0; y:102>=0; __cost:105>=0; x:101>=0|]
post:
  [|-m:103+y':256-1>=0; y':256-1>=0; x':255-1>=0; __cost':254-1>=0;
    n:104-x':255>=0|]],
[!((-x:101 + n:104) <= 0)
  (y':256) = (1)*(y:102) + 1
 (x':255) = (1)*(x:101) + 1
 (__cost':254) = (1)*(__cost:105) + 1
 } pre:   [|-x:101+n:104-1>=0; y:102>=0; __cost:105>=0; x:101>=0|] post:
  [|y':256-1>=0; x':255-1>=0; __cost':254-1>=0; n:104-x':255>=0|]
 (x':255) = (1)*(x:101) + 1 (y':256) = (1)*(y:102) + 1
(__cost':254) = (1)*(__cost:105) + 1 } pre:
  [|-y:102+m:103-1>=0; x:101-n:104>=0; x:101>=0; __cost:105>=0; y:102>=0|]
post:
  [|-n:104+x':255-1>=0; y':256-1>=0; x':255-1>=0; __cost':254-1>=0;
    m:103-y':256>=0|]]>}
**** star transition: 
  {__cost := __cost':254
   x := x':255
   y := y':256
   when ((!(0 <= K:304) \/ mid_y:306 = (y:102 + K:304))
           /\ (!(0 <= K:304) \/ mid_x:307 = (x:101 + K:304))
           /\ (!(0 <= K:304) \/ mid___cost:308 = (__cost:105 + K:304))
           /\ ((K:304 = 0 /\ y:102 = mid_y:306 /\ x:101 = mid_x:307
                  /\ __cost:105 = mid___cost:308)
                 \/ (1 <= K:304 /\ 0 <= (-1 + -x:101 + n:104) /\ 0 <= y:102
                       /\ 0 <= __cost:105 /\ 0 <= x:101
                       /\ 0 <= (-1 + mid_y:306) /\ 0 <= (-1 + mid_x:307)
                       /\ 0 <= (-1 + mid___cost:308)
                       /\ 0 <= (n:104 + -mid_x:307)))
           /\ (0 = K:304 \/ (x:101 + -n:104) < 0)
           /\ (!(0 <= K:305) \/ x':255 = (mid_x:307 + K:305))
           /\ (!(0 <= K:305) \/ y':256 = (mid_y:306 + K:305))
           /\ (!(0 <= K:305) \/ __cost':254 = (mid___cost:308 + K:305))
           /\ ((K:305 = 0 /\ mid_y:306 = y':256 /\ mid_x:307 = x':255
                  /\ mid___cost:308 = __cost':254)
                 \/ (1 <= K:305 /\ 0 <= (-1 + -mid_y:306 + m:103)
                       /\ 0 <= (mid_x:307 + -n:104) /\ 0 <= mid_x:307
                       /\ 0 <= mid___cost:308 /\ 0 <= mid_y:306
                       /\ 0 <= (-1 + -n:104 + x':255) /\ 0 <= (-1 + y':256)
                       /\ 0 <= (-1 + x':255) /\ 0 <= (-1 + __cost':254)
                       /\ 0 <= (m:103 + -y':256)))
           /\ (0 = K:305 \/ !((mid_x:307 + -n:104) < 0))
           /\ (K:304 + K:305) = K:303
           /\ (!(0 <= K:309) \/ mid___cost:313 = (__cost:105 + K:309))
           /\ (!(0 <= K:309) \/ mid_y:311 = (y:102 + K:309))
           /\ (!(0 <= K:309) \/ mid_x:312 = (x:101 + K:309))
           /\ ((K:309 = 0 /\ y:102 = mid_y:311 /\ x:101 = mid_x:312
                  /\ __cost:105 = mid___cost:313)
                 \/ (1 <= K:309 /\ 0 <= (-1 + -y:102 + m:103) /\ 0 <= x:101
                       /\ 0 <= __cost:105 /\ 0 <= y:102
                       /\ 0 <= (-mid_y:311 + m:103) /\ 0 <= (-1 + mid_x:312)
                       /\ 0 <= (-1 + mid___cost:313) /\ 0 <= (-1 + mid_y:311)))
           /\ (0 = K:309 \/ (y:102 + -m:103) < 0)
           /\ (!(0 <= K:310) \/ x':255 = (mid_x:312 + K:310))
           /\ (!(0 <= K:310) \/ __cost':254 = (mid___cost:313 + K:310))
           /\ (!(0 <= K:310) \/ y':256 = (mid_y:311 + K:310))
           /\ ((K:310 = 0 /\ mid_y:311 = y':256 /\ mid_x:312 = x':255
                  /\ mid___cost:313 = __cost':254)
                 \/ (1 <= K:310 /\ 0 <= (-1 + -mid_x:312 + n:104)
                       /\ 0 <= (mid_y:311 + -m:103) /\ 0 <= mid_y:311
                       /\ 0 <= mid___cost:313 /\ 0 <= mid_x:312
                       /\ 0 <= (-1 + -m:103 + y':256) /\ 0 <= (-1 + y':256)
                       /\ 0 <= (-1 + x':255) /\ 0 <= (-1 + __cost':254)
                       /\ 0 <= (n:104 + -x':255)))
           /\ (0 = K:310 \/ !((mid_y:311 + -m:103) < 0))
           /\ (K:309 + K:310) = K:303
           /\ (!(0 <= K:314) \/ mid_y:316 = (y:102 + K:314))
           /\ (!(0 <= K:314) \/ mid_x:317 = (x:101 + K:314))
           /\ (!(0 <= K:314) \/ mid___cost:318 = (__cost:105 + K:314))
           /\ ((K:314 = 0 /\ y:102 = mid_y:316 /\ x:101 = mid_x:317
                  /\ __cost:105 = mid___cost:318)
                 \/ (1 <= K:314 /\ 0 <= (-1 + -x:101 + n:104) /\ 0 <= y:102
                       /\ 0 <= __cost:105 /\ 0 <= x:101
                       /\ 0 <= (-1 + mid_y:316) /\ 0 <= (-1 + mid_x:317)
                       /\ 0 <= (-1 + mid___cost:318)
                       /\ 0 <= (n:104 + -mid_x:317)))
           /\ (0 = K:314 \/ !((-x:101 + n:104) <= 0))
           /\ (!(0 <= K:315) \/ x':255 = (mid_x:317 + K:315))
           /\ (!(0 <= K:315) \/ y':256 = (mid_y:316 + K:315))
           /\ (!(0 <= K:315) \/ __cost':254 = (mid___cost:318 + K:315))
           /\ ((K:315 = 0 /\ mid_y:316 = y':256 /\ mid_x:317 = x':255
                  /\ mid___cost:318 = __cost':254)
                 \/ (1 <= K:315 /\ 0 <= (-1 + -mid_y:316 + m:103)
                       /\ 0 <= (mid_x:317 + -n:104) /\ 0 <= mid_x:317
                       /\ 0 <= mid___cost:318 /\ 0 <= mid_y:316
                       /\ 0 <= (-1 + -n:104 + x':255) /\ 0 <= (-1 + y':256)
                       /\ 0 <= (-1 + x':255) /\ 0 <= (-1 + __cost':254)
                       /\ 0 <= (m:103 + -y':256)))
           /\ (0 = K:315 \/ (-mid_x:317 + n:104) <= 0)
           /\ (K:314 + K:315) = K:303 /\ 0 <= K:303)}
}
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:21
       m := 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 (((0 < n:4 /\ n:4 = phi_tmp___1:23)
              \/ (n:4 <= 0 /\ 0 = phi_tmp___1:23))
             /\ ((0 < m:5 /\ m:5 = phi_tmp___2:31)
                   \/ (m: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(21)
  )
  ,
  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=21: 
Weight(Base relation: 
  {__cost := __cost':326
   x := x':324
   y := y':325
   n := param0:80
   m := param1:83
   return := havoc:338
   return@pos := type_err:339
   return@width := type_err:340
   when ((!(0 <= K:319) \/ mid_y:320 = K:319)
           /\ (!(0 <= K:319) \/ mid_x:321 = K:319)
           /\ (!(0 <= K:319) \/ mid___cost:322 = (__cost:105 + K:319))
           /\ ((K:319 = 0 /\ 0 = mid_y:320 /\ 0 = mid_x:321
                  /\ __cost:105 = mid___cost:322)
                 \/ (1 <= K:319 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                       /\ 0 <= (-1 + mid_y:320) /\ 0 <= (-1 + mid_x:321)
                       /\ 0 <= (-1 + mid___cost:322)
                       /\ 0 <= (param0:80 + -mid_x:321)))
           /\ (0 = K:319 \/ -param0:80 < 0)
           /\ (!(0 <= K:323) \/ x':324 = (mid_x:321 + K:323))
           /\ (!(0 <= K:323) \/ y':325 = (mid_y:320 + K:323))
           /\ (!(0 <= K:323) \/ __cost':326 = (mid___cost:322 + K:323))
           /\ ((K:323 = 0 /\ mid_y:320 = y':325 /\ mid_x:321 = x':324
                  /\ mid___cost:322 = __cost':326)
                 \/ (1 <= K:323 /\ 0 <= (-1 + -mid_y:320 + param1:83)
                       /\ 0 <= (mid_x:321 + -param0:80) /\ 0 <= mid_x:321
                       /\ 0 <= mid___cost:322 /\ 0 <= mid_y:320
                       /\ 0 <= (-1 + -param0:80 + x':324)
                       /\ 0 <= (-1 + y':325) /\ 0 <= (-1 + x':324)
                       /\ 0 <= (-1 + __cost':326)
                       /\ 0 <= (param1:83 + -y':325)))
           /\ (0 = K:323 \/ !((mid_x:321 + -param0:80) < 0))
           /\ (K:319 + K:323) = K:327
           /\ (!(0 <= K:328) \/ mid___cost:329 = (__cost:105 + K:328))
           /\ (!(0 <= K:328) \/ mid_y:330 = K:328)
           /\ (!(0 <= K:328) \/ mid_x:331 = K:328)
           /\ ((K:328 = 0 /\ 0 = mid_y:330 /\ 0 = mid_x:331
                  /\ __cost:105 = mid___cost:329)
                 \/ (1 <= K:328 /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:105
                       /\ 0 <= (-mid_y:330 + param1:83)
                       /\ 0 <= (-1 + mid_x:331) /\ 0 <= (-1 + mid___cost:329)
                       /\ 0 <= (-1 + mid_y:330)))
           /\ (0 = K:328 \/ -param1:83 < 0)
           /\ (!(0 <= K:332) \/ x':324 = (mid_x:331 + K:332))
           /\ (!(0 <= K:332) \/ __cost':326 = (mid___cost:329 + K:332))
           /\ (!(0 <= K:332) \/ y':325 = (mid_y:330 + K:332))
           /\ ((K:332 = 0 /\ mid_y:330 = y':325 /\ mid_x:331 = x':324
                  /\ mid___cost:329 = __cost':326)
                 \/ (1 <= K:332 /\ 0 <= (-1 + -mid_x:331 + param0:80)
                       /\ 0 <= (mid_y:330 + -param1:83) /\ 0 <= mid_y:330
                       /\ 0 <= mid___cost:329 /\ 0 <= mid_x:331
                       /\ 0 <= (-1 + -param1:83 + y':325)
                       /\ 0 <= (-1 + y':325) /\ 0 <= (-1 + x':324)
                       /\ 0 <= (-1 + __cost':326)
                       /\ 0 <= (param0:80 + -x':324)))
           /\ (0 = K:332 \/ !((mid_y:330 + -param1:83) < 0))
           /\ (K:328 + K:332) = K:327 /\ (!(0 <= K:333) \/ mid_y:334 = K:333)
           /\ (!(0 <= K:333) \/ mid_x:335 = K:333)
           /\ (!(0 <= K:333) \/ mid___cost:336 = (__cost:105 + K:333))
           /\ ((K:333 = 0 /\ 0 = mid_y:334 /\ 0 = mid_x:335
                  /\ __cost:105 = mid___cost:336)
                 \/ (1 <= K:333 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                       /\ 0 <= (-1 + mid_y:334) /\ 0 <= (-1 + mid_x:335)
                       /\ 0 <= (-1 + mid___cost:336)
                       /\ 0 <= (param0:80 + -mid_x:335)))
           /\ (0 = K:333 \/ !(param0:80 <= 0))
           /\ (!(0 <= K:337) \/ x':324 = (mid_x:335 + K:337))
           /\ (!(0 <= K:337) \/ y':325 = (mid_y:334 + K:337))
           /\ (!(0 <= K:337) \/ __cost':326 = (mid___cost:336 + K:337))
           /\ ((K:337 = 0 /\ mid_y:334 = y':325 /\ mid_x:335 = x':324
                  /\ mid___cost:336 = __cost':326)
                 \/ (1 <= K:337 /\ 0 <= (-1 + -mid_y:334 + param1:83)
                       /\ 0 <= (mid_x:335 + -param0:80) /\ 0 <= mid_x:335
                       /\ 0 <= mid___cost:336 /\ 0 <= mid_y:334
                       /\ 0 <= (-1 + -param0:80 + x':324)
                       /\ 0 <= (-1 + y':325) /\ 0 <= (-1 + x':324)
                       /\ 0 <= (-1 + __cost':326)
                       /\ 0 <= (param1:83 + -y':325)))
           /\ (0 = K:337 \/ (-mid_x:335 + param0:80) <= 0)
           /\ (K:333 + K:337) = K:327 /\ 0 <= K:327 /\ 0 <= y':325
           /\ 0 <= x':324 /\ param0:80 <= x':324 /\ param1:83 <= y':325)})



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:21
         m := 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 (((0 < n:4 /\ n:4 = phi_tmp___1:23)
                \/ (n:4 <= 0 /\ 0 = phi_tmp___1:23))
               /\ ((0 < m:5 /\ m:5 = phi_tmp___2:31)
                     \/ (m: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(21)
    )
    ,
    Weight(Base relation: 
      {return := havoc:63
       return@pos := type_err:66
       return@width := type_err:67}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':326
   return := havoc:338
   return@pos := type_err:339
   return@width := type_err:340
   when ((!(0 <= K:319) \/ mid_y:320 = K:319)
           /\ (!(0 <= K:319) \/ mid_x:321 = K:319)
           /\ (!(0 <= K:319) \/ mid___cost:322 = (__cost:105 + K:319))
           /\ ((K:319 = 0 /\ 0 = mid_y:320 /\ 0 = mid_x:321
                  /\ __cost:105 = mid___cost:322)
                 \/ (1 <= K:319 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                       /\ 0 <= (-1 + mid_y:320) /\ 0 <= (-1 + mid_x:321)
                       /\ 0 <= (-1 + mid___cost:322)
                       /\ 0 <= (param0:80 + -mid_x:321)))
           /\ (0 = K:319 \/ -param0:80 < 0)
           /\ (!(0 <= K:323) \/ x':324 = (mid_x:321 + K:323))
           /\ (!(0 <= K:323) \/ y':325 = (mid_y:320 + K:323))
           /\ (!(0 <= K:323) \/ __cost':326 = (mid___cost:322 + K:323))
           /\ ((K:323 = 0 /\ mid_y:320 = y':325 /\ mid_x:321 = x':324
                  /\ mid___cost:322 = __cost':326)
                 \/ (1 <= K:323 /\ 0 <= (-1 + -mid_y:320 + param1:83)
                       /\ 0 <= (mid_x:321 + -param0:80) /\ 0 <= mid_x:321
                       /\ 0 <= mid___cost:322 /\ 0 <= mid_y:320
                       /\ 0 <= (-1 + -param0:80 + x':324)
                       /\ 0 <= (-1 + y':325) /\ 0 <= (-1 + x':324)
                       /\ 0 <= (-1 + __cost':326)
                       /\ 0 <= (param1:83 + -y':325)))
           /\ (0 = K:323 \/ !((mid_x:321 + -param0:80) < 0))
           /\ (K:319 + K:323) = K:327
           /\ (!(0 <= K:328) \/ mid___cost:329 = (__cost:105 + K:328))
           /\ (!(0 <= K:328) \/ mid_y:330 = K:328)
           /\ (!(0 <= K:328) \/ mid_x:331 = K:328)
           /\ ((K:328 = 0 /\ 0 = mid_y:330 /\ 0 = mid_x:331
                  /\ __cost:105 = mid___cost:329)
                 \/ (1 <= K:328 /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:105
                       /\ 0 <= (-mid_y:330 + param1:83)
                       /\ 0 <= (-1 + mid_x:331) /\ 0 <= (-1 + mid___cost:329)
                       /\ 0 <= (-1 + mid_y:330)))
           /\ (0 = K:328 \/ -param1:83 < 0)
           /\ (!(0 <= K:332) \/ x':324 = (mid_x:331 + K:332))
           /\ (!(0 <= K:332) \/ __cost':326 = (mid___cost:329 + K:332))
           /\ (!(0 <= K:332) \/ y':325 = (mid_y:330 + K:332))
           /\ ((K:332 = 0 /\ mid_y:330 = y':325 /\ mid_x:331 = x':324
                  /\ mid___cost:329 = __cost':326)
                 \/ (1 <= K:332 /\ 0 <= (-1 + -mid_x:331 + param0:80)
                       /\ 0 <= (mid_y:330 + -param1:83) /\ 0 <= mid_y:330
                       /\ 0 <= mid___cost:329 /\ 0 <= mid_x:331
                       /\ 0 <= (-1 + -param1:83 + y':325)
                       /\ 0 <= (-1 + y':325) /\ 0 <= (-1 + x':324)
                       /\ 0 <= (-1 + __cost':326)
                       /\ 0 <= (param0:80 + -x':324)))
           /\ (0 = K:332 \/ !((mid_y:330 + -param1:83) < 0))
           /\ (K:328 + K:332) = K:327 /\ (!(0 <= K:333) \/ mid_y:334 = K:333)
           /\ (!(0 <= K:333) \/ mid_x:335 = K:333)
           /\ (!(0 <= K:333) \/ mid___cost:336 = (__cost:105 + K:333))
           /\ ((K:333 = 0 /\ 0 = mid_y:334 /\ 0 = mid_x:335
                  /\ __cost:105 = mid___cost:336)
                 \/ (1 <= K:333 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                       /\ 0 <= (-1 + mid_y:334) /\ 0 <= (-1 + mid_x:335)
                       /\ 0 <= (-1 + mid___cost:336)
                       /\ 0 <= (param0:80 + -mid_x:335)))
           /\ (0 = K:333 \/ !(param0:80 <= 0))
           /\ (!(0 <= K:337) \/ x':324 = (mid_x:335 + K:337))
           /\ (!(0 <= K:337) \/ y':325 = (mid_y:334 + K:337))
           /\ (!(0 <= K:337) \/ __cost':326 = (mid___cost:336 + K:337))
           /\ ((K:337 = 0 /\ mid_y:334 = y':325 /\ mid_x:335 = x':324
                  /\ mid___cost:336 = __cost':326)
                 \/ (1 <= K:337 /\ 0 <= (-1 + -mid_y:334 + param1:83)
                       /\ 0 <= (mid_x:335 + -param0:80) /\ 0 <= mid_x:335
                       /\ 0 <= mid___cost:336 /\ 0 <= mid_y:334
                       /\ 0 <= (-1 + -param0:80 + x':324)
                       /\ 0 <= (-1 + y':325) /\ 0 <= (-1 + x':324)
                       /\ 0 <= (-1 + __cost':326)
                       /\ 0 <= (param1:83 + -y':325)))
           /\ (0 = K:337 \/ (-mid_x:335 + param0:80) <= 0)
           /\ (K:333 + K:337) = K:327 /\ 0 <= K:327 /\ 0 <= y':325
           /\ 0 <= x':324 /\ param0:80 <= x':324 /\ param1:83 <= y':325)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':373
   return := 0
   param0 := havoc:21
   param1 := havoc:22
   return@pos := type_err:394
   param0@pos := type_err:387
   param1@pos := type_err:388
   return@width := type_err:395
   param0@width := type_err:390
   param1@width := type_err:391
   when ((!(0 <= K:366) \/ mid_y:367 = K:366)
           /\ (!(0 <= K:366) \/ mid_x:368 = K:366)
           /\ (!(0 <= K:366) \/ mid___cost:369 = K:366)
           /\ ((K:366 = 0 /\ 0 = mid_y:367 /\ 0 = mid_x:368
                  /\ 0 = mid___cost:369)
                 \/ (1 <= K:366 /\ 0 <= (-1 + havoc:21)
                       /\ 0 <= (-1 + mid_y:367) /\ 0 <= (-1 + mid_x:368)
                       /\ 0 <= (-1 + mid___cost:369)
                       /\ 0 <= (havoc:21 + -mid_x:368)))
           /\ (0 = K:366 \/ -havoc:21 < 0)
           /\ (!(0 <= K:370) \/ x':371 = (mid_x:368 + K:370))
           /\ (!(0 <= K:370) \/ y':372 = (mid_y:367 + K:370))
           /\ (!(0 <= K:370) \/ __cost':373 = (mid___cost:369 + K:370))
           /\ ((K:370 = 0 /\ mid_y:367 = y':372 /\ mid_x:368 = x':371
                  /\ mid___cost:369 = __cost':373)
                 \/ (1 <= K:370 /\ 0 <= (-1 + -mid_y:367 + havoc:22)
                       /\ 0 <= (mid_x:368 + -havoc:21) /\ 0 <= mid_x:368
                       /\ 0 <= mid___cost:369 /\ 0 <= mid_y:367
                       /\ 0 <= (-1 + -havoc:21 + x':371)
                       /\ 0 <= (-1 + y':372) /\ 0 <= (-1 + x':371)
                       /\ 0 <= (-1 + __cost':373)
                       /\ 0 <= (havoc:22 + -y':372)))
           /\ (0 = K:370 \/ !((mid_x:368 + -havoc:21) < 0))
           /\ (K:366 + K:370) = K:374
           /\ (!(0 <= K:375) \/ mid___cost:376 = K:375)
           /\ (!(0 <= K:375) \/ mid_y:377 = K:375)
           /\ (!(0 <= K:375) \/ mid_x:378 = K:375)
           /\ ((K:375 = 0 /\ 0 = mid_y:377 /\ 0 = mid_x:378
                  /\ 0 = mid___cost:376)
                 \/ (1 <= K:375 /\ 0 <= (-1 + havoc:22)
                       /\ 0 <= (-mid_y:377 + havoc:22)
                       /\ 0 <= (-1 + mid_x:378) /\ 0 <= (-1 + mid___cost:376)
                       /\ 0 <= (-1 + mid_y:377)))
           /\ (0 = K:375 \/ -havoc:22 < 0)
           /\ (!(0 <= K:379) \/ x':371 = (mid_x:378 + K:379))
           /\ (!(0 <= K:379) \/ __cost':373 = (mid___cost:376 + K:379))
           /\ (!(0 <= K:379) \/ y':372 = (mid_y:377 + K:379))
           /\ ((K:379 = 0 /\ mid_y:377 = y':372 /\ mid_x:378 = x':371
                  /\ mid___cost:376 = __cost':373)
                 \/ (1 <= K:379 /\ 0 <= (-1 + -mid_x:378 + havoc:21)
                       /\ 0 <= (mid_y:377 + -havoc:22) /\ 0 <= mid_y:377
                       /\ 0 <= mid___cost:376 /\ 0 <= mid_x:378
                       /\ 0 <= (-1 + -havoc:22 + y':372)
                       /\ 0 <= (-1 + y':372) /\ 0 <= (-1 + x':371)
                       /\ 0 <= (-1 + __cost':373)
                       /\ 0 <= (havoc:21 + -x':371)))
           /\ (0 = K:379 \/ !((mid_y:377 + -havoc:22) < 0))
           /\ (K:375 + K:379) = K:374 /\ (!(0 <= K:380) \/ mid_y:381 = K:380)
           /\ (!(0 <= K:380) \/ mid_x:382 = K:380)
           /\ (!(0 <= K:380) \/ mid___cost:383 = K:380)
           /\ ((K:380 = 0 /\ 0 = mid_y:381 /\ 0 = mid_x:382
                  /\ 0 = mid___cost:383)
                 \/ (1 <= K:380 /\ 0 <= (-1 + havoc:21)
                       /\ 0 <= (-1 + mid_y:381) /\ 0 <= (-1 + mid_x:382)
                       /\ 0 <= (-1 + mid___cost:383)
                       /\ 0 <= (havoc:21 + -mid_x:382)))
           /\ (0 = K:380 \/ !(havoc:21 <= 0))
           /\ (!(0 <= K:384) \/ x':371 = (mid_x:382 + K:384))
           /\ (!(0 <= K:384) \/ y':372 = (mid_y:381 + K:384))
           /\ (!(0 <= K:384) \/ __cost':373 = (mid___cost:383 + K:384))
           /\ ((K:384 = 0 /\ mid_y:381 = y':372 /\ mid_x:382 = x':371
                  /\ mid___cost:383 = __cost':373)
                 \/ (1 <= K:384 /\ 0 <= (-1 + -mid_y:381 + havoc:22)
                       /\ 0 <= (mid_x:382 + -havoc:21) /\ 0 <= mid_x:382
                       /\ 0 <= mid___cost:383 /\ 0 <= mid_y:381
                       /\ 0 <= (-1 + -havoc:21 + x':371)
                       /\ 0 <= (-1 + y':372) /\ 0 <= (-1 + x':371)
                       /\ 0 <= (-1 + __cost':373)
                       /\ 0 <= (havoc:22 + -y':372)))
           /\ (0 = K:384 \/ (-mid_x:382 + havoc:21) <= 0)
           /\ (K:380 + K:384) = K:374 /\ 0 <= K:374 /\ 0 <= y':372
           /\ 0 <= x':371 /\ havoc:21 <= x':371 /\ havoc:22 <= y':372
           /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:392)
                 \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:392))
           /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:393)
                 \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:393)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':403
   return := havoc:418
   param0 := param0:80
   param1 := param1:83
   return@pos := type_err:419
   param0@pos := type_err:88
   param1@pos := type_err:89
   return@width := type_err:420
   param0@width := type_err:90
   param1@width := type_err:91
   when ((!(0 <= K:396) \/ mid_y:397 = K:396)
           /\ (!(0 <= K:396) \/ mid_x:398 = K:396)
           /\ (!(0 <= K:396) \/ mid___cost:399 = (__cost:105 + K:396))
           /\ ((K:396 = 0 /\ 0 = mid_y:397 /\ 0 = mid_x:398
                  /\ __cost:105 = mid___cost:399)
                 \/ (1 <= K:396 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                       /\ 0 <= (-1 + mid_y:397) /\ 0 <= (-1 + mid_x:398)
                       /\ 0 <= (-1 + mid___cost:399)
                       /\ 0 <= (param0:80 + -mid_x:398)))
           /\ (0 = K:396 \/ -param0:80 < 0)
           /\ (!(0 <= K:400) \/ x':401 = (mid_x:398 + K:400))
           /\ (!(0 <= K:400) \/ y':402 = (mid_y:397 + K:400))
           /\ (!(0 <= K:400) \/ __cost':403 = (mid___cost:399 + K:400))
           /\ ((K:400 = 0 /\ mid_y:397 = y':402 /\ mid_x:398 = x':401
                  /\ mid___cost:399 = __cost':403)
                 \/ (1 <= K:400 /\ 0 <= (-1 + -mid_y:397 + param1:83)
                       /\ 0 <= (mid_x:398 + -param0:80) /\ 0 <= mid_x:398
                       /\ 0 <= mid___cost:399 /\ 0 <= mid_y:397
                       /\ 0 <= (-1 + -param0:80 + x':401)
                       /\ 0 <= (-1 + y':402) /\ 0 <= (-1 + x':401)
                       /\ 0 <= (-1 + __cost':403)
                       /\ 0 <= (param1:83 + -y':402)))
           /\ (0 = K:400 \/ !((mid_x:398 + -param0:80) < 0))
           /\ (K:396 + K:400) = K:404
           /\ (!(0 <= K:405) \/ mid___cost:406 = (__cost:105 + K:405))
           /\ (!(0 <= K:405) \/ mid_y:407 = K:405)
           /\ (!(0 <= K:405) \/ mid_x:408 = K:405)
           /\ ((K:405 = 0 /\ 0 = mid_y:407 /\ 0 = mid_x:408
                  /\ __cost:105 = mid___cost:406)
                 \/ (1 <= K:405 /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:105
                       /\ 0 <= (-mid_y:407 + param1:83)
                       /\ 0 <= (-1 + mid_x:408) /\ 0 <= (-1 + mid___cost:406)
                       /\ 0 <= (-1 + mid_y:407)))
           /\ (0 = K:405 \/ -param1:83 < 0)
           /\ (!(0 <= K:409) \/ x':401 = (mid_x:408 + K:409))
           /\ (!(0 <= K:409) \/ __cost':403 = (mid___cost:406 + K:409))
           /\ (!(0 <= K:409) \/ y':402 = (mid_y:407 + K:409))
           /\ ((K:409 = 0 /\ mid_y:407 = y':402 /\ mid_x:408 = x':401
                  /\ mid___cost:406 = __cost':403)
                 \/ (1 <= K:409 /\ 0 <= (-1 + -mid_x:408 + param0:80)
                       /\ 0 <= (mid_y:407 + -param1:83) /\ 0 <= mid_y:407
                       /\ 0 <= mid___cost:406 /\ 0 <= mid_x:408
                       /\ 0 <= (-1 + -param1:83 + y':402)
                       /\ 0 <= (-1 + y':402) /\ 0 <= (-1 + x':401)
                       /\ 0 <= (-1 + __cost':403)
                       /\ 0 <= (param0:80 + -x':401)))
           /\ (0 = K:409 \/ !((mid_y:407 + -param1:83) < 0))
           /\ (K:405 + K:409) = K:404 /\ (!(0 <= K:410) \/ mid_y:411 = K:410)
           /\ (!(0 <= K:410) \/ mid_x:412 = K:410)
           /\ (!(0 <= K:410) \/ mid___cost:413 = (__cost:105 + K:410))
           /\ ((K:410 = 0 /\ 0 = mid_y:411 /\ 0 = mid_x:412
                  /\ __cost:105 = mid___cost:413)
                 \/ (1 <= K:410 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                       /\ 0 <= (-1 + mid_y:411) /\ 0 <= (-1 + mid_x:412)
                       /\ 0 <= (-1 + mid___cost:413)
                       /\ 0 <= (param0:80 + -mid_x:412)))
           /\ (0 = K:410 \/ !(param0:80 <= 0))
           /\ (!(0 <= K:414) \/ x':401 = (mid_x:412 + K:414))
           /\ (!(0 <= K:414) \/ y':402 = (mid_y:411 + K:414))
           /\ (!(0 <= K:414) \/ __cost':403 = (mid___cost:413 + K:414))
           /\ ((K:414 = 0 /\ mid_y:411 = y':402 /\ mid_x:412 = x':401
                  /\ mid___cost:413 = __cost':403)
                 \/ (1 <= K:414 /\ 0 <= (-1 + -mid_y:411 + param1:83)
                       /\ 0 <= (mid_x:412 + -param0:80) /\ 0 <= mid_x:412
                       /\ 0 <= mid___cost:413 /\ 0 <= mid_y:411
                       /\ 0 <= (-1 + -param0:80 + x':401)
                       /\ 0 <= (-1 + y':402) /\ 0 <= (-1 + x':401)
                       /\ 0 <= (-1 + __cost':403)
                       /\ 0 <= (param1:83 + -y':402)))
           /\ (0 = K:414 \/ (-mid_x:412 + param0:80) <= 0)
           /\ (K:410 + K:414) = K:404 /\ 0 <= K:404 /\ 0 <= y':402
           /\ 0 <= x':401 /\ param0:80 <= x':401 /\ param1:83 <= y':402)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=21: 
Weight(Base relation: 
  {__cost := __cost':326
   return := havoc:338
   return@pos := type_err:339
   return@width := type_err:340
   when ((!(0 <= K:319) \/ mid_y:320 = K:319)
           /\ (!(0 <= K:319) \/ mid_x:321 = K:319)
           /\ (!(0 <= K:319) \/ mid___cost:322 = (__cost:105 + K:319))
           /\ ((K:319 = 0 /\ 0 = mid_y:320 /\ 0 = mid_x:321
                  /\ __cost:105 = mid___cost:322)
                 \/ (1 <= K:319 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                       /\ 0 <= (-1 + mid_y:320) /\ 0 <= (-1 + mid_x:321)
                       /\ 0 <= (-1 + mid___cost:322)
                       /\ 0 <= (param0:80 + -mid_x:321)))
           /\ (0 = K:319 \/ -param0:80 < 0)
           /\ (!(0 <= K:323) \/ x':324 = (mid_x:321 + K:323))
           /\ (!(0 <= K:323) \/ y':325 = (mid_y:320 + K:323))
           /\ (!(0 <= K:323) \/ __cost':326 = (mid___cost:322 + K:323))
           /\ ((K:323 = 0 /\ mid_y:320 = y':325 /\ mid_x:321 = x':324
                  /\ mid___cost:322 = __cost':326)
                 \/ (1 <= K:323 /\ 0 <= (-1 + -mid_y:320 + param1:83)
                       /\ 0 <= (mid_x:321 + -param0:80) /\ 0 <= mid_x:321
                       /\ 0 <= mid___cost:322 /\ 0 <= mid_y:320
                       /\ 0 <= (-1 + -param0:80 + x':324)
                       /\ 0 <= (-1 + y':325) /\ 0 <= (-1 + x':324)
                       /\ 0 <= (-1 + __cost':326)
                       /\ 0 <= (param1:83 + -y':325)))
           /\ (0 = K:323 \/ !((mid_x:321 + -param0:80) < 0))
           /\ (K:319 + K:323) = K:327
           /\ (!(0 <= K:328) \/ mid___cost:329 = (__cost:105 + K:328))
           /\ (!(0 <= K:328) \/ mid_y:330 = K:328)
           /\ (!(0 <= K:328) \/ mid_x:331 = K:328)
           /\ ((K:328 = 0 /\ 0 = mid_y:330 /\ 0 = mid_x:331
                  /\ __cost:105 = mid___cost:329)
                 \/ (1 <= K:328 /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:105
                       /\ 0 <= (-mid_y:330 + param1:83)
                       /\ 0 <= (-1 + mid_x:331) /\ 0 <= (-1 + mid___cost:329)
                       /\ 0 <= (-1 + mid_y:330)))
           /\ (0 = K:328 \/ -param1:83 < 0)
           /\ (!(0 <= K:332) \/ x':324 = (mid_x:331 + K:332))
           /\ (!(0 <= K:332) \/ __cost':326 = (mid___cost:329 + K:332))
           /\ (!(0 <= K:332) \/ y':325 = (mid_y:330 + K:332))
           /\ ((K:332 = 0 /\ mid_y:330 = y':325 /\ mid_x:331 = x':324
                  /\ mid___cost:329 = __cost':326)
                 \/ (1 <= K:332 /\ 0 <= (-1 + -mid_x:331 + param0:80)
                       /\ 0 <= (mid_y:330 + -param1:83) /\ 0 <= mid_y:330
                       /\ 0 <= mid___cost:329 /\ 0 <= mid_x:331
                       /\ 0 <= (-1 + -param1:83 + y':325)
                       /\ 0 <= (-1 + y':325) /\ 0 <= (-1 + x':324)
                       /\ 0 <= (-1 + __cost':326)
                       /\ 0 <= (param0:80 + -x':324)))
           /\ (0 = K:332 \/ !((mid_y:330 + -param1:83) < 0))
           /\ (K:328 + K:332) = K:327 /\ (!(0 <= K:333) \/ mid_y:334 = K:333)
           /\ (!(0 <= K:333) \/ mid_x:335 = K:333)
           /\ (!(0 <= K:333) \/ mid___cost:336 = (__cost:105 + K:333))
           /\ ((K:333 = 0 /\ 0 = mid_y:334 /\ 0 = mid_x:335
                  /\ __cost:105 = mid___cost:336)
                 \/ (1 <= K:333 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                       /\ 0 <= (-1 + mid_y:334) /\ 0 <= (-1 + mid_x:335)
                       /\ 0 <= (-1 + mid___cost:336)
                       /\ 0 <= (param0:80 + -mid_x:335)))
           /\ (0 = K:333 \/ !(param0:80 <= 0))
           /\ (!(0 <= K:337) \/ x':324 = (mid_x:335 + K:337))
           /\ (!(0 <= K:337) \/ y':325 = (mid_y:334 + K:337))
           /\ (!(0 <= K:337) \/ __cost':326 = (mid___cost:336 + K:337))
           /\ ((K:337 = 0 /\ mid_y:334 = y':325 /\ mid_x:335 = x':324
                  /\ mid___cost:336 = __cost':326)
                 \/ (1 <= K:337 /\ 0 <= (-1 + -mid_y:334 + param1:83)
                       /\ 0 <= (mid_x:335 + -param0:80) /\ 0 <= mid_x:335
                       /\ 0 <= mid___cost:336 /\ 0 <= mid_y:334
                       /\ 0 <= (-1 + -param0:80 + x':324)
                       /\ 0 <= (-1 + y':325) /\ 0 <= (-1 + x':324)
                       /\ 0 <= (-1 + __cost':326)
                       /\ 0 <= (param1:83 + -y':325)))
           /\ (0 = K:337 \/ (-mid_x:335 + param0:80) <= 0)
           /\ (K:333 + K:337) = K:327 /\ 0 <= K:327 /\ 0 <= y':325
           /\ 0 <= x':324 /\ param0:80 <= x':324 /\ param1:83 <= y':325)})


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':373
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:394
 param0@pos := type_err:387
 param1@pos := type_err:388
 return@width := type_err:395
 param0@width := type_err:390
 param1@width := type_err:391
 when ((!(0 <= K:366) \/ mid_y:367 = K:366)
         /\ (!(0 <= K:366) \/ mid_x:368 = K:366)
         /\ (!(0 <= K:366) \/ mid___cost:369 = K:366)
         /\ ((K:366 = 0 /\ 0 = mid_y:367 /\ 0 = mid_x:368
                /\ 0 = mid___cost:369)
               \/ (1 <= K:366 /\ 0 <= (-1 + havoc:21)
                     /\ 0 <= (-1 + mid_y:367) /\ 0 <= (-1 + mid_x:368)
                     /\ 0 <= (-1 + mid___cost:369)
                     /\ 0 <= (havoc:21 + -mid_x:368)))
         /\ (0 = K:366 \/ -havoc:21 < 0)
         /\ (!(0 <= K:370) \/ x':371 = (mid_x:368 + K:370))
         /\ (!(0 <= K:370) \/ y':372 = (mid_y:367 + K:370))
         /\ (!(0 <= K:370) \/ __cost':373 = (mid___cost:369 + K:370))
         /\ ((K:370 = 0 /\ mid_y:367 = y':372 /\ mid_x:368 = x':371
                /\ mid___cost:369 = __cost':373)
               \/ (1 <= K:370 /\ 0 <= (-1 + -mid_y:367 + havoc:22)
                     /\ 0 <= (mid_x:368 + -havoc:21) /\ 0 <= mid_x:368
                     /\ 0 <= mid___cost:369 /\ 0 <= mid_y:367
                     /\ 0 <= (-1 + -havoc:21 + x':371) /\ 0 <= (-1 + y':372)
                     /\ 0 <= (-1 + x':371) /\ 0 <= (-1 + __cost':373)
                     /\ 0 <= (havoc:22 + -y':372)))
         /\ (0 = K:370 \/ !((mid_x:368 + -havoc:21) < 0))
         /\ (K:366 + K:370) = K:374
         /\ (!(0 <= K:375) \/ mid___cost:376 = K:375)
         /\ (!(0 <= K:375) \/ mid_y:377 = K:375)
         /\ (!(0 <= K:375) \/ mid_x:378 = K:375)
         /\ ((K:375 = 0 /\ 0 = mid_y:377 /\ 0 = mid_x:378
                /\ 0 = mid___cost:376)
               \/ (1 <= K:375 /\ 0 <= (-1 + havoc:22)
                     /\ 0 <= (-mid_y:377 + havoc:22) /\ 0 <= (-1 + mid_x:378)
                     /\ 0 <= (-1 + mid___cost:376) /\ 0 <= (-1 + mid_y:377)))
         /\ (0 = K:375 \/ -havoc:22 < 0)
         /\ (!(0 <= K:379) \/ x':371 = (mid_x:378 + K:379))
         /\ (!(0 <= K:379) \/ __cost':373 = (mid___cost:376 + K:379))
         /\ (!(0 <= K:379) \/ y':372 = (mid_y:377 + K:379))
         /\ ((K:379 = 0 /\ mid_y:377 = y':372 /\ mid_x:378 = x':371
                /\ mid___cost:376 = __cost':373)
               \/ (1 <= K:379 /\ 0 <= (-1 + -mid_x:378 + havoc:21)
                     /\ 0 <= (mid_y:377 + -havoc:22) /\ 0 <= mid_y:377
                     /\ 0 <= mid___cost:376 /\ 0 <= mid_x:378
                     /\ 0 <= (-1 + -havoc:22 + y':372) /\ 0 <= (-1 + y':372)
                     /\ 0 <= (-1 + x':371) /\ 0 <= (-1 + __cost':373)
                     /\ 0 <= (havoc:21 + -x':371)))
         /\ (0 = K:379 \/ !((mid_y:377 + -havoc:22) < 0))
         /\ (K:375 + K:379) = K:374 /\ (!(0 <= K:380) \/ mid_y:381 = K:380)
         /\ (!(0 <= K:380) \/ mid_x:382 = K:380)
         /\ (!(0 <= K:380) \/ mid___cost:383 = K:380)
         /\ ((K:380 = 0 /\ 0 = mid_y:381 /\ 0 = mid_x:382
                /\ 0 = mid___cost:383)
               \/ (1 <= K:380 /\ 0 <= (-1 + havoc:21)
                     /\ 0 <= (-1 + mid_y:381) /\ 0 <= (-1 + mid_x:382)
                     /\ 0 <= (-1 + mid___cost:383)
                     /\ 0 <= (havoc:21 + -mid_x:382)))
         /\ (0 = K:380 \/ !(havoc:21 <= 0))
         /\ (!(0 <= K:384) \/ x':371 = (mid_x:382 + K:384))
         /\ (!(0 <= K:384) \/ y':372 = (mid_y:381 + K:384))
         /\ (!(0 <= K:384) \/ __cost':373 = (mid___cost:383 + K:384))
         /\ ((K:384 = 0 /\ mid_y:381 = y':372 /\ mid_x:382 = x':371
                /\ mid___cost:383 = __cost':373)
               \/ (1 <= K:384 /\ 0 <= (-1 + -mid_y:381 + havoc:22)
                     /\ 0 <= (mid_x:382 + -havoc:21) /\ 0 <= mid_x:382
                     /\ 0 <= mid___cost:383 /\ 0 <= mid_y:381
                     /\ 0 <= (-1 + -havoc:21 + x':371) /\ 0 <= (-1 + y':372)
                     /\ 0 <= (-1 + x':371) /\ 0 <= (-1 + __cost':373)
                     /\ 0 <= (havoc:22 + -y':372)))
         /\ (0 = K:384 \/ (-mid_x:382 + havoc:21) <= 0)
         /\ (K:380 + K:384) = K:374 /\ 0 <= K:374 /\ 0 <= y':372
         /\ 0 <= x':371 /\ havoc:21 <= x':371 /\ havoc:22 <= y':372
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:392)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:392))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:393)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:393)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':403
 return := havoc:418
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:419
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:420
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:396) \/ mid_y:397 = K:396)
         /\ (!(0 <= K:396) \/ mid_x:398 = K:396)
         /\ (!(0 <= K:396) \/ mid___cost:399 = (__cost:105 + K:396))
         /\ ((K:396 = 0 /\ 0 = mid_y:397 /\ 0 = mid_x:398
                /\ __cost:105 = mid___cost:399)
               \/ (1 <= K:396 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                     /\ 0 <= (-1 + mid_y:397) /\ 0 <= (-1 + mid_x:398)
                     /\ 0 <= (-1 + mid___cost:399)
                     /\ 0 <= (param0:80 + -mid_x:398)))
         /\ (0 = K:396 \/ -param0:80 < 0)
         /\ (!(0 <= K:400) \/ x':401 = (mid_x:398 + K:400))
         /\ (!(0 <= K:400) \/ y':402 = (mid_y:397 + K:400))
         /\ (!(0 <= K:400) \/ __cost':403 = (mid___cost:399 + K:400))
         /\ ((K:400 = 0 /\ mid_y:397 = y':402 /\ mid_x:398 = x':401
                /\ mid___cost:399 = __cost':403)
               \/ (1 <= K:400 /\ 0 <= (-1 + -mid_y:397 + param1:83)
                     /\ 0 <= (mid_x:398 + -param0:80) /\ 0 <= mid_x:398
                     /\ 0 <= mid___cost:399 /\ 0 <= mid_y:397
                     /\ 0 <= (-1 + -param0:80 + x':401) /\ 0 <= (-1 + y':402)
                     /\ 0 <= (-1 + x':401) /\ 0 <= (-1 + __cost':403)
                     /\ 0 <= (param1:83 + -y':402)))
         /\ (0 = K:400 \/ !((mid_x:398 + -param0:80) < 0))
         /\ (K:396 + K:400) = K:404
         /\ (!(0 <= K:405) \/ mid___cost:406 = (__cost:105 + K:405))
         /\ (!(0 <= K:405) \/ mid_y:407 = K:405)
         /\ (!(0 <= K:405) \/ mid_x:408 = K:405)
         /\ ((K:405 = 0 /\ 0 = mid_y:407 /\ 0 = mid_x:408
                /\ __cost:105 = mid___cost:406)
               \/ (1 <= K:405 /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:105
                     /\ 0 <= (-mid_y:407 + param1:83)
                     /\ 0 <= (-1 + mid_x:408) /\ 0 <= (-1 + mid___cost:406)
                     /\ 0 <= (-1 + mid_y:407)))
         /\ (0 = K:405 \/ -param1:83 < 0)
         /\ (!(0 <= K:409) \/ x':401 = (mid_x:408 + K:409))
         /\ (!(0 <= K:409) \/ __cost':403 = (mid___cost:406 + K:409))
         /\ (!(0 <= K:409) \/ y':402 = (mid_y:407 + K:409))
         /\ ((K:409 = 0 /\ mid_y:407 = y':402 /\ mid_x:408 = x':401
                /\ mid___cost:406 = __cost':403)
               \/ (1 <= K:409 /\ 0 <= (-1 + -mid_x:408 + param0:80)
                     /\ 0 <= (mid_y:407 + -param1:83) /\ 0 <= mid_y:407
                     /\ 0 <= mid___cost:406 /\ 0 <= mid_x:408
                     /\ 0 <= (-1 + -param1:83 + y':402) /\ 0 <= (-1 + y':402)
                     /\ 0 <= (-1 + x':401) /\ 0 <= (-1 + __cost':403)
                     /\ 0 <= (param0:80 + -x':401)))
         /\ (0 = K:409 \/ !((mid_y:407 + -param1:83) < 0))
         /\ (K:405 + K:409) = K:404 /\ (!(0 <= K:410) \/ mid_y:411 = K:410)
         /\ (!(0 <= K:410) \/ mid_x:412 = K:410)
         /\ (!(0 <= K:410) \/ mid___cost:413 = (__cost:105 + K:410))
         /\ ((K:410 = 0 /\ 0 = mid_y:411 /\ 0 = mid_x:412
                /\ __cost:105 = mid___cost:413)
               \/ (1 <= K:410 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                     /\ 0 <= (-1 + mid_y:411) /\ 0 <= (-1 + mid_x:412)
                     /\ 0 <= (-1 + mid___cost:413)
                     /\ 0 <= (param0:80 + -mid_x:412)))
         /\ (0 = K:410 \/ !(param0:80 <= 0))
         /\ (!(0 <= K:414) \/ x':401 = (mid_x:412 + K:414))
         /\ (!(0 <= K:414) \/ y':402 = (mid_y:411 + K:414))
         /\ (!(0 <= K:414) \/ __cost':403 = (mid___cost:413 + K:414))
         /\ ((K:414 = 0 /\ mid_y:411 = y':402 /\ mid_x:412 = x':401
                /\ mid___cost:413 = __cost':403)
               \/ (1 <= K:414 /\ 0 <= (-1 + -mid_y:411 + param1:83)
                     /\ 0 <= (mid_x:412 + -param0:80) /\ 0 <= mid_x:412
                     /\ 0 <= mid___cost:413 /\ 0 <= mid_y:411
                     /\ 0 <= (-1 + -param0:80 + x':401) /\ 0 <= (-1 + y':402)
                     /\ 0 <= (-1 + x':401) /\ 0 <= (-1 + __cost':403)
                     /\ 0 <= (param1:83 + -y':402)))
         /\ (0 = K:414 \/ (-mid_x:412 + param0:80) <= 0)
         /\ (K:410 + K:414) = K:404 /\ 0 <= K:404 /\ 0 <= y':402
         /\ 0 <= x':401 /\ param0:80 <= x':401 /\ param1:83 <= y':402)}

Evaluating variable number 21 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':326
 return := havoc:338
 return@pos := type_err:339
 return@width := type_err:340
 when ((!(0 <= K:319) \/ mid_y:320 = K:319)
         /\ (!(0 <= K:319) \/ mid_x:321 = K:319)
         /\ (!(0 <= K:319) \/ mid___cost:322 = (__cost:105 + K:319))
         /\ ((K:319 = 0 /\ 0 = mid_y:320 /\ 0 = mid_x:321
                /\ __cost:105 = mid___cost:322)
               \/ (1 <= K:319 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                     /\ 0 <= (-1 + mid_y:320) /\ 0 <= (-1 + mid_x:321)
                     /\ 0 <= (-1 + mid___cost:322)
                     /\ 0 <= (param0:80 + -mid_x:321)))
         /\ (0 = K:319 \/ -param0:80 < 0)
         /\ (!(0 <= K:323) \/ x':324 = (mid_x:321 + K:323))
         /\ (!(0 <= K:323) \/ y':325 = (mid_y:320 + K:323))
         /\ (!(0 <= K:323) \/ __cost':326 = (mid___cost:322 + K:323))
         /\ ((K:323 = 0 /\ mid_y:320 = y':325 /\ mid_x:321 = x':324
                /\ mid___cost:322 = __cost':326)
               \/ (1 <= K:323 /\ 0 <= (-1 + -mid_y:320 + param1:83)
                     /\ 0 <= (mid_x:321 + -param0:80) /\ 0 <= mid_x:321
                     /\ 0 <= mid___cost:322 /\ 0 <= mid_y:320
                     /\ 0 <= (-1 + -param0:80 + x':324) /\ 0 <= (-1 + y':325)
                     /\ 0 <= (-1 + x':324) /\ 0 <= (-1 + __cost':326)
                     /\ 0 <= (param1:83 + -y':325)))
         /\ (0 = K:323 \/ !((mid_x:321 + -param0:80) < 0))
         /\ (K:319 + K:323) = K:327
         /\ (!(0 <= K:328) \/ mid___cost:329 = (__cost:105 + K:328))
         /\ (!(0 <= K:328) \/ mid_y:330 = K:328)
         /\ (!(0 <= K:328) \/ mid_x:331 = K:328)
         /\ ((K:328 = 0 /\ 0 = mid_y:330 /\ 0 = mid_x:331
                /\ __cost:105 = mid___cost:329)
               \/ (1 <= K:328 /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:105
                     /\ 0 <= (-mid_y:330 + param1:83)
                     /\ 0 <= (-1 + mid_x:331) /\ 0 <= (-1 + mid___cost:329)
                     /\ 0 <= (-1 + mid_y:330)))
         /\ (0 = K:328 \/ -param1:83 < 0)
         /\ (!(0 <= K:332) \/ x':324 = (mid_x:331 + K:332))
         /\ (!(0 <= K:332) \/ __cost':326 = (mid___cost:329 + K:332))
         /\ (!(0 <= K:332) \/ y':325 = (mid_y:330 + K:332))
         /\ ((K:332 = 0 /\ mid_y:330 = y':325 /\ mid_x:331 = x':324
                /\ mid___cost:329 = __cost':326)
               \/ (1 <= K:332 /\ 0 <= (-1 + -mid_x:331 + param0:80)
                     /\ 0 <= (mid_y:330 + -param1:83) /\ 0 <= mid_y:330
                     /\ 0 <= mid___cost:329 /\ 0 <= mid_x:331
                     /\ 0 <= (-1 + -param1:83 + y':325) /\ 0 <= (-1 + y':325)
                     /\ 0 <= (-1 + x':324) /\ 0 <= (-1 + __cost':326)
                     /\ 0 <= (param0:80 + -x':324)))
         /\ (0 = K:332 \/ !((mid_y:330 + -param1:83) < 0))
         /\ (K:328 + K:332) = K:327 /\ (!(0 <= K:333) \/ mid_y:334 = K:333)
         /\ (!(0 <= K:333) \/ mid_x:335 = K:333)
         /\ (!(0 <= K:333) \/ mid___cost:336 = (__cost:105 + K:333))
         /\ ((K:333 = 0 /\ 0 = mid_y:334 /\ 0 = mid_x:335
                /\ __cost:105 = mid___cost:336)
               \/ (1 <= K:333 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                     /\ 0 <= (-1 + mid_y:334) /\ 0 <= (-1 + mid_x:335)
                     /\ 0 <= (-1 + mid___cost:336)
                     /\ 0 <= (param0:80 + -mid_x:335)))
         /\ (0 = K:333 \/ !(param0:80 <= 0))
         /\ (!(0 <= K:337) \/ x':324 = (mid_x:335 + K:337))
         /\ (!(0 <= K:337) \/ y':325 = (mid_y:334 + K:337))
         /\ (!(0 <= K:337) \/ __cost':326 = (mid___cost:336 + K:337))
         /\ ((K:337 = 0 /\ mid_y:334 = y':325 /\ mid_x:335 = x':324
                /\ mid___cost:336 = __cost':326)
               \/ (1 <= K:337 /\ 0 <= (-1 + -mid_y:334 + param1:83)
                     /\ 0 <= (mid_x:335 + -param0:80) /\ 0 <= mid_x:335
                     /\ 0 <= mid___cost:336 /\ 0 <= mid_y:334
                     /\ 0 <= (-1 + -param0:80 + x':324) /\ 0 <= (-1 + y':325)
                     /\ 0 <= (-1 + x':324) /\ 0 <= (-1 + __cost':326)
                     /\ 0 <= (param1:83 + -y':325)))
         /\ (0 = K:337 \/ (-mid_x:335 + param0:80) <= 0)
         /\ (K:333 + K:337) = K:327 /\ 0 <= K:327 /\ 0 <= y':325
         /\ 0 <= x':324 /\ param0:80 <= x':324 /\ param1:83 <= y':325)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,61)_g1> -> <__pstate, (Unique State Name,55)_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,61)_g1>	Base relation: 
{__cost := 0
 n := havoc:21
 m := 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: 
__done 0x82fa570: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x825e990: 
	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,55)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:21
 m := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:476
 param1@pos := type_err:477
 param0@width := type_err:478
 param1@width := type_err:479}
    ( __pstate , (Unique State Name,61)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:21
 m := 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: 
__done 0x831c410: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x8182460: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
================================================
Procedure Summaries

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

Base relation: 
{__cost := __cost':428
 n := havoc:21
 m := havoc:22
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:449
 param0@pos := type_err:442
 param1@pos := type_err:443
 return@width := type_err:450
 param0@width := type_err:445
 param1@width := type_err:446
 when ((!(0 <= K:421) \/ mid_y:422 = K:421)
         /\ (!(0 <= K:421) \/ mid_x:423 = K:421)
         /\ (!(0 <= K:421) \/ mid___cost:424 = K:421)
         /\ ((K:421 = 0 /\ 0 = mid_y:422 /\ 0 = mid_x:423
                /\ 0 = mid___cost:424)
               \/ (1 <= K:421 /\ 0 <= (-1 + havoc:21)
                     /\ 0 <= (-1 + mid_y:422) /\ 0 <= (-1 + mid_x:423)
                     /\ 0 <= (-1 + mid___cost:424)
                     /\ 0 <= (havoc:21 + -mid_x:423)))
         /\ (0 = K:421 \/ -havoc:21 < 0)
         /\ (!(0 <= K:425) \/ x':426 = (mid_x:423 + K:425))
         /\ (!(0 <= K:425) \/ y':427 = (mid_y:422 + K:425))
         /\ (!(0 <= K:425) \/ __cost':428 = (mid___cost:424 + K:425))
         /\ ((K:425 = 0 /\ mid_y:422 = y':427 /\ mid_x:423 = x':426
                /\ mid___cost:424 = __cost':428)
               \/ (1 <= K:425 /\ 0 <= (-1 + -mid_y:422 + havoc:22)
                     /\ 0 <= (mid_x:423 + -havoc:21) /\ 0 <= mid_x:423
                     /\ 0 <= mid___cost:424 /\ 0 <= mid_y:422
                     /\ 0 <= (-1 + -havoc:21 + x':426) /\ 0 <= (-1 + y':427)
                     /\ 0 <= (-1 + x':426) /\ 0 <= (-1 + __cost':428)
                     /\ 0 <= (havoc:22 + -y':427)))
         /\ (0 = K:425 \/ !((mid_x:423 + -havoc:21) < 0))
         /\ (K:421 + K:425) = K:429
         /\ (!(0 <= K:430) \/ mid___cost:431 = K:430)
         /\ (!(0 <= K:430) \/ mid_y:432 = K:430)
         /\ (!(0 <= K:430) \/ mid_x:433 = K:430)
         /\ ((K:430 = 0 /\ 0 = mid_y:432 /\ 0 = mid_x:433
                /\ 0 = mid___cost:431)
               \/ (1 <= K:430 /\ 0 <= (-1 + havoc:22)
                     /\ 0 <= (-mid_y:432 + havoc:22) /\ 0 <= (-1 + mid_x:433)
                     /\ 0 <= (-1 + mid___cost:431) /\ 0 <= (-1 + mid_y:432)))
         /\ (0 = K:430 \/ -havoc:22 < 0)
         /\ (!(0 <= K:434) \/ x':426 = (mid_x:433 + K:434))
         /\ (!(0 <= K:434) \/ __cost':428 = (mid___cost:431 + K:434))
         /\ (!(0 <= K:434) \/ y':427 = (mid_y:432 + K:434))
         /\ ((K:434 = 0 /\ mid_y:432 = y':427 /\ mid_x:433 = x':426
                /\ mid___cost:431 = __cost':428)
               \/ (1 <= K:434 /\ 0 <= (-1 + -mid_x:433 + havoc:21)
                     /\ 0 <= (mid_y:432 + -havoc:22) /\ 0 <= mid_y:432
                     /\ 0 <= mid___cost:431 /\ 0 <= mid_x:433
                     /\ 0 <= (-1 + -havoc:22 + y':427) /\ 0 <= (-1 + y':427)
                     /\ 0 <= (-1 + x':426) /\ 0 <= (-1 + __cost':428)
                     /\ 0 <= (havoc:21 + -x':426)))
         /\ (0 = K:434 \/ !((mid_y:432 + -havoc:22) < 0))
         /\ (K:430 + K:434) = K:429 /\ (!(0 <= K:435) \/ mid_y:436 = K:435)
         /\ (!(0 <= K:435) \/ mid_x:437 = K:435)
         /\ (!(0 <= K:435) \/ mid___cost:438 = K:435)
         /\ ((K:435 = 0 /\ 0 = mid_y:436 /\ 0 = mid_x:437
                /\ 0 = mid___cost:438)
               \/ (1 <= K:435 /\ 0 <= (-1 + havoc:21)
                     /\ 0 <= (-1 + mid_y:436) /\ 0 <= (-1 + mid_x:437)
                     /\ 0 <= (-1 + mid___cost:438)
                     /\ 0 <= (havoc:21 + -mid_x:437)))
         /\ (0 = K:435 \/ !(havoc:21 <= 0))
         /\ (!(0 <= K:439) \/ x':426 = (mid_x:437 + K:439))
         /\ (!(0 <= K:439) \/ y':427 = (mid_y:436 + K:439))
         /\ (!(0 <= K:439) \/ __cost':428 = (mid___cost:438 + K:439))
         /\ ((K:439 = 0 /\ mid_y:436 = y':427 /\ mid_x:437 = x':426
                /\ mid___cost:438 = __cost':428)
               \/ (1 <= K:439 /\ 0 <= (-1 + -mid_y:436 + havoc:22)
                     /\ 0 <= (mid_x:437 + -havoc:21) /\ 0 <= mid_x:437
                     /\ 0 <= mid___cost:438 /\ 0 <= mid_y:436
                     /\ 0 <= (-1 + -havoc:21 + x':426) /\ 0 <= (-1 + y':427)
                     /\ 0 <= (-1 + x':426) /\ 0 <= (-1 + __cost':428)
                     /\ 0 <= (havoc:22 + -y':427)))
         /\ (0 = K:439 \/ (-mid_x:437 + havoc:21) <= 0)
         /\ (K:435 + K:439) = K:429 /\ 0 <= K:429 /\ 0 <= y':427
         /\ 0 <= x':426 /\ havoc:21 <= x':426 /\ havoc:22 <= y':427
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:447)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:447))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:448)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:448)))}

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

Base relation: 
{__cost := __cost':458
 return := havoc:473
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:474
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:475
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:451) \/ mid_y:452 = K:451)
         /\ (!(0 <= K:451) \/ mid_x:453 = K:451)
         /\ (!(0 <= K:451) \/ mid___cost:454 = (__cost:105 + K:451))
         /\ ((K:451 = 0 /\ 0 = mid_y:452 /\ 0 = mid_x:453
                /\ __cost:105 = mid___cost:454)
               \/ (1 <= K:451 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                     /\ 0 <= (-1 + mid_y:452) /\ 0 <= (-1 + mid_x:453)
                     /\ 0 <= (-1 + mid___cost:454)
                     /\ 0 <= (param0:80 + -mid_x:453)))
         /\ (0 = K:451 \/ -param0:80 < 0)
         /\ (!(0 <= K:455) \/ x':456 = (mid_x:453 + K:455))
         /\ (!(0 <= K:455) \/ y':457 = (mid_y:452 + K:455))
         /\ (!(0 <= K:455) \/ __cost':458 = (mid___cost:454 + K:455))
         /\ ((K:455 = 0 /\ mid_y:452 = y':457 /\ mid_x:453 = x':456
                /\ mid___cost:454 = __cost':458)
               \/ (1 <= K:455 /\ 0 <= (-1 + -mid_y:452 + param1:83)
                     /\ 0 <= (mid_x:453 + -param0:80) /\ 0 <= mid_x:453
                     /\ 0 <= mid___cost:454 /\ 0 <= mid_y:452
                     /\ 0 <= (-1 + -param0:80 + x':456) /\ 0 <= (-1 + y':457)
                     /\ 0 <= (-1 + x':456) /\ 0 <= (-1 + __cost':458)
                     /\ 0 <= (param1:83 + -y':457)))
         /\ (0 = K:455 \/ !((mid_x:453 + -param0:80) < 0))
         /\ (K:451 + K:455) = K:459
         /\ (!(0 <= K:460) \/ mid___cost:461 = (__cost:105 + K:460))
         /\ (!(0 <= K:460) \/ mid_y:462 = K:460)
         /\ (!(0 <= K:460) \/ mid_x:463 = K:460)
         /\ ((K:460 = 0 /\ 0 = mid_y:462 /\ 0 = mid_x:463
                /\ __cost:105 = mid___cost:461)
               \/ (1 <= K:460 /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:105
                     /\ 0 <= (-mid_y:462 + param1:83)
                     /\ 0 <= (-1 + mid_x:463) /\ 0 <= (-1 + mid___cost:461)
                     /\ 0 <= (-1 + mid_y:462)))
         /\ (0 = K:460 \/ -param1:83 < 0)
         /\ (!(0 <= K:464) \/ x':456 = (mid_x:463 + K:464))
         /\ (!(0 <= K:464) \/ __cost':458 = (mid___cost:461 + K:464))
         /\ (!(0 <= K:464) \/ y':457 = (mid_y:462 + K:464))
         /\ ((K:464 = 0 /\ mid_y:462 = y':457 /\ mid_x:463 = x':456
                /\ mid___cost:461 = __cost':458)
               \/ (1 <= K:464 /\ 0 <= (-1 + -mid_x:463 + param0:80)
                     /\ 0 <= (mid_y:462 + -param1:83) /\ 0 <= mid_y:462
                     /\ 0 <= mid___cost:461 /\ 0 <= mid_x:463
                     /\ 0 <= (-1 + -param1:83 + y':457) /\ 0 <= (-1 + y':457)
                     /\ 0 <= (-1 + x':456) /\ 0 <= (-1 + __cost':458)
                     /\ 0 <= (param0:80 + -x':456)))
         /\ (0 = K:464 \/ !((mid_y:462 + -param1:83) < 0))
         /\ (K:460 + K:464) = K:459 /\ (!(0 <= K:465) \/ mid_y:466 = K:465)
         /\ (!(0 <= K:465) \/ mid_x:467 = K:465)
         /\ (!(0 <= K:465) \/ mid___cost:468 = (__cost:105 + K:465))
         /\ ((K:465 = 0 /\ 0 = mid_y:466 /\ 0 = mid_x:467
                /\ __cost:105 = mid___cost:468)
               \/ (1 <= K:465 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                     /\ 0 <= (-1 + mid_y:466) /\ 0 <= (-1 + mid_x:467)
                     /\ 0 <= (-1 + mid___cost:468)
                     /\ 0 <= (param0:80 + -mid_x:467)))
         /\ (0 = K:465 \/ !(param0:80 <= 0))
         /\ (!(0 <= K:469) \/ x':456 = (mid_x:467 + K:469))
         /\ (!(0 <= K:469) \/ y':457 = (mid_y:466 + K:469))
         /\ (!(0 <= K:469) \/ __cost':458 = (mid___cost:468 + K:469))
         /\ ((K:469 = 0 /\ mid_y:466 = y':457 /\ mid_x:467 = x':456
                /\ mid___cost:468 = __cost':458)
               \/ (1 <= K:469 /\ 0 <= (-1 + -mid_y:466 + param1:83)
                     /\ 0 <= (mid_x:467 + -param0:80) /\ 0 <= mid_x:467
                     /\ 0 <= mid___cost:468 /\ 0 <= mid_y:466
                     /\ 0 <= (-1 + -param0:80 + x':456) /\ 0 <= (-1 + y':457)
                     /\ 0 <= (-1 + x':456) /\ 0 <= (-1 + __cost':458)
                     /\ 0 <= (param1:83 + -y':457)))
         /\ (0 = K:469 \/ (-mid_x:467 + param0:80) <= 0)
         /\ (K:465 + K:469) = K:459 /\ 0 <= K:459 /\ 0 <= y':457
         /\ 0 <= x':456 /\ param0:80 <= x':456 /\ param1:83 <= y':457)}

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

Base relation: 
{__cost := __cost':326
 x := x':324
 y := y':325
 n := param0:80
 m := param1:83
 return := havoc:338
 return@pos := type_err:339
 return@width := type_err:340
 when ((!(0 <= K:319) \/ mid_y:320 = K:319)
         /\ (!(0 <= K:319) \/ mid_x:321 = K:319)
         /\ (!(0 <= K:319) \/ mid___cost:322 = (__cost:105 + K:319))
         /\ ((K:319 = 0 /\ 0 = mid_y:320 /\ 0 = mid_x:321
                /\ __cost:105 = mid___cost:322)
               \/ (1 <= K:319 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                     /\ 0 <= (-1 + mid_y:320) /\ 0 <= (-1 + mid_x:321)
                     /\ 0 <= (-1 + mid___cost:322)
                     /\ 0 <= (param0:80 + -mid_x:321)))
         /\ (0 = K:319 \/ -param0:80 < 0)
         /\ (!(0 <= K:323) \/ x':324 = (mid_x:321 + K:323))
         /\ (!(0 <= K:323) \/ y':325 = (mid_y:320 + K:323))
         /\ (!(0 <= K:323) \/ __cost':326 = (mid___cost:322 + K:323))
         /\ ((K:323 = 0 /\ mid_y:320 = y':325 /\ mid_x:321 = x':324
                /\ mid___cost:322 = __cost':326)
               \/ (1 <= K:323 /\ 0 <= (-1 + -mid_y:320 + param1:83)
                     /\ 0 <= (mid_x:321 + -param0:80) /\ 0 <= mid_x:321
                     /\ 0 <= mid___cost:322 /\ 0 <= mid_y:320
                     /\ 0 <= (-1 + -param0:80 + x':324) /\ 0 <= (-1 + y':325)
                     /\ 0 <= (-1 + x':324) /\ 0 <= (-1 + __cost':326)
                     /\ 0 <= (param1:83 + -y':325)))
         /\ (0 = K:323 \/ !((mid_x:321 + -param0:80) < 0))
         /\ (K:319 + K:323) = K:327
         /\ (!(0 <= K:328) \/ mid___cost:329 = (__cost:105 + K:328))
         /\ (!(0 <= K:328) \/ mid_y:330 = K:328)
         /\ (!(0 <= K:328) \/ mid_x:331 = K:328)
         /\ ((K:328 = 0 /\ 0 = mid_y:330 /\ 0 = mid_x:331
                /\ __cost:105 = mid___cost:329)
               \/ (1 <= K:328 /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:105
                     /\ 0 <= (-mid_y:330 + param1:83)
                     /\ 0 <= (-1 + mid_x:331) /\ 0 <= (-1 + mid___cost:329)
                     /\ 0 <= (-1 + mid_y:330)))
         /\ (0 = K:328 \/ -param1:83 < 0)
         /\ (!(0 <= K:332) \/ x':324 = (mid_x:331 + K:332))
         /\ (!(0 <= K:332) \/ __cost':326 = (mid___cost:329 + K:332))
         /\ (!(0 <= K:332) \/ y':325 = (mid_y:330 + K:332))
         /\ ((K:332 = 0 /\ mid_y:330 = y':325 /\ mid_x:331 = x':324
                /\ mid___cost:329 = __cost':326)
               \/ (1 <= K:332 /\ 0 <= (-1 + -mid_x:331 + param0:80)
                     /\ 0 <= (mid_y:330 + -param1:83) /\ 0 <= mid_y:330
                     /\ 0 <= mid___cost:329 /\ 0 <= mid_x:331
                     /\ 0 <= (-1 + -param1:83 + y':325) /\ 0 <= (-1 + y':325)
                     /\ 0 <= (-1 + x':324) /\ 0 <= (-1 + __cost':326)
                     /\ 0 <= (param0:80 + -x':324)))
         /\ (0 = K:332 \/ !((mid_y:330 + -param1:83) < 0))
         /\ (K:328 + K:332) = K:327 /\ (!(0 <= K:333) \/ mid_y:334 = K:333)
         /\ (!(0 <= K:333) \/ mid_x:335 = K:333)
         /\ (!(0 <= K:333) \/ mid___cost:336 = (__cost:105 + K:333))
         /\ ((K:333 = 0 /\ 0 = mid_y:334 /\ 0 = mid_x:335
                /\ __cost:105 = mid___cost:336)
               \/ (1 <= K:333 /\ 0 <= (-1 + param0:80) /\ 0 <= __cost:105
                     /\ 0 <= (-1 + mid_y:334) /\ 0 <= (-1 + mid_x:335)
                     /\ 0 <= (-1 + mid___cost:336)
                     /\ 0 <= (param0:80 + -mid_x:335)))
         /\ (0 = K:333 \/ !(param0:80 <= 0))
         /\ (!(0 <= K:337) \/ x':324 = (mid_x:335 + K:337))
         /\ (!(0 <= K:337) \/ y':325 = (mid_y:334 + K:337))
         /\ (!(0 <= K:337) \/ __cost':326 = (mid___cost:336 + K:337))
         /\ ((K:337 = 0 /\ mid_y:334 = y':325 /\ mid_x:335 = x':324
                /\ mid___cost:336 = __cost':326)
               \/ (1 <= K:337 /\ 0 <= (-1 + -mid_y:334 + param1:83)
                     /\ 0 <= (mid_x:335 + -param0:80) /\ 0 <= mid_x:335
                     /\ 0 <= mid___cost:336 /\ 0 <= mid_y:334
                     /\ 0 <= (-1 + -param0:80 + x':324) /\ 0 <= (-1 + y':325)
                     /\ 0 <= (-1 + x':324) /\ 0 <= (-1 + __cost':326)
                     /\ 0 <= (param1:83 + -y':325)))
         /\ (0 = K:337 \/ (-mid_x:335 + param0:80) <= 0)
         /\ (K:333 + K:337) = K:327 /\ 0 <= K:327 /\ 0 <= y':325
         /\ 0 <= x':324 /\ param0:80 <= x':324 /\ param1:83 <= y':325)}

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

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

Variable bounds at line 28 in run

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

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