/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, 97> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 96> -> <Unique State Name, 91 95>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 99> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 29> -> <Unique State Name, 96>	Base relation: 
{__cost := 0
 x := havoc:22
 y := havoc:23
 param0 := havoc:22
 param1 := havoc:23
 param0@pos := type_err:29
 param1@pos := type_err:31
 param0@width := type_err:30
 param1@width := type_err:32}	
<Unique State Name, 31> -> <Unique State Name, 98>	Base relation: 
{return := havoc:70
 return@pos := type_err:73
 return@width := type_err:74}	
<Unique State Name, 90> -> <Unique State Name, 85 89>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 89> -> <Unique State Name, 31>	Base relation: 
{}	
<Unique State Name, 71> -> <Unique State Name, 67>	Base relation: 
{__cost := (__cost:110 + 1)
 x := (x:109 + 1)
 when (x:109 < 0 /\ 0 <= __cost:110 /\ 0 <= (__cost:110 + 1))}	
<Unique State Name, 71> -> <Unique State Name, 97>	Base relation: 
{return := havoc:116
 return@pos := type_err:117
 return@width := type_err:118
 when 0 <= x:109}	
<Unique State Name, 39> -> <Unique State Name, 35>	Base relation: 
{__cost := (__cost:110 + 1)
 x := ((x:109 + -1) + 1000)
 y := (y:108 + 1000)
 when (y:108 < x:109 /\ 0 <= __cost:110 /\ 0 <= (__cost:110 + 1))}	
<Unique State Name, 39> -> <Unique State Name, 52>	Base relation: 
{when x:109 <= y:108}	
<Unique State Name, 85> -> <Unique State Name, 35>	Base relation: 
{x := param0:87
 y := param1:90}	
<Unique State Name, 101> -> <Unique State Name, 56>	Base relation: 
{}	
<Unique State Name, 91> -> <Unique State Name, 90>	Base relation: 
{param0 := param0:87
 param1 := param1:90
 param0@pos := type_err:95
 param1@pos := type_err:96
 param0@width := type_err:97
 param1@width := type_err:98}	
<Unique State Name, 35> -> <Unique State Name, 102>	Base relation: 
{}	
<Unique State Name, 98> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 100> -> <Unique State Name, 71>	Base relation: 
{}	
<Unique State Name, 102> -> <Unique State Name, 39>	Base relation: 
{}	
<Unique State Name, 95> -> <Unique State Name, 99>	Base relation: 
{return := 0
 return@pos := type_err:35
 return@width := type_err:36
 when (((x:4 < 0 /\ -x:4 = phi_tmp___1:24)
          \/ (0 <= x:4 /\ 0 = phi_tmp___1:24))
         /\ ((0 < y:5 /\ y:5 = phi_tmp___2:33)
               \/ (y:5 <= 0 /\ 0 = phi_tmp___2:33))
         /\ ((y:5 < x:4 /\ (x:4 + -y:5) = phi_tmp___3:34)
               \/ (x:4 <= y:5 /\ 0 = phi_tmp___3:34)))}	
<Unique State Name, 52> -> <Unique State Name, 101>	Base relation: 
{}	
<Unique State Name, 56> -> <Unique State Name, 52>	Base relation: 
{__cost := (__cost:110 + 1)
 y := (y:108 + -1)
 when (0 < y:108 /\ 0 <= __cost:110 /\ 0 <= (__cost:110 + 1))}	
<Unique State Name, 56> -> <Unique State Name, 67>	Base relation: 
{when y:108 <= 0}	
<Unique State Name, 67> -> <Unique State Name, 100>	Base relation: 
{}	
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:110 + 1)
 x := ((x:109 + -1) + 1000)
 y := (y:108 + 1000)
 when (y:108 < x:109 /\ 0 <= __cost:110 /\ 0 <= (__cost:110 + 1))}
