/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, 33> -> <Unique State Name, 29>	Base relation: 
{y := (y:4 + -1)
 x := (x:103 + 1)
 __cost := (__cost:102 + 1)
 when (0 < y:4 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}	
<Unique State Name, 33> -> <Unique State Name, 86>	Base relation: 
{return := havoc:109
 return@pos := type_err:110
 return@width := type_err:111
 when y:4 <= 0}	
<Unique State Name, 66> -> <Unique State Name, 48>	Base relation: 
{}	
<Unique State Name, 70> -> <Unique State Name, 47 69>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 19> -> <Unique State Name, 88>	Base relation: 
{return := havoc:56
 return@pos := type_err:59
 return@width := type_err:60}	
<Unique State Name, 84> -> <Unique State Name, 79 83>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 83> -> <Unique State Name, 89>	Base relation: 
{return := 0
 return@pos := type_err:24
 return@width := type_err:25}	
<Unique State Name, 52> -> <Unique State Name, 48>	Base relation: 
{y := (y:4 + 1)
 x := (x:103 + -1)
 __cost := (__cost:102 + -1)
 when (0 < x:103 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + -1))}	
<Unique State Name, 52> -> <Unique State Name, 85>	Base relation: 
{return := havoc:130
 return@pos := type_err:131
 return@width := type_err:132
 when x:103 <= 0}	
<Unique State Name, 17> -> <Unique State Name, 84>	Base relation: 
{y := havoc:21
 x := havoc:20
 __cost := 0
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:31
 param1@pos := type_err:32
 param0@width := type_err:33
 param1@width := type_err:34
 when ((0 < havoc:21 /\ havoc:21 = phi_tmp___0:30)
         \/ (havoc:21 <= 0 /\ 0 = phi_tmp___0:30))}	
<Unique State Name, 89> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 69> -> <Unique State Name, 72>	Base relation: 
{}	
<Unique State Name, 67> -> <Unique State Name, 87>	Base relation: 
{return := havoc:94
 return@pos := type_err:97
 return@width := type_err:98}	
<Unique State Name, 85> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 68> -> <Unique State Name, 47 67>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 78> -> <Unique State Name, 73 77>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 77> -> <Unique State Name, 19>	Base relation: 
{}	
<Unique State Name, 87> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 48> -> <Unique State Name, 91>	Base relation: 
{}	
<Unique State Name, 71> -> <Unique State Name, 68>	Base relation: 
{}	
<Unique State Name, 91> -> <Unique State Name, 52>	Base relation: 
{}	
<Unique State Name, 47> -> <Unique State Name, 29>	Base relation: 
{}	
<Unique State Name, 29> -> <Unique State Name, 90>	Base relation: 
{}	
<Unique State Name, 79> -> <Unique State Name, 78>	Base relation: 
{param0 := param0:73
 param1 := param1:76
 param0@pos := type_err:81
 param1@pos := type_err:82
 param0@width := type_err:83
 param1@width := type_err:84}	
<Unique State Name, 72> -> <Unique State Name, 66 71>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 90> -> <Unique State Name, 33>	Base relation: 
{}	
<Unique State Name, 73> -> <Unique State Name, 70>	Base relation: 
{}	
<Unique State Name, 86> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 88> -> <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: 
{y := (y:4 + 1)
 x := (x:103 + -1)
 __cost := (__cost:102 + -1)
 when (0 < x:103 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + -1))}
