/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, 45> -> <Unique State Name, 53>	Base relation: 
{tmp := havoc:173
 when y:163 < m:164}	
<Unique State Name, 45> -> <Unique State Name, 63>	Base relation: 
{when m:164 <= y:163}	
<Unique State Name, 29> -> <Unique State Name, 92>	Base relation: 
{return := havoc:93
 return@pos := type_err:96
 return@width := type_err:97}	
<Unique State Name, 27> -> <Unique State Name, 90>	Base relation: 
{__cost := 0
 x := havoc:35
 y := havoc:36
 n := havoc:37
 m := havoc:38
 param0 := havoc:35
 param1 := havoc:37
 param2 := havoc:36
 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, 33> -> <Unique State Name, 95>	Base relation: 
{}	
<Unique State Name, 63> -> <Unique State Name, 33>	Base relation: 
{x := (x:161 + 1)}	
<Unique State Name, 89> -> <Unique State Name, 93>	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, 81> -> <Unique State Name, 80>	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, 93> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 79> -> <Unique State Name, 29>	Base relation: 
{}	
<Unique State Name, 91> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 53> -> <Unique State Name, 41>	Base relation: 
{__cost := (__cost:167 + 1)
 y := (y:163 + 1)
 when (tmp:166 = 0 /\ 0 <= __cost:167 /\ 0 <= (__cost:167 + 1))}	
<Unique State Name, 53> -> <Unique State Name, 63>	Base relation: 
{when !(tmp:166 = 0)}	
<Unique State Name, 92> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 94> -> <Unique State Name, 45>	Base relation: 
{}	
<Unique State Name, 80> -> <Unique State Name, 71 79>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 71> -> <Unique State Name, 33>	Base relation: 
{x := param0:120
 n := param1:123
 y := param2:126
 m := param3:129}	
<Unique State Name, 95> -> <Unique State Name, 37>	Base relation: 
{}	
<Unique State Name, 90> -> <Unique State Name, 81 89>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 41> -> <Unique State Name, 94>	Base relation: 
{}	
<Unique State Name, 37> -> <Unique State Name, 41>	Base relation: 
{when x:161 < n:162}	
<Unique State Name, 37> -> <Unique State Name, 91>	Base relation: 
{return := havoc:174
 return@pos := type_err:175
 return@width := type_err:176
 when n:162 <= x:161}	
#################################################################
           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:167 + 1)
 tmp := havoc:173
 y := (y:163 + 1)
 when (y:163 < m:164 /\ havoc:173 = 0 /\ 0 <= __cost:167
         /\ 0 <= (__cost:167 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':249) = (1)*(__cost:167) + 1
           (tmp':250) = 0
           (y':251) = (1)*(y:163) + 1
           }
          pre:
            [|-y:163+m:164-1>=0; __cost:167>=0|]
          post:
            [|tmp':250=0; __cost':249-1>=0; m:164-y':251>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':249
   tmp := tmp':250
   y := y':251
   when ((!(0 <= K:263) \/ mid___cost:267 = (__cost:167 + K:263))
           /\ (!((0 <= K:263 /\ K:263 <= 0)) \/ mid_tmp:266 = tmp:166)
           /\ (!(1 <= K:263) \/ mid_tmp:266 = 0)
           /\ (!(0 <= K:263) \/ mid_y:265 = (y:163 + K:263))
           /\ ((K:263 = 0 /\ y:163 = mid_y:265 /\ tmp:166 = mid_tmp:266
                  /\ __cost:167 = mid___cost:267)
                 \/ (1 <= K:263 /\ 0 <= (-1 + -y:163 + m:164)
                       /\ 0 <= __cost:167 /\ mid_tmp:266 = 0
                       /\ 0 <= (-1 + mid___cost:267)
                       /\ 0 <= (m:164 + -mid_y:265))) /\ K:264 = 0
           /\ mid_y:265 = y':251 /\ mid_tmp:266 = tmp':250
           /\ mid___cost:267 = __cost':249 /\ 0 = K:264
           /\ (K:263 + K:264) = K:262 /\ 0 <= K:262)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':275
 tmp := phi_tmp:278
 x := (x:161 + 1)
 y := y':273
 when (x:161 < n:162
         /\ (!(0 <= K:268) \/ mid___cost:269 = (__cost:167 + K:268))
         /\ (!((0 <= K:268 /\ K:268 <= 0)) \/ mid_tmp:270 = tmp:166)
         /\ (!(1 <= K:268) \/ mid_tmp:270 = 0)
         /\ (!(0 <= K:268) \/ mid_y:271 = (y:163 + K:268))
         /\ ((K:268 = 0 /\ y:163 = mid_y:271 /\ tmp:166 = mid_tmp:270
                /\ __cost:167 = mid___cost:269)
               \/ (1 <= K:268 /\ 0 <= (-1 + -y:163 + m:164)
                     /\ 0 <= __cost:167 /\ mid_tmp:270 = 0
                     /\ 0 <= (-1 + mid___cost:269)
                     /\ 0 <= (m:164 + -mid_y:271))) /\ K:272 = 0
         /\ mid_y:271 = y':273 /\ mid_tmp:270 = tmp':274
         /\ mid___cost:269 = __cost':275 /\ 0 = K:272
         /\ (K:268 + K:272) = K:276 /\ 0 <= K:276
         /\ ((m:164 <= y':273 /\ tmp':274 = phi_tmp:278)
               \/ (y':273 < m:164 /\ !(havoc:279 = 0)
                     /\ havoc:279 = phi_tmp:278)))}
**** alpha hat: 
  {<Split [(1 + y:163 + -m:164) <= 0
            (x':280) = (1)*(x:161) + 1
           ((-y':251 + __cost':249)) = (1)*((-y:163 + __cost:167)) + 0
           (-y':251) <= (1)*(-y:163) + 0
           }
          pre:
            [|-x:161+n:162-1>=0; -y:163+m:164-1>=0|]
          post:
            [|-x':280+n:162>=0; -y':251+m:164>=0|]
           (x':280) = (1)*(x:161) + 1
          (y':251) = (1)*(y:163) + 0
          (tmp':250) = (1)*(tmp:166) + 0
          (__cost':249) = (1)*(__cost:167) + 0
          }
  pre:
    [|-x:161+n:162-1>=0; y:163-m:164>=0|]
  post:
    [|-m:164+y':251>=0; n:162-x':280>=0|]],
[!(-__cost:167 <= 0)
  (__cost':249) = (1)*(__cost:167) + 0
 (y':251) = (1)*(y:163) + 0
 (x':280) = (1)*(x:161) + 1
 } pre:   [|-__cost:167-1>=0; -x:161+n:162-1>=0|] post:
  [|-__cost':249-1>=0; -x':280+n:162>=0|]  (x':280) = (1)*(x:161) + 1
((-y':251 + __cost':249)) = (1)*((-y:163 + __cost:167)) + 0
(-y':251) <= (1)*(-y:163) + 0 } pre:   [|-x:161+n:162-1>=0; __cost:167>=0|]
post:
  [|-x':280+n:162>=0; __cost':249>=0|]]>}
**** star transition: 
  {__cost := __cost':249
   tmp := tmp':250
   x := x':280
   y := y':251
   when ((!(0 <= K:317) \/ mid_x:320 = (x:161 + K:317))
           /\ (!(0 <= K:317)
                 \/ (-mid_y:319 + mid___cost:322) = (-y:163 + __cost:167))
           /\ (!(0 <= K:317) \/ -mid_y:319 <= -y:163)
           /\ ((K:317 = 0 /\ y:163 = mid_y:319 /\ x:161 = mid_x:320
                  /\ tmp:166 = mid_tmp:321 /\ __cost:167 = mid___cost:322)
                 \/ (1 <= K:317 /\ 0 <= (-1 + -x:161 + n:162)
                       /\ 0 <= (-1 + -y:163 + m:164)
                       /\ 0 <= (-mid_x:320 + n:162)
                       /\ 0 <= (-mid_y:319 + m:164)))
           /\ (0 = K:317 \/ (1 + y:163 + -m:164) <= 0)
           /\ (!(0 <= K:318) \/ x':280 = (mid_x:320 + K:318))
           /\ (!(0 <= K:318) \/ y':251 = mid_y:319)
           /\ (!(0 <= K:318) \/ tmp':250 = mid_tmp:321)
           /\ (!(0 <= K:318) \/ __cost':249 = mid___cost:322)
           /\ ((K:318 = 0 /\ mid_y:319 = y':251 /\ mid_x:320 = x':280
                  /\ mid_tmp:321 = tmp':250 /\ mid___cost:322 = __cost':249)
                 \/ (1 <= K:318 /\ 0 <= (-1 + -mid_x:320 + n:162)
                       /\ 0 <= (mid_y:319 + -m:164) /\ 0 <= (-m:164 + y':251)
                       /\ 0 <= (n:162 + -x':280)))
           /\ (0 = K:318 \/ !((1 + mid_y:319 + -m:164) <= 0))
           /\ (K:317 + K:318) = K:316
           /\ (!(0 <= K:323) \/ mid___cost:328 = __cost:167)
           /\ (!(0 <= K:323) \/ mid_y:325 = y:163)
           /\ (!(0 <= K:323) \/ mid_x:326 = (x:161 + K:323))
           /\ ((K:323 = 0 /\ y:163 = mid_y:325 /\ x:161 = mid_x:326
                  /\ tmp:166 = mid_tmp:327 /\ __cost:167 = mid___cost:328)
                 \/ (1 <= K:323 /\ 0 <= (-1 + -__cost:167)
                       /\ 0 <= (-1 + -x:161 + n:162)
                       /\ 0 <= (-1 + -mid___cost:328)
                       /\ 0 <= (-mid_x:326 + n:162)))
           /\ (0 = K:323 \/ !(-__cost:167 <= 0))
           /\ (!(0 <= K:324) \/ x':280 = (mid_x:326 + K:324))
           /\ (!(0 <= K:324)
                 \/ (-y':251 + __cost':249) = (-mid_y:325 + mid___cost:328))
           /\ (!(0 <= K:324) \/ -y':251 <= -mid_y:325)
           /\ ((K:324 = 0 /\ mid_y:325 = y':251 /\ mid_x:326 = x':280
                  /\ mid_tmp:327 = tmp':250 /\ mid___cost:328 = __cost':249)
                 \/ (1 <= K:324 /\ 0 <= (-1 + -mid_x:326 + n:162)
                       /\ 0 <= mid___cost:328 /\ 0 <= (-x':280 + n:162)
                       /\ 0 <= __cost':249))
           /\ (0 = K:324 \/ -mid___cost:328 <= 0) /\ (K:323 + K:324) = K:316
           /\ 0 <= K:316)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  20  


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:37
       param2 := havoc:36
       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(20)
  )
  ,
  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=20: 
Weight(Base relation: 
  {__cost := __cost':338
   tmp := tmp':337
   x := x':335
   n := param1:123
   y := y':336
   m := param3:129
   return := havoc:367
   return@pos := type_err:368
   return@width := type_err:369
   when ((!(0 <= K:329) \/ mid_x:330 = (param0:120 + K:329))
           /\ (!(0 <= K:329)
                 \/ (-mid_y:331 + mid___cost:332) = (-param2:126 + __cost:167))
           /\ (!(0 <= K:329) \/ -mid_y:331 <= -param2:126)
           /\ ((K:329 = 0 /\ param2:126 = mid_y:331 /\ param0:120 = mid_x:330
                  /\ tmp:166 = mid_tmp:333 /\ __cost:167 = mid___cost:332)
                 \/ (1 <= K:329 /\ 0 <= (-1 + -param0:120 + param1:123)
                       /\ 0 <= (-1 + -param2:126 + param3:129)
                       /\ 0 <= (-mid_x:330 + param1:123)
                       /\ 0 <= (-mid_y:331 + param3:129)))
           /\ (0 = K:329 \/ (1 + param2:126 + -param3:129) <= 0)
           /\ (!(0 <= K:334) \/ x':335 = (mid_x:330 + K:334))
           /\ (!(0 <= K:334) \/ y':336 = mid_y:331)
           /\ (!(0 <= K:334) \/ tmp':337 = mid_tmp:333)
           /\ (!(0 <= K:334) \/ __cost':338 = mid___cost:332)
           /\ ((K:334 = 0 /\ mid_y:331 = y':336 /\ mid_x:330 = x':335
                  /\ mid_tmp:333 = tmp':337 /\ mid___cost:332 = __cost':338)
                 \/ (1 <= K:334 /\ 0 <= (-1 + -mid_x:330 + param1:123)
                       /\ 0 <= (mid_y:331 + -param3:129)
                       /\ 0 <= (-param3:129 + y':336)
                       /\ 0 <= (param1:123 + -x':335)))
           /\ (0 = K:334 \/ !((1 + mid_y:331 + -param3:129) <= 0))
           /\ (K:329 + K:334) = K:339
           /\ (!(0 <= K:340) \/ mid___cost:341 = __cost:167)
           /\ (!(0 <= K:340) \/ mid_y:342 = param2:126)
           /\ (!(0 <= K:340) \/ mid_x:343 = (param0:120 + K:340))
           /\ ((K:340 = 0 /\ param2:126 = mid_y:342 /\ param0:120 = mid_x:343
                  /\ tmp:166 = mid_tmp:344 /\ __cost:167 = mid___cost:341)
                 \/ (1 <= K:340 /\ 0 <= (-1 + -__cost:167)
                       /\ 0 <= (-1 + -param0:120 + param1:123)
                       /\ 0 <= (-1 + -mid___cost:341)
                       /\ 0 <= (-mid_x:343 + param1:123)))
           /\ (0 = K:340 \/ !(-__cost:167 <= 0))
           /\ (!(0 <= K:345) \/ x':335 = (mid_x:343 + K:345))
           /\ (!(0 <= K:345)
                 \/ (-y':336 + __cost':338) = (-mid_y:342 + mid___cost:341))
           /\ (!(0 <= K:345) \/ -y':336 <= -mid_y:342)
           /\ ((K:345 = 0 /\ mid_y:342 = y':336 /\ mid_x:343 = x':335
                  /\ mid_tmp:344 = tmp':337 /\ mid___cost:341 = __cost':338)
                 \/ (1 <= K:345 /\ 0 <= (-1 + -mid_x:343 + param1:123)
                       /\ 0 <= mid___cost:341 /\ 0 <= (-x':335 + param1:123)
                       /\ 0 <= __cost':338))
           /\ (0 = K:345 \/ -mid___cost:341 <= 0) /\ (K:340 + K:345) = K:339
           /\ 0 <= K:339 /\ param1:123 <= x':335)})



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:37
         param2 := havoc:36
         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(20)
    )
    ,
    Weight(Base relation: 
      {return := havoc:93
       return@pos := type_err:96
       return@width := type_err:97}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':338
   return := havoc:367
   return@pos := type_err:368
   return@width := type_err:369
   when ((!(0 <= K:329) \/ mid_x:330 = (param0:120 + K:329))
           /\ (!(0 <= K:329)
                 \/ (-mid_y:331 + mid___cost:332) = (-param2:126 + __cost:167))
           /\ (!(0 <= K:329) \/ -mid_y:331 <= -param2:126)
           /\ ((K:329 = 0 /\ param2:126 = mid_y:331 /\ param0:120 = mid_x:330
                  /\ tmp:370 = mid_tmp:333 /\ __cost:167 = mid___cost:332)
                 \/ (1 <= K:329 /\ 0 <= (-1 + -param0:120 + param1:123)
                       /\ 0 <= (-1 + -param2:126 + param3:129)
                       /\ 0 <= (-mid_x:330 + param1:123)
                       /\ 0 <= (-mid_y:331 + param3:129)))
           /\ (0 = K:329 \/ (1 + param2:126 + -param3:129) <= 0)
           /\ (!(0 <= K:334) \/ x':335 = (mid_x:330 + K:334))
           /\ (!(0 <= K:334) \/ y':336 = mid_y:331)
           /\ (!(0 <= K:334) \/ tmp':337 = mid_tmp:333)
           /\ (!(0 <= K:334) \/ __cost':338 = mid___cost:332)
           /\ ((K:334 = 0 /\ mid_y:331 = y':336 /\ mid_x:330 = x':335
                  /\ mid_tmp:333 = tmp':337 /\ mid___cost:332 = __cost':338)
                 \/ (1 <= K:334 /\ 0 <= (-1 + -mid_x:330 + param1:123)
                       /\ 0 <= (mid_y:331 + -param3:129)
                       /\ 0 <= (-param3:129 + y':336)
                       /\ 0 <= (param1:123 + -x':335)))
           /\ (0 = K:334 \/ !((1 + mid_y:331 + -param3:129) <= 0))
           /\ (K:329 + K:334) = K:339
           /\ (!(0 <= K:340) \/ mid___cost:341 = __cost:167)
           /\ (!(0 <= K:340) \/ mid_y:342 = param2:126)
           /\ (!(0 <= K:340) \/ mid_x:343 = (param0:120 + K:340))
           /\ ((K:340 = 0 /\ param2:126 = mid_y:342 /\ param0:120 = mid_x:343
                  /\ tmp:370 = mid_tmp:344 /\ __cost:167 = mid___cost:341)
                 \/ (1 <= K:340 /\ 0 <= (-1 + -__cost:167)
                       /\ 0 <= (-1 + -param0:120 + param1:123)
                       /\ 0 <= (-1 + -mid___cost:341)
                       /\ 0 <= (-mid_x:343 + param1:123)))
           /\ (0 = K:340 \/ !(-__cost:167 <= 0))
           /\ (!(0 <= K:345) \/ x':335 = (mid_x:343 + K:345))
           /\ (!(0 <= K:345)
                 \/ (-y':336 + __cost':338) = (-mid_y:342 + mid___cost:341))
           /\ (!(0 <= K:345) \/ -y':336 <= -mid_y:342)
           /\ ((K:345 = 0 /\ mid_y:342 = y':336 /\ mid_x:343 = x':335
                  /\ mid_tmp:344 = tmp':337 /\ mid___cost:341 = __cost':338)
                 \/ (1 <= K:345 /\ 0 <= (-1 + -mid_x:343 + param1:123)
                       /\ 0 <= mid___cost:341 /\ 0 <= (-x':335 + param1:123)
                       /\ 0 <= __cost':338))
           /\ (0 = K:345 \/ -mid___cost:341 <= 0) /\ (K:340 + K:345) = K:339
           /\ 0 <= K:339 /\ param1:123 <= x':335)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':405
   return := 0
   param0 := havoc:35
   param1 := havoc:37
   param2 := havoc:36
   param3 := havoc:38
   return@pos := type_err:426
   param0@pos := type_err:415
   param1@pos := type_err:416
   param2@pos := type_err:417
   param3@pos := type_err:418
   return@width := type_err:427
   param0@width := type_err:420
   param1@width := type_err:421
   param2@width := type_err:422
   param3@width := type_err:423
   when ((!(0 <= K:395) \/ mid_x:396 = (havoc:35 + K:395))
           /\ (!(0 <= K:395) \/ (-mid_y:397 + mid___cost:398) = -havoc:36)
           /\ (!(0 <= K:395) \/ -mid_y:397 <= -havoc:36)
           /\ ((K:395 = 0 /\ havoc:36 = mid_y:397 /\ havoc:35 = mid_x:396
                  /\ tmp:399 = mid_tmp:400 /\ 0 = mid___cost:398)
                 \/ (1 <= K:395 /\ 0 <= (-1 + -havoc:35 + havoc:37)
                       /\ 0 <= (-1 + -havoc:36 + havoc:38)
                       /\ 0 <= (-mid_x:396 + havoc:37)
                       /\ 0 <= (-mid_y:397 + havoc:38)))
           /\ (0 = K:395 \/ (1 + havoc:36 + -havoc:38) <= 0)
           /\ (!(0 <= K:401) \/ x':402 = (mid_x:396 + K:401))
           /\ (!(0 <= K:401) \/ y':403 = mid_y:397)
           /\ (!(0 <= K:401) \/ tmp':404 = mid_tmp:400)
           /\ (!(0 <= K:401) \/ __cost':405 = mid___cost:398)
           /\ ((K:401 = 0 /\ mid_y:397 = y':403 /\ mid_x:396 = x':402
                  /\ mid_tmp:400 = tmp':404 /\ mid___cost:398 = __cost':405)
                 \/ (1 <= K:401 /\ 0 <= (-1 + -mid_x:396 + havoc:37)
                       /\ 0 <= (mid_y:397 + -havoc:38)
                       /\ 0 <= (-havoc:38 + y':403)
                       /\ 0 <= (havoc:37 + -x':402)))
           /\ (0 = K:401 \/ !((1 + mid_y:397 + -havoc:38) <= 0))
           /\ (K:395 + K:401) = K:406
           /\ (!(0 <= K:407) \/ mid___cost:408 = 0)
           /\ (!(0 <= K:407) \/ mid_y:409 = havoc:36)
           /\ (!(0 <= K:407) \/ mid_x:410 = (havoc:35 + K:407)) /\ K:407 = 0
           /\ havoc:36 = mid_y:409 /\ havoc:35 = mid_x:410
           /\ tmp:399 = mid_tmp:411 /\ 0 = mid___cost:408 /\ 0 = K:407
           /\ (!(0 <= K:412) \/ x':402 = (mid_x:410 + K:412))
           /\ (!(0 <= K:412)
                 \/ (-y':403 + __cost':405) = (-mid_y:409 + mid___cost:408))
           /\ (!(0 <= K:412) \/ -y':403 <= -mid_y:409)
           /\ ((K:412 = 0 /\ mid_y:409 = y':403 /\ mid_x:410 = x':402
                  /\ mid_tmp:411 = tmp':404 /\ mid___cost:408 = __cost':405)
                 \/ (1 <= K:412 /\ 0 <= (-1 + -mid_x:410 + havoc:37)
                       /\ 0 <= mid___cost:408 /\ 0 <= (-x':402 + havoc:37)
                       /\ 0 <= __cost':405))
           /\ (0 = K:412 \/ -mid___cost:408 <= 0) /\ (K:407 + K:412) = K:406
           /\ 0 <= K:406 /\ havoc:37 <= x':402
           /\ ((havoc:35 < havoc:37
                  /\ (havoc:37 + -havoc:35) = phi_tmp___3:424)
                 \/ (havoc:37 <= havoc:35 /\ 0 = phi_tmp___3:424))
           /\ ((havoc:36 < havoc:38
                  /\ (havoc:38 + -havoc:36) = phi_tmp___4:425)
                 \/ (havoc:38 <= havoc:36 /\ 0 = phi_tmp___4:425)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':438
   return := havoc:449
   param0 := param0:120
   param1 := param1:123
   param2 := param2:126
   param3 := param3:129
   return@pos := type_err:450
   param0@pos := type_err:138
   param1@pos := type_err:139
   param2@pos := type_err:140
   param3@pos := type_err:141
   return@width := type_err:451
   param0@width := type_err:142
   param1@width := type_err:143
   param2@width := type_err:144
   param3@width := type_err:145
   when ((!(0 <= K:428) \/ mid_x:429 = (param0:120 + K:428))
           /\ (!(0 <= K:428)
                 \/ (-mid_y:430 + mid___cost:431) = (-param2:126 + __cost:167))
           /\ (!(0 <= K:428) \/ -mid_y:430 <= -param2:126)
           /\ ((K:428 = 0 /\ param2:126 = mid_y:430 /\ param0:120 = mid_x:429
                  /\ tmp:432 = mid_tmp:433 /\ __cost:167 = mid___cost:431)
                 \/ (1 <= K:428 /\ 0 <= (-1 + -param0:120 + param1:123)
                       /\ 0 <= (-1 + -param2:126 + param3:129)
                       /\ 0 <= (-mid_x:429 + param1:123)
                       /\ 0 <= (-mid_y:430 + param3:129)))
           /\ (0 = K:428 \/ (1 + param2:126 + -param3:129) <= 0)
           /\ (!(0 <= K:434) \/ x':435 = (mid_x:429 + K:434))
           /\ (!(0 <= K:434) \/ y':436 = mid_y:430)
           /\ (!(0 <= K:434) \/ tmp':437 = mid_tmp:433)
           /\ (!(0 <= K:434) \/ __cost':438 = mid___cost:431)
           /\ ((K:434 = 0 /\ mid_y:430 = y':436 /\ mid_x:429 = x':435
                  /\ mid_tmp:433 = tmp':437 /\ mid___cost:431 = __cost':438)
                 \/ (1 <= K:434 /\ 0 <= (-1 + -mid_x:429 + param1:123)
                       /\ 0 <= (mid_y:430 + -param3:129)
                       /\ 0 <= (-param3:129 + y':436)
                       /\ 0 <= (param1:123 + -x':435)))
           /\ (0 = K:434 \/ !((1 + mid_y:430 + -param3:129) <= 0))
           /\ (K:428 + K:434) = K:439
           /\ (!(0 <= K:440) \/ mid___cost:441 = __cost:167)
           /\ (!(0 <= K:440) \/ mid_y:442 = param2:126)
           /\ (!(0 <= K:440) \/ mid_x:443 = (param0:120 + K:440))
           /\ ((K:440 = 0 /\ param2:126 = mid_y:442 /\ param0:120 = mid_x:443
                  /\ tmp:432 = mid_tmp:444 /\ __cost:167 = mid___cost:441)
                 \/ (1 <= K:440 /\ 0 <= (-1 + -__cost:167)
                       /\ 0 <= (-1 + -param0:120 + param1:123)
                       /\ 0 <= (-1 + -mid___cost:441)
                       /\ 0 <= (-mid_x:443 + param1:123)))
           /\ (0 = K:440 \/ !(-__cost:167 <= 0))
           /\ (!(0 <= K:445) \/ x':435 = (mid_x:443 + K:445))
           /\ (!(0 <= K:445)
                 \/ (-y':436 + __cost':438) = (-mid_y:442 + mid___cost:441))
           /\ (!(0 <= K:445) \/ -y':436 <= -mid_y:442)
           /\ ((K:445 = 0 /\ mid_y:442 = y':436 /\ mid_x:443 = x':435
                  /\ mid_tmp:444 = tmp':437 /\ mid___cost:441 = __cost':438)
                 \/ (1 <= K:445 /\ 0 <= (-1 + -mid_x:443 + param1:123)
                       /\ 0 <= mid___cost:441 /\ 0 <= (-x':435 + param1:123)
                       /\ 0 <= __cost':438))
           /\ (0 = K:445 \/ -mid___cost:441 <= 0) /\ (K:440 + K:445) = K:439
           /\ 0 <= K:439 /\ param1:123 <= x':435)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=20: 
Weight(Base relation: 
  {__cost := __cost':338
   return := havoc:367
   return@pos := type_err:368
   return@width := type_err:369
   when ((!(0 <= K:329) \/ mid_x:330 = (param0:120 + K:329))
           /\ (!(0 <= K:329)
                 \/ (-mid_y:331 + mid___cost:332) = (-param2:126 + __cost:167))
           /\ (!(0 <= K:329) \/ -mid_y:331 <= -param2:126)
           /\ ((K:329 = 0 /\ param2:126 = mid_y:331 /\ param0:120 = mid_x:330
                  /\ tmp:370 = mid_tmp:333 /\ __cost:167 = mid___cost:332)
                 \/ (1 <= K:329 /\ 0 <= (-1 + -param0:120 + param1:123)
                       /\ 0 <= (-1 + -param2:126 + param3:129)
                       /\ 0 <= (-mid_x:330 + param1:123)
                       /\ 0 <= (-mid_y:331 + param3:129)))
           /\ (0 = K:329 \/ (1 + param2:126 + -param3:129) <= 0)
           /\ (!(0 <= K:334) \/ x':335 = (mid_x:330 + K:334))
           /\ (!(0 <= K:334) \/ y':336 = mid_y:331)
           /\ (!(0 <= K:334) \/ tmp':337 = mid_tmp:333)
           /\ (!(0 <= K:334) \/ __cost':338 = mid___cost:332)
           /\ ((K:334 = 0 /\ mid_y:331 = y':336 /\ mid_x:330 = x':335
                  /\ mid_tmp:333 = tmp':337 /\ mid___cost:332 = __cost':338)
                 \/ (1 <= K:334 /\ 0 <= (-1 + -mid_x:330 + param1:123)
                       /\ 0 <= (mid_y:331 + -param3:129)
                       /\ 0 <= (-param3:129 + y':336)
                       /\ 0 <= (param1:123 + -x':335)))
           /\ (0 = K:334 \/ !((1 + mid_y:331 + -param3:129) <= 0))
           /\ (K:329 + K:334) = K:339
           /\ (!(0 <= K:340) \/ mid___cost:341 = __cost:167)
           /\ (!(0 <= K:340) \/ mid_y:342 = param2:126)
           /\ (!(0 <= K:340) \/ mid_x:343 = (param0:120 + K:340))
           /\ ((K:340 = 0 /\ param2:126 = mid_y:342 /\ param0:120 = mid_x:343
                  /\ tmp:370 = mid_tmp:344 /\ __cost:167 = mid___cost:341)
                 \/ (1 <= K:340 /\ 0 <= (-1 + -__cost:167)
                       /\ 0 <= (-1 + -param0:120 + param1:123)
                       /\ 0 <= (-1 + -mid___cost:341)
                       /\ 0 <= (-mid_x:343 + param1:123)))
           /\ (0 = K:340 \/ !(-__cost:167 <= 0))
           /\ (!(0 <= K:345) \/ x':335 = (mid_x:343 + K:345))
           /\ (!(0 <= K:345)
                 \/ (-y':336 + __cost':338) = (-mid_y:342 + mid___cost:341))
           /\ (!(0 <= K:345) \/ -y':336 <= -mid_y:342)
           /\ ((K:345 = 0 /\ mid_y:342 = y':336 /\ mid_x:343 = x':335
                  /\ mid_tmp:344 = tmp':337 /\ mid___cost:341 = __cost':338)
                 \/ (1 <= K:345 /\ 0 <= (-1 + -mid_x:343 + param1:123)
                       /\ 0 <= mid___cost:341 /\ 0 <= (-x':335 + param1:123)
                       /\ 0 <= __cost':338))
           /\ (0 = K:345 \/ -mid___cost:341 <= 0) /\ (K:340 + K:345) = K:339
           /\ 0 <= K:339 /\ param1:123 <= x':335)})


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':405
 return := 0
 param0 := havoc:35
 param1 := havoc:37
 param2 := havoc:36
 param3 := havoc:38
 return@pos := type_err:426
 param0@pos := type_err:415
 param1@pos := type_err:416
 param2@pos := type_err:417
 param3@pos := type_err:418
 return@width := type_err:427
 param0@width := type_err:420
 param1@width := type_err:421
 param2@width := type_err:422
 param3@width := type_err:423
 when ((!(0 <= K:395) \/ mid_x:396 = (havoc:35 + K:395))
         /\ (!(0 <= K:395) \/ (-mid_y:397 + mid___cost:398) = -havoc:36)
         /\ (!(0 <= K:395) \/ -mid_y:397 <= -havoc:36)
         /\ ((K:395 = 0 /\ havoc:36 = mid_y:397 /\ havoc:35 = mid_x:396
                /\ tmp:399 = mid_tmp:400 /\ 0 = mid___cost:398)
               \/ (1 <= K:395 /\ 0 <= (-1 + -havoc:35 + havoc:37)
                     /\ 0 <= (-1 + -havoc:36 + havoc:38)
                     /\ 0 <= (-mid_x:396 + havoc:37)
                     /\ 0 <= (-mid_y:397 + havoc:38)))
         /\ (0 = K:395 \/ (1 + havoc:36 + -havoc:38) <= 0)
         /\ (!(0 <= K:401) \/ x':402 = (mid_x:396 + K:401))
         /\ (!(0 <= K:401) \/ y':403 = mid_y:397)
         /\ (!(0 <= K:401) \/ tmp':404 = mid_tmp:400)
         /\ (!(0 <= K:401) \/ __cost':405 = mid___cost:398)
         /\ ((K:401 = 0 /\ mid_y:397 = y':403 /\ mid_x:396 = x':402
                /\ mid_tmp:400 = tmp':404 /\ mid___cost:398 = __cost':405)
               \/ (1 <= K:401 /\ 0 <= (-1 + -mid_x:396 + havoc:37)
                     /\ 0 <= (mid_y:397 + -havoc:38)
                     /\ 0 <= (-havoc:38 + y':403)
                     /\ 0 <= (havoc:37 + -x':402)))
         /\ (0 = K:401 \/ !((1 + mid_y:397 + -havoc:38) <= 0))
         /\ (K:395 + K:401) = K:406 /\ (!(0 <= K:407) \/ mid___cost:408 = 0)
         /\ (!(0 <= K:407) \/ mid_y:409 = havoc:36)
         /\ (!(0 <= K:407) \/ mid_x:410 = (havoc:35 + K:407)) /\ K:407 = 0
         /\ havoc:36 = mid_y:409 /\ havoc:35 = mid_x:410
         /\ tmp:399 = mid_tmp:411 /\ 0 = mid___cost:408 /\ 0 = K:407
         /\ (!(0 <= K:412) \/ x':402 = (mid_x:410 + K:412))
         /\ (!(0 <= K:412)
               \/ (-y':403 + __cost':405) = (-mid_y:409 + mid___cost:408))
         /\ (!(0 <= K:412) \/ -y':403 <= -mid_y:409)
         /\ ((K:412 = 0 /\ mid_y:409 = y':403 /\ mid_x:410 = x':402
                /\ mid_tmp:411 = tmp':404 /\ mid___cost:408 = __cost':405)
               \/ (1 <= K:412 /\ 0 <= (-1 + -mid_x:410 + havoc:37)
                     /\ 0 <= mid___cost:408 /\ 0 <= (-x':402 + havoc:37)
                     /\ 0 <= __cost':405))
         /\ (0 = K:412 \/ -mid___cost:408 <= 0) /\ (K:407 + K:412) = K:406
         /\ 0 <= K:406 /\ havoc:37 <= x':402
         /\ ((havoc:35 < havoc:37 /\ (havoc:37 + -havoc:35) = phi_tmp___3:424)
               \/ (havoc:37 <= havoc:35 /\ 0 = phi_tmp___3:424))
         /\ ((havoc:36 < havoc:38 /\ (havoc:38 + -havoc:36) = phi_tmp___4:425)
               \/ (havoc:38 <= havoc:36 /\ 0 = phi_tmp___4:425)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':438
 return := havoc:449
 param0 := param0:120
 param1 := param1:123
 param2 := param2:126
 param3 := param3:129
 return@pos := type_err:450
 param0@pos := type_err:138
 param1@pos := type_err:139
 param2@pos := type_err:140
 param3@pos := type_err:141
 return@width := type_err:451
 param0@width := type_err:142
 param1@width := type_err:143
 param2@width := type_err:144
 param3@width := type_err:145
 when ((!(0 <= K:428) \/ mid_x:429 = (param0:120 + K:428))
         /\ (!(0 <= K:428)
               \/ (-mid_y:430 + mid___cost:431) = (-param2:126 + __cost:167))
         /\ (!(0 <= K:428) \/ -mid_y:430 <= -param2:126)
         /\ ((K:428 = 0 /\ param2:126 = mid_y:430 /\ param0:120 = mid_x:429
                /\ tmp:432 = mid_tmp:433 /\ __cost:167 = mid___cost:431)
               \/ (1 <= K:428 /\ 0 <= (-1 + -param0:120 + param1:123)
                     /\ 0 <= (-1 + -param2:126 + param3:129)
                     /\ 0 <= (-mid_x:429 + param1:123)
                     /\ 0 <= (-mid_y:430 + param3:129)))
         /\ (0 = K:428 \/ (1 + param2:126 + -param3:129) <= 0)
         /\ (!(0 <= K:434) \/ x':435 = (mid_x:429 + K:434))
         /\ (!(0 <= K:434) \/ y':436 = mid_y:430)
         /\ (!(0 <= K:434) \/ tmp':437 = mid_tmp:433)
         /\ (!(0 <= K:434) \/ __cost':438 = mid___cost:431)
         /\ ((K:434 = 0 /\ mid_y:430 = y':436 /\ mid_x:429 = x':435
                /\ mid_tmp:433 = tmp':437 /\ mid___cost:431 = __cost':438)
               \/ (1 <= K:434 /\ 0 <= (-1 + -mid_x:429 + param1:123)
                     /\ 0 <= (mid_y:430 + -param3:129)
                     /\ 0 <= (-param3:129 + y':436)
                     /\ 0 <= (param1:123 + -x':435)))
         /\ (0 = K:434 \/ !((1 + mid_y:430 + -param3:129) <= 0))
         /\ (K:428 + K:434) = K:439
         /\ (!(0 <= K:440) \/ mid___cost:441 = __cost:167)
         /\ (!(0 <= K:440) \/ mid_y:442 = param2:126)
         /\ (!(0 <= K:440) \/ mid_x:443 = (param0:120 + K:440))
         /\ ((K:440 = 0 /\ param2:126 = mid_y:442 /\ param0:120 = mid_x:443
                /\ tmp:432 = mid_tmp:444 /\ __cost:167 = mid___cost:441)
               \/ (1 <= K:440 /\ 0 <= (-1 + -__cost:167)
                     /\ 0 <= (-1 + -param0:120 + param1:123)
                     /\ 0 <= (-1 + -mid___cost:441)
                     /\ 0 <= (-mid_x:443 + param1:123)))
         /\ (0 = K:440 \/ !(-__cost:167 <= 0))
         /\ (!(0 <= K:445) \/ x':435 = (mid_x:443 + K:445))
         /\ (!(0 <= K:445)
               \/ (-y':436 + __cost':438) = (-mid_y:442 + mid___cost:441))
         /\ (!(0 <= K:445) \/ -y':436 <= -mid_y:442)
         /\ ((K:445 = 0 /\ mid_y:442 = y':436 /\ mid_x:443 = x':435
                /\ mid_tmp:444 = tmp':437 /\ mid___cost:441 = __cost':438)
               \/ (1 <= K:445 /\ 0 <= (-1 + -mid_x:443 + param1:123)
                     /\ 0 <= mid___cost:441 /\ 0 <= (-x':435 + param1:123)
                     /\ 0 <= __cost':438))
         /\ (0 = K:445 \/ -mid___cost:441 <= 0) /\ (K:440 + K:445) = K:439
         /\ 0 <= K:439 /\ param1:123 <= x':435)}

Evaluating variable number 20 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':338
 return := havoc:367
 return@pos := type_err:368
 return@width := type_err:369
 when ((!(0 <= K:329) \/ mid_x:330 = (param0:120 + K:329))
         /\ (!(0 <= K:329)
               \/ (-mid_y:331 + mid___cost:332) = (-param2:126 + __cost:167))
         /\ (!(0 <= K:329) \/ -mid_y:331 <= -param2:126)
         /\ ((K:329 = 0 /\ param2:126 = mid_y:331 /\ param0:120 = mid_x:330
                /\ tmp:370 = mid_tmp:333 /\ __cost:167 = mid___cost:332)
               \/ (1 <= K:329 /\ 0 <= (-1 + -param0:120 + param1:123)
                     /\ 0 <= (-1 + -param2:126 + param3:129)
                     /\ 0 <= (-mid_x:330 + param1:123)
                     /\ 0 <= (-mid_y:331 + param3:129)))
         /\ (0 = K:329 \/ (1 + param2:126 + -param3:129) <= 0)
         /\ (!(0 <= K:334) \/ x':335 = (mid_x:330 + K:334))
         /\ (!(0 <= K:334) \/ y':336 = mid_y:331)
         /\ (!(0 <= K:334) \/ tmp':337 = mid_tmp:333)
         /\ (!(0 <= K:334) \/ __cost':338 = mid___cost:332)
         /\ ((K:334 = 0 /\ mid_y:331 = y':336 /\ mid_x:330 = x':335
                /\ mid_tmp:333 = tmp':337 /\ mid___cost:332 = __cost':338)
               \/ (1 <= K:334 /\ 0 <= (-1 + -mid_x:330 + param1:123)
                     /\ 0 <= (mid_y:331 + -param3:129)
                     /\ 0 <= (-param3:129 + y':336)
                     /\ 0 <= (param1:123 + -x':335)))
         /\ (0 = K:334 \/ !((1 + mid_y:331 + -param3:129) <= 0))
         /\ (K:329 + K:334) = K:339
         /\ (!(0 <= K:340) \/ mid___cost:341 = __cost:167)
         /\ (!(0 <= K:340) \/ mid_y:342 = param2:126)
         /\ (!(0 <= K:340) \/ mid_x:343 = (param0:120 + K:340))
         /\ ((K:340 = 0 /\ param2:126 = mid_y:342 /\ param0:120 = mid_x:343
                /\ tmp:370 = mid_tmp:344 /\ __cost:167 = mid___cost:341)
               \/ (1 <= K:340 /\ 0 <= (-1 + -__cost:167)
                     /\ 0 <= (-1 + -param0:120 + param1:123)
                     /\ 0 <= (-1 + -mid___cost:341)
                     /\ 0 <= (-mid_x:343 + param1:123)))
         /\ (0 = K:340 \/ !(-__cost:167 <= 0))
         /\ (!(0 <= K:345) \/ x':335 = (mid_x:343 + K:345))
         /\ (!(0 <= K:345)
               \/ (-y':336 + __cost':338) = (-mid_y:342 + mid___cost:341))
         /\ (!(0 <= K:345) \/ -y':336 <= -mid_y:342)
         /\ ((K:345 = 0 /\ mid_y:342 = y':336 /\ mid_x:343 = x':335
                /\ mid_tmp:344 = tmp':337 /\ mid___cost:341 = __cost':338)
               \/ (1 <= K:345 /\ 0 <= (-1 + -mid_x:343 + param1:123)
                     /\ 0 <= mid___cost:341 /\ 0 <= (-x':335 + param1:123)
                     /\ 0 <= __cost':338))
         /\ (0 = K:345 \/ -mid___cost:341 <= 0) /\ (K:340 + K:345) = K:339
         /\ 0 <= K:339 /\ param1:123 <= x':335)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, accept> -> <__pstate, (Unique State Name,81)_g1>	Base relation: 
{__cost := 0
 x := havoc:35
 y := havoc:36
 n := havoc:37
 m := havoc:38
 param0 := havoc:35
 param1 := havoc:37
 param2 := havoc:36
 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}	
<__pstate, (Unique State Name,81)_g1> -> <__pstate, (Unique State Name,71)_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}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x52c7c80: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x5dacdd0: 
	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,81)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:35
 y := havoc:36
 n := havoc:37
 m := havoc:38
 param0 := havoc:35
 param1 := havoc:37
 param2 := havoc:36
 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}
    ( __pstate , (Unique State Name,71)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:35
 y := havoc:36
 n := havoc:37
 m := havoc:38
 param0 := havoc:35
 param1 := havoc:37
 param2 := havoc:36
 param3 := havoc:38
 param0@pos := type_err:509
 param1@pos := type_err:510
 param2@pos := type_err:511
 param3@pos := type_err:512
 param0@width := type_err:513
 param1@width := type_err:514
 param2@width := type_err:515
 param3@width := type_err:516}

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

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

Base relation: 
{__cost := __cost':462
 x := havoc:35
 y := havoc:36
 n := havoc:37
 m := havoc:38
 return := 0
 param0 := havoc:35
 param1 := havoc:37
 param2 := havoc:36
 param3 := havoc:38
 return@pos := type_err:483
 param0@pos := type_err:472
 param1@pos := type_err:473
 param2@pos := type_err:474
 param3@pos := type_err:475
 return@width := type_err:484
 param0@width := type_err:477
 param1@width := type_err:478
 param2@width := type_err:479
 param3@width := type_err:480
 when ((!(0 <= K:452) \/ mid_x:453 = (havoc:35 + K:452))
         /\ (!(0 <= K:452) \/ (-mid_y:454 + mid___cost:455) = -havoc:36)
         /\ (!(0 <= K:452) \/ -mid_y:454 <= -havoc:36)
         /\ ((K:452 = 0 /\ havoc:36 = mid_y:454 /\ havoc:35 = mid_x:453
                /\ tmp:456 = mid_tmp:457 /\ 0 = mid___cost:455)
               \/ (1 <= K:452 /\ 0 <= (-1 + -havoc:35 + havoc:37)
                     /\ 0 <= (-1 + -havoc:36 + havoc:38)
                     /\ 0 <= (-mid_x:453 + havoc:37)
                     /\ 0 <= (-mid_y:454 + havoc:38)))
         /\ (0 = K:452 \/ (1 + havoc:36 + -havoc:38) <= 0)
         /\ (!(0 <= K:458) \/ x':459 = (mid_x:453 + K:458))
         /\ (!(0 <= K:458) \/ y':460 = mid_y:454)
         /\ (!(0 <= K:458) \/ tmp':461 = mid_tmp:457)
         /\ (!(0 <= K:458) \/ __cost':462 = mid___cost:455)
         /\ ((K:458 = 0 /\ mid_y:454 = y':460 /\ mid_x:453 = x':459
                /\ mid_tmp:457 = tmp':461 /\ mid___cost:455 = __cost':462)
               \/ (1 <= K:458 /\ 0 <= (-1 + -mid_x:453 + havoc:37)
                     /\ 0 <= (mid_y:454 + -havoc:38)
                     /\ 0 <= (-havoc:38 + y':460)
                     /\ 0 <= (havoc:37 + -x':459)))
         /\ (0 = K:458 \/ !((1 + mid_y:454 + -havoc:38) <= 0))
         /\ (K:452 + K:458) = K:463 /\ (!(0 <= K:464) \/ mid___cost:465 = 0)
         /\ (!(0 <= K:464) \/ mid_y:466 = havoc:36)
         /\ (!(0 <= K:464) \/ mid_x:467 = (havoc:35 + K:464)) /\ K:464 = 0
         /\ havoc:36 = mid_y:466 /\ havoc:35 = mid_x:467
         /\ tmp:456 = mid_tmp:468 /\ 0 = mid___cost:465 /\ 0 = K:464
         /\ (!(0 <= K:469) \/ x':459 = (mid_x:467 + K:469))
         /\ (!(0 <= K:469)
               \/ (-y':460 + __cost':462) = (-mid_y:466 + mid___cost:465))
         /\ (!(0 <= K:469) \/ -y':460 <= -mid_y:466)
         /\ ((K:469 = 0 /\ mid_y:466 = y':460 /\ mid_x:467 = x':459
                /\ mid_tmp:468 = tmp':461 /\ mid___cost:465 = __cost':462)
               \/ (1 <= K:469 /\ 0 <= (-1 + -mid_x:467 + havoc:37)
                     /\ 0 <= mid___cost:465 /\ 0 <= (-x':459 + havoc:37)
                     /\ 0 <= __cost':462))
         /\ (0 = K:469 \/ -mid___cost:465 <= 0) /\ (K:464 + K:469) = K:463
         /\ 0 <= K:463 /\ havoc:37 <= x':459
         /\ ((havoc:35 < havoc:37 /\ (havoc:37 + -havoc:35) = phi_tmp___3:481)
               \/ (havoc:37 <= havoc:35 /\ 0 = phi_tmp___3:481))
         /\ ((havoc:36 < havoc:38 /\ (havoc:38 + -havoc:36) = phi_tmp___4:482)
               \/ (havoc:38 <= havoc:36 /\ 0 = phi_tmp___4:482)))}

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

Base relation: 
{__cost := __cost':495
 return := havoc:506
 param0 := param0:120
 param1 := param1:123
 param2 := param2:126
 param3 := param3:129
 return@pos := type_err:507
 param0@pos := type_err:138
 param1@pos := type_err:139
 param2@pos := type_err:140
 param3@pos := type_err:141
 return@width := type_err:508
 param0@width := type_err:142
 param1@width := type_err:143
 param2@width := type_err:144
 param3@width := type_err:145
 when ((!(0 <= K:485) \/ mid_x:486 = (param0:120 + K:485))
         /\ (!(0 <= K:485)
               \/ (-mid_y:487 + mid___cost:488) = (-param2:126 + __cost:167))
         /\ (!(0 <= K:485) \/ -mid_y:487 <= -param2:126)
         /\ ((K:485 = 0 /\ param2:126 = mid_y:487 /\ param0:120 = mid_x:486
                /\ tmp:489 = mid_tmp:490 /\ __cost:167 = mid___cost:488)
               \/ (1 <= K:485 /\ 0 <= (-1 + -param0:120 + param1:123)
                     /\ 0 <= (-1 + -param2:126 + param3:129)
                     /\ 0 <= (-mid_x:486 + param1:123)
                     /\ 0 <= (-mid_y:487 + param3:129)))
         /\ (0 = K:485 \/ (1 + param2:126 + -param3:129) <= 0)
         /\ (!(0 <= K:491) \/ x':492 = (mid_x:486 + K:491))
         /\ (!(0 <= K:491) \/ y':493 = mid_y:487)
         /\ (!(0 <= K:491) \/ tmp':494 = mid_tmp:490)
         /\ (!(0 <= K:491) \/ __cost':495 = mid___cost:488)
         /\ ((K:491 = 0 /\ mid_y:487 = y':493 /\ mid_x:486 = x':492
                /\ mid_tmp:490 = tmp':494 /\ mid___cost:488 = __cost':495)
               \/ (1 <= K:491 /\ 0 <= (-1 + -mid_x:486 + param1:123)
                     /\ 0 <= (mid_y:487 + -param3:129)
                     /\ 0 <= (-param3:129 + y':493)
                     /\ 0 <= (param1:123 + -x':492)))
         /\ (0 = K:491 \/ !((1 + mid_y:487 + -param3:129) <= 0))
         /\ (K:485 + K:491) = K:496
         /\ (!(0 <= K:497) \/ mid___cost:498 = __cost:167)
         /\ (!(0 <= K:497) \/ mid_y:499 = param2:126)
         /\ (!(0 <= K:497) \/ mid_x:500 = (param0:120 + K:497))
         /\ ((K:497 = 0 /\ param2:126 = mid_y:499 /\ param0:120 = mid_x:500
                /\ tmp:489 = mid_tmp:501 /\ __cost:167 = mid___cost:498)
               \/ (1 <= K:497 /\ 0 <= (-1 + -__cost:167)
                     /\ 0 <= (-1 + -param0:120 + param1:123)
                     /\ 0 <= (-1 + -mid___cost:498)
                     /\ 0 <= (-mid_x:500 + param1:123)))
         /\ (0 = K:497 \/ !(-__cost:167 <= 0))
         /\ (!(0 <= K:502) \/ x':492 = (mid_x:500 + K:502))
         /\ (!(0 <= K:502)
               \/ (-y':493 + __cost':495) = (-mid_y:499 + mid___cost:498))
         /\ (!(0 <= K:502) \/ -y':493 <= -mid_y:499)
         /\ ((K:502 = 0 /\ mid_y:499 = y':493 /\ mid_x:500 = x':492
                /\ mid_tmp:501 = tmp':494 /\ mid___cost:498 = __cost':495)
               \/ (1 <= K:502 /\ 0 <= (-1 + -mid_x:500 + param1:123)
                     /\ 0 <= mid___cost:498 /\ 0 <= (-x':492 + param1:123)
                     /\ 0 <= __cost':495))
         /\ (0 = K:502 \/ -mid___cost:498 <= 0) /\ (K:497 + K:502) = K:496
         /\ 0 <= K:496 /\ param1:123 <= x':492)}

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

Base relation: 
{__cost := __cost':338
 tmp := tmp':337
 x := x':335
 n := param1:123
 y := y':336
 m := param3:129
 return := havoc:367
 return@pos := type_err:368
 return@width := type_err:369
 when ((!(0 <= K:329) \/ mid_x:330 = (param0:120 + K:329))
         /\ (!(0 <= K:329)
               \/ (-mid_y:331 + mid___cost:332) = (-param2:126 + __cost:167))
         /\ (!(0 <= K:329) \/ -mid_y:331 <= -param2:126)
         /\ ((K:329 = 0 /\ param2:126 = mid_y:331 /\ param0:120 = mid_x:330
                /\ tmp:166 = mid_tmp:333 /\ __cost:167 = mid___cost:332)
               \/ (1 <= K:329 /\ 0 <= (-1 + -param0:120 + param1:123)
                     /\ 0 <= (-1 + -param2:126 + param3:129)
                     /\ 0 <= (-mid_x:330 + param1:123)
                     /\ 0 <= (-mid_y:331 + param3:129)))
         /\ (0 = K:329 \/ (1 + param2:126 + -param3:129) <= 0)
         /\ (!(0 <= K:334) \/ x':335 = (mid_x:330 + K:334))
         /\ (!(0 <= K:334) \/ y':336 = mid_y:331)
         /\ (!(0 <= K:334) \/ tmp':337 = mid_tmp:333)
         /\ (!(0 <= K:334) \/ __cost':338 = mid___cost:332)
         /\ ((K:334 = 0 /\ mid_y:331 = y':336 /\ mid_x:330 = x':335
                /\ mid_tmp:333 = tmp':337 /\ mid___cost:332 = __cost':338)
               \/ (1 <= K:334 /\ 0 <= (-1 + -mid_x:330 + param1:123)
                     /\ 0 <= (mid_y:331 + -param3:129)
                     /\ 0 <= (-param3:129 + y':336)
                     /\ 0 <= (param1:123 + -x':335)))
         /\ (0 = K:334 \/ !((1 + mid_y:331 + -param3:129) <= 0))
         /\ (K:329 + K:334) = K:339
         /\ (!(0 <= K:340) \/ mid___cost:341 = __cost:167)
         /\ (!(0 <= K:340) \/ mid_y:342 = param2:126)
         /\ (!(0 <= K:340) \/ mid_x:343 = (param0:120 + K:340))
         /\ ((K:340 = 0 /\ param2:126 = mid_y:342 /\ param0:120 = mid_x:343
                /\ tmp:166 = mid_tmp:344 /\ __cost:167 = mid___cost:341)
               \/ (1 <= K:340 /\ 0 <= (-1 + -__cost:167)
                     /\ 0 <= (-1 + -param0:120 + param1:123)
                     /\ 0 <= (-1 + -mid___cost:341)
                     /\ 0 <= (-mid_x:343 + param1:123)))
         /\ (0 = K:340 \/ !(-__cost:167 <= 0))
         /\ (!(0 <= K:345) \/ x':335 = (mid_x:343 + K:345))
         /\ (!(0 <= K:345)
               \/ (-y':336 + __cost':338) = (-mid_y:342 + mid___cost:341))
         /\ (!(0 <= K:345) \/ -y':336 <= -mid_y:342)
         /\ ((K:345 = 0 /\ mid_y:342 = y':336 /\ mid_x:343 = x':335
                /\ mid_tmp:344 = tmp':337 /\ mid___cost:341 = __cost':338)
               \/ (1 <= K:345 /\ 0 <= (-1 + -mid_x:343 + param1:123)
                     /\ 0 <= mid___cost:341 /\ 0 <= (-x':335 + param1:123)
                     /\ 0 <= __cost':338))
         /\ (0 = K:345 \/ -mid___cost:341 <= 0) /\ (K:340 + K:345) = K:339
         /\ 0 <= K:339 /\ param1:123 <= x':335)}

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

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

Variable bounds at line 21 in run

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

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