/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, 75> -> <Unique State Name, 66 74>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 27> -> <Unique State Name, 75>	Base relation: 
{__cost := 0
 x := havoc:35
 y := havoc:36
 n := havoc:37
 m := havoc:38
 param0 := havoc:35
 param1 := havoc:36
 param2 := havoc:37
 param3 := havoc:38
 param0@pos := type_err:43
 param1@pos := type_err:45
 param2@pos := type_err:47
 param3@pos := type_err:49
 param0@width := type_err:44
 param1@width := type_err:46
 param2@width := type_err:48
 param3@width := type_err:50}	
<Unique State Name, 78> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 56> -> <Unique State Name, 33>	Base relation: 
{x := param0:120
 y := param1:123
 n := param2:126
 m := param3:129}	
<Unique State Name, 33> -> <Unique State Name, 79>	Base relation: 
{}	
<Unique State Name, 64> -> <Unique State Name, 29>	Base relation: 
{}	
<Unique State Name, 76> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 65> -> <Unique State Name, 56 64>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 79> -> <Unique State Name, 37>	Base relation: 
{}	
<Unique State Name, 29> -> <Unique State Name, 77>	Base relation: 
{return := havoc:93
 return@pos := type_err:96
 return@width := type_err:97}	
<Unique State Name, 66> -> <Unique State Name, 65>	Base relation: 
{param0 := param0:120
 param1 := param1:123
 param2 := param2:126
 param3 := param3:129
 param0@pos := type_err:138
 param1@pos := type_err:139
 param2@pos := type_err:140
 param3@pos := type_err:141
 param0@width := type_err:142
 param1@width := type_err:143
 param2@width := type_err:144
 param3@width := type_err:145}	
<Unique State Name, 74> -> <Unique State Name, 78>	Base relation: 
{return := 0
 return@pos := type_err:52
 return@width := type_err:53
 when (((x:8 < n:9 /\ (n:9 + -x:8) = phi_tmp___3:39)
          \/ (n:9 <= x:8 /\ 0 = phi_tmp___3:39))
         /\ ((y:10 < m:11 /\ (m:11 + -y:10) = phi_tmp___4:51)
               \/ (m:11 <= y:10 /\ 0 = phi_tmp___4:51)))}	
<Unique State Name, 37> -> <Unique State Name, 33>	Base relation: 
{__cost := (__cost:163 + 1)
 x := phi_x:176
 y := phi_y:177
 when (x:161 < n:162 /\ 0 <= __cost:163 /\ 0 <= (__cost:163 + 1)
         /\ ((y:164 < m:165 /\ x:161 = phi_x:176 /\ (y:164 + 1) = phi_y:177)
               \/ (m:165 <= y:164 /\ (x:161 + 1) = phi_x:176
                     /\ y:164 = phi_y:177)))}	
<Unique State Name, 37> -> <Unique State Name, 76>	Base relation: 
{return := havoc:173
 return@pos := type_err:174
 return@width := type_err:175
 when n:162 <= x:161}	
<Unique State Name, 77> -> <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:163 + 1)
 x := phi_x:176
 y := phi_y:177
 when (x:161 < n:162 /\ 0 <= __cost:163 /\ 0 <= (__cost:163 + 1)
         /\ ((y:164 < m:165 /\ x:161 = phi_x:176 /\ (y:164 + 1) = phi_y:177)
               \/ (m:165 <= y:164 /\ (x:161 + 1) = phi_x:176
                     /\ y:164 = phi_y:177)))}