**** alpha hat: 
  {<Split [true
            (__cost':148) = (1)*(__cost:102) + (-1)*1
           (y':146) = (1)*(y:4) + 1
           (x':147) = (1)*(x:103) + (-1)*1
           }
          pre:
            [|__cost:102-1>=0; x:103-1>=0|]
          post:
            [|x':147>=0; __cost':148>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {y := y':146
   x := x':147
   __cost := __cost':148
   when ((!(0 <= K:159) \/ mid___cost:161 = (__cost:102 + -K:159))
           /\ (!(0 <= K:159) \/ mid_y:163 = (y:4 + K:159))
           /\ (!(0 <= K:159) \/ mid_x:162 = (x:103 + -K:159))
           /\ ((K:159 = 0 /\ __cost:102 = mid___cost:161 /\ x:103 = mid_x:162
                  /\ y:4 = mid_y:163)
                 \/ (1 <= K:159 /\ 0 <= (-1 + __cost:102)
                       /\ 0 <= (-1 + x:103) /\ 0 <= mid_x:162
                       /\ 0 <= mid___cost:161)) /\ K:160 = 0
           /\ mid___cost:161 = __cost':148 /\ mid_x:162 = x':147
           /\ mid_y:163 = y':146 /\ 0 = K:160 /\ (K:159 + K:160) = K:158
           /\ 0 <= K:158)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{y := (y:4 + -1)
 x := (x:103 + 1)
 __cost := (__cost:102 + 1)
 when (0 < y:4 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':148) = (1)*(__cost:102) + 1
           (x':147) = (1)*(x:103) + 1
           (y':146) = (1)*(y:4) + (-1)*1
           }
          pre:
            [|__cost:102>=0; y:4-1>=0|]
          post:
            [|y':146>=0; __cost':148-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {y := y':146
   x := x':147
   __cost := __cost':148
   when ((!(0 <= K:177) \/ mid___cost:179 = (__cost:102 + K:177))
           /\ (!(0 <= K:177) \/ mid_x:180 = (x:103 + K:177))
           /\ (!(0 <= K:177) \/ mid_y:181 = (y:4 + -K:177))
           /\ ((K:177 = 0 /\ __cost:102 = mid___cost:179 /\ x:103 = mid_x:180
                  /\ y:4 = mid_y:181)
                 \/ (1 <= K:177 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                       /\ 0 <= mid_y:181 /\ 0 <= (-1 + mid___cost:179)))
           /\ K:178 = 0 /\ mid___cost:179 = __cost':148 /\ mid_x:180 = x':147
           /\ mid_y:181 = y':146 /\ 0 = K:178 /\ (K:177 + K:178) = K:176
           /\ 0 <= K:176)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  25  31  37  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {y := havoc:21
       x := havoc:20
       __cost := 0
       param0 := havoc:21
       param1 := havoc:22
       param0@pos := type_err:31
       param1@pos := type_err:32
       param0@width := type_err:33
       param1@width := type_err:34
       when ((0 < havoc:21 /\ havoc:21 = phi_tmp___0:30)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___0:30))}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:24
     return@width := type_err:25}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:73
       param1 := param1:76
       param0@pos := type_err:81
       param1@pos := type_err:82
       param0@width := type_err:83
       param1@width := type_err:84}    )
    ,
    Var(25)
  )
  ,
  Weight(Base relation: 
    {return := havoc:56
     return@pos := type_err:59
     return@width := type_err:60}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=25: 
Dot(
  Dot(
    Dot(
      Var(31)
      ,
      Var(37)
    )
    ,
    Var(31)
  )
  ,
  Weight(Base relation: 
    {return := havoc:94
     return@pos := type_err:97
     return@width := type_err:98}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=31: 
Weight(Base relation: 
  {y := y':146
   x := x':147
   __cost := __cost':148
   return := havoc:182
   return@pos := type_err:183
   return@width := type_err:184
   when ((!(0 <= K:177) \/ mid___cost:179 = (__cost:102 + K:177))
           /\ (!(0 <= K:177) \/ mid_x:180 = (x:103 + K:177))
           /\ (!(0 <= K:177) \/ mid_y:181 = (y:4 + -K:177))
           /\ ((K:177 = 0 /\ __cost:102 = mid___cost:179 /\ x:103 = mid_x:180
                  /\ y:4 = mid_y:181)
                 \/ (1 <= K:177 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                       /\ 0 <= mid_y:181 /\ 0 <= (-1 + mid___cost:179)))
           /\ K:178 = 0 /\ mid___cost:179 = __cost':148 /\ mid_x:180 = x':147
           /\ mid_y:181 = y':146 /\ 0 = K:178 /\ (K:177 + K:178) = K:176
           /\ 0 <= K:176 /\ y':146 <= 0)})


New-style (IRE) regular expression in IREregExpMap for reID=37: 
Weight(Base relation: 
  {y := y':146
   x := x':147
   __cost := __cost':148
   return := havoc:164
   return@pos := type_err:165
   return@width := type_err:166
   when ((!(0 <= K:159) \/ mid___cost:161 = (__cost:102 + -K:159))
           /\ (!(0 <= K:159) \/ mid_y:163 = (y:4 + K:159))
           /\ (!(0 <= K:159) \/ mid_x:162 = (x:103 + -K:159))
           /\ ((K:159 = 0 /\ __cost:102 = mid___cost:161 /\ x:103 = mid_x:162
                  /\ y:4 = mid_y:163)
                 \/ (1 <= K:159 /\ 0 <= (-1 + __cost:102)
                       /\ 0 <= (-1 + x:103) /\ 0 <= mid_x:162
                       /\ 0 <= mid___cost:161)) /\ K:160 = 0
           /\ mid___cost:161 = __cost':148 /\ mid_x:162 = x':147
           /\ mid_y:163 = y':146 /\ 0 = K:160 /\ (K:159 + K:160) = K:158
           /\ 0 <= K:158 /\ x':147 <= 0)})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {y := havoc:21
         x := havoc:20
         __cost := 0
         param0 := havoc:21
         param1 := havoc:22
         param0@pos := type_err:31
         param1@pos := type_err:32
         param0@width := type_err:33
         param1@width := type_err:34
         when ((0 < havoc:21 /\ havoc:21 = phi_tmp___0:30)
                 \/ (havoc:21 <= 0 /\ 0 = phi_tmp___0:30))}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:24
       return@width := type_err:25}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:73
         param1 := param1:76
         param0@pos := type_err:81
         param1@pos := type_err:82
         param0@width := type_err:83
         param1@width := type_err:84}      )
      ,
      Var(25)
    )
    ,
    Weight(Base relation: 
      {return := havoc:56
       return@pos := type_err:59
       return@width := type_err:60}    )
  )
)



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

Project(
  Dot(
    Dot(
      Dot(
        Var(31)
        ,
        Var(37)
      )
      ,
      Var(31)
    )
    ,
    Weight(Base relation: 
      {return := havoc:94
       return@pos := type_err:97
       return@width := type_err:98}    )
  )
)



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

Weight(Base relation: 
  {y := y':146
   x := x':147
   __cost := __cost':148
   return := havoc:182
   return@pos := type_err:183
   return@width := type_err:184
   when ((!(0 <= K:177) \/ mid___cost:179 = (__cost:102 + K:177))
           /\ (!(0 <= K:177) \/ mid_x:180 = (x:103 + K:177))
           /\ (!(0 <= K:177) \/ mid_y:181 = (y:4 + -K:177))
           /\ ((K:177 = 0 /\ __cost:102 = mid___cost:179 /\ x:103 = mid_x:180
                  /\ y:4 = mid_y:181)
                 \/ (1 <= K:177 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                       /\ 0 <= mid_y:181 /\ 0 <= (-1 + mid___cost:179)))
           /\ K:178 = 0 /\ mid___cost:179 = __cost':148 /\ mid_x:180 = x':147
           /\ mid_y:181 = y':146 /\ 0 = K:178 /\ (K:177 + K:178) = K:176
           /\ 0 <= K:176 /\ y':146 <= 0)})



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

Weight(Base relation: 
  {y := y':146
   x := x':147
   __cost := __cost':148
   return := havoc:164
   return@pos := type_err:165
   return@width := type_err:166
   when ((!(0 <= K:159) \/ mid___cost:161 = (__cost:102 + -K:159))
           /\ (!(0 <= K:159) \/ mid_y:163 = (y:4 + K:159))
           /\ (!(0 <= K:159) \/ mid_x:162 = (x:103 + -K:159))
           /\ ((K:159 = 0 /\ __cost:102 = mid___cost:161 /\ x:103 = mid_x:162
                  /\ y:4 = mid_y:163)
                 \/ (1 <= K:159 /\ 0 <= (-1 + __cost:102)
                       /\ 0 <= (-1 + x:103) /\ 0 <= mid_x:162
                       /\ 0 <= mid___cost:161)) /\ K:160 = 0
           /\ mid___cost:161 = __cost':148 /\ mid_x:162 = x':147
           /\ mid_y:163 = y':146 /\ 0 = K:160 /\ (K:159 + K:160) = K:158
           /\ 0 <= K:158 /\ x':147 <= 0)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {y := y':276
   x := x':275
   __cost := __cost':274
   return := 0
   param0 := havoc:21
   param1 := havoc:22
   return@pos := type_err:285
   param0@pos := type_err:280
   param1@pos := type_err:281
   return@width := type_err:286
   param0@width := type_err:283
   param1@width := type_err:284
   when (((0 < havoc:21 /\ havoc:21 = phi_tmp___0:30)
            \/ (havoc:21 <= 0 /\ 0 = phi_tmp___0:30))
           /\ (!(0 <= K:251) \/ mid___cost:252 = K:251)
           /\ (!(0 <= K:251) \/ mid_x:253 = (havoc:20 + K:251))
           /\ (!(0 <= K:251) \/ mid_y:254 = (havoc:21 + -K:251))
           /\ ((K:251 = 0 /\ 0 = mid___cost:252 /\ havoc:20 = mid_x:253
                  /\ havoc:21 = mid_y:254)
                 \/ (1 <= K:251 /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_y:254
                       /\ 0 <= (-1 + mid___cost:252))) /\ K:255 = 0
           /\ mid___cost:252 = __cost':256 /\ mid_x:253 = x':257
           /\ mid_y:254 = y':258 /\ 0 = K:255 /\ (K:251 + K:255) = K:259
           /\ 0 <= K:259 /\ y':258 <= 0
           /\ (!(0 <= K:260) \/ mid___cost:261 = (__cost':256 + -K:260))
           /\ (!(0 <= K:260) \/ mid_y:262 = (y':258 + K:260))
           /\ (!(0 <= K:260) \/ mid_x:263 = (x':257 + -K:260))
           /\ ((K:260 = 0 /\ __cost':256 = mid___cost:261
                  /\ x':257 = mid_x:263 /\ y':258 = mid_y:262)
                 \/ (1 <= K:260 /\ 0 <= (-1 + __cost':256)
                       /\ 0 <= (-1 + x':257) /\ 0 <= mid_x:263
                       /\ 0 <= mid___cost:261)) /\ K:264 = 0
           /\ mid___cost:261 = __cost':265 /\ mid_x:263 = x':266
           /\ mid_y:262 = y':267 /\ 0 = K:264 /\ (K:260 + K:264) = K:268
           /\ 0 <= K:268 /\ x':266 <= 0
           /\ (!(0 <= K:269) \/ mid___cost:270 = (__cost':265 + K:269))
           /\ (!(0 <= K:269) \/ mid_x:271 = (x':266 + K:269))
           /\ (!(0 <= K:269) \/ mid_y:272 = (y':267 + -K:269))
           /\ ((K:269 = 0 /\ __cost':265 = mid___cost:270
                  /\ x':266 = mid_x:271 /\ y':267 = mid_y:272)
                 \/ (1 <= K:269 /\ 0 <= __cost':265 /\ 0 <= (-1 + y':267)
                       /\ 0 <= mid_y:272 /\ 0 <= (-1 + mid___cost:270)))
           /\ K:273 = 0 /\ mid___cost:270 = __cost':274 /\ mid_x:271 = x':275
           /\ mid_y:272 = y':276 /\ 0 = K:273 /\ (K:269 + K:273) = K:277
           /\ 0 <= K:277 /\ y':276 <= 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {y := y':336
   x := x':335
   __cost := __cost':334
   return := havoc:341
   param0 := param0:73
   param1 := param1:76
   return@pos := type_err:342
   param0@pos := type_err:81
   param1@pos := type_err:82
   return@width := type_err:343
   param0@width := type_err:83
   param1@width := type_err:84
   when ((!(0 <= K:311) \/ mid___cost:312 = (__cost:102 + K:311))
           /\ (!(0 <= K:311) \/ mid_x:313 = (x:103 + K:311))
           /\ (!(0 <= K:311) \/ mid_y:314 = (y:4 + -K:311))
           /\ ((K:311 = 0 /\ __cost:102 = mid___cost:312 /\ x:103 = mid_x:313
                  /\ y:4 = mid_y:314)
                 \/ (1 <= K:311 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                       /\ 0 <= mid_y:314 /\ 0 <= (-1 + mid___cost:312)))
           /\ K:315 = 0 /\ mid___cost:312 = __cost':316 /\ mid_x:313 = x':317
           /\ mid_y:314 = y':318 /\ 0 = K:315 /\ (K:311 + K:315) = K:319
           /\ 0 <= K:319 /\ y':318 <= 0
           /\ (!(0 <= K:320) \/ mid___cost:321 = (__cost':316 + -K:320))
           /\ (!(0 <= K:320) \/ mid_y:322 = (y':318 + K:320))
           /\ (!(0 <= K:320) \/ mid_x:323 = (x':317 + -K:320))
           /\ ((K:320 = 0 /\ __cost':316 = mid___cost:321
                  /\ x':317 = mid_x:323 /\ y':318 = mid_y:322)
                 \/ (1 <= K:320 /\ 0 <= (-1 + __cost':316)
                       /\ 0 <= (-1 + x':317) /\ 0 <= mid_x:323
                       /\ 0 <= mid___cost:321)) /\ K:324 = 0
           /\ mid___cost:321 = __cost':325 /\ mid_x:323 = x':326
           /\ mid_y:322 = y':327 /\ 0 = K:324 /\ (K:320 + K:324) = K:328
           /\ 0 <= K:328 /\ x':326 <= 0
           /\ (!(0 <= K:329) \/ mid___cost:330 = (__cost':325 + K:329))
           /\ (!(0 <= K:329) \/ mid_x:331 = (x':326 + K:329))
           /\ (!(0 <= K:329) \/ mid_y:332 = (y':327 + -K:329))
           /\ ((K:329 = 0 /\ __cost':325 = mid___cost:330
                  /\ x':326 = mid_x:331 /\ y':327 = mid_y:332)
                 \/ (1 <= K:329 /\ 0 <= __cost':325 /\ 0 <= (-1 + y':327)
                       /\ 0 <= mid_y:332 /\ 0 <= (-1 + mid___cost:330)))
           /\ K:333 = 0 /\ mid___cost:330 = __cost':334 /\ mid_x:331 = x':335
           /\ mid_y:332 = y':336 /\ 0 = K:333 /\ (K:329 + K:333) = K:337
           /\ 0 <= K:337 /\ y':336 <= 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=25: 
Weight(Base relation: 
  {y := y':363
   x := x':362
   __cost := __cost':361
   return := havoc:365
   return@pos := type_err:366
   return@width := type_err:367
   when ((!(0 <= K:177) \/ mid___cost:179 = (__cost:102 + K:177))
           /\ (!(0 <= K:177) \/ mid_x:180 = (x:103 + K:177))
           /\ (!(0 <= K:177) \/ mid_y:181 = (y:4 + -K:177))
           /\ ((K:177 = 0 /\ __cost:102 = mid___cost:179 /\ x:103 = mid_x:180
                  /\ y:4 = mid_y:181)
                 \/ (1 <= K:177 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                       /\ 0 <= mid_y:181 /\ 0 <= (-1 + mid___cost:179)))
           /\ K:178 = 0 /\ mid___cost:179 = __cost':148 /\ mid_x:180 = x':147
           /\ mid_y:181 = y':146 /\ 0 = K:178 /\ (K:177 + K:178) = K:176
           /\ 0 <= K:176 /\ y':146 <= 0
           /\ (!(0 <= K:344) \/ mid___cost:345 = (__cost':148 + -K:344))
           /\ (!(0 <= K:344) \/ mid_y:346 = (y':146 + K:344))
           /\ (!(0 <= K:344) \/ mid_x:347 = (x':147 + -K:344))
           /\ ((K:344 = 0 /\ __cost':148 = mid___cost:345
                  /\ x':147 = mid_x:347 /\ y':146 = mid_y:346)
                 \/ (1 <= K:344 /\ 0 <= (-1 + __cost':148)
                       /\ 0 <= (-1 + x':147) /\ 0 <= mid_x:347
                       /\ 0 <= mid___cost:345)) /\ K:348 = 0
           /\ mid___cost:345 = __cost':349 /\ mid_x:347 = x':350
           /\ mid_y:346 = y':351 /\ 0 = K:348 /\ (K:344 + K:348) = K:352
           /\ 0 <= K:352 /\ x':350 <= 0
           /\ (!(0 <= K:356) \/ mid___cost:357 = (__cost':349 + K:356))
           /\ (!(0 <= K:356) \/ mid_x:358 = (x':350 + K:356))
           /\ (!(0 <= K:356) \/ mid_y:359 = (y':351 + -K:356))
           /\ ((K:356 = 0 /\ __cost':349 = mid___cost:357
                  /\ x':350 = mid_x:358 /\ y':351 = mid_y:359)
                 \/ (1 <= K:356 /\ 0 <= __cost':349 /\ 0 <= (-1 + y':351)
                       /\ 0 <= mid_y:359 /\ 0 <= (-1 + mid___cost:357)))
           /\ K:360 = 0 /\ mid___cost:357 = __cost':361 /\ mid_x:358 = x':362
           /\ mid_y:359 = y':363 /\ 0 = K:360 /\ (K:356 + K:360) = K:364
           /\ 0 <= K:364 /\ y':363 <= 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=31: 
Weight(Base relation: 
  {y := y':146
   x := x':147
   __cost := __cost':148
   return := havoc:182
   return@pos := type_err:183
   return@width := type_err:184
   when ((!(0 <= K:177) \/ mid___cost:179 = (__cost:102 + K:177))
           /\ (!(0 <= K:177) \/ mid_x:180 = (x:103 + K:177))
           /\ (!(0 <= K:177) \/ mid_y:181 = (y:4 + -K:177))
           /\ ((K:177 = 0 /\ __cost:102 = mid___cost:179 /\ x:103 = mid_x:180
                  /\ y:4 = mid_y:181)
                 \/ (1 <= K:177 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                       /\ 0 <= mid_y:181 /\ 0 <= (-1 + mid___cost:179)))
           /\ K:178 = 0 /\ mid___cost:179 = __cost':148 /\ mid_x:180 = x':147
           /\ mid_y:181 = y':146 /\ 0 = K:178 /\ (K:177 + K:178) = K:176
           /\ 0 <= K:176 /\ y':146 <= 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=37: 
Weight(Base relation: 
  {y := y':146
   x := x':147
   __cost := __cost':148
   return := havoc:164
   return@pos := type_err:165
   return@width := type_err:166
   when ((!(0 <= K:159) \/ mid___cost:161 = (__cost:102 + -K:159))
           /\ (!(0 <= K:159) \/ mid_y:163 = (y:4 + K:159))
           /\ (!(0 <= K:159) \/ mid_x:162 = (x:103 + -K:159))
           /\ ((K:159 = 0 /\ __cost:102 = mid___cost:161 /\ x:103 = mid_x:162
                  /\ y:4 = mid_y:163)
                 \/ (1 <= K:159 /\ 0 <= (-1 + __cost:102)
                       /\ 0 <= (-1 + x:103) /\ 0 <= mid_x:162
                       /\ 0 <= mid___cost:161)) /\ K:160 = 0
           /\ mid___cost:161 = __cost':148 /\ mid_x:162 = x':147
           /\ mid_y:163 = y':146 /\ 0 = K:160 /\ (K:159 + K:160) = K:158
           /\ 0 <= K:158 /\ x':147 <= 0)})


Step 5: =========================================================
[Newton] Running Newton
-------------------------------------------------------------------------------
Round 0:
Evaluating variable number 6 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{y := y':276
 x := x':275
 __cost := __cost':274
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:285
 param0@pos := type_err:280
 param1@pos := type_err:281
 return@width := type_err:286
 param0@width := type_err:283
 param1@width := type_err:284
 when (((0 < havoc:21 /\ havoc:21 = phi_tmp___0:30)
          \/ (havoc:21 <= 0 /\ 0 = phi_tmp___0:30))
         /\ (!(0 <= K:251) \/ mid___cost:252 = K:251)
         /\ (!(0 <= K:251) \/ mid_x:253 = (havoc:20 + K:251))
         /\ (!(0 <= K:251) \/ mid_y:254 = (havoc:21 + -K:251))
         /\ ((K:251 = 0 /\ 0 = mid___cost:252 /\ havoc:20 = mid_x:253
                /\ havoc:21 = mid_y:254)
               \/ (1 <= K:251 /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_y:254
                     /\ 0 <= (-1 + mid___cost:252))) /\ K:255 = 0
         /\ mid___cost:252 = __cost':256 /\ mid_x:253 = x':257
         /\ mid_y:254 = y':258 /\ 0 = K:255 /\ (K:251 + K:255) = K:259
         /\ 0 <= K:259 /\ y':258 <= 0
         /\ (!(0 <= K:260) \/ mid___cost:261 = (__cost':256 + -K:260))
         /\ (!(0 <= K:260) \/ mid_y:262 = (y':258 + K:260))
         /\ (!(0 <= K:260) \/ mid_x:263 = (x':257 + -K:260))
         /\ ((K:260 = 0 /\ __cost':256 = mid___cost:261 /\ x':257 = mid_x:263
                /\ y':258 = mid_y:262)
               \/ (1 <= K:260 /\ 0 <= (-1 + __cost':256)
                     /\ 0 <= (-1 + x':257) /\ 0 <= mid_x:263
                     /\ 0 <= mid___cost:261)) /\ K:264 = 0
         /\ mid___cost:261 = __cost':265 /\ mid_x:263 = x':266
         /\ mid_y:262 = y':267 /\ 0 = K:264 /\ (K:260 + K:264) = K:268
         /\ 0 <= K:268 /\ x':266 <= 0
         /\ (!(0 <= K:269) \/ mid___cost:270 = (__cost':265 + K:269))
         /\ (!(0 <= K:269) \/ mid_x:271 = (x':266 + K:269))
         /\ (!(0 <= K:269) \/ mid_y:272 = (y':267 + -K:269))
         /\ ((K:269 = 0 /\ __cost':265 = mid___cost:270 /\ x':266 = mid_x:271
                /\ y':267 = mid_y:272)
               \/ (1 <= K:269 /\ 0 <= __cost':265 /\ 0 <= (-1 + y':267)
                     /\ 0 <= mid_y:272 /\ 0 <= (-1 + mid___cost:270)))
         /\ K:273 = 0 /\ mid___cost:270 = __cost':274 /\ mid_x:271 = x':275
         /\ mid_y:272 = y':276 /\ 0 = K:273 /\ (K:269 + K:273) = K:277
         /\ 0 <= K:277 /\ y':276 <= 0)}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{y := y':336
 x := x':335
 __cost := __cost':334
 return := havoc:341
 param0 := param0:73
 param1 := param1:76
 return@pos := type_err:342
 param0@pos := type_err:81
 param1@pos := type_err:82
 return@width := type_err:343
 param0@width := type_err:83
 param1@width := type_err:84
 when ((!(0 <= K:311) \/ mid___cost:312 = (__cost:102 + K:311))
         /\ (!(0 <= K:311) \/ mid_x:313 = (x:103 + K:311))
         /\ (!(0 <= K:311) \/ mid_y:314 = (y:4 + -K:311))
         /\ ((K:311 = 0 /\ __cost:102 = mid___cost:312 /\ x:103 = mid_x:313
                /\ y:4 = mid_y:314)
               \/ (1 <= K:311 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                     /\ 0 <= mid_y:314 /\ 0 <= (-1 + mid___cost:312)))
         /\ K:315 = 0 /\ mid___cost:312 = __cost':316 /\ mid_x:313 = x':317
         /\ mid_y:314 = y':318 /\ 0 = K:315 /\ (K:311 + K:315) = K:319
         /\ 0 <= K:319 /\ y':318 <= 0
         /\ (!(0 <= K:320) \/ mid___cost:321 = (__cost':316 + -K:320))
         /\ (!(0 <= K:320) \/ mid_y:322 = (y':318 + K:320))
         /\ (!(0 <= K:320) \/ mid_x:323 = (x':317 + -K:320))
         /\ ((K:320 = 0 /\ __cost':316 = mid___cost:321 /\ x':317 = mid_x:323
                /\ y':318 = mid_y:322)
               \/ (1 <= K:320 /\ 0 <= (-1 + __cost':316)
                     /\ 0 <= (-1 + x':317) /\ 0 <= mid_x:323
                     /\ 0 <= mid___cost:321)) /\ K:324 = 0
         /\ mid___cost:321 = __cost':325 /\ mid_x:323 = x':326
         /\ mid_y:322 = y':327 /\ 0 = K:324 /\ (K:320 + K:324) = K:328
         /\ 0 <= K:328 /\ x':326 <= 0
         /\ (!(0 <= K:329) \/ mid___cost:330 = (__cost':325 + K:329))
         /\ (!(0 <= K:329) \/ mid_x:331 = (x':326 + K:329))
         /\ (!(0 <= K:329) \/ mid_y:332 = (y':327 + -K:329))
         /\ ((K:329 = 0 /\ __cost':325 = mid___cost:330 /\ x':326 = mid_x:331
                /\ y':327 = mid_y:332)
               \/ (1 <= K:329 /\ 0 <= __cost':325 /\ 0 <= (-1 + y':327)
                     /\ 0 <= mid_y:332 /\ 0 <= (-1 + mid___cost:330)))
         /\ K:333 = 0 /\ mid___cost:330 = __cost':334 /\ mid_x:331 = x':335
         /\ mid_y:332 = y':336 /\ 0 = K:333 /\ (K:329 + K:333) = K:337
         /\ 0 <= K:337 /\ y':336 <= 0)}

Evaluating variable number 25 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{y := y':363
 x := x':362
 __cost := __cost':361
 return := havoc:365
 return@pos := type_err:366
 return@width := type_err:367
 when ((!(0 <= K:177) \/ mid___cost:179 = (__cost:102 + K:177))
         /\ (!(0 <= K:177) \/ mid_x:180 = (x:103 + K:177))
         /\ (!(0 <= K:177) \/ mid_y:181 = (y:4 + -K:177))
         /\ ((K:177 = 0 /\ __cost:102 = mid___cost:179 /\ x:103 = mid_x:180
                /\ y:4 = mid_y:181)
               \/ (1 <= K:177 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                     /\ 0 <= mid_y:181 /\ 0 <= (-1 + mid___cost:179)))
         /\ K:178 = 0 /\ mid___cost:179 = __cost':148 /\ mid_x:180 = x':147
         /\ mid_y:181 = y':146 /\ 0 = K:178 /\ (K:177 + K:178) = K:176
         /\ 0 <= K:176 /\ y':146 <= 0
         /\ (!(0 <= K:344) \/ mid___cost:345 = (__cost':148 + -K:344))
         /\ (!(0 <= K:344) \/ mid_y:346 = (y':146 + K:344))
         /\ (!(0 <= K:344) \/ mid_x:347 = (x':147 + -K:344))
         /\ ((K:344 = 0 /\ __cost':148 = mid___cost:345 /\ x':147 = mid_x:347
                /\ y':146 = mid_y:346)
               \/ (1 <= K:344 /\ 0 <= (-1 + __cost':148)
                     /\ 0 <= (-1 + x':147) /\ 0 <= mid_x:347
                     /\ 0 <= mid___cost:345)) /\ K:348 = 0
         /\ mid___cost:345 = __cost':349 /\ mid_x:347 = x':350
         /\ mid_y:346 = y':351 /\ 0 = K:348 /\ (K:344 + K:348) = K:352
         /\ 0 <= K:352 /\ x':350 <= 0
         /\ (!(0 <= K:356) \/ mid___cost:357 = (__cost':349 + K:356))
         /\ (!(0 <= K:356) \/ mid_x:358 = (x':350 + K:356))
         /\ (!(0 <= K:356) \/ mid_y:359 = (y':351 + -K:356))
         /\ ((K:356 = 0 /\ __cost':349 = mid___cost:357 /\ x':350 = mid_x:358
                /\ y':351 = mid_y:359)
               \/ (1 <= K:356 /\ 0 <= __cost':349 /\ 0 <= (-1 + y':351)
                     /\ 0 <= mid_y:359 /\ 0 <= (-1 + mid___cost:357)))
         /\ K:360 = 0 /\ mid___cost:357 = __cost':361 /\ mid_x:358 = x':362
         /\ mid_y:359 = y':363 /\ 0 = K:360 /\ (K:356 + K:360) = K:364
         /\ 0 <= K:364 /\ y':363 <= 0)}

Evaluating variable number 31 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{y := y':146
 x := x':147
 __cost := __cost':148
 return := havoc:182
 return@pos := type_err:183
 return@width := type_err:184
 when ((!(0 <= K:177) \/ mid___cost:179 = (__cost:102 + K:177))
         /\ (!(0 <= K:177) \/ mid_x:180 = (x:103 + K:177))
         /\ (!(0 <= K:177) \/ mid_y:181 = (y:4 + -K:177))
         /\ ((K:177 = 0 /\ __cost:102 = mid___cost:179 /\ x:103 = mid_x:180
                /\ y:4 = mid_y:181)
               \/ (1 <= K:177 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                     /\ 0 <= mid_y:181 /\ 0 <= (-1 + mid___cost:179)))
         /\ K:178 = 0 /\ mid___cost:179 = __cost':148 /\ mid_x:180 = x':147
         /\ mid_y:181 = y':146 /\ 0 = K:178 /\ (K:177 + K:178) = K:176
         /\ 0 <= K:176 /\ y':146 <= 0)}

Evaluating variable number 37 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{y := y':146
 x := x':147
 __cost := __cost':148
 return := havoc:164
 return@pos := type_err:165
 return@width := type_err:166
 when ((!(0 <= K:159) \/ mid___cost:161 = (__cost:102 + -K:159))
         /\ (!(0 <= K:159) \/ mid_y:163 = (y:4 + K:159))
         /\ (!(0 <= K:159) \/ mid_x:162 = (x:103 + -K:159))
         /\ ((K:159 = 0 /\ __cost:102 = mid___cost:161 /\ x:103 = mid_x:162
                /\ y:4 = mid_y:163)
               \/ (1 <= K:159 /\ 0 <= (-1 + __cost:102) /\ 0 <= (-1 + x:103)
                     /\ 0 <= mid_x:162 /\ 0 <= mid___cost:161)) /\ K:160 = 0
         /\ mid___cost:161 = __cost':148 /\ mid_x:162 = x':147
         /\ mid_y:163 = y':146 /\ 0 = K:160 /\ (K:159 + K:160) = K:158
         /\ 0 <= K:158 /\ x':147 <= 0)}

    (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,79)_g1>	Base relation: 
{y := havoc:21
 x := havoc:20
 __cost := 0
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:31
 param1@pos := type_err:32
 param0@width := type_err:33
 param1@width := type_err:34
 when ((0 < havoc:21 /\ havoc:21 = phi_tmp___0:30)
         \/ (havoc:21 <= 0 /\ 0 = phi_tmp___0:30))}	
<__pstate, (Unique State Name,79)_g1> -> <__pstate, (Unique State Name,73)_g1>	Base relation: 
{param0 := param0:73
 param1 := param1:76
 param0@pos := type_err:81
 param1@pos := type_err:82
 param0@width := type_err:83
 param1@width := type_err:84}	
<__pstate, (Unique State Name,73)_g1> -> <__pstate, (Unique State Name,47)_g1>	Base relation: 
{y := phi_y:472
 x := phi_x:471
 __cost := phi___cost:470
 return := phi_return:468
 return@pos := phi_return@pos:466
 return@width := phi_return@width:464
 when (((!(0 <= K:177) \/ mid___cost:179 = (__cost:102 + K:177))
          /\ (!(0 <= K:177) \/ mid_x:180 = (x:103 + K:177))
          /\ (!(0 <= K:177) \/ mid_y:181 = (y:4 + -K:177))
          /\ ((K:177 = 0 /\ __cost:102 = mid___cost:179 /\ x:103 = mid_x:180
                 /\ y:4 = mid_y:181)
                \/ (1 <= K:177 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                      /\ 0 <= mid_y:181 /\ 0 <= (-1 + mid___cost:179)))
          /\ K:178 = 0 /\ mid___cost:179 = __cost':148 /\ mid_x:180 = x':147
          /\ mid_y:181 = y':146 /\ 0 = K:178 /\ (K:177 + K:178) = K:176
          /\ 0 <= K:176 /\ y':146 <= 0
          /\ (!(0 <= K:437) \/ mid___cost:438 = (__cost':148 + -K:437))
          /\ (!(0 <= K:437) \/ mid_y:439 = (y':146 + K:437))
          /\ (!(0 <= K:437) \/ mid_x:440 = (x':147 + -K:437))
          /\ ((K:437 = 0 /\ __cost':148 = mid___cost:438
                 /\ x':147 = mid_x:440 /\ y':146 = mid_y:439)
                \/ (1 <= K:437 /\ 0 <= (-1 + __cost':148)
                      /\ 0 <= (-1 + x':147) /\ 0 <= mid_x:440
                      /\ 0 <= mid___cost:438)) /\ K:441 = 0
          /\ mid___cost:438 = __cost':442 /\ mid_x:440 = x':443
          /\ mid_y:439 = y':444 /\ 0 = K:441 /\ (K:437 + K:441) = K:445
          /\ 0 <= K:445 /\ x':443 <= 0 /\ y':444 = phi_y:472
          /\ x':443 = phi_x:471 /\ __cost':442 = phi___cost:470
          /\ havoc:446 = phi_return:468 /\ type_err:447 = phi_return@pos:466
          /\ type_err:448 = phi_return@width:464)
         \/ (y:4 = phi_y:472 /\ x:103 = phi_x:471
               /\ __cost:102 = phi___cost:470 /\ return:469 = phi_return:468
               /\ return@pos:467 = phi_return@pos:466
               /\ return@width:465 = phi_return@width:464))}	
<__pstate, (Unique State Name,73)_g1> -> <__pstate, (Unique State Name,66)_g1>	Base relation: 
{y := y':146
 x := x':147
 __cost := __cost':148
 return := havoc:182
 return@pos := type_err:183
 return@width := type_err:184
 when ((!(0 <= K:177) \/ mid___cost:179 = (__cost:102 + K:177))
         /\ (!(0 <= K:177) \/ mid_x:180 = (x:103 + K:177))
         /\ (!(0 <= K:177) \/ mid_y:181 = (y:4 + -K:177))
         /\ ((K:177 = 0 /\ __cost:102 = mid___cost:179 /\ x:103 = mid_x:180
                /\ y:4 = mid_y:181)
               \/ (1 <= K:177 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                     /\ 0 <= mid_y:181 /\ 0 <= (-1 + mid___cost:179)))
         /\ K:178 = 0 /\ mid___cost:179 = __cost':148 /\ mid_x:180 = x':147
         /\ mid_y:181 = y':146 /\ 0 = K:178 /\ (K:177 + K:178) = K:176
         /\ 0 <= K:176 /\ y':146 <= 0)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x44df260: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x4e38040: 
	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,47)_g1 , __done )	Base relation: 
{y := phi_y:495
 x := phi_x:496
 __cost := phi___cost:497
 return := phi_return:499
 param0 := havoc:21
 param1 := havoc:22
 return@pos := phi_return@pos:501
 param0@pos := type_err:473
 param1@pos := type_err:474
 return@width := phi_return@width:503
 param0@width := type_err:475
 param1@width := type_err:476
 when (((0 < havoc:21 /\ havoc:21 = phi_tmp___0:30)
          \/ (havoc:21 <= 0 /\ 0 = phi_tmp___0:30))
         /\ (((!(0 <= K:477) \/ mid___cost:478 = K:477)
                /\ (!(0 <= K:477) \/ mid_x:479 = (havoc:20 + K:477))
                /\ (!(0 <= K:477) \/ mid_y:480 = (havoc:21 + -K:477))
                /\ ((K:477 = 0 /\ 0 = mid___cost:478 /\ havoc:20 = mid_x:479
                       /\ havoc:21 = mid_y:480)
                      \/ (1 <= K:477 /\ 0 <= (-1 + havoc:21)
                            /\ 0 <= mid_y:480 /\ 0 <= (-1 + mid___cost:478)))
                /\ K:481 = 0 /\ mid___cost:478 = __cost':482
                /\ mid_x:479 = x':483 /\ mid_y:480 = y':484 /\ 0 = K:481
                /\ (K:477 + K:481) = K:485 /\ 0 <= K:485 /\ y':484 <= 0
                /\ (!(0 <= K:486) \/ mid___cost:487 = (__cost':482 + -K:486))
                /\ (!(0 <= K:486) \/ mid_y:488 = (y':484 + K:486))
                /\ (!(0 <= K:486) \/ mid_x:489 = (x':483 + -K:486))
                /\ ((K:486 = 0 /\ __cost':482 = mid___cost:487
                       /\ x':483 = mid_x:489 /\ y':484 = mid_y:488)
                      \/ (1 <= K:486 /\ 0 <= (-1 + __cost':482)
                            /\ 0 <= (-1 + x':483) /\ 0 <= mid_x:489
                            /\ 0 <= mid___cost:487)) /\ K:490 = 0
                /\ mid___cost:487 = __cost':491 /\ mid_x:489 = x':492
                /\ mid_y:488 = y':493 /\ 0 = K:490 /\ (K:486 + K:490) = K:494
                /\ 0 <= K:494 /\ x':492 <= 0 /\ y':493 = phi_y:495
                /\ x':492 = phi_x:496 /\ __cost':491 = phi___cost:497
                /\ havoc:498 = phi_return:499
                /\ type_err:500 = phi_return@pos:501
                /\ type_err:502 = phi_return@width:503)
               \/ (havoc:21 = phi_y:495 /\ havoc:20 = phi_x:496
                     /\ 0 = phi___cost:497 /\ return:469 = phi_return:499
                     /\ return@pos:467 = phi_return@pos:501
                     /\ return@width:465 = phi_return@width:503)))}
    ( __pstate , (Unique State Name,79)_g1 , __done )	Base relation: 
{y := havoc:21
 x := havoc:20
 __cost := 0
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:31
 param1@pos := type_err:32
 param0@width := type_err:33
 param1@width := type_err:34
 when ((0 < havoc:21 /\ havoc:21 = phi_tmp___0:30)
         \/ (havoc:21 <= 0 /\ 0 = phi_tmp___0:30))}
    ( __pstate , (Unique State Name,73)_g1 , __done )	Base relation: 
{y := havoc:21
 x := havoc:20
 __cost := 0
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:504
 param1@pos := type_err:505
 param0@width := type_err:506
 param1@width := type_err:507
 when ((0 < havoc:21 /\ havoc:21 = phi_tmp___0:30)
         \/ (havoc:21 <= 0 /\ 0 = phi_tmp___0:30))}
    ( __pstate , (Unique State Name,66)_g1 , __done )	Base relation: 
{y := y':519
 x := x':518
 __cost := __cost':517
 return := havoc:521
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:522
 param0@pos := type_err:508
 param1@pos := type_err:509
 return@width := type_err:523
 param0@width := type_err:510
 param1@width := type_err:511
 when (((0 < havoc:21 /\ havoc:21 = phi_tmp___0:30)
          \/ (havoc:21 <= 0 /\ 0 = phi_tmp___0:30))
         /\ (!(0 <= K:512) \/ mid___cost:513 = K:512)
         /\ (!(0 <= K:512) \/ mid_x:514 = (havoc:20 + K:512))
         /\ (!(0 <= K:512) \/ mid_y:515 = (havoc:21 + -K:512))
         /\ ((K:512 = 0 /\ 0 = mid___cost:513 /\ havoc:20 = mid_x:514
                /\ havoc:21 = mid_y:515)
               \/ (1 <= K:512 /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_y:515
                     /\ 0 <= (-1 + mid___cost:513))) /\ K:516 = 0
         /\ mid___cost:513 = __cost':517 /\ mid_x:514 = x':518
         /\ mid_y:515 = y':519 /\ 0 = K:516 /\ (K:512 + K:516) = K:520
         /\ 0 <= K:520 /\ y':519 <= 0)}

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

------------------------------------------------
Procedure summary for consume

Base relation: 
{y := y':146
 x := x':147
 __cost := __cost':148
 return := havoc:182
 return@pos := type_err:183
 return@width := type_err:184
 when ((!(0 <= K:177) \/ mid___cost:179 = (__cost:102 + K:177))
         /\ (!(0 <= K:177) \/ mid_x:180 = (x:103 + K:177))
         /\ (!(0 <= K:177) \/ mid_y:181 = (y:4 + -K:177))
         /\ ((K:177 = 0 /\ __cost:102 = mid___cost:179 /\ x:103 = mid_x:180
                /\ y:4 = mid_y:181)
               \/ (1 <= K:177 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                     /\ 0 <= mid_y:181 /\ 0 <= (-1 + mid___cost:179)))
         /\ K:178 = 0 /\ mid___cost:179 = __cost':148 /\ mid_x:180 = x':147
         /\ mid_y:181 = y':146 /\ 0 = K:178 /\ (K:177 + K:178) = K:176
         /\ 0 <= K:176 /\ y':146 <= 0)}

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

Base relation: 
{y := y':393
 x := x':392
 __cost := __cost':391
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:402
 param0@pos := type_err:397
 param1@pos := type_err:398
 return@width := type_err:403
 param0@width := type_err:400
 param1@width := type_err:401
 when (((0 < havoc:21 /\ havoc:21 = phi_tmp___0:30)
          \/ (havoc:21 <= 0 /\ 0 = phi_tmp___0:30))
         /\ (!(0 <= K:368) \/ mid___cost:369 = K:368)
         /\ (!(0 <= K:368) \/ mid_x:370 = (havoc:20 + K:368))
         /\ (!(0 <= K:368) \/ mid_y:371 = (havoc:21 + -K:368))
         /\ ((K:368 = 0 /\ 0 = mid___cost:369 /\ havoc:20 = mid_x:370
                /\ havoc:21 = mid_y:371)
               \/ (1 <= K:368 /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_y:371
                     /\ 0 <= (-1 + mid___cost:369))) /\ K:372 = 0
         /\ mid___cost:369 = __cost':373 /\ mid_x:370 = x':374
         /\ mid_y:371 = y':375 /\ 0 = K:372 /\ (K:368 + K:372) = K:376
         /\ 0 <= K:376 /\ y':375 <= 0
         /\ (!(0 <= K:377) \/ mid___cost:378 = (__cost':373 + -K:377))
         /\ (!(0 <= K:377) \/ mid_y:379 = (y':375 + K:377))
         /\ (!(0 <= K:377) \/ mid_x:380 = (x':374 + -K:377))
         /\ ((K:377 = 0 /\ __cost':373 = mid___cost:378 /\ x':374 = mid_x:380
                /\ y':375 = mid_y:379)
               \/ (1 <= K:377 /\ 0 <= (-1 + __cost':373)
                     /\ 0 <= (-1 + x':374) /\ 0 <= mid_x:380
                     /\ 0 <= mid___cost:378)) /\ K:381 = 0
         /\ mid___cost:378 = __cost':382 /\ mid_x:380 = x':383
         /\ mid_y:379 = y':384 /\ 0 = K:381 /\ (K:377 + K:381) = K:385
         /\ 0 <= K:385 /\ x':383 <= 0
         /\ (!(0 <= K:386) \/ mid___cost:387 = (__cost':382 + K:386))
         /\ (!(0 <= K:386) \/ mid_x:388 = (x':383 + K:386))
         /\ (!(0 <= K:386) \/ mid_y:389 = (y':384 + -K:386))
         /\ ((K:386 = 0 /\ __cost':382 = mid___cost:387 /\ x':383 = mid_x:388
                /\ y':384 = mid_y:389)
               \/ (1 <= K:386 /\ 0 <= __cost':382 /\ 0 <= (-1 + y':384)
                     /\ 0 <= mid_y:389 /\ 0 <= (-1 + mid___cost:387)))
         /\ K:390 = 0 /\ mid___cost:387 = __cost':391 /\ mid_x:388 = x':392
         /\ mid_y:389 = y':393 /\ 0 = K:390 /\ (K:386 + K:390) = K:394
         /\ 0 <= K:394 /\ y':393 <= 0)}

------------------------------------------------
Procedure summary for produce

Base relation: 
{y := y':146
 x := x':147
 __cost := __cost':148
 return := havoc:164
 return@pos := type_err:165
 return@width := type_err:166
 when ((!(0 <= K:159) \/ mid___cost:161 = (__cost:102 + -K:159))
         /\ (!(0 <= K:159) \/ mid_y:163 = (y:4 + K:159))
         /\ (!(0 <= K:159) \/ mid_x:162 = (x:103 + -K:159))
         /\ ((K:159 = 0 /\ __cost:102 = mid___cost:161 /\ x:103 = mid_x:162
                /\ y:4 = mid_y:163)
               \/ (1 <= K:159 /\ 0 <= (-1 + __cost:102) /\ 0 <= (-1 + x:103)
                     /\ 0 <= mid_x:162 /\ 0 <= mid___cost:161)) /\ K:160 = 0
         /\ mid___cost:161 = __cost':148 /\ mid_x:162 = x':147
         /\ mid_y:163 = y':146 /\ 0 = K:160 /\ (K:159 + K:160) = K:158
         /\ 0 <= K:158 /\ x':147 <= 0)}

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

Base relation: 
{y := y':429
 x := x':428
 __cost := __cost':427
 return := havoc:434
 param0 := param0:73
 param1 := param1:76
 return@pos := type_err:435
 param0@pos := type_err:81
 param1@pos := type_err:82
 return@width := type_err:436
 param0@width := type_err:83
 param1@width := type_err:84
 when ((!(0 <= K:404) \/ mid___cost:405 = (__cost:102 + K:404))
         /\ (!(0 <= K:404) \/ mid_x:406 = (x:103 + K:404))
         /\ (!(0 <= K:404) \/ mid_y:407 = (y:4 + -K:404))
         /\ ((K:404 = 0 /\ __cost:102 = mid___cost:405 /\ x:103 = mid_x:406
                /\ y:4 = mid_y:407)
               \/ (1 <= K:404 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                     /\ 0 <= mid_y:407 /\ 0 <= (-1 + mid___cost:405)))
         /\ K:408 = 0 /\ mid___cost:405 = __cost':409 /\ mid_x:406 = x':410
         /\ mid_y:407 = y':411 /\ 0 = K:408 /\ (K:404 + K:408) = K:412
         /\ 0 <= K:412 /\ y':411 <= 0
         /\ (!(0 <= K:413) \/ mid___cost:414 = (__cost':409 + -K:413))
         /\ (!(0 <= K:413) \/ mid_y:415 = (y':411 + K:413))
         /\ (!(0 <= K:413) \/ mid_x:416 = (x':410 + -K:413))
         /\ ((K:413 = 0 /\ __cost':409 = mid___cost:414 /\ x':410 = mid_x:416
                /\ y':411 = mid_y:415)
               \/ (1 <= K:413 /\ 0 <= (-1 + __cost':409)
                     /\ 0 <= (-1 + x':410) /\ 0 <= mid_x:416
                     /\ 0 <= mid___cost:414)) /\ K:417 = 0
         /\ mid___cost:414 = __cost':418 /\ mid_x:416 = x':419
         /\ mid_y:415 = y':420 /\ 0 = K:417 /\ (K:413 + K:417) = K:421
         /\ 0 <= K:421 /\ x':419 <= 0
         /\ (!(0 <= K:422) \/ mid___cost:423 = (__cost':418 + K:422))
         /\ (!(0 <= K:422) \/ mid_x:424 = (x':419 + K:422))
         /\ (!(0 <= K:422) \/ mid_y:425 = (y':420 + -K:422))
         /\ ((K:422 = 0 /\ __cost':418 = mid___cost:423 /\ x':419 = mid_x:424
                /\ y':420 = mid_y:425)
               \/ (1 <= K:422 /\ 0 <= __cost':418 /\ 0 <= (-1 + y':420)
                     /\ 0 <= mid_y:425 /\ 0 <= (-1 + mid___cost:423)))
         /\ K:426 = 0 /\ mid___cost:423 = __cost':427 /\ mid_x:424 = x':428
         /\ mid_y:425 = y':429 /\ 0 = K:426 /\ (K:422 + K:426) = K:430
         /\ 0 <= K:430 /\ y':429 <= 0)}

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

Base relation: 
{y := y':456
 x := x':455
 __cost := __cost':454
 return := havoc:461
 return@pos := type_err:462
 return@width := type_err:463
 when ((!(0 <= K:177) \/ mid___cost:179 = (__cost:102 + K:177))
         /\ (!(0 <= K:177) \/ mid_x:180 = (x:103 + K:177))
         /\ (!(0 <= K:177) \/ mid_y:181 = (y:4 + -K:177))
         /\ ((K:177 = 0 /\ __cost:102 = mid___cost:179 /\ x:103 = mid_x:180
                /\ y:4 = mid_y:181)
               \/ (1 <= K:177 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:4)
                     /\ 0 <= mid_y:181 /\ 0 <= (-1 + mid___cost:179)))
         /\ K:178 = 0 /\ mid___cost:179 = __cost':148 /\ mid_x:180 = x':147
         /\ mid_y:181 = y':146 /\ 0 = K:178 /\ (K:177 + K:178) = K:176
         /\ 0 <= K:176 /\ y':146 <= 0
         /\ (!(0 <= K:437) \/ mid___cost:438 = (__cost':148 + -K:437))
         /\ (!(0 <= K:437) \/ mid_y:439 = (y':146 + K:437))
         /\ (!(0 <= K:437) \/ mid_x:440 = (x':147 + -K:437))
         /\ ((K:437 = 0 /\ __cost':148 = mid___cost:438 /\ x':147 = mid_x:440
                /\ y':146 = mid_y:439)
               \/ (1 <= K:437 /\ 0 <= (-1 + __cost':148)
                     /\ 0 <= (-1 + x':147) /\ 0 <= mid_x:440
                     /\ 0 <= mid___cost:438)) /\ K:441 = 0
         /\ mid___cost:438 = __cost':442 /\ mid_x:440 = x':443
         /\ mid_y:439 = y':444 /\ 0 = K:441 /\ (K:437 + K:441) = K:445
         /\ 0 <= K:445 /\ x':443 <= 0
         /\ (!(0 <= K:449) \/ mid___cost:450 = (__cost':442 + K:449))
         /\ (!(0 <= K:449) \/ mid_x:451 = (x':443 + K:449))
         /\ (!(0 <= K:449) \/ mid_y:452 = (y':444 + -K:449))
         /\ ((K:449 = 0 /\ __cost':442 = mid___cost:450 /\ x':443 = mid_x:451
                /\ y':444 = mid_y:452)
               \/ (1 <= K:449 /\ 0 <= __cost':442 /\ 0 <= (-1 + y':444)
                     /\ 0 <= mid_y:452 /\ 0 <= (-1 + mid___cost:450)))
         /\ K:453 = 0 /\ mid___cost:450 = __cost':454 /\ mid_x:451 = x':455
         /\ mid_y:452 = y':456 /\ 0 = K:453 /\ (K:449 + K:453) = K:457
         /\ 0 <= K:457 /\ y':456 <= 0)}

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

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

Variable bounds at line 28 in run

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

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