/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, 65> -> <Unique State Name, 60 64>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 23> -> <Unique State Name, 65>	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, 68> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 54> -> <Unique State Name, 31>	Base relation: 
{x := 0
 y := 0
 n := param0:80
 m := param1:83}	
<Unique State Name, 31> -> <Unique State Name, 69>	Base relation: 
{when (0 <= y:104 /\ 0 <= x:101)}	
<Unique State Name, 58> -> <Unique State Name, 25>	Base relation: 
{}	
<Unique State Name, 66> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 59> -> <Unique State Name, 54 58>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 69> -> <Unique State Name, 35>	Base relation: 
{}	
<Unique State Name, 25> -> <Unique State Name, 67>	Base relation: 
{return := havoc:63
 return@pos := type_err:66
 return@width := type_err:67}	
<Unique State Name, 60> -> <Unique State Name, 59>	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, 64> -> <Unique State Name, 68>	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, 35> -> <Unique State Name, 31>	Base relation: 
{__cost := (__cost:103 + 1)
 x := phi_x:116
 y := phi_y:117
 when (x:101 < n:102 /\ 0 <= __cost:103 /\ 0 <= (__cost:103 + 1)
         /\ ((y:104 < m:105 /\ x:101 = phi_x:116 /\ (y:104 + 1) = phi_y:117)
               \/ (m:105 <= y:104 /\ (x:101 + 1) = phi_x:116
                     /\ y:104 = phi_y:117)))}	
<Unique State Name, 35> -> <Unique State Name, 66>	Base relation: 
{return := havoc:113
 return@pos := type_err:114
 return@width := type_err:115
 when n:102 <= x:101}	
<Unique State Name, 67> -> <Unique State Name, >	Base relation: 
{}	
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:103 + 1)
 x := phi_x:209
 y := phi_y:210
 when (0 <= y:104 /\ 0 <= x:101 /\ x:101 < n:102 /\ 0 <= __cost:103
         /\ 0 <= (__cost:103 + 1)
         /\ ((y:104 < m:105 /\ x:101 = phi_x:209 /\ (y:104 + 1) = phi_y:210)
               \/ (m:105 <= y:104 /\ (x:101 + 1) = phi_x:209
                     /\ y:104 = phi_y:210)))}