**** alpha hat: 
  {<Split [true
            (y':223) = (1)*(y:108) + 1000*1
           (x':222) = (1)*(x:109) + 999*1
           (__cost':221) = (1)*(__cost:110) + 1
           }
          pre:
            [|-y:108+x:109-1>=0; __cost:110>=0|]
          post:
            [|-y':223+x':222>=0; __cost':221-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':221
   x := x':222
   y := y':223
   when ((!(0 <= K:234) \/ mid_y:236 = (y:108 + (1000 * K:234)))
           /\ (!(0 <= K:234) \/ mid_x:237 = (x:109 + (999 * K:234)))
           /\ (!(0 <= K:234) \/ mid___cost:238 = (__cost:110 + K:234))
           /\ ((K:234 = 0 /\ y:108 = mid_y:236 /\ x:109 = mid_x:237
                  /\ __cost:110 = mid___cost:238)
                 \/ (1 <= K:234 /\ 0 <= (-1 + -y:108 + x:109)
                       /\ 0 <= __cost:110 /\ 0 <= (-mid_y:236 + mid_x:237)
                       /\ 0 <= (-1 + mid___cost:238))) /\ K:235 = 0
           /\ mid_y:236 = y':223 /\ mid_x:237 = x':222
           /\ mid___cost:238 = __cost':221 /\ 0 = K:235
           /\ (K:234 + K:235) = K:233 /\ 0 <= K:233)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:110 + 1)
 y := (y:108 + -1)
 when (0 < y:108 /\ 0 <= __cost:110 /\ 0 <= (__cost:110 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':221) = (1)*(__cost:110) + 1
           (y':223) = (1)*(y:108) + (-1)*1
           }
          pre:
            [|__cost:110>=0; y:108-1>=0|]
          post:
            [|y':223>=0; __cost':221-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':221
   y := y':223
   when ((!(0 <= K:255) \/ mid___cost:258 = (__cost:110 + K:255))
           /\ (!(0 <= K:255) \/ mid_y:257 = (y:108 + -K:255))
           /\ ((K:255 = 0 /\ y:108 = mid_y:257 /\ __cost:110 = mid___cost:258)
                 \/ (1 <= K:255 /\ 0 <= __cost:110 /\ 0 <= (-1 + y:108)
                       /\ 0 <= mid_y:257 /\ 0 <= (-1 + mid___cost:258)))
           /\ K:256 = 0 /\ mid_y:257 = y':223 /\ mid___cost:258 = __cost':221
           /\ 0 = K:256 /\ (K:255 + K:256) = K:254 /\ 0 <= K:254)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:110 + 1)
 x := (x:109 + 1)
 when (x:109 < 0 /\ 0 <= __cost:110 /\ 0 <= (__cost:110 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':221) = (1)*(__cost:110) + 1
           (x':222) = (1)*(x:109) + 1
           }
          pre:
            [|-x:109-1>=0; __cost:110>=0|]
          post:
            [|-x':222>=0; __cost':221-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':221
   x := x':222
   when ((!(0 <= K:273) \/ mid___cost:276 = (__cost:110 + K:273))
           /\ (!(0 <= K:273) \/ mid_x:275 = (x:109 + K:273))
           /\ ((K:273 = 0 /\ x:109 = mid_x:275 /\ __cost:110 = mid___cost:276)
                 \/ (1 <= K:273 /\ 0 <= (-1 + -x:109) /\ 0 <= __cost:110
                       /\ 0 <= -mid_x:275 /\ 0 <= (-1 + mid___cost:276)))
           /\ K:274 = 0 /\ mid_x:275 = x':222 /\ mid___cost:276 = __cost':221
           /\ 0 = K:274 /\ (K:273 + K:274) = K:272 /\ 0 <= K:272)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  25  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       x := havoc:22
       y := havoc:23
       param0 := havoc:22
       param1 := havoc:23
       param0@pos := type_err:29
       param1@pos := type_err:31
       param0@width := type_err:30
       param1@width := type_err:32}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:35
     return@width := type_err:36
     when (((x:4 < 0 /\ -x:4 = phi_tmp___1:24)
              \/ (0 <= x:4 /\ 0 = phi_tmp___1:24))
             /\ ((0 < y:5 /\ y:5 = phi_tmp___2:33)
                   \/ (y:5 <= 0 /\ 0 = phi_tmp___2:33))
             /\ ((y:5 < x:4 /\ (x:4 + -y:5) = phi_tmp___3:34)
                   \/ (x:4 <= y:5 /\ 0 = phi_tmp___3:34)))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:87
       param1 := param1:90
       param0@pos := type_err:95
       param1@pos := type_err:96
       param0@width := type_err:97
       param1@width := type_err:98}    )
    ,
    Var(25)
  )
  ,
  Weight(Base relation: 
    {return := havoc:70
     return@pos := type_err:73
     return@width := type_err:74}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=25: 
Weight(Base relation: 
  {__cost := __cost':282
   x := x':281
   y := y':263
   return := havoc:284
   return@pos := type_err:285
   return@width := type_err:286
   when ((!(0 <= K:239) \/ mid_y:240 = (param1:90 + (1000 * K:239)))
           /\ (!(0 <= K:239) \/ mid_x:241 = (param0:87 + (999 * K:239)))
           /\ (!(0 <= K:239) \/ mid___cost:242 = (__cost:110 + K:239))
           /\ ((K:239 = 0 /\ param1:90 = mid_y:240 /\ param0:87 = mid_x:241
                  /\ __cost:110 = mid___cost:242)
                 \/ (1 <= K:239 /\ 0 <= (-1 + -param1:90 + param0:87)
                       /\ 0 <= __cost:110 /\ 0 <= (-mid_y:240 + mid_x:241)
                       /\ 0 <= (-1 + mid___cost:242))) /\ K:243 = 0
           /\ mid_y:240 = y':244 /\ mid_x:241 = x':245
           /\ mid___cost:242 = __cost':246 /\ 0 = K:243
           /\ (K:239 + K:243) = K:247 /\ 0 <= K:247 /\ x':245 <= y':244
           /\ (!(0 <= K:259) \/ mid___cost:260 = (__cost':246 + K:259))
           /\ (!(0 <= K:259) \/ mid_y:261 = (y':244 + -K:259))
           /\ ((K:259 = 0 /\ y':244 = mid_y:261
                  /\ __cost':246 = mid___cost:260)
                 \/ (1 <= K:259 /\ 0 <= __cost':246 /\ 0 <= (-1 + y':244)
                       /\ 0 <= mid_y:261 /\ 0 <= (-1 + mid___cost:260)))
           /\ K:262 = 0 /\ mid_y:261 = y':263 /\ mid___cost:260 = __cost':264
           /\ 0 = K:262 /\ (K:259 + K:262) = K:265 /\ 0 <= K:265
           /\ y':263 <= 0
           /\ (!(0 <= K:277) \/ mid___cost:278 = (__cost':264 + K:277))
           /\ (!(0 <= K:277) \/ mid_x:279 = (x':245 + K:277))
           /\ ((K:277 = 0 /\ x':245 = mid_x:279
                  /\ __cost':264 = mid___cost:278)
                 \/ (1 <= K:277 /\ 0 <= (-1 + -x':245) /\ 0 <= __cost':264
                       /\ 0 <= -mid_x:279 /\ 0 <= (-1 + mid___cost:278)))
           /\ K:280 = 0 /\ mid_x:279 = x':281 /\ mid___cost:278 = __cost':282
           /\ 0 = K:280 /\ (K:277 + K:280) = K:283 /\ 0 <= K:283
           /\ 0 <= x':281)})



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:22
         y := havoc:23
         param0 := havoc:22
         param1 := havoc:23
         param0@pos := type_err:29
         param1@pos := type_err:31
         param0@width := type_err:30
         param1@width := type_err:32}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:35
       return@width := type_err:36
       when (((x:4 < 0 /\ -x:4 = phi_tmp___1:24)
                \/ (0 <= x:4 /\ 0 = phi_tmp___1:24))
               /\ ((0 < y:5 /\ y:5 = phi_tmp___2:33)
                     \/ (y:5 <= 0 /\ 0 = phi_tmp___2:33))
               /\ ((y:5 < x:4 /\ (x:4 + -y:5) = phi_tmp___3:34)
                     \/ (x:4 <= y:5 /\ 0 = phi_tmp___3:34)))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:87
         param1 := param1:90
         param0@pos := type_err:95
         param1@pos := type_err:96
         param0@width := type_err:97
         param1@width := type_err:98}      )
      ,
      Var(25)
    )
    ,
    Weight(Base relation: 
      {return := havoc:70
       return@pos := type_err:73
       return@width := type_err:74}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':282
   return := havoc:284
   return@pos := type_err:285
   return@width := type_err:286
   when ((!(0 <= K:239) \/ mid_y:240 = (param1:90 + (1000 * K:239)))
           /\ (!(0 <= K:239) \/ mid_x:241 = (param0:87 + (999 * K:239)))
           /\ (!(0 <= K:239) \/ mid___cost:242 = (__cost:110 + K:239))
           /\ ((K:239 = 0 /\ param1:90 = mid_y:240 /\ param0:87 = mid_x:241
                  /\ __cost:110 = mid___cost:242)
                 \/ (1 <= K:239 /\ 0 <= (-1 + -param1:90 + param0:87)
                       /\ 0 <= __cost:110 /\ 0 <= (-mid_y:240 + mid_x:241)
                       /\ 0 <= (-1 + mid___cost:242))) /\ K:243 = 0
           /\ mid_y:240 = y':244 /\ mid_x:241 = x':245
           /\ mid___cost:242 = __cost':246 /\ 0 = K:243
           /\ (K:239 + K:243) = K:247 /\ 0 <= K:247 /\ x':245 <= y':244
           /\ (!(0 <= K:259) \/ mid___cost:260 = (__cost':246 + K:259))
           /\ (!(0 <= K:259) \/ mid_y:261 = (y':244 + -K:259))
           /\ ((K:259 = 0 /\ y':244 = mid_y:261
                  /\ __cost':246 = mid___cost:260)
                 \/ (1 <= K:259 /\ 0 <= __cost':246 /\ 0 <= (-1 + y':244)
                       /\ 0 <= mid_y:261 /\ 0 <= (-1 + mid___cost:260)))
           /\ K:262 = 0 /\ mid_y:261 = y':263 /\ mid___cost:260 = __cost':264
           /\ 0 = K:262 /\ (K:259 + K:262) = K:265 /\ 0 <= K:265
           /\ y':263 <= 0
           /\ (!(0 <= K:277) \/ mid___cost:278 = (__cost':264 + K:277))
           /\ (!(0 <= K:277) \/ mid_x:279 = (x':245 + K:277))
           /\ ((K:277 = 0 /\ x':245 = mid_x:279
                  /\ __cost':264 = mid___cost:278)
                 \/ (1 <= K:277 /\ 0 <= (-1 + -x':245) /\ 0 <= __cost':264
                       /\ 0 <= -mid_x:279 /\ 0 <= (-1 + mid___cost:278)))
           /\ K:280 = 0 /\ mid_x:279 = x':281 /\ mid___cost:278 = __cost':282
           /\ 0 = K:280 /\ (K:277 + K:280) = K:283 /\ 0 <= K:283
           /\ 0 <= x':281)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':337
   return := 0
   param0 := havoc:22
   param1 := havoc:23
   return@pos := type_err:349
   param0@pos := type_err:341
   param1@pos := type_err:342
   return@width := type_err:350
   param0@width := type_err:344
   param1@width := type_err:345
   when ((!(0 <= K:316) \/ mid_y:317 = (havoc:23 + (1000 * K:316)))
           /\ (!(0 <= K:316) \/ mid_x:318 = (havoc:22 + (999 * K:316)))
           /\ (!(0 <= K:316) \/ mid___cost:319 = K:316)
           /\ ((K:316 = 0 /\ havoc:23 = mid_y:317 /\ havoc:22 = mid_x:318
                  /\ 0 = mid___cost:319)
                 \/ (1 <= K:316 /\ 0 <= (-1 + -havoc:23 + havoc:22)
                       /\ 0 <= (-mid_y:317 + mid_x:318)
                       /\ 0 <= (-1 + mid___cost:319))) /\ K:320 = 0
           /\ mid_y:317 = y':321 /\ mid_x:318 = x':322
           /\ mid___cost:319 = __cost':323 /\ 0 = K:320
           /\ (K:316 + K:320) = K:324 /\ 0 <= K:324 /\ x':322 <= y':321
           /\ (!(0 <= K:325) \/ mid___cost:326 = (__cost':323 + K:325))
           /\ (!(0 <= K:325) \/ mid_y:327 = (y':321 + -K:325))
           /\ ((K:325 = 0 /\ y':321 = mid_y:327
                  /\ __cost':323 = mid___cost:326)
                 \/ (1 <= K:325 /\ 0 <= __cost':323 /\ 0 <= (-1 + y':321)
                       /\ 0 <= mid_y:327 /\ 0 <= (-1 + mid___cost:326)))
           /\ K:328 = 0 /\ mid_y:327 = y':329 /\ mid___cost:326 = __cost':330
           /\ 0 = K:328 /\ (K:325 + K:328) = K:331 /\ 0 <= K:331
           /\ y':329 <= 0
           /\ (!(0 <= K:332) \/ mid___cost:333 = (__cost':330 + K:332))
           /\ (!(0 <= K:332) \/ mid_x:334 = (x':322 + K:332))
           /\ ((K:332 = 0 /\ x':322 = mid_x:334
                  /\ __cost':330 = mid___cost:333)
                 \/ (1 <= K:332 /\ 0 <= (-1 + -x':322) /\ 0 <= __cost':330
                       /\ 0 <= -mid_x:334 /\ 0 <= (-1 + mid___cost:333)))
           /\ K:335 = 0 /\ mid_x:334 = x':336 /\ mid___cost:333 = __cost':337
           /\ 0 = K:335 /\ (K:332 + K:335) = K:338 /\ 0 <= K:338
           /\ 0 <= x':336
           /\ ((havoc:22 < 0 /\ -havoc:22 = phi_tmp___1:346)
                 \/ (0 <= havoc:22 /\ 0 = phi_tmp___1:346))
           /\ ((0 < havoc:23 /\ havoc:23 = phi_tmp___2:347)
                 \/ (havoc:23 <= 0 /\ 0 = phi_tmp___2:347))
           /\ ((havoc:23 < havoc:22
                  /\ (havoc:22 + -havoc:23) = phi_tmp___3:348)
                 \/ (havoc:22 <= havoc:23 /\ 0 = phi_tmp___3:348)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':372
   return := havoc:377
   param0 := param0:87
   param1 := param1:90
   return@pos := type_err:378
   param0@pos := type_err:95
   param1@pos := type_err:96
   return@width := type_err:379
   param0@width := type_err:97
   param1@width := type_err:98
   when ((!(0 <= K:351) \/ mid_y:352 = (param1:90 + (1000 * K:351)))
           /\ (!(0 <= K:351) \/ mid_x:353 = (param0:87 + (999 * K:351)))
           /\ (!(0 <= K:351) \/ mid___cost:354 = (__cost:110 + K:351))
           /\ ((K:351 = 0 /\ param1:90 = mid_y:352 /\ param0:87 = mid_x:353
                  /\ __cost:110 = mid___cost:354)
                 \/ (1 <= K:351 /\ 0 <= (-1 + -param1:90 + param0:87)
                       /\ 0 <= __cost:110 /\ 0 <= (-mid_y:352 + mid_x:353)
                       /\ 0 <= (-1 + mid___cost:354))) /\ K:355 = 0
           /\ mid_y:352 = y':356 /\ mid_x:353 = x':357
           /\ mid___cost:354 = __cost':358 /\ 0 = K:355
           /\ (K:351 + K:355) = K:359 /\ 0 <= K:359 /\ x':357 <= y':356
           /\ (!(0 <= K:360) \/ mid___cost:361 = (__cost':358 + K:360))
           /\ (!(0 <= K:360) \/ mid_y:362 = (y':356 + -K:360))
           /\ ((K:360 = 0 /\ y':356 = mid_y:362
                  /\ __cost':358 = mid___cost:361)
                 \/ (1 <= K:360 /\ 0 <= __cost':358 /\ 0 <= (-1 + y':356)
                       /\ 0 <= mid_y:362 /\ 0 <= (-1 + mid___cost:361)))
           /\ K:363 = 0 /\ mid_y:362 = y':364 /\ mid___cost:361 = __cost':365
           /\ 0 = K:363 /\ (K:360 + K:363) = K:366 /\ 0 <= K:366
           /\ y':364 <= 0
           /\ (!(0 <= K:367) \/ mid___cost:368 = (__cost':365 + K:367))
           /\ (!(0 <= K:367) \/ mid_x:369 = (x':357 + K:367))
           /\ ((K:367 = 0 /\ x':357 = mid_x:369
                  /\ __cost':365 = mid___cost:368)
                 \/ (1 <= K:367 /\ 0 <= (-1 + -x':357) /\ 0 <= __cost':365
                       /\ 0 <= -mid_x:369 /\ 0 <= (-1 + mid___cost:368)))
           /\ K:370 = 0 /\ mid_x:369 = x':371 /\ mid___cost:368 = __cost':372
           /\ 0 = K:370 /\ (K:367 + K:370) = K:373 /\ 0 <= K:373
           /\ 0 <= x':371)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=25: 
Weight(Base relation: 
  {__cost := __cost':282
   return := havoc:284
   return@pos := type_err:285
   return@width := type_err:286
   when ((!(0 <= K:239) \/ mid_y:240 = (param1:90 + (1000 * K:239)))
           /\ (!(0 <= K:239) \/ mid_x:241 = (param0:87 + (999 * K:239)))
           /\ (!(0 <= K:239) \/ mid___cost:242 = (__cost:110 + K:239))
           /\ ((K:239 = 0 /\ param1:90 = mid_y:240 /\ param0:87 = mid_x:241
                  /\ __cost:110 = mid___cost:242)
                 \/ (1 <= K:239 /\ 0 <= (-1 + -param1:90 + param0:87)
                       /\ 0 <= __cost:110 /\ 0 <= (-mid_y:240 + mid_x:241)
                       /\ 0 <= (-1 + mid___cost:242))) /\ K:243 = 0
           /\ mid_y:240 = y':244 /\ mid_x:241 = x':245
           /\ mid___cost:242 = __cost':246 /\ 0 = K:243
           /\ (K:239 + K:243) = K:247 /\ 0 <= K:247 /\ x':245 <= y':244
           /\ (!(0 <= K:259) \/ mid___cost:260 = (__cost':246 + K:259))
           /\ (!(0 <= K:259) \/ mid_y:261 = (y':244 + -K:259))
           /\ ((K:259 = 0 /\ y':244 = mid_y:261
                  /\ __cost':246 = mid___cost:260)
                 \/ (1 <= K:259 /\ 0 <= __cost':246 /\ 0 <= (-1 + y':244)
                       /\ 0 <= mid_y:261 /\ 0 <= (-1 + mid___cost:260)))
           /\ K:262 = 0 /\ mid_y:261 = y':263 /\ mid___cost:260 = __cost':264
           /\ 0 = K:262 /\ (K:259 + K:262) = K:265 /\ 0 <= K:265
           /\ y':263 <= 0
           /\ (!(0 <= K:277) \/ mid___cost:278 = (__cost':264 + K:277))
           /\ (!(0 <= K:277) \/ mid_x:279 = (x':245 + K:277))
           /\ ((K:277 = 0 /\ x':245 = mid_x:279
                  /\ __cost':264 = mid___cost:278)
                 \/ (1 <= K:277 /\ 0 <= (-1 + -x':245) /\ 0 <= __cost':264
                       /\ 0 <= -mid_x:279 /\ 0 <= (-1 + mid___cost:278)))
           /\ K:280 = 0 /\ mid_x:279 = x':281 /\ mid___cost:278 = __cost':282
           /\ 0 = K:280 /\ (K:277 + K:280) = K:283 /\ 0 <= K:283
           /\ 0 <= x':281)})


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':337
 return := 0
 param0 := havoc:22
 param1 := havoc:23
 return@pos := type_err:349
 param0@pos := type_err:341
 param1@pos := type_err:342
 return@width := type_err:350
 param0@width := type_err:344
 param1@width := type_err:345
 when ((!(0 <= K:316) \/ mid_y:317 = (havoc:23 + (1000 * K:316)))
         /\ (!(0 <= K:316) \/ mid_x:318 = (havoc:22 + (999 * K:316)))
         /\ (!(0 <= K:316) \/ mid___cost:319 = K:316)
         /\ ((K:316 = 0 /\ havoc:23 = mid_y:317 /\ havoc:22 = mid_x:318
                /\ 0 = mid___cost:319)
               \/ (1 <= K:316 /\ 0 <= (-1 + -havoc:23 + havoc:22)
                     /\ 0 <= (-mid_y:317 + mid_x:318)
                     /\ 0 <= (-1 + mid___cost:319))) /\ K:320 = 0
         /\ mid_y:317 = y':321 /\ mid_x:318 = x':322
         /\ mid___cost:319 = __cost':323 /\ 0 = K:320
         /\ (K:316 + K:320) = K:324 /\ 0 <= K:324 /\ x':322 <= y':321
         /\ (!(0 <= K:325) \/ mid___cost:326 = (__cost':323 + K:325))
         /\ (!(0 <= K:325) \/ mid_y:327 = (y':321 + -K:325))
         /\ ((K:325 = 0 /\ y':321 = mid_y:327 /\ __cost':323 = mid___cost:326)
               \/ (1 <= K:325 /\ 0 <= __cost':323 /\ 0 <= (-1 + y':321)
                     /\ 0 <= mid_y:327 /\ 0 <= (-1 + mid___cost:326)))
         /\ K:328 = 0 /\ mid_y:327 = y':329 /\ mid___cost:326 = __cost':330
         /\ 0 = K:328 /\ (K:325 + K:328) = K:331 /\ 0 <= K:331 /\ y':329 <= 0
         /\ (!(0 <= K:332) \/ mid___cost:333 = (__cost':330 + K:332))
         /\ (!(0 <= K:332) \/ mid_x:334 = (x':322 + K:332))
         /\ ((K:332 = 0 /\ x':322 = mid_x:334 /\ __cost':330 = mid___cost:333)
               \/ (1 <= K:332 /\ 0 <= (-1 + -x':322) /\ 0 <= __cost':330
                     /\ 0 <= -mid_x:334 /\ 0 <= (-1 + mid___cost:333)))
         /\ K:335 = 0 /\ mid_x:334 = x':336 /\ mid___cost:333 = __cost':337
         /\ 0 = K:335 /\ (K:332 + K:335) = K:338 /\ 0 <= K:338 /\ 0 <= x':336
         /\ ((havoc:22 < 0 /\ -havoc:22 = phi_tmp___1:346)
               \/ (0 <= havoc:22 /\ 0 = phi_tmp___1:346))
         /\ ((0 < havoc:23 /\ havoc:23 = phi_tmp___2:347)
               \/ (havoc:23 <= 0 /\ 0 = phi_tmp___2:347))
         /\ ((havoc:23 < havoc:22 /\ (havoc:22 + -havoc:23) = phi_tmp___3:348)
               \/ (havoc:22 <= havoc:23 /\ 0 = phi_tmp___3:348)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':372
 return := havoc:377
 param0 := param0:87
 param1 := param1:90
 return@pos := type_err:378
 param0@pos := type_err:95
 param1@pos := type_err:96
 return@width := type_err:379
 param0@width := type_err:97
 param1@width := type_err:98
 when ((!(0 <= K:351) \/ mid_y:352 = (param1:90 + (1000 * K:351)))
         /\ (!(0 <= K:351) \/ mid_x:353 = (param0:87 + (999 * K:351)))
         /\ (!(0 <= K:351) \/ mid___cost:354 = (__cost:110 + K:351))
         /\ ((K:351 = 0 /\ param1:90 = mid_y:352 /\ param0:87 = mid_x:353
                /\ __cost:110 = mid___cost:354)
               \/ (1 <= K:351 /\ 0 <= (-1 + -param1:90 + param0:87)
                     /\ 0 <= __cost:110 /\ 0 <= (-mid_y:352 + mid_x:353)
                     /\ 0 <= (-1 + mid___cost:354))) /\ K:355 = 0
         /\ mid_y:352 = y':356 /\ mid_x:353 = x':357
         /\ mid___cost:354 = __cost':358 /\ 0 = K:355
         /\ (K:351 + K:355) = K:359 /\ 0 <= K:359 /\ x':357 <= y':356
         /\ (!(0 <= K:360) \/ mid___cost:361 = (__cost':358 + K:360))
         /\ (!(0 <= K:360) \/ mid_y:362 = (y':356 + -K:360))
         /\ ((K:360 = 0 /\ y':356 = mid_y:362 /\ __cost':358 = mid___cost:361)
               \/ (1 <= K:360 /\ 0 <= __cost':358 /\ 0 <= (-1 + y':356)
                     /\ 0 <= mid_y:362 /\ 0 <= (-1 + mid___cost:361)))
         /\ K:363 = 0 /\ mid_y:362 = y':364 /\ mid___cost:361 = __cost':365
         /\ 0 = K:363 /\ (K:360 + K:363) = K:366 /\ 0 <= K:366 /\ y':364 <= 0
         /\ (!(0 <= K:367) \/ mid___cost:368 = (__cost':365 + K:367))
         /\ (!(0 <= K:367) \/ mid_x:369 = (x':357 + K:367))
         /\ ((K:367 = 0 /\ x':357 = mid_x:369 /\ __cost':365 = mid___cost:368)
               \/ (1 <= K:367 /\ 0 <= (-1 + -x':357) /\ 0 <= __cost':365
                     /\ 0 <= -mid_x:369 /\ 0 <= (-1 + mid___cost:368)))
         /\ K:370 = 0 /\ mid_x:369 = x':371 /\ mid___cost:368 = __cost':372
         /\ 0 = K:370 /\ (K:367 + K:370) = K:373 /\ 0 <= K:373 /\ 0 <= x':371)}

Evaluating variable number 25 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':282
 return := havoc:284
 return@pos := type_err:285
 return@width := type_err:286
 when ((!(0 <= K:239) \/ mid_y:240 = (param1:90 + (1000 * K:239)))
         /\ (!(0 <= K:239) \/ mid_x:241 = (param0:87 + (999 * K:239)))
         /\ (!(0 <= K:239) \/ mid___cost:242 = (__cost:110 + K:239))
         /\ ((K:239 = 0 /\ param1:90 = mid_y:240 /\ param0:87 = mid_x:241
                /\ __cost:110 = mid___cost:242)
               \/ (1 <= K:239 /\ 0 <= (-1 + -param1:90 + param0:87)
                     /\ 0 <= __cost:110 /\ 0 <= (-mid_y:240 + mid_x:241)
                     /\ 0 <= (-1 + mid___cost:242))) /\ K:243 = 0
         /\ mid_y:240 = y':244 /\ mid_x:241 = x':245
         /\ mid___cost:242 = __cost':246 /\ 0 = K:243
         /\ (K:239 + K:243) = K:247 /\ 0 <= K:247 /\ x':245 <= y':244
         /\ (!(0 <= K:259) \/ mid___cost:260 = (__cost':246 + K:259))
         /\ (!(0 <= K:259) \/ mid_y:261 = (y':244 + -K:259))
         /\ ((K:259 = 0 /\ y':244 = mid_y:261 /\ __cost':246 = mid___cost:260)
               \/ (1 <= K:259 /\ 0 <= __cost':246 /\ 0 <= (-1 + y':244)
                     /\ 0 <= mid_y:261 /\ 0 <= (-1 + mid___cost:260)))
         /\ K:262 = 0 /\ mid_y:261 = y':263 /\ mid___cost:260 = __cost':264
         /\ 0 = K:262 /\ (K:259 + K:262) = K:265 /\ 0 <= K:265 /\ y':263 <= 0
         /\ (!(0 <= K:277) \/ mid___cost:278 = (__cost':264 + K:277))
         /\ (!(0 <= K:277) \/ mid_x:279 = (x':245 + K:277))
         /\ ((K:277 = 0 /\ x':245 = mid_x:279 /\ __cost':264 = mid___cost:278)
               \/ (1 <= K:277 /\ 0 <= (-1 + -x':245) /\ 0 <= __cost':264
                     /\ 0 <= -mid_x:279 /\ 0 <= (-1 + mid___cost:278)))
         /\ K:280 = 0 /\ mid_x:279 = x':281 /\ mid___cost:278 = __cost':282
         /\ 0 = K:280 /\ (K:277 + K:280) = K:283 /\ 0 <= K:283 /\ 0 <= x':281)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,91)_g1> -> <__pstate, (Unique State Name,85)_g1>	Base relation: 
{param0 := param0:87
 param1 := param1:90
 param0@pos := type_err:95
 param1@pos := type_err:96
 param0@width := type_err:97
 param1@width := type_err:98}	
<__pstate, accept> -> <__pstate, (Unique State Name,91)_g1>	Base relation: 
{__cost := 0
 x := havoc:22
 y := havoc:23
 param0 := havoc:22
 param1 := havoc:23
 param0@pos := type_err:29
 param1@pos := type_err:31
 param0@width := type_err:30
 param1@width := type_err:32}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x7a01ff0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x75da1f0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
##### ANS
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}
    ( __pstate , (Unique State Name,85)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:22
 y := havoc:23
 param0 := havoc:22
 param1 := havoc:23
 param0@pos := type_err:444
 param1@pos := type_err:445
 param0@width := type_err:446
 param1@width := type_err:447}
    ( __pstate , (Unique State Name,91)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:22
 y := havoc:23
 param0 := havoc:22
 param1 := havoc:23
 param0@pos := type_err:29
 param1@pos := type_err:31
 param0@width := type_err:30
 param1@width := type_err:32}

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

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

Base relation: 
{__cost := __cost':401
 x := havoc:22
 y := havoc:23
 return := 0
 param0 := havoc:22
 param1 := havoc:23
 return@pos := type_err:413
 param0@pos := type_err:405
 param1@pos := type_err:406
 return@width := type_err:414
 param0@width := type_err:408
 param1@width := type_err:409
 when ((!(0 <= K:380) \/ mid_y:381 = (havoc:23 + (1000 * K:380)))
         /\ (!(0 <= K:380) \/ mid_x:382 = (havoc:22 + (999 * K:380)))
         /\ (!(0 <= K:380) \/ mid___cost:383 = K:380)
         /\ ((K:380 = 0 /\ havoc:23 = mid_y:381 /\ havoc:22 = mid_x:382
                /\ 0 = mid___cost:383)
               \/ (1 <= K:380 /\ 0 <= (-1 + -havoc:23 + havoc:22)
                     /\ 0 <= (-mid_y:381 + mid_x:382)
                     /\ 0 <= (-1 + mid___cost:383))) /\ K:384 = 0
         /\ mid_y:381 = y':385 /\ mid_x:382 = x':386
         /\ mid___cost:383 = __cost':387 /\ 0 = K:384
         /\ (K:380 + K:384) = K:388 /\ 0 <= K:388 /\ x':386 <= y':385
         /\ (!(0 <= K:389) \/ mid___cost:390 = (__cost':387 + K:389))
         /\ (!(0 <= K:389) \/ mid_y:391 = (y':385 + -K:389))
         /\ ((K:389 = 0 /\ y':385 = mid_y:391 /\ __cost':387 = mid___cost:390)
               \/ (1 <= K:389 /\ 0 <= __cost':387 /\ 0 <= (-1 + y':385)
                     /\ 0 <= mid_y:391 /\ 0 <= (-1 + mid___cost:390)))
         /\ K:392 = 0 /\ mid_y:391 = y':393 /\ mid___cost:390 = __cost':394
         /\ 0 = K:392 /\ (K:389 + K:392) = K:395 /\ 0 <= K:395 /\ y':393 <= 0
         /\ (!(0 <= K:396) \/ mid___cost:397 = (__cost':394 + K:396))
         /\ (!(0 <= K:396) \/ mid_x:398 = (x':386 + K:396))
         /\ ((K:396 = 0 /\ x':386 = mid_x:398 /\ __cost':394 = mid___cost:397)
               \/ (1 <= K:396 /\ 0 <= (-1 + -x':386) /\ 0 <= __cost':394
                     /\ 0 <= -mid_x:398 /\ 0 <= (-1 + mid___cost:397)))
         /\ K:399 = 0 /\ mid_x:398 = x':400 /\ mid___cost:397 = __cost':401
         /\ 0 = K:399 /\ (K:396 + K:399) = K:402 /\ 0 <= K:402 /\ 0 <= x':400
         /\ ((havoc:22 < 0 /\ -havoc:22 = phi_tmp___1:410)
               \/ (0 <= havoc:22 /\ 0 = phi_tmp___1:410))
         /\ ((0 < havoc:23 /\ havoc:23 = phi_tmp___2:411)
               \/ (havoc:23 <= 0 /\ 0 = phi_tmp___2:411))
         /\ ((havoc:23 < havoc:22 /\ (havoc:22 + -havoc:23) = phi_tmp___3:412)
               \/ (havoc:22 <= havoc:23 /\ 0 = phi_tmp___3:412)))}

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

Base relation: 
{__cost := __cost':436
 return := havoc:441
 param0 := param0:87
 param1 := param1:90
 return@pos := type_err:442
 param0@pos := type_err:95
 param1@pos := type_err:96
 return@width := type_err:443
 param0@width := type_err:97
 param1@width := type_err:98
 when ((!(0 <= K:415) \/ mid_y:416 = (param1:90 + (1000 * K:415)))
         /\ (!(0 <= K:415) \/ mid_x:417 = (param0:87 + (999 * K:415)))
         /\ (!(0 <= K:415) \/ mid___cost:418 = (__cost:110 + K:415))
         /\ ((K:415 = 0 /\ param1:90 = mid_y:416 /\ param0:87 = mid_x:417
                /\ __cost:110 = mid___cost:418)
               \/ (1 <= K:415 /\ 0 <= (-1 + -param1:90 + param0:87)
                     /\ 0 <= __cost:110 /\ 0 <= (-mid_y:416 + mid_x:417)
                     /\ 0 <= (-1 + mid___cost:418))) /\ K:419 = 0
         /\ mid_y:416 = y':420 /\ mid_x:417 = x':421
         /\ mid___cost:418 = __cost':422 /\ 0 = K:419
         /\ (K:415 + K:419) = K:423 /\ 0 <= K:423 /\ x':421 <= y':420
         /\ (!(0 <= K:424) \/ mid___cost:425 = (__cost':422 + K:424))
         /\ (!(0 <= K:424) \/ mid_y:426 = (y':420 + -K:424))
         /\ ((K:424 = 0 /\ y':420 = mid_y:426 /\ __cost':422 = mid___cost:425)
               \/ (1 <= K:424 /\ 0 <= __cost':422 /\ 0 <= (-1 + y':420)
                     /\ 0 <= mid_y:426 /\ 0 <= (-1 + mid___cost:425)))
         /\ K:427 = 0 /\ mid_y:426 = y':428 /\ mid___cost:425 = __cost':429
         /\ 0 = K:427 /\ (K:424 + K:427) = K:430 /\ 0 <= K:430 /\ y':428 <= 0
         /\ (!(0 <= K:431) \/ mid___cost:432 = (__cost':429 + K:431))
         /\ (!(0 <= K:431) \/ mid_x:433 = (x':421 + K:431))
         /\ ((K:431 = 0 /\ x':421 = mid_x:433 /\ __cost':429 = mid___cost:432)
               \/ (1 <= K:431 /\ 0 <= (-1 + -x':421) /\ 0 <= __cost':429
                     /\ 0 <= -mid_x:433 /\ 0 <= (-1 + mid___cost:432)))
         /\ K:434 = 0 /\ mid_x:433 = x':435 /\ mid___cost:432 = __cost':436
         /\ 0 = K:434 /\ (K:431 + K:434) = K:437 /\ 0 <= K:437 /\ 0 <= x':435)}

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

Base relation: 
{__cost := __cost':282
 x := x':281
 y := y':263
 return := havoc:284
 return@pos := type_err:285
 return@width := type_err:286
 when ((!(0 <= K:239) \/ mid_y:240 = (param1:90 + (1000 * K:239)))
         /\ (!(0 <= K:239) \/ mid_x:241 = (param0:87 + (999 * K:239)))
         /\ (!(0 <= K:239) \/ mid___cost:242 = (__cost:110 + K:239))
         /\ ((K:239 = 0 /\ param1:90 = mid_y:240 /\ param0:87 = mid_x:241
                /\ __cost:110 = mid___cost:242)
               \/ (1 <= K:239 /\ 0 <= (-1 + -param1:90 + param0:87)
                     /\ 0 <= __cost:110 /\ 0 <= (-mid_y:240 + mid_x:241)
                     /\ 0 <= (-1 + mid___cost:242))) /\ K:243 = 0
         /\ mid_y:240 = y':244 /\ mid_x:241 = x':245
         /\ mid___cost:242 = __cost':246 /\ 0 = K:243
         /\ (K:239 + K:243) = K:247 /\ 0 <= K:247 /\ x':245 <= y':244
         /\ (!(0 <= K:259) \/ mid___cost:260 = (__cost':246 + K:259))
         /\ (!(0 <= K:259) \/ mid_y:261 = (y':244 + -K:259))
         /\ ((K:259 = 0 /\ y':244 = mid_y:261 /\ __cost':246 = mid___cost:260)
               \/ (1 <= K:259 /\ 0 <= __cost':246 /\ 0 <= (-1 + y':244)
                     /\ 0 <= mid_y:261 /\ 0 <= (-1 + mid___cost:260)))
         /\ K:262 = 0 /\ mid_y:261 = y':263 /\ mid___cost:260 = __cost':264
         /\ 0 = K:262 /\ (K:259 + K:262) = K:265 /\ 0 <= K:265 /\ y':263 <= 0
         /\ (!(0 <= K:277) \/ mid___cost:278 = (__cost':264 + K:277))
         /\ (!(0 <= K:277) \/ mid_x:279 = (x':245 + K:277))
         /\ ((K:277 = 0 /\ x':245 = mid_x:279 /\ __cost':264 = mid___cost:278)
               \/ (1 <= K:277 /\ 0 <= (-1 + -x':245) /\ 0 <= __cost':264
                     /\ 0 <= -mid_x:279 /\ 0 <= (-1 + mid___cost:278)))
         /\ K:280 = 0 /\ mid_x:279 = x':281 /\ mid___cost:278 = __cost':282
         /\ 0 = K:280 /\ (K:277 + K:280) = K:283 /\ 0 <= K:283 /\ 0 <= x':281)}

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

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

Variable bounds at line 27 in run

min(min(min(min(min((__cost + (-999 * x) + (998 * y)),
                    (__cost + (1001 * x) + (-1000 * y))),
                (__cost + (-1/999 * x))),
            (__cost + y)),
        (__cost + -x)),
    (__cost + -x + y)) <= __cost
__cost is o(n)
__cost <= max(max(max(max(max((__cost + (-999 * x) + (998 * y)),
                              (__cost + (1001 * x) + (-1000 * y))),
                          (__cost + (-1/999 * x))),
                      (__cost + y)),
                  (__cost + -x)),
              (__cost + -x + y))
__cost is O(n)

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