**** alpha hat: 
  {<Split [(y:164 + -m:165) < 0
            (y':214) = (1)*(y:164) + 1
           (x':213) = (1)*(x:161) + 0
           (__cost':212) = (1)*(__cost:163) + 1
           }
          pre:
            [|-y:164+m:165-1>=0; -x:161+n:162-1>=0; __cost:163>=0|]
          post:
            [|__cost':212-1>=0; n:162-x':213-1>=0; m:165-y':214>=0|]
           (__cost':212) = (1)*(__cost:163) + 1
          (x':213) = (1)*(x:161) + 1
          (y':214) = (1)*(y:164) + 0
          }
  pre:
    [|-x:161+n:162-1>=0; __cost:163>=0; y:164-m:165>=0|]
  post:
    [|-m:165+y':214>=0; __cost':212-1>=0; n:162-x':213>=0|]],
[!((-y:164 + m:165) <= 0)
  (y':214) = (1)*(y:164) + 1
 (x':213) = (1)*(x:161) + 0
 (__cost':212) = (1)*(__cost:163) + 1
 } pre:   [|-y:164+m:165-1>=0; -x:161+n:162-1>=0; __cost:163>=0|] post:
  [|__cost':212-1>=0; n:162-x':213-1>=0; m:165-y':214>=0|]
 (__cost':212) = (1)*(__cost:163) + 1 (x':213) = (1)*(x:161) + 1
(y':214) = (1)*(y:164) + 0 } pre:
  [|-x:161+n:162-1>=0; __cost:163>=0; y:164-m:165>=0|] post:
  [|-m:165+y':214>=0; __cost':212-1>=0; n:162-x':213>=0|]]>}
**** star transition: 
  {__cost := __cost':212
   x := x':213
   y := y':214
   when ((!(0 <= K:248) \/ mid_y:250 = (y:164 + K:248))
           /\ (!(0 <= K:248) \/ mid_x:251 = x:161)
           /\ (!(0 <= K:248) \/ mid___cost:252 = (__cost:163 + K:248))
           /\ ((K:248 = 0 /\ y:164 = mid_y:250 /\ x:161 = mid_x:251
                  /\ __cost:163 = mid___cost:252)
                 \/ (1 <= K:248 /\ 0 <= (-1 + -y:164 + m:165)
                       /\ 0 <= (-1 + -x:161 + n:162) /\ 0 <= __cost:163
                       /\ 0 <= (-1 + mid___cost:252)
                       /\ 0 <= (-1 + n:162 + -mid_x:251)
                       /\ 0 <= (m:165 + -mid_y:250)))
           /\ (0 = K:248 \/ (y:164 + -m:165) < 0)
           /\ (!(0 <= K:249) \/ __cost':212 = (mid___cost:252 + K:249))
           /\ (!(0 <= K:249) \/ x':213 = (mid_x:251 + K:249))
           /\ (!(0 <= K:249) \/ y':214 = mid_y:250)
           /\ ((K:249 = 0 /\ mid_y:250 = y':214 /\ mid_x:251 = x':213
                  /\ mid___cost:252 = __cost':212)
                 \/ (1 <= K:249 /\ 0 <= (-1 + -mid_x:251 + n:162)
                       /\ 0 <= mid___cost:252 /\ 0 <= (mid_y:250 + -m:165)
                       /\ 0 <= (-m:165 + y':214) /\ 0 <= (-1 + __cost':212)
                       /\ 0 <= (n:162 + -x':213)))
           /\ (0 = K:249 \/ !((mid_y:250 + -m:165) < 0))
           /\ (K:248 + K:249) = K:247
           /\ (!(0 <= K:253) \/ mid_y:255 = (y:164 + K:253))
           /\ (!(0 <= K:253) \/ mid_x:256 = x:161)
           /\ (!(0 <= K:253) \/ mid___cost:257 = (__cost:163 + K:253))
           /\ ((K:253 = 0 /\ y:164 = mid_y:255 /\ x:161 = mid_x:256
                  /\ __cost:163 = mid___cost:257)
                 \/ (1 <= K:253 /\ 0 <= (-1 + -y:164 + m:165)
                       /\ 0 <= (-1 + -x:161 + n:162) /\ 0 <= __cost:163
                       /\ 0 <= (-1 + mid___cost:257)
                       /\ 0 <= (-1 + n:162 + -mid_x:256)
                       /\ 0 <= (m:165 + -mid_y:255)))
           /\ (0 = K:253 \/ !((-y:164 + m:165) <= 0))
           /\ (!(0 <= K:254) \/ __cost':212 = (mid___cost:257 + K:254))
           /\ (!(0 <= K:254) \/ x':213 = (mid_x:256 + K:254))
           /\ (!(0 <= K:254) \/ y':214 = mid_y:255)
           /\ ((K:254 = 0 /\ mid_y:255 = y':214 /\ mid_x:256 = x':213
                  /\ mid___cost:257 = __cost':212)
                 \/ (1 <= K:254 /\ 0 <= (-1 + -mid_x:256 + n:162)
                       /\ 0 <= mid___cost:257 /\ 0 <= (mid_y:255 + -m:165)
                       /\ 0 <= (-m:165 + y':214) /\ 0 <= (-1 + __cost':212)
                       /\ 0 <= (n:162 + -x':213)))
           /\ (0 = K:254 \/ (-mid_y:255 + m:165) <= 0)
           /\ (K:253 + K:254) = K:247 /\ 0 <= K:247)}
}
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
       x := havoc:35
       y := havoc:36
       n := havoc:37
       m := havoc:38
       param0 := havoc:35
       param1 := havoc:36
       param2 := havoc:37
       param3 := havoc:38
       param0@pos := type_err:43
       param1@pos := type_err:45
       param2@pos := type_err:47
       param3@pos := type_err:49
       param0@width := type_err:44
       param1@width := type_err:46
       param2@width := type_err:48
       param3@width := type_err:50}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:52
     return@width := type_err:53
     when (((x:8 < n:9 /\ (n:9 + -x:8) = phi_tmp___3:39)
              \/ (n:9 <= x:8 /\ 0 = phi_tmp___3:39))
             /\ ((y:10 < m:11 /\ (m:11 + -y:10) = phi_tmp___4:51)
                   \/ (m:11 <= y:10 /\ 0 = phi_tmp___4:51)))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:120
       param1 := param1:123
       param2 := param2:126
       param3 := param3:129
       param0@pos := type_err:138
       param1@pos := type_err:139
       param2@pos := type_err:140
       param3@pos := type_err:141
       param0@width := type_err:142
       param1@width := type_err:143
       param2@width := type_err:144
       param3@width := type_err:145}    )
    ,
    Var(19)
  )
  ,
  Weight(Base relation: 
    {return := havoc:93
     return@pos := type_err:96
     return@width := type_err:97}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=19: 
Weight(Base relation: 
  {__cost := __cost':263
   x := x':264
   y := y':265
   n := param2:126
   m := param3:129
   return := havoc:272
   return@pos := type_err:273
   return@width := type_err:274
   when ((!(0 <= K:258) \/ mid_y:259 = (param1:123 + K:258))
           /\ (!(0 <= K:258) \/ mid_x:260 = param0:120)
           /\ (!(0 <= K:258) \/ mid___cost:261 = (__cost:163 + K:258))
           /\ ((K:258 = 0 /\ param1:123 = mid_y:259 /\ param0:120 = mid_x:260
                  /\ __cost:163 = mid___cost:261)
                 \/ (1 <= K:258 /\ 0 <= (-1 + -param1:123 + param3:129)
                       /\ 0 <= (-1 + -param0:120 + param2:126)
                       /\ 0 <= __cost:163 /\ 0 <= (-1 + mid___cost:261)
                       /\ 0 <= (-1 + param2:126 + -mid_x:260)
                       /\ 0 <= (param3:129 + -mid_y:259)))
           /\ (0 = K:258 \/ (param1:123 + -param3:129) < 0)
           /\ (!(0 <= K:262) \/ __cost':263 = (mid___cost:261 + K:262))
           /\ (!(0 <= K:262) \/ x':264 = (mid_x:260 + K:262))
           /\ (!(0 <= K:262) \/ y':265 = mid_y:259)
           /\ ((K:262 = 0 /\ mid_y:259 = y':265 /\ mid_x:260 = x':264
                  /\ mid___cost:261 = __cost':263)
                 \/ (1 <= K:262 /\ 0 <= (-1 + -mid_x:260 + param2:126)
                       /\ 0 <= mid___cost:261
                       /\ 0 <= (mid_y:259 + -param3:129)
                       /\ 0 <= (-param3:129 + y':265)
                       /\ 0 <= (-1 + __cost':263)
                       /\ 0 <= (param2:126 + -x':264)))
           /\ (0 = K:262 \/ !((mid_y:259 + -param3:129) < 0))
           /\ (K:258 + K:262) = K:266
           /\ (!(0 <= K:267) \/ mid_y:268 = (param1:123 + K:267))
           /\ (!(0 <= K:267) \/ mid_x:269 = param0:120)
           /\ (!(0 <= K:267) \/ mid___cost:270 = (__cost:163 + K:267))
           /\ ((K:267 = 0 /\ param1:123 = mid_y:268 /\ param0:120 = mid_x:269
                  /\ __cost:163 = mid___cost:270)
                 \/ (1 <= K:267 /\ 0 <= (-1 + -param1:123 + param3:129)
                       /\ 0 <= (-1 + -param0:120 + param2:126)
                       /\ 0 <= __cost:163 /\ 0 <= (-1 + mid___cost:270)
                       /\ 0 <= (-1 + param2:126 + -mid_x:269)
                       /\ 0 <= (param3:129 + -mid_y:268)))
           /\ (0 = K:267 \/ !((-param1:123 + param3:129) <= 0))
           /\ (!(0 <= K:271) \/ __cost':263 = (mid___cost:270 + K:271))
           /\ (!(0 <= K:271) \/ x':264 = (mid_x:269 + K:271))
           /\ (!(0 <= K:271) \/ y':265 = mid_y:268)
           /\ ((K:271 = 0 /\ mid_y:268 = y':265 /\ mid_x:269 = x':264
                  /\ mid___cost:270 = __cost':263)
                 \/ (1 <= K:271 /\ 0 <= (-1 + -mid_x:269 + param2:126)
                       /\ 0 <= mid___cost:270
                       /\ 0 <= (mid_y:268 + -param3:129)
                       /\ 0 <= (-param3:129 + y':265)
                       /\ 0 <= (-1 + __cost':263)
                       /\ 0 <= (param2:126 + -x':264)))
           /\ (0 = K:271 \/ (-mid_y:268 + param3:129) <= 0)
           /\ (K:267 + K:271) = K:266 /\ 0 <= K:266 /\ param2:126 <= x':264)})



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
         x := havoc:35
         y := havoc:36
         n := havoc:37
         m := havoc:38
         param0 := havoc:35
         param1 := havoc:36
         param2 := havoc:37
         param3 := havoc:38
         param0@pos := type_err:43
         param1@pos := type_err:45
         param2@pos := type_err:47
         param3@pos := type_err:49
         param0@width := type_err:44
         param1@width := type_err:46
         param2@width := type_err:48
         param3@width := type_err:50}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:52
       return@width := type_err:53
       when (((x:8 < n:9 /\ (n:9 + -x:8) = phi_tmp___3:39)
                \/ (n:9 <= x:8 /\ 0 = phi_tmp___3:39))
               /\ ((y:10 < m:11 /\ (m:11 + -y:10) = phi_tmp___4:51)
                     \/ (m:11 <= y:10 /\ 0 = phi_tmp___4:51)))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:120
         param1 := param1:123
         param2 := param2:126
         param3 := param3:129
         param0@pos := type_err:138
         param1@pos := type_err:139
         param2@pos := type_err:140
         param3@pos := type_err:141
         param0@width := type_err:142
         param1@width := type_err:143
         param2@width := type_err:144
         param3@width := type_err:145}      )
      ,
      Var(19)
    )
    ,
    Weight(Base relation: 
      {return := havoc:93
       return@pos := type_err:96
       return@width := type_err:97}    )
  )
)



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

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



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':300
   return := 0
   param0 := havoc:35
   param1 := havoc:36
   param2 := havoc:37
   param3 := havoc:38
   return@pos := type_err:322
   param0@pos := type_err:311
   param1@pos := type_err:312
   param2@pos := type_err:313
   param3@pos := type_err:314
   return@width := type_err:323
   param0@width := type_err:316
   param1@width := type_err:317
   param2@width := type_err:318
   param3@width := type_err:319
   when ((!(0 <= K:295) \/ mid_y:296 = (havoc:36 + K:295))
           /\ (!(0 <= K:295) \/ mid_x:297 = havoc:35)
           /\ (!(0 <= K:295) \/ mid___cost:298 = K:295)
           /\ ((K:295 = 0 /\ havoc:36 = mid_y:296 /\ havoc:35 = mid_x:297
                  /\ 0 = mid___cost:298)
                 \/ (1 <= K:295 /\ 0 <= (-1 + -havoc:36 + havoc:38)
                       /\ 0 <= (-1 + -havoc:35 + havoc:37)
                       /\ 0 <= (-1 + mid___cost:298)
                       /\ 0 <= (-1 + havoc:37 + -mid_x:297)
                       /\ 0 <= (havoc:38 + -mid_y:296)))
           /\ (0 = K:295 \/ (havoc:36 + -havoc:38) < 0)
           /\ (!(0 <= K:299) \/ __cost':300 = (mid___cost:298 + K:299))
           /\ (!(0 <= K:299) \/ x':301 = (mid_x:297 + K:299))
           /\ (!(0 <= K:299) \/ y':302 = mid_y:296)
           /\ ((K:299 = 0 /\ mid_y:296 = y':302 /\ mid_x:297 = x':301
                  /\ mid___cost:298 = __cost':300)
                 \/ (1 <= K:299 /\ 0 <= (-1 + -mid_x:297 + havoc:37)
                       /\ 0 <= mid___cost:298 /\ 0 <= (mid_y:296 + -havoc:38)
                       /\ 0 <= (-havoc:38 + y':302)
                       /\ 0 <= (-1 + __cost':300)
                       /\ 0 <= (havoc:37 + -x':301)))
           /\ (0 = K:299 \/ !((mid_y:296 + -havoc:38) < 0))
           /\ (K:295 + K:299) = K:303
           /\ (!(0 <= K:304) \/ mid_y:305 = (havoc:36 + K:304))
           /\ (!(0 <= K:304) \/ mid_x:306 = havoc:35)
           /\ (!(0 <= K:304) \/ mid___cost:307 = K:304)
           /\ ((K:304 = 0 /\ havoc:36 = mid_y:305 /\ havoc:35 = mid_x:306
                  /\ 0 = mid___cost:307)
                 \/ (1 <= K:304 /\ 0 <= (-1 + -havoc:36 + havoc:38)
                       /\ 0 <= (-1 + -havoc:35 + havoc:37)
                       /\ 0 <= (-1 + mid___cost:307)
                       /\ 0 <= (-1 + havoc:37 + -mid_x:306)
                       /\ 0 <= (havoc:38 + -mid_y:305)))
           /\ (0 = K:304 \/ !((-havoc:36 + havoc:38) <= 0))
           /\ (!(0 <= K:308) \/ __cost':300 = (mid___cost:307 + K:308))
           /\ (!(0 <= K:308) \/ x':301 = (mid_x:306 + K:308))
           /\ (!(0 <= K:308) \/ y':302 = mid_y:305)
           /\ ((K:308 = 0 /\ mid_y:305 = y':302 /\ mid_x:306 = x':301
                  /\ mid___cost:307 = __cost':300)
                 \/ (1 <= K:308 /\ 0 <= (-1 + -mid_x:306 + havoc:37)
                       /\ 0 <= mid___cost:307 /\ 0 <= (mid_y:305 + -havoc:38)
                       /\ 0 <= (-havoc:38 + y':302)
                       /\ 0 <= (-1 + __cost':300)
                       /\ 0 <= (havoc:37 + -x':301)))
           /\ (0 = K:308 \/ (-mid_y:305 + havoc:38) <= 0)
           /\ (K:304 + K:308) = K:303 /\ 0 <= K:303 /\ havoc:37 <= x':301
           /\ ((havoc:35 < havoc:37
                  /\ (havoc:37 + -havoc:35) = phi_tmp___3:320)
                 \/ (havoc:37 <= havoc:35 /\ 0 = phi_tmp___3:320))
           /\ ((havoc:36 < havoc:38
                  /\ (havoc:38 + -havoc:36) = phi_tmp___4:321)
                 \/ (havoc:38 <= havoc:36 /\ 0 = phi_tmp___4:321)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':329
   return := havoc:341
   param0 := param0:120
   param1 := param1:123
   param2 := param2:126
   param3 := param3:129
   return@pos := type_err:342
   param0@pos := type_err:138
   param1@pos := type_err:139
   param2@pos := type_err:140
   param3@pos := type_err:141
   return@width := type_err:343
   param0@width := type_err:142
   param1@width := type_err:143
   param2@width := type_err:144
   param3@width := type_err:145
   when ((!(0 <= K:324) \/ mid_y:325 = (param1:123 + K:324))
           /\ (!(0 <= K:324) \/ mid_x:326 = param0:120)
           /\ (!(0 <= K:324) \/ mid___cost:327 = (__cost:163 + K:324))
           /\ ((K:324 = 0 /\ param1:123 = mid_y:325 /\ param0:120 = mid_x:326
                  /\ __cost:163 = mid___cost:327)
                 \/ (1 <= K:324 /\ 0 <= (-1 + -param1:123 + param3:129)
                       /\ 0 <= (-1 + -param0:120 + param2:126)
                       /\ 0 <= __cost:163 /\ 0 <= (-1 + mid___cost:327)
                       /\ 0 <= (-1 + param2:126 + -mid_x:326)
                       /\ 0 <= (param3:129 + -mid_y:325)))
           /\ (0 = K:324 \/ (param1:123 + -param3:129) < 0)
           /\ (!(0 <= K:328) \/ __cost':329 = (mid___cost:327 + K:328))
           /\ (!(0 <= K:328) \/ x':330 = (mid_x:326 + K:328))
           /\ (!(0 <= K:328) \/ y':331 = mid_y:325)
           /\ ((K:328 = 0 /\ mid_y:325 = y':331 /\ mid_x:326 = x':330
                  /\ mid___cost:327 = __cost':329)
                 \/ (1 <= K:328 /\ 0 <= (-1 + -mid_x:326 + param2:126)
                       /\ 0 <= mid___cost:327
                       /\ 0 <= (mid_y:325 + -param3:129)
                       /\ 0 <= (-param3:129 + y':331)
                       /\ 0 <= (-1 + __cost':329)
                       /\ 0 <= (param2:126 + -x':330)))
           /\ (0 = K:328 \/ !((mid_y:325 + -param3:129) < 0))
           /\ (K:324 + K:328) = K:332
           /\ (!(0 <= K:333) \/ mid_y:334 = (param1:123 + K:333))
           /\ (!(0 <= K:333) \/ mid_x:335 = param0:120)
           /\ (!(0 <= K:333) \/ mid___cost:336 = (__cost:163 + K:333))
           /\ ((K:333 = 0 /\ param1:123 = mid_y:334 /\ param0:120 = mid_x:335
                  /\ __cost:163 = mid___cost:336)
                 \/ (1 <= K:333 /\ 0 <= (-1 + -param1:123 + param3:129)
                       /\ 0 <= (-1 + -param0:120 + param2:126)
                       /\ 0 <= __cost:163 /\ 0 <= (-1 + mid___cost:336)
                       /\ 0 <= (-1 + param2:126 + -mid_x:335)
                       /\ 0 <= (param3:129 + -mid_y:334)))
           /\ (0 = K:333 \/ !((-param1:123 + param3:129) <= 0))
           /\ (!(0 <= K:337) \/ __cost':329 = (mid___cost:336 + K:337))
           /\ (!(0 <= K:337) \/ x':330 = (mid_x:335 + K:337))
           /\ (!(0 <= K:337) \/ y':331 = mid_y:334)
           /\ ((K:337 = 0 /\ mid_y:334 = y':331 /\ mid_x:335 = x':330
                  /\ mid___cost:336 = __cost':329)
                 \/ (1 <= K:337 /\ 0 <= (-1 + -mid_x:335 + param2:126)
                       /\ 0 <= mid___cost:336
                       /\ 0 <= (mid_y:334 + -param3:129)
                       /\ 0 <= (-param3:129 + y':331)
                       /\ 0 <= (-1 + __cost':329)
                       /\ 0 <= (param2:126 + -x':330)))
           /\ (0 = K:337 \/ (-mid_y:334 + param3:129) <= 0)
           /\ (K:333 + K:337) = K:332 /\ 0 <= K:332 /\ param2:126 <= x':330)})


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


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':300
 return := 0
 param0 := havoc:35
 param1 := havoc:36
 param2 := havoc:37
 param3 := havoc:38
 return@pos := type_err:322
 param0@pos := type_err:311
 param1@pos := type_err:312
 param2@pos := type_err:313
 param3@pos := type_err:314
 return@width := type_err:323
 param0@width := type_err:316
 param1@width := type_err:317
 param2@width := type_err:318
 param3@width := type_err:319
 when ((!(0 <= K:295) \/ mid_y:296 = (havoc:36 + K:295))
         /\ (!(0 <= K:295) \/ mid_x:297 = havoc:35)
         /\ (!(0 <= K:295) \/ mid___cost:298 = K:295)
         /\ ((K:295 = 0 /\ havoc:36 = mid_y:296 /\ havoc:35 = mid_x:297
                /\ 0 = mid___cost:298)
               \/ (1 <= K:295 /\ 0 <= (-1 + -havoc:36 + havoc:38)
                     /\ 0 <= (-1 + -havoc:35 + havoc:37)
                     /\ 0 <= (-1 + mid___cost:298)
                     /\ 0 <= (-1 + havoc:37 + -mid_x:297)
                     /\ 0 <= (havoc:38 + -mid_y:296)))
         /\ (0 = K:295 \/ (havoc:36 + -havoc:38) < 0)
         /\ (!(0 <= K:299) \/ __cost':300 = (mid___cost:298 + K:299))
         /\ (!(0 <= K:299) \/ x':301 = (mid_x:297 + K:299))
         /\ (!(0 <= K:299) \/ y':302 = mid_y:296)
         /\ ((K:299 = 0 /\ mid_y:296 = y':302 /\ mid_x:297 = x':301
                /\ mid___cost:298 = __cost':300)
               \/ (1 <= K:299 /\ 0 <= (-1 + -mid_x:297 + havoc:37)
                     /\ 0 <= mid___cost:298 /\ 0 <= (mid_y:296 + -havoc:38)
                     /\ 0 <= (-havoc:38 + y':302) /\ 0 <= (-1 + __cost':300)
                     /\ 0 <= (havoc:37 + -x':301)))
         /\ (0 = K:299 \/ !((mid_y:296 + -havoc:38) < 0))
         /\ (K:295 + K:299) = K:303
         /\ (!(0 <= K:304) \/ mid_y:305 = (havoc:36 + K:304))
         /\ (!(0 <= K:304) \/ mid_x:306 = havoc:35)
         /\ (!(0 <= K:304) \/ mid___cost:307 = K:304)
         /\ ((K:304 = 0 /\ havoc:36 = mid_y:305 /\ havoc:35 = mid_x:306
                /\ 0 = mid___cost:307)
               \/ (1 <= K:304 /\ 0 <= (-1 + -havoc:36 + havoc:38)
                     /\ 0 <= (-1 + -havoc:35 + havoc:37)
                     /\ 0 <= (-1 + mid___cost:307)
                     /\ 0 <= (-1 + havoc:37 + -mid_x:306)
                     /\ 0 <= (havoc:38 + -mid_y:305)))
         /\ (0 = K:304 \/ !((-havoc:36 + havoc:38) <= 0))
         /\ (!(0 <= K:308) \/ __cost':300 = (mid___cost:307 + K:308))
         /\ (!(0 <= K:308) \/ x':301 = (mid_x:306 + K:308))
         /\ (!(0 <= K:308) \/ y':302 = mid_y:305)
         /\ ((K:308 = 0 /\ mid_y:305 = y':302 /\ mid_x:306 = x':301
                /\ mid___cost:307 = __cost':300)
               \/ (1 <= K:308 /\ 0 <= (-1 + -mid_x:306 + havoc:37)
                     /\ 0 <= mid___cost:307 /\ 0 <= (mid_y:305 + -havoc:38)
                     /\ 0 <= (-havoc:38 + y':302) /\ 0 <= (-1 + __cost':300)
                     /\ 0 <= (havoc:37 + -x':301)))
         /\ (0 = K:308 \/ (-mid_y:305 + havoc:38) <= 0)
         /\ (K:304 + K:308) = K:303 /\ 0 <= K:303 /\ havoc:37 <= x':301
         /\ ((havoc:35 < havoc:37 /\ (havoc:37 + -havoc:35) = phi_tmp___3:320)
               \/ (havoc:37 <= havoc:35 /\ 0 = phi_tmp___3:320))
         /\ ((havoc:36 < havoc:38 /\ (havoc:38 + -havoc:36) = phi_tmp___4:321)
               \/ (havoc:38 <= havoc:36 /\ 0 = phi_tmp___4:321)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':329
 return := havoc:341
 param0 := param0:120
 param1 := param1:123
 param2 := param2:126
 param3 := param3:129
 return@pos := type_err:342
 param0@pos := type_err:138
 param1@pos := type_err:139
 param2@pos := type_err:140
 param3@pos := type_err:141
 return@width := type_err:343
 param0@width := type_err:142
 param1@width := type_err:143
 param2@width := type_err:144
 param3@width := type_err:145
 when ((!(0 <= K:324) \/ mid_y:325 = (param1:123 + K:324))
         /\ (!(0 <= K:324) \/ mid_x:326 = param0:120)
         /\ (!(0 <= K:324) \/ mid___cost:327 = (__cost:163 + K:324))
         /\ ((K:324 = 0 /\ param1:123 = mid_y:325 /\ param0:120 = mid_x:326
                /\ __cost:163 = mid___cost:327)
               \/ (1 <= K:324 /\ 0 <= (-1 + -param1:123 + param3:129)
                     /\ 0 <= (-1 + -param0:120 + param2:126)
                     /\ 0 <= __cost:163 /\ 0 <= (-1 + mid___cost:327)
                     /\ 0 <= (-1 + param2:126 + -mid_x:326)
                     /\ 0 <= (param3:129 + -mid_y:325)))
         /\ (0 = K:324 \/ (param1:123 + -param3:129) < 0)
         /\ (!(0 <= K:328) \/ __cost':329 = (mid___cost:327 + K:328))
         /\ (!(0 <= K:328) \/ x':330 = (mid_x:326 + K:328))
         /\ (!(0 <= K:328) \/ y':331 = mid_y:325)
         /\ ((K:328 = 0 /\ mid_y:325 = y':331 /\ mid_x:326 = x':330
                /\ mid___cost:327 = __cost':329)
               \/ (1 <= K:328 /\ 0 <= (-1 + -mid_x:326 + param2:126)
                     /\ 0 <= mid___cost:327 /\ 0 <= (mid_y:325 + -param3:129)
                     /\ 0 <= (-param3:129 + y':331)
                     /\ 0 <= (-1 + __cost':329)
                     /\ 0 <= (param2:126 + -x':330)))
         /\ (0 = K:328 \/ !((mid_y:325 + -param3:129) < 0))
         /\ (K:324 + K:328) = K:332
         /\ (!(0 <= K:333) \/ mid_y:334 = (param1:123 + K:333))
         /\ (!(0 <= K:333) \/ mid_x:335 = param0:120)
         /\ (!(0 <= K:333) \/ mid___cost:336 = (__cost:163 + K:333))
         /\ ((K:333 = 0 /\ param1:123 = mid_y:334 /\ param0:120 = mid_x:335
                /\ __cost:163 = mid___cost:336)
               \/ (1 <= K:333 /\ 0 <= (-1 + -param1:123 + param3:129)
                     /\ 0 <= (-1 + -param0:120 + param2:126)
                     /\ 0 <= __cost:163 /\ 0 <= (-1 + mid___cost:336)
                     /\ 0 <= (-1 + param2:126 + -mid_x:335)
                     /\ 0 <= (param3:129 + -mid_y:334)))
         /\ (0 = K:333 \/ !((-param1:123 + param3:129) <= 0))
         /\ (!(0 <= K:337) \/ __cost':329 = (mid___cost:336 + K:337))
         /\ (!(0 <= K:337) \/ x':330 = (mid_x:335 + K:337))
         /\ (!(0 <= K:337) \/ y':331 = mid_y:334)
         /\ ((K:337 = 0 /\ mid_y:334 = y':331 /\ mid_x:335 = x':330
                /\ mid___cost:336 = __cost':329)
               \/ (1 <= K:337 /\ 0 <= (-1 + -mid_x:335 + param2:126)
                     /\ 0 <= mid___cost:336 /\ 0 <= (mid_y:334 + -param3:129)
                     /\ 0 <= (-param3:129 + y':331)
                     /\ 0 <= (-1 + __cost':329)
                     /\ 0 <= (param2:126 + -x':330)))
         /\ (0 = K:337 \/ (-mid_y:334 + param3:129) <= 0)
         /\ (K:333 + K:337) = K:332 /\ 0 <= K:332 /\ param2:126 <= x':330)}

Evaluating variable number 19 (using IRE) 

  The IRE-evaluated value on this round is: 

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

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,66)_g1> -> <__pstate, (Unique State Name,56)_g1>	Base relation: 
{param0 := param0:120
 param1 := param1:123
 param2 := param2:126
 param3 := param3:129
 param0@pos := type_err:138
 param1@pos := type_err:139
 param2@pos := type_err:140
 param3@pos := type_err:141
 param0@width := type_err:142
 param1@width := type_err:143
 param2@width := type_err:144
 param3@width := type_err:145}	
<__pstate, accept> -> <__pstate, (Unique State Name,66)_g1>	Base relation: 
{__cost := 0
 x := havoc:35
 y := havoc:36
 n := havoc:37
 m := havoc:38
 param0 := havoc:35
 param1 := havoc:36
 param2 := havoc:37
 param3 := havoc:38
 param0@pos := type_err:43
 param1@pos := type_err:45
 param2@pos := type_err:47
 param3@pos := type_err:49
 param0@width := type_err:44
 param1@width := type_err:46
 param2@width := type_err:48
 param3@width := type_err:50}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x4a59600: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x4a592c0: 
	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,56)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:35
 y := havoc:36
 n := havoc:37
 m := havoc:38
 param0 := havoc:35
 param1 := havoc:36
 param2 := havoc:37
 param3 := havoc:38
 param0@pos := type_err:393
 param1@pos := type_err:394
 param2@pos := type_err:395
 param3@pos := type_err:396
 param0@width := type_err:397
 param1@width := type_err:398
 param2@width := type_err:399
 param3@width := type_err:400}
    ( __pstate , (Unique State Name,66)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:35
 y := havoc:36
 n := havoc:37
 m := havoc:38
 param0 := havoc:35
 param1 := havoc:36
 param2 := havoc:37
 param3 := havoc:38
 param0@pos := type_err:43
 param1@pos := type_err:45
 param2@pos := type_err:47
 param3@pos := type_err:49
 param0@width := type_err:44
 param1@width := type_err:46
 param2@width := type_err:48
 param3@width := type_err:50}

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

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

Base relation: 
{__cost := __cost':349
 x := havoc:35
 y := havoc:36
 n := havoc:37
 m := havoc:38
 return := 0
 param0 := havoc:35
 param1 := havoc:36
 param2 := havoc:37
 param3 := havoc:38
 return@pos := type_err:371
 param0@pos := type_err:360
 param1@pos := type_err:361
 param2@pos := type_err:362
 param3@pos := type_err:363
 return@width := type_err:372
 param0@width := type_err:365
 param1@width := type_err:366
 param2@width := type_err:367
 param3@width := type_err:368
 when ((!(0 <= K:344) \/ mid_y:345 = (havoc:36 + K:344))
         /\ (!(0 <= K:344) \/ mid_x:346 = havoc:35)
         /\ (!(0 <= K:344) \/ mid___cost:347 = K:344)
         /\ ((K:344 = 0 /\ havoc:36 = mid_y:345 /\ havoc:35 = mid_x:346
                /\ 0 = mid___cost:347)
               \/ (1 <= K:344 /\ 0 <= (-1 + -havoc:36 + havoc:38)
                     /\ 0 <= (-1 + -havoc:35 + havoc:37)
                     /\ 0 <= (-1 + mid___cost:347)
                     /\ 0 <= (-1 + havoc:37 + -mid_x:346)
                     /\ 0 <= (havoc:38 + -mid_y:345)))
         /\ (0 = K:344 \/ (havoc:36 + -havoc:38) < 0)
         /\ (!(0 <= K:348) \/ __cost':349 = (mid___cost:347 + K:348))
         /\ (!(0 <= K:348) \/ x':350 = (mid_x:346 + K:348))
         /\ (!(0 <= K:348) \/ y':351 = mid_y:345)
         /\ ((K:348 = 0 /\ mid_y:345 = y':351 /\ mid_x:346 = x':350
                /\ mid___cost:347 = __cost':349)
               \/ (1 <= K:348 /\ 0 <= (-1 + -mid_x:346 + havoc:37)
                     /\ 0 <= mid___cost:347 /\ 0 <= (mid_y:345 + -havoc:38)
                     /\ 0 <= (-havoc:38 + y':351) /\ 0 <= (-1 + __cost':349)
                     /\ 0 <= (havoc:37 + -x':350)))
         /\ (0 = K:348 \/ !((mid_y:345 + -havoc:38) < 0))
         /\ (K:344 + K:348) = K:352
         /\ (!(0 <= K:353) \/ mid_y:354 = (havoc:36 + K:353))
         /\ (!(0 <= K:353) \/ mid_x:355 = havoc:35)
         /\ (!(0 <= K:353) \/ mid___cost:356 = K:353)
         /\ ((K:353 = 0 /\ havoc:36 = mid_y:354 /\ havoc:35 = mid_x:355
                /\ 0 = mid___cost:356)
               \/ (1 <= K:353 /\ 0 <= (-1 + -havoc:36 + havoc:38)
                     /\ 0 <= (-1 + -havoc:35 + havoc:37)
                     /\ 0 <= (-1 + mid___cost:356)
                     /\ 0 <= (-1 + havoc:37 + -mid_x:355)
                     /\ 0 <= (havoc:38 + -mid_y:354)))
         /\ (0 = K:353 \/ !((-havoc:36 + havoc:38) <= 0))
         /\ (!(0 <= K:357) \/ __cost':349 = (mid___cost:356 + K:357))
         /\ (!(0 <= K:357) \/ x':350 = (mid_x:355 + K:357))
         /\ (!(0 <= K:357) \/ y':351 = mid_y:354)
         /\ ((K:357 = 0 /\ mid_y:354 = y':351 /\ mid_x:355 = x':350
                /\ mid___cost:356 = __cost':349)
               \/ (1 <= K:357 /\ 0 <= (-1 + -mid_x:355 + havoc:37)
                     /\ 0 <= mid___cost:356 /\ 0 <= (mid_y:354 + -havoc:38)
                     /\ 0 <= (-havoc:38 + y':351) /\ 0 <= (-1 + __cost':349)
                     /\ 0 <= (havoc:37 + -x':350)))
         /\ (0 = K:357 \/ (-mid_y:354 + havoc:38) <= 0)
         /\ (K:353 + K:357) = K:352 /\ 0 <= K:352 /\ havoc:37 <= x':350
         /\ ((havoc:35 < havoc:37 /\ (havoc:37 + -havoc:35) = phi_tmp___3:369)
               \/ (havoc:37 <= havoc:35 /\ 0 = phi_tmp___3:369))
         /\ ((havoc:36 < havoc:38 /\ (havoc:38 + -havoc:36) = phi_tmp___4:370)
               \/ (havoc:38 <= havoc:36 /\ 0 = phi_tmp___4:370)))}

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

Base relation: 
{__cost := __cost':378
 return := havoc:390
 param0 := param0:120
 param1 := param1:123
 param2 := param2:126
 param3 := param3:129
 return@pos := type_err:391
 param0@pos := type_err:138
 param1@pos := type_err:139
 param2@pos := type_err:140
 param3@pos := type_err:141
 return@width := type_err:392
 param0@width := type_err:142
 param1@width := type_err:143
 param2@width := type_err:144
 param3@width := type_err:145
 when ((!(0 <= K:373) \/ mid_y:374 = (param1:123 + K:373))
         /\ (!(0 <= K:373) \/ mid_x:375 = param0:120)
         /\ (!(0 <= K:373) \/ mid___cost:376 = (__cost:163 + K:373))
         /\ ((K:373 = 0 /\ param1:123 = mid_y:374 /\ param0:120 = mid_x:375
                /\ __cost:163 = mid___cost:376)
               \/ (1 <= K:373 /\ 0 <= (-1 + -param1:123 + param3:129)
                     /\ 0 <= (-1 + -param0:120 + param2:126)
                     /\ 0 <= __cost:163 /\ 0 <= (-1 + mid___cost:376)
                     /\ 0 <= (-1 + param2:126 + -mid_x:375)
                     /\ 0 <= (param3:129 + -mid_y:374)))
         /\ (0 = K:373 \/ (param1:123 + -param3:129) < 0)
         /\ (!(0 <= K:377) \/ __cost':378 = (mid___cost:376 + K:377))
         /\ (!(0 <= K:377) \/ x':379 = (mid_x:375 + K:377))
         /\ (!(0 <= K:377) \/ y':380 = mid_y:374)
         /\ ((K:377 = 0 /\ mid_y:374 = y':380 /\ mid_x:375 = x':379
                /\ mid___cost:376 = __cost':378)
               \/ (1 <= K:377 /\ 0 <= (-1 + -mid_x:375 + param2:126)
                     /\ 0 <= mid___cost:376 /\ 0 <= (mid_y:374 + -param3:129)
                     /\ 0 <= (-param3:129 + y':380)
                     /\ 0 <= (-1 + __cost':378)
                     /\ 0 <= (param2:126 + -x':379)))
         /\ (0 = K:377 \/ !((mid_y:374 + -param3:129) < 0))
         /\ (K:373 + K:377) = K:381
         /\ (!(0 <= K:382) \/ mid_y:383 = (param1:123 + K:382))
         /\ (!(0 <= K:382) \/ mid_x:384 = param0:120)
         /\ (!(0 <= K:382) \/ mid___cost:385 = (__cost:163 + K:382))
         /\ ((K:382 = 0 /\ param1:123 = mid_y:383 /\ param0:120 = mid_x:384
                /\ __cost:163 = mid___cost:385)
               \/ (1 <= K:382 /\ 0 <= (-1 + -param1:123 + param3:129)
                     /\ 0 <= (-1 + -param0:120 + param2:126)
                     /\ 0 <= __cost:163 /\ 0 <= (-1 + mid___cost:385)
                     /\ 0 <= (-1 + param2:126 + -mid_x:384)
                     /\ 0 <= (param3:129 + -mid_y:383)))
         /\ (0 = K:382 \/ !((-param1:123 + param3:129) <= 0))
         /\ (!(0 <= K:386) \/ __cost':378 = (mid___cost:385 + K:386))
         /\ (!(0 <= K:386) \/ x':379 = (mid_x:384 + K:386))
         /\ (!(0 <= K:386) \/ y':380 = mid_y:383)
         /\ ((K:386 = 0 /\ mid_y:383 = y':380 /\ mid_x:384 = x':379
                /\ mid___cost:385 = __cost':378)
               \/ (1 <= K:386 /\ 0 <= (-1 + -mid_x:384 + param2:126)
                     /\ 0 <= mid___cost:385 /\ 0 <= (mid_y:383 + -param3:129)
                     /\ 0 <= (-param3:129 + y':380)
                     /\ 0 <= (-1 + __cost':378)
                     /\ 0 <= (param2:126 + -x':379)))
         /\ (0 = K:386 \/ (-mid_y:383 + param3:129) <= 0)
         /\ (K:382 + K:386) = K:381 /\ 0 <= K:381 /\ param2:126 <= x':379)}

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

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

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

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

Variable bounds at line 19 in run

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

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