**** alpha hat: 
  {<Split [(y:104 + -m:105) < 0
            (__cost':211) = (1)*(__cost:103) + 1
           (x':212) = (1)*(x:101) + 0
           (y':213) = (1)*(y:104) + 1
           }
          pre:
            [|-x:101+n:102-1>=0; -y:104+m:105-1>=0; __cost:103>=0; y:104>=0;
              x:101>=0|]
          post:
            [|y':213-1>=0; __cost':211-1>=0; x':212>=0; m:105-y':213>=0;
              n:102-x':212-1>=0|]
           (__cost':211) = (1)*(__cost:103) + 1
          (x':212) = (1)*(x:101) + 1
          (y':213) = (1)*(y:104) + 0
          }
  pre:
    [|-x:101+n:102-1>=0; y:104-m:105>=0; y:104>=0; __cost:103>=0; x:101>=0|]
  post:
    [|-m:105+y':213>=0; x':212-1>=0; __cost':211-1>=0; y':213>=0;
      n:102-x':212>=0|]],
[!((-y:104 + m:105) <= 0)
  (__cost':211) = (1)*(__cost:103) + 1
 (x':212) = (1)*(x:101) + 0
 (y':213) = (1)*(y:104) + 1
 } pre:
  [|-x:101+n:102-1>=0; -y:104+m:105-1>=0; __cost:103>=0; y:104>=0; x:101>=0|]
post:
  [|y':213-1>=0; __cost':211-1>=0; x':212>=0; m:105-y':213>=0;
    n:102-x':212-1>=0|]  (__cost':211) = (1)*(__cost:103) + 1
(x':212) = (1)*(x:101) + 1 (y':213) = (1)*(y:104) + 0 } pre:
  [|-x:101+n:102-1>=0; y:104-m:105>=0; y:104>=0; __cost:103>=0; x:101>=0|]
post:
  [|-m:105+y':213>=0; x':212-1>=0; __cost':211-1>=0; y':213>=0;
    n:102-x':212>=0|]]>}
**** star transition: 
  {__cost := __cost':211
   x := x':212
   y := y':213
   when ((!(0 <= K:247) \/ mid___cost:251 = (__cost:103 + K:247))
           /\ (!(0 <= K:247) \/ mid_x:250 = x:101)
           /\ (!(0 <= K:247) \/ mid_y:249 = (y:104 + K:247))
           /\ ((K:247 = 0 /\ y:104 = mid_y:249 /\ x:101 = mid_x:250
                  /\ __cost:103 = mid___cost:251)
                 \/ (1 <= K:247 /\ 0 <= (-1 + -x:101 + n:102)
                       /\ 0 <= (-1 + -y:104 + m:105) /\ 0 <= __cost:103
                       /\ 0 <= y:104 /\ 0 <= x:101 /\ 0 <= (-1 + mid_y:249)
                       /\ 0 <= (-1 + mid___cost:251) /\ 0 <= mid_x:250
                       /\ 0 <= (m:105 + -mid_y:249)
                       /\ 0 <= (-1 + n:102 + -mid_x:250)))
           /\ (0 = K:247 \/ (y:104 + -m:105) < 0)
           /\ (!(0 <= K:248) \/ __cost':211 = (mid___cost:251 + K:248))
           /\ (!(0 <= K:248) \/ x':212 = (mid_x:250 + K:248))
           /\ (!(0 <= K:248) \/ y':213 = mid_y:249)
           /\ ((K:248 = 0 /\ mid_y:249 = y':213 /\ mid_x:250 = x':212
                  /\ mid___cost:251 = __cost':211)
                 \/ (1 <= K:248 /\ 0 <= (-1 + -mid_x:250 + n:102)
                       /\ 0 <= (mid_y:249 + -m:105) /\ 0 <= mid_y:249
                       /\ 0 <= mid___cost:251 /\ 0 <= mid_x:250
                       /\ 0 <= (-m:105 + y':213) /\ 0 <= (-1 + x':212)
                       /\ 0 <= (-1 + __cost':211) /\ 0 <= y':213
                       /\ 0 <= (n:102 + -x':212)))
           /\ (0 = K:248 \/ !((mid_y:249 + -m:105) < 0))
           /\ (K:247 + K:248) = K:246
           /\ (!(0 <= K:252) \/ mid___cost:256 = (__cost:103 + K:252))
           /\ (!(0 <= K:252) \/ mid_x:255 = x:101)
           /\ (!(0 <= K:252) \/ mid_y:254 = (y:104 + K:252))
           /\ ((K:252 = 0 /\ y:104 = mid_y:254 /\ x:101 = mid_x:255
                  /\ __cost:103 = mid___cost:256)
                 \/ (1 <= K:252 /\ 0 <= (-1 + -x:101 + n:102)
                       /\ 0 <= (-1 + -y:104 + m:105) /\ 0 <= __cost:103
                       /\ 0 <= y:104 /\ 0 <= x:101 /\ 0 <= (-1 + mid_y:254)
                       /\ 0 <= (-1 + mid___cost:256) /\ 0 <= mid_x:255
                       /\ 0 <= (m:105 + -mid_y:254)
                       /\ 0 <= (-1 + n:102 + -mid_x:255)))
           /\ (0 = K:252 \/ !((-y:104 + m:105) <= 0))
           /\ (!(0 <= K:253) \/ __cost':211 = (mid___cost:256 + K:253))
           /\ (!(0 <= K:253) \/ x':212 = (mid_x:255 + K:253))
           /\ (!(0 <= K:253) \/ y':213 = mid_y:254)
           /\ ((K:253 = 0 /\ mid_y:254 = y':213 /\ mid_x:255 = x':212
                  /\ mid___cost:256 = __cost':211)
                 \/ (1 <= K:253 /\ 0 <= (-1 + -mid_x:255 + n:102)
                       /\ 0 <= (mid_y:254 + -m:105) /\ 0 <= mid_y:254
                       /\ 0 <= mid___cost:256 /\ 0 <= mid_x:255
                       /\ 0 <= (-m:105 + y':213) /\ 0 <= (-1 + x':212)
                       /\ 0 <= (-1 + __cost':211) /\ 0 <= y':213
                       /\ 0 <= (n:102 + -x':212)))
           /\ (0 = K:253 \/ (-mid_y:254 + m:105) <= 0)
           /\ (K:252 + K:253) = K:246 /\ 0 <= K:246)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  19  


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(19)
  )
  ,
  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=19: 
Weight(Base relation: 
  {__cost := __cost':262
   x := x':263
   y := y':264
   n := param0:80
   m := param1:83
   return := havoc:271
   return@pos := type_err:272
   return@width := type_err:273
   when ((!(0 <= K:257) \/ mid___cost:258 = (__cost:103 + K:257))
           /\ (!(0 <= K:257) \/ mid_x:259 = 0)
           /\ (!(0 <= K:257) \/ mid_y:260 = K:257)
           /\ ((K:257 = 0 /\ 0 = mid_y:260 /\ 0 = mid_x:259
                  /\ __cost:103 = mid___cost:258)
                 \/ (1 <= K:257 /\ 0 <= (-1 + param0:80)
                       /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:103
                       /\ 0 <= (-1 + mid_y:260) /\ 0 <= (-1 + mid___cost:258)
                       /\ 0 <= mid_x:259 /\ 0 <= (param1:83 + -mid_y:260)
                       /\ 0 <= (-1 + param0:80 + -mid_x:259)))
           /\ (0 = K:257 \/ -param1:83 < 0)
           /\ (!(0 <= K:261) \/ __cost':262 = (mid___cost:258 + K:261))
           /\ (!(0 <= K:261) \/ x':263 = (mid_x:259 + K:261))
           /\ (!(0 <= K:261) \/ y':264 = mid_y:260)
           /\ ((K:261 = 0 /\ mid_y:260 = y':264 /\ mid_x:259 = x':263
                  /\ mid___cost:258 = __cost':262)
                 \/ (1 <= K:261 /\ 0 <= (-1 + -mid_x:259 + param0:80)
                       /\ 0 <= (mid_y:260 + -param1:83) /\ 0 <= mid_y:260
                       /\ 0 <= mid___cost:258 /\ 0 <= mid_x:259
                       /\ 0 <= (-param1:83 + y':264) /\ 0 <= (-1 + x':263)
                       /\ 0 <= (-1 + __cost':262) /\ 0 <= y':264
                       /\ 0 <= (param0:80 + -x':263)))
           /\ (0 = K:261 \/ !((mid_y:260 + -param1:83) < 0))
           /\ (K:257 + K:261) = K:265
           /\ (!(0 <= K:266) \/ mid___cost:267 = (__cost:103 + K:266))
           /\ (!(0 <= K:266) \/ mid_x:268 = 0)
           /\ (!(0 <= K:266) \/ mid_y:269 = K:266)
           /\ ((K:266 = 0 /\ 0 = mid_y:269 /\ 0 = mid_x:268
                  /\ __cost:103 = mid___cost:267)
                 \/ (1 <= K:266 /\ 0 <= (-1 + param0:80)
                       /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:103
                       /\ 0 <= (-1 + mid_y:269) /\ 0 <= (-1 + mid___cost:267)
                       /\ 0 <= mid_x:268 /\ 0 <= (param1:83 + -mid_y:269)
                       /\ 0 <= (-1 + param0:80 + -mid_x:268)))
           /\ (0 = K:266 \/ !(param1:83 <= 0))
           /\ (!(0 <= K:270) \/ __cost':262 = (mid___cost:267 + K:270))
           /\ (!(0 <= K:270) \/ x':263 = (mid_x:268 + K:270))
           /\ (!(0 <= K:270) \/ y':264 = mid_y:269)
           /\ ((K:270 = 0 /\ mid_y:269 = y':264 /\ mid_x:268 = x':263
                  /\ mid___cost:267 = __cost':262)
                 \/ (1 <= K:270 /\ 0 <= (-1 + -mid_x:268 + param0:80)
                       /\ 0 <= (mid_y:269 + -param1:83) /\ 0 <= mid_y:269
                       /\ 0 <= mid___cost:267 /\ 0 <= mid_x:268
                       /\ 0 <= (-param1:83 + y':264) /\ 0 <= (-1 + x':263)
                       /\ 0 <= (-1 + __cost':262) /\ 0 <= y':264
                       /\ 0 <= (param0:80 + -x':263)))
           /\ (0 = K:270 \/ (-mid_y:269 + param1:83) <= 0)
           /\ (K:266 + K:270) = K:265 /\ 0 <= K:265 /\ 0 <= y':264
           /\ 0 <= x':263 /\ param0:80 <= x':263)})



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(19)
    )
    ,
    Weight(Base relation: 
      {return := havoc:63
       return@pos := type_err:66
       return@width := type_err:67}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':262
   return := havoc:271
   return@pos := type_err:272
   return@width := type_err:273
   when ((!(0 <= K:257) \/ mid___cost:258 = (__cost:103 + K:257))
           /\ (!(0 <= K:257) \/ mid_x:259 = 0)
           /\ (!(0 <= K:257) \/ mid_y:260 = K:257)
           /\ ((K:257 = 0 /\ 0 = mid_y:260 /\ 0 = mid_x:259
                  /\ __cost:103 = mid___cost:258)
                 \/ (1 <= K:257 /\ 0 <= (-1 + param0:80)
                       /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:103
                       /\ 0 <= (-1 + mid_y:260) /\ 0 <= (-1 + mid___cost:258)
                       /\ 0 <= mid_x:259 /\ 0 <= (param1:83 + -mid_y:260)
                       /\ 0 <= (-1 + param0:80 + -mid_x:259)))
           /\ (0 = K:257 \/ -param1:83 < 0)
           /\ (!(0 <= K:261) \/ __cost':262 = (mid___cost:258 + K:261))
           /\ (!(0 <= K:261) \/ x':263 = (mid_x:259 + K:261))
           /\ (!(0 <= K:261) \/ y':264 = mid_y:260)
           /\ ((K:261 = 0 /\ mid_y:260 = y':264 /\ mid_x:259 = x':263
                  /\ mid___cost:258 = __cost':262)
                 \/ (1 <= K:261 /\ 0 <= (-1 + -mid_x:259 + param0:80)
                       /\ 0 <= (mid_y:260 + -param1:83) /\ 0 <= mid_y:260
                       /\ 0 <= mid___cost:258 /\ 0 <= mid_x:259
                       /\ 0 <= (-param1:83 + y':264) /\ 0 <= (-1 + x':263)
                       /\ 0 <= (-1 + __cost':262) /\ 0 <= y':264
                       /\ 0 <= (param0:80 + -x':263)))
           /\ (0 = K:261 \/ !((mid_y:260 + -param1:83) < 0))
           /\ (K:257 + K:261) = K:265
           /\ (!(0 <= K:266) \/ mid___cost:267 = (__cost:103 + K:266))
           /\ (!(0 <= K:266) \/ mid_x:268 = 0)
           /\ (!(0 <= K:266) \/ mid_y:269 = K:266)
           /\ ((K:266 = 0 /\ 0 = mid_y:269 /\ 0 = mid_x:268
                  /\ __cost:103 = mid___cost:267)
                 \/ (1 <= K:266 /\ 0 <= (-1 + param0:80)
                       /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:103
                       /\ 0 <= (-1 + mid_y:269) /\ 0 <= (-1 + mid___cost:267)
                       /\ 0 <= mid_x:268 /\ 0 <= (param1:83 + -mid_y:269)
                       /\ 0 <= (-1 + param0:80 + -mid_x:268)))
           /\ (0 = K:266 \/ !(param1:83 <= 0))
           /\ (!(0 <= K:270) \/ __cost':262 = (mid___cost:267 + K:270))
           /\ (!(0 <= K:270) \/ x':263 = (mid_x:268 + K:270))
           /\ (!(0 <= K:270) \/ y':264 = mid_y:269)
           /\ ((K:270 = 0 /\ mid_y:269 = y':264 /\ mid_x:268 = x':263
                  /\ mid___cost:267 = __cost':262)
                 \/ (1 <= K:270 /\ 0 <= (-1 + -mid_x:268 + param0:80)
                       /\ 0 <= (mid_y:269 + -param1:83) /\ 0 <= mid_y:269
                       /\ 0 <= mid___cost:267 /\ 0 <= mid_x:268
                       /\ 0 <= (-param1:83 + y':264) /\ 0 <= (-1 + x':263)
                       /\ 0 <= (-1 + __cost':262) /\ 0 <= y':264
                       /\ 0 <= (param0:80 + -x':263)))
           /\ (0 = K:270 \/ (-mid_y:269 + param1:83) <= 0)
           /\ (K:266 + K:270) = K:265 /\ 0 <= K:265 /\ 0 <= y':264
           /\ 0 <= x':263 /\ param0:80 <= x':263)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':299
   return := 0
   param0 := havoc:21
   param1 := havoc:22
   return@pos := type_err:317
   param0@pos := type_err:310
   param1@pos := type_err:311
   return@width := type_err:318
   param0@width := type_err:313
   param1@width := type_err:314
   when ((!(0 <= K:294) \/ mid___cost:295 = K:294)
           /\ (!(0 <= K:294) \/ mid_x:296 = 0)
           /\ (!(0 <= K:294) \/ mid_y:297 = K:294)
           /\ ((K:294 = 0 /\ 0 = mid_y:297 /\ 0 = mid_x:296
                  /\ 0 = mid___cost:295)
                 \/ (1 <= K:294 /\ 0 <= (-1 + havoc:21)
                       /\ 0 <= (-1 + havoc:22) /\ 0 <= (-1 + mid_y:297)
                       /\ 0 <= (-1 + mid___cost:295) /\ 0 <= mid_x:296
                       /\ 0 <= (havoc:22 + -mid_y:297)
                       /\ 0 <= (-1 + havoc:21 + -mid_x:296)))
           /\ (0 = K:294 \/ -havoc:22 < 0)
           /\ (!(0 <= K:298) \/ __cost':299 = (mid___cost:295 + K:298))
           /\ (!(0 <= K:298) \/ x':300 = (mid_x:296 + K:298))
           /\ (!(0 <= K:298) \/ y':301 = mid_y:297)
           /\ ((K:298 = 0 /\ mid_y:297 = y':301 /\ mid_x:296 = x':300
                  /\ mid___cost:295 = __cost':299)
                 \/ (1 <= K:298 /\ 0 <= (-1 + -mid_x:296 + havoc:21)
                       /\ 0 <= (mid_y:297 + -havoc:22) /\ 0 <= mid_y:297
                       /\ 0 <= mid___cost:295 /\ 0 <= mid_x:296
                       /\ 0 <= (-havoc:22 + y':301) /\ 0 <= (-1 + x':300)
                       /\ 0 <= (-1 + __cost':299) /\ 0 <= y':301
                       /\ 0 <= (havoc:21 + -x':300)))
           /\ (0 = K:298 \/ !((mid_y:297 + -havoc:22) < 0))
           /\ (K:294 + K:298) = K:302
           /\ (!(0 <= K:303) \/ mid___cost:304 = K:303)
           /\ (!(0 <= K:303) \/ mid_x:305 = 0)
           /\ (!(0 <= K:303) \/ mid_y:306 = K:303)
           /\ ((K:303 = 0 /\ 0 = mid_y:306 /\ 0 = mid_x:305
                  /\ 0 = mid___cost:304)
                 \/ (1 <= K:303 /\ 0 <= (-1 + havoc:21)
                       /\ 0 <= (-1 + havoc:22) /\ 0 <= (-1 + mid_y:306)
                       /\ 0 <= (-1 + mid___cost:304) /\ 0 <= mid_x:305
                       /\ 0 <= (havoc:22 + -mid_y:306)
                       /\ 0 <= (-1 + havoc:21 + -mid_x:305)))
           /\ (0 = K:303 \/ !(havoc:22 <= 0))
           /\ (!(0 <= K:307) \/ __cost':299 = (mid___cost:304 + K:307))
           /\ (!(0 <= K:307) \/ x':300 = (mid_x:305 + K:307))
           /\ (!(0 <= K:307) \/ y':301 = mid_y:306)
           /\ ((K:307 = 0 /\ mid_y:306 = y':301 /\ mid_x:305 = x':300
                  /\ mid___cost:304 = __cost':299)
                 \/ (1 <= K:307 /\ 0 <= (-1 + -mid_x:305 + havoc:21)
                       /\ 0 <= (mid_y:306 + -havoc:22) /\ 0 <= mid_y:306
                       /\ 0 <= mid___cost:304 /\ 0 <= mid_x:305
                       /\ 0 <= (-havoc:22 + y':301) /\ 0 <= (-1 + x':300)
                       /\ 0 <= (-1 + __cost':299) /\ 0 <= y':301
                       /\ 0 <= (havoc:21 + -x':300)))
           /\ (0 = K:307 \/ (-mid_y:306 + havoc:22) <= 0)
           /\ (K:303 + K:307) = K:302 /\ 0 <= K:302 /\ 0 <= y':301
           /\ 0 <= x':300 /\ havoc:21 <= x':300
           /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:315)
                 \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:315))
           /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:316)
                 \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:316)))})


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


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=19: 
Weight(Base relation: 
  {__cost := __cost':262
   return := havoc:271
   return@pos := type_err:272
   return@width := type_err:273
   when ((!(0 <= K:257) \/ mid___cost:258 = (__cost:103 + K:257))
           /\ (!(0 <= K:257) \/ mid_x:259 = 0)
           /\ (!(0 <= K:257) \/ mid_y:260 = K:257)
           /\ ((K:257 = 0 /\ 0 = mid_y:260 /\ 0 = mid_x:259
                  /\ __cost:103 = mid___cost:258)
                 \/ (1 <= K:257 /\ 0 <= (-1 + param0:80)
                       /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:103
                       /\ 0 <= (-1 + mid_y:260) /\ 0 <= (-1 + mid___cost:258)
                       /\ 0 <= mid_x:259 /\ 0 <= (param1:83 + -mid_y:260)
                       /\ 0 <= (-1 + param0:80 + -mid_x:259)))
           /\ (0 = K:257 \/ -param1:83 < 0)
           /\ (!(0 <= K:261) \/ __cost':262 = (mid___cost:258 + K:261))
           /\ (!(0 <= K:261) \/ x':263 = (mid_x:259 + K:261))
           /\ (!(0 <= K:261) \/ y':264 = mid_y:260)
           /\ ((K:261 = 0 /\ mid_y:260 = y':264 /\ mid_x:259 = x':263
                  /\ mid___cost:258 = __cost':262)
                 \/ (1 <= K:261 /\ 0 <= (-1 + -mid_x:259 + param0:80)
                       /\ 0 <= (mid_y:260 + -param1:83) /\ 0 <= mid_y:260
                       /\ 0 <= mid___cost:258 /\ 0 <= mid_x:259
                       /\ 0 <= (-param1:83 + y':264) /\ 0 <= (-1 + x':263)
                       /\ 0 <= (-1 + __cost':262) /\ 0 <= y':264
                       /\ 0 <= (param0:80 + -x':263)))
           /\ (0 = K:261 \/ !((mid_y:260 + -param1:83) < 0))
           /\ (K:257 + K:261) = K:265
           /\ (!(0 <= K:266) \/ mid___cost:267 = (__cost:103 + K:266))
           /\ (!(0 <= K:266) \/ mid_x:268 = 0)
           /\ (!(0 <= K:266) \/ mid_y:269 = K:266)
           /\ ((K:266 = 0 /\ 0 = mid_y:269 /\ 0 = mid_x:268
                  /\ __cost:103 = mid___cost:267)
                 \/ (1 <= K:266 /\ 0 <= (-1 + param0:80)
                       /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:103
                       /\ 0 <= (-1 + mid_y:269) /\ 0 <= (-1 + mid___cost:267)
                       /\ 0 <= mid_x:268 /\ 0 <= (param1:83 + -mid_y:269)
                       /\ 0 <= (-1 + param0:80 + -mid_x:268)))
           /\ (0 = K:266 \/ !(param1:83 <= 0))
           /\ (!(0 <= K:270) \/ __cost':262 = (mid___cost:267 + K:270))
           /\ (!(0 <= K:270) \/ x':263 = (mid_x:268 + K:270))
           /\ (!(0 <= K:270) \/ y':264 = mid_y:269)
           /\ ((K:270 = 0 /\ mid_y:269 = y':264 /\ mid_x:268 = x':263
                  /\ mid___cost:267 = __cost':262)
                 \/ (1 <= K:270 /\ 0 <= (-1 + -mid_x:268 + param0:80)
                       /\ 0 <= (mid_y:269 + -param1:83) /\ 0 <= mid_y:269
                       /\ 0 <= mid___cost:267 /\ 0 <= mid_x:268
                       /\ 0 <= (-param1:83 + y':264) /\ 0 <= (-1 + x':263)
                       /\ 0 <= (-1 + __cost':262) /\ 0 <= y':264
                       /\ 0 <= (param0:80 + -x':263)))
           /\ (0 = K:270 \/ (-mid_y:269 + param1:83) <= 0)
           /\ (K:266 + K:270) = K:265 /\ 0 <= K:265 /\ 0 <= y':264
           /\ 0 <= x':263 /\ param0:80 <= x':263)})


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':299
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:317
 param0@pos := type_err:310
 param1@pos := type_err:311
 return@width := type_err:318
 param0@width := type_err:313
 param1@width := type_err:314
 when ((!(0 <= K:294) \/ mid___cost:295 = K:294)
         /\ (!(0 <= K:294) \/ mid_x:296 = 0)
         /\ (!(0 <= K:294) \/ mid_y:297 = K:294)
         /\ ((K:294 = 0 /\ 0 = mid_y:297 /\ 0 = mid_x:296
                /\ 0 = mid___cost:295)
               \/ (1 <= K:294 /\ 0 <= (-1 + havoc:21) /\ 0 <= (-1 + havoc:22)
                     /\ 0 <= (-1 + mid_y:297) /\ 0 <= (-1 + mid___cost:295)
                     /\ 0 <= mid_x:296 /\ 0 <= (havoc:22 + -mid_y:297)
                     /\ 0 <= (-1 + havoc:21 + -mid_x:296)))
         /\ (0 = K:294 \/ -havoc:22 < 0)
         /\ (!(0 <= K:298) \/ __cost':299 = (mid___cost:295 + K:298))
         /\ (!(0 <= K:298) \/ x':300 = (mid_x:296 + K:298))
         /\ (!(0 <= K:298) \/ y':301 = mid_y:297)
         /\ ((K:298 = 0 /\ mid_y:297 = y':301 /\ mid_x:296 = x':300
                /\ mid___cost:295 = __cost':299)
               \/ (1 <= K:298 /\ 0 <= (-1 + -mid_x:296 + havoc:21)
                     /\ 0 <= (mid_y:297 + -havoc:22) /\ 0 <= mid_y:297
                     /\ 0 <= mid___cost:295 /\ 0 <= mid_x:296
                     /\ 0 <= (-havoc:22 + y':301) /\ 0 <= (-1 + x':300)
                     /\ 0 <= (-1 + __cost':299) /\ 0 <= y':301
                     /\ 0 <= (havoc:21 + -x':300)))
         /\ (0 = K:298 \/ !((mid_y:297 + -havoc:22) < 0))
         /\ (K:294 + K:298) = K:302
         /\ (!(0 <= K:303) \/ mid___cost:304 = K:303)
         /\ (!(0 <= K:303) \/ mid_x:305 = 0)
         /\ (!(0 <= K:303) \/ mid_y:306 = K:303)
         /\ ((K:303 = 0 /\ 0 = mid_y:306 /\ 0 = mid_x:305
                /\ 0 = mid___cost:304)
               \/ (1 <= K:303 /\ 0 <= (-1 + havoc:21) /\ 0 <= (-1 + havoc:22)
                     /\ 0 <= (-1 + mid_y:306) /\ 0 <= (-1 + mid___cost:304)
                     /\ 0 <= mid_x:305 /\ 0 <= (havoc:22 + -mid_y:306)
                     /\ 0 <= (-1 + havoc:21 + -mid_x:305)))
         /\ (0 = K:303 \/ !(havoc:22 <= 0))
         /\ (!(0 <= K:307) \/ __cost':299 = (mid___cost:304 + K:307))
         /\ (!(0 <= K:307) \/ x':300 = (mid_x:305 + K:307))
         /\ (!(0 <= K:307) \/ y':301 = mid_y:306)
         /\ ((K:307 = 0 /\ mid_y:306 = y':301 /\ mid_x:305 = x':300
                /\ mid___cost:304 = __cost':299)
               \/ (1 <= K:307 /\ 0 <= (-1 + -mid_x:305 + havoc:21)
                     /\ 0 <= (mid_y:306 + -havoc:22) /\ 0 <= mid_y:306
                     /\ 0 <= mid___cost:304 /\ 0 <= mid_x:305
                     /\ 0 <= (-havoc:22 + y':301) /\ 0 <= (-1 + x':300)
                     /\ 0 <= (-1 + __cost':299) /\ 0 <= y':301
                     /\ 0 <= (havoc:21 + -x':300)))
         /\ (0 = K:307 \/ (-mid_y:306 + havoc:22) <= 0)
         /\ (K:303 + K:307) = K:302 /\ 0 <= K:302 /\ 0 <= y':301
         /\ 0 <= x':300 /\ havoc:21 <= x':300
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:315)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:315))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:316)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:316)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

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

Evaluating variable number 19 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':262
 return := havoc:271
 return@pos := type_err:272
 return@width := type_err:273
 when ((!(0 <= K:257) \/ mid___cost:258 = (__cost:103 + K:257))
         /\ (!(0 <= K:257) \/ mid_x:259 = 0)
         /\ (!(0 <= K:257) \/ mid_y:260 = K:257)
         /\ ((K:257 = 0 /\ 0 = mid_y:260 /\ 0 = mid_x:259
                /\ __cost:103 = mid___cost:258)
               \/ (1 <= K:257 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:103
                     /\ 0 <= (-1 + mid_y:260) /\ 0 <= (-1 + mid___cost:258)
                     /\ 0 <= mid_x:259 /\ 0 <= (param1:83 + -mid_y:260)
                     /\ 0 <= (-1 + param0:80 + -mid_x:259)))
         /\ (0 = K:257 \/ -param1:83 < 0)
         /\ (!(0 <= K:261) \/ __cost':262 = (mid___cost:258 + K:261))
         /\ (!(0 <= K:261) \/ x':263 = (mid_x:259 + K:261))
         /\ (!(0 <= K:261) \/ y':264 = mid_y:260)
         /\ ((K:261 = 0 /\ mid_y:260 = y':264 /\ mid_x:259 = x':263
                /\ mid___cost:258 = __cost':262)
               \/ (1 <= K:261 /\ 0 <= (-1 + -mid_x:259 + param0:80)
                     /\ 0 <= (mid_y:260 + -param1:83) /\ 0 <= mid_y:260
                     /\ 0 <= mid___cost:258 /\ 0 <= mid_x:259
                     /\ 0 <= (-param1:83 + y':264) /\ 0 <= (-1 + x':263)
                     /\ 0 <= (-1 + __cost':262) /\ 0 <= y':264
                     /\ 0 <= (param0:80 + -x':263)))
         /\ (0 = K:261 \/ !((mid_y:260 + -param1:83) < 0))
         /\ (K:257 + K:261) = K:265
         /\ (!(0 <= K:266) \/ mid___cost:267 = (__cost:103 + K:266))
         /\ (!(0 <= K:266) \/ mid_x:268 = 0)
         /\ (!(0 <= K:266) \/ mid_y:269 = K:266)
         /\ ((K:266 = 0 /\ 0 = mid_y:269 /\ 0 = mid_x:268
                /\ __cost:103 = mid___cost:267)
               \/ (1 <= K:266 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:103
                     /\ 0 <= (-1 + mid_y:269) /\ 0 <= (-1 + mid___cost:267)
                     /\ 0 <= mid_x:268 /\ 0 <= (param1:83 + -mid_y:269)
                     /\ 0 <= (-1 + param0:80 + -mid_x:268)))
         /\ (0 = K:266 \/ !(param1:83 <= 0))
         /\ (!(0 <= K:270) \/ __cost':262 = (mid___cost:267 + K:270))
         /\ (!(0 <= K:270) \/ x':263 = (mid_x:268 + K:270))
         /\ (!(0 <= K:270) \/ y':264 = mid_y:269)
         /\ ((K:270 = 0 /\ mid_y:269 = y':264 /\ mid_x:268 = x':263
                /\ mid___cost:267 = __cost':262)
               \/ (1 <= K:270 /\ 0 <= (-1 + -mid_x:268 + param0:80)
                     /\ 0 <= (mid_y:269 + -param1:83) /\ 0 <= mid_y:269
                     /\ 0 <= mid___cost:267 /\ 0 <= mid_x:268
                     /\ 0 <= (-param1:83 + y':264) /\ 0 <= (-1 + x':263)
                     /\ 0 <= (-1 + __cost':262) /\ 0 <= y':264
                     /\ 0 <= (param0:80 + -x':263)))
         /\ (0 = K:270 \/ (-mid_y:269 + param1:83) <= 0)
         /\ (K:266 + K:270) = K:265 /\ 0 <= K:265 /\ 0 <= y':264
         /\ 0 <= x':263 /\ param0:80 <= x':263)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,60)_g1> -> <__pstate, (Unique State Name,54)_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,60)_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 0x5b53550: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x60ebb00: 
	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,54)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:21
 m := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:384
 param1@pos := type_err:385
 param0@width := type_err:386
 param1@width := type_err:387}
    ( __pstate , (Unique State Name,60)_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 0x626c910: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x6026450: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
================================================
Procedure Summaries

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

Base relation: 
{__cost := __cost':344
 n := havoc:21
 m := havoc:22
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:362
 param0@pos := type_err:355
 param1@pos := type_err:356
 return@width := type_err:363
 param0@width := type_err:358
 param1@width := type_err:359
 when ((!(0 <= K:339) \/ mid___cost:340 = K:339)
         /\ (!(0 <= K:339) \/ mid_x:341 = 0)
         /\ (!(0 <= K:339) \/ mid_y:342 = K:339)
         /\ ((K:339 = 0 /\ 0 = mid_y:342 /\ 0 = mid_x:341
                /\ 0 = mid___cost:340)
               \/ (1 <= K:339 /\ 0 <= (-1 + havoc:21) /\ 0 <= (-1 + havoc:22)
                     /\ 0 <= (-1 + mid_y:342) /\ 0 <= (-1 + mid___cost:340)
                     /\ 0 <= mid_x:341 /\ 0 <= (havoc:22 + -mid_y:342)
                     /\ 0 <= (-1 + havoc:21 + -mid_x:341)))
         /\ (0 = K:339 \/ -havoc:22 < 0)
         /\ (!(0 <= K:343) \/ __cost':344 = (mid___cost:340 + K:343))
         /\ (!(0 <= K:343) \/ x':345 = (mid_x:341 + K:343))
         /\ (!(0 <= K:343) \/ y':346 = mid_y:342)
         /\ ((K:343 = 0 /\ mid_y:342 = y':346 /\ mid_x:341 = x':345
                /\ mid___cost:340 = __cost':344)
               \/ (1 <= K:343 /\ 0 <= (-1 + -mid_x:341 + havoc:21)
                     /\ 0 <= (mid_y:342 + -havoc:22) /\ 0 <= mid_y:342
                     /\ 0 <= mid___cost:340 /\ 0 <= mid_x:341
                     /\ 0 <= (-havoc:22 + y':346) /\ 0 <= (-1 + x':345)
                     /\ 0 <= (-1 + __cost':344) /\ 0 <= y':346
                     /\ 0 <= (havoc:21 + -x':345)))
         /\ (0 = K:343 \/ !((mid_y:342 + -havoc:22) < 0))
         /\ (K:339 + K:343) = K:347
         /\ (!(0 <= K:348) \/ mid___cost:349 = K:348)
         /\ (!(0 <= K:348) \/ mid_x:350 = 0)
         /\ (!(0 <= K:348) \/ mid_y:351 = K:348)
         /\ ((K:348 = 0 /\ 0 = mid_y:351 /\ 0 = mid_x:350
                /\ 0 = mid___cost:349)
               \/ (1 <= K:348 /\ 0 <= (-1 + havoc:21) /\ 0 <= (-1 + havoc:22)
                     /\ 0 <= (-1 + mid_y:351) /\ 0 <= (-1 + mid___cost:349)
                     /\ 0 <= mid_x:350 /\ 0 <= (havoc:22 + -mid_y:351)
                     /\ 0 <= (-1 + havoc:21 + -mid_x:350)))
         /\ (0 = K:348 \/ !(havoc:22 <= 0))
         /\ (!(0 <= K:352) \/ __cost':344 = (mid___cost:349 + K:352))
         /\ (!(0 <= K:352) \/ x':345 = (mid_x:350 + K:352))
         /\ (!(0 <= K:352) \/ y':346 = mid_y:351)
         /\ ((K:352 = 0 /\ mid_y:351 = y':346 /\ mid_x:350 = x':345
                /\ mid___cost:349 = __cost':344)
               \/ (1 <= K:352 /\ 0 <= (-1 + -mid_x:350 + havoc:21)
                     /\ 0 <= (mid_y:351 + -havoc:22) /\ 0 <= mid_y:351
                     /\ 0 <= mid___cost:349 /\ 0 <= mid_x:350
                     /\ 0 <= (-havoc:22 + y':346) /\ 0 <= (-1 + x':345)
                     /\ 0 <= (-1 + __cost':344) /\ 0 <= y':346
                     /\ 0 <= (havoc:21 + -x':345)))
         /\ (0 = K:352 \/ (-mid_y:351 + havoc:22) <= 0)
         /\ (K:348 + K:352) = K:347 /\ 0 <= K:347 /\ 0 <= y':346
         /\ 0 <= x':345 /\ havoc:21 <= x':345
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:360)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:360))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:361)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:361)))}

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

Base relation: 
{__cost := __cost':369
 return := havoc:381
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:382
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:383
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:364) \/ mid___cost:365 = (__cost:103 + K:364))
         /\ (!(0 <= K:364) \/ mid_x:366 = 0)
         /\ (!(0 <= K:364) \/ mid_y:367 = K:364)
         /\ ((K:364 = 0 /\ 0 = mid_y:367 /\ 0 = mid_x:366
                /\ __cost:103 = mid___cost:365)
               \/ (1 <= K:364 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:103
                     /\ 0 <= (-1 + mid_y:367) /\ 0 <= (-1 + mid___cost:365)
                     /\ 0 <= mid_x:366 /\ 0 <= (param1:83 + -mid_y:367)
                     /\ 0 <= (-1 + param0:80 + -mid_x:366)))
         /\ (0 = K:364 \/ -param1:83 < 0)
         /\ (!(0 <= K:368) \/ __cost':369 = (mid___cost:365 + K:368))
         /\ (!(0 <= K:368) \/ x':370 = (mid_x:366 + K:368))
         /\ (!(0 <= K:368) \/ y':371 = mid_y:367)
         /\ ((K:368 = 0 /\ mid_y:367 = y':371 /\ mid_x:366 = x':370
                /\ mid___cost:365 = __cost':369)
               \/ (1 <= K:368 /\ 0 <= (-1 + -mid_x:366 + param0:80)
                     /\ 0 <= (mid_y:367 + -param1:83) /\ 0 <= mid_y:367
                     /\ 0 <= mid___cost:365 /\ 0 <= mid_x:366
                     /\ 0 <= (-param1:83 + y':371) /\ 0 <= (-1 + x':370)
                     /\ 0 <= (-1 + __cost':369) /\ 0 <= y':371
                     /\ 0 <= (param0:80 + -x':370)))
         /\ (0 = K:368 \/ !((mid_y:367 + -param1:83) < 0))
         /\ (K:364 + K:368) = K:372
         /\ (!(0 <= K:373) \/ mid___cost:374 = (__cost:103 + K:373))
         /\ (!(0 <= K:373) \/ mid_x:375 = 0)
         /\ (!(0 <= K:373) \/ mid_y:376 = K:373)
         /\ ((K:373 = 0 /\ 0 = mid_y:376 /\ 0 = mid_x:375
                /\ __cost:103 = mid___cost:374)
               \/ (1 <= K:373 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:103
                     /\ 0 <= (-1 + mid_y:376) /\ 0 <= (-1 + mid___cost:374)
                     /\ 0 <= mid_x:375 /\ 0 <= (param1:83 + -mid_y:376)
                     /\ 0 <= (-1 + param0:80 + -mid_x:375)))
         /\ (0 = K:373 \/ !(param1:83 <= 0))
         /\ (!(0 <= K:377) \/ __cost':369 = (mid___cost:374 + K:377))
         /\ (!(0 <= K:377) \/ x':370 = (mid_x:375 + K:377))
         /\ (!(0 <= K:377) \/ y':371 = mid_y:376)
         /\ ((K:377 = 0 /\ mid_y:376 = y':371 /\ mid_x:375 = x':370
                /\ mid___cost:374 = __cost':369)
               \/ (1 <= K:377 /\ 0 <= (-1 + -mid_x:375 + param0:80)
                     /\ 0 <= (mid_y:376 + -param1:83) /\ 0 <= mid_y:376
                     /\ 0 <= mid___cost:374 /\ 0 <= mid_x:375
                     /\ 0 <= (-param1:83 + y':371) /\ 0 <= (-1 + x':370)
                     /\ 0 <= (-1 + __cost':369) /\ 0 <= y':371
                     /\ 0 <= (param0:80 + -x':370)))
         /\ (0 = K:377 \/ (-mid_y:376 + param1:83) <= 0)
         /\ (K:373 + K:377) = K:372 /\ 0 <= K:372 /\ 0 <= y':371
         /\ 0 <= x':370 /\ param0:80 <= x':370)}

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

Base relation: 
{__cost := __cost':262
 x := x':263
 y := y':264
 n := param0:80
 m := param1:83
 return := havoc:271
 return@pos := type_err:272
 return@width := type_err:273
 when ((!(0 <= K:257) \/ mid___cost:258 = (__cost:103 + K:257))
         /\ (!(0 <= K:257) \/ mid_x:259 = 0)
         /\ (!(0 <= K:257) \/ mid_y:260 = K:257)
         /\ ((K:257 = 0 /\ 0 = mid_y:260 /\ 0 = mid_x:259
                /\ __cost:103 = mid___cost:258)
               \/ (1 <= K:257 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:103
                     /\ 0 <= (-1 + mid_y:260) /\ 0 <= (-1 + mid___cost:258)
                     /\ 0 <= mid_x:259 /\ 0 <= (param1:83 + -mid_y:260)
                     /\ 0 <= (-1 + param0:80 + -mid_x:259)))
         /\ (0 = K:257 \/ -param1:83 < 0)
         /\ (!(0 <= K:261) \/ __cost':262 = (mid___cost:258 + K:261))
         /\ (!(0 <= K:261) \/ x':263 = (mid_x:259 + K:261))
         /\ (!(0 <= K:261) \/ y':264 = mid_y:260)
         /\ ((K:261 = 0 /\ mid_y:260 = y':264 /\ mid_x:259 = x':263
                /\ mid___cost:258 = __cost':262)
               \/ (1 <= K:261 /\ 0 <= (-1 + -mid_x:259 + param0:80)
                     /\ 0 <= (mid_y:260 + -param1:83) /\ 0 <= mid_y:260
                     /\ 0 <= mid___cost:258 /\ 0 <= mid_x:259
                     /\ 0 <= (-param1:83 + y':264) /\ 0 <= (-1 + x':263)
                     /\ 0 <= (-1 + __cost':262) /\ 0 <= y':264
                     /\ 0 <= (param0:80 + -x':263)))
         /\ (0 = K:261 \/ !((mid_y:260 + -param1:83) < 0))
         /\ (K:257 + K:261) = K:265
         /\ (!(0 <= K:266) \/ mid___cost:267 = (__cost:103 + K:266))
         /\ (!(0 <= K:266) \/ mid_x:268 = 0)
         /\ (!(0 <= K:266) \/ mid_y:269 = K:266)
         /\ ((K:266 = 0 /\ 0 = mid_y:269 /\ 0 = mid_x:268
                /\ __cost:103 = mid___cost:267)
               \/ (1 <= K:266 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= (-1 + param1:83) /\ 0 <= __cost:103
                     /\ 0 <= (-1 + mid_y:269) /\ 0 <= (-1 + mid___cost:267)
                     /\ 0 <= mid_x:268 /\ 0 <= (param1:83 + -mid_y:269)
                     /\ 0 <= (-1 + param0:80 + -mid_x:268)))
         /\ (0 = K:266 \/ !(param1:83 <= 0))
         /\ (!(0 <= K:270) \/ __cost':262 = (mid___cost:267 + K:270))
         /\ (!(0 <= K:270) \/ x':263 = (mid_x:268 + K:270))
         /\ (!(0 <= K:270) \/ y':264 = mid_y:269)
         /\ ((K:270 = 0 /\ mid_y:269 = y':264 /\ mid_x:268 = x':263
                /\ mid___cost:267 = __cost':262)
               \/ (1 <= K:270 /\ 0 <= (-1 + -mid_x:268 + param0:80)
                     /\ 0 <= (mid_y:269 + -param1:83) /\ 0 <= mid_y:269
                     /\ 0 <= mid___cost:267 /\ 0 <= mid_x:268
                     /\ 0 <= (-param1:83 + y':264) /\ 0 <= (-1 + x':263)
                     /\ 0 <= (-1 + __cost':262) /\ 0 <= y':264
                     /\ 0 <= (param0:80 + -x':263)))
         /\ (0 = K:270 \/ (-mid_y:269 + param1:83) <= 0)
         /\ (K:266 + K:270) = K:265 /\ 0 <= K:265 /\ 0 <= y':264
         /\ 0 <= x':263 /\ param0:80 <= x':263)}

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

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

Variable bounds at line 22 in run

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

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