/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, 82> -> <Unique State Name, 61>	Base relation: 
{}	
<Unique State Name, 29> -> <Unique State Name, 102>	Base relation: 
{}	
<Unique State Name, 23> -> <Unique State Name, 95>	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}	
<Unique State Name, 96> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 99> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 83> -> <Unique State Name, 81 82>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 101> -> <Unique State Name, 49>	Base relation: 
{}	
<Unique State Name, 88> -> <Unique State Name, 25>	Base relation: 
{}	
<Unique State Name, 98> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 81> -> <Unique State Name, 96>	Base relation: 
{return := havoc:169
 return@pos := type_err:172
 return@width := type_err:173}	
<Unique State Name, 97> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 102> -> <Unique State Name, 33>	Base relation: 
{}	
<Unique State Name, 100> -> <Unique State Name, 65>	Base relation: 
{}	
<Unique State Name, 61> -> <Unique State Name, 100>	Base relation: 
{when (y:103 <= 0 /\ y:103 <= 0)}	
<Unique State Name, 89> -> <Unique State Name, 84 88>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 95> -> <Unique State Name, 90 94>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 90> -> <Unique State Name, 89>	Base relation: 
{param0 := param0:80
 param1 := param1:83
 param0@pos := type_err:88
 param1@pos := type_err:89
 param0@width := type_err:90
 param1@width := type_err:91}	
<Unique State Name, 33> -> <Unique State Name, 29>	Base relation: 
{__cost := (__cost:102 + 1)
 x := (x:101 + -1)
 y := (y:103 + 2)
 when (0 < x:101 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}	
<Unique State Name, 33> -> <Unique State Name, 45>	Base relation: 
{when x:101 <= 0}	
<Unique State Name, 94> -> <Unique State Name, 99>	Base relation: 
{return := 0
 return@pos := type_err:32
 return@width := type_err:33
 when (((0 < x:4 /\ x:4 = phi_tmp___1:23) \/ (x:4 <= 0 /\ 0 = phi_tmp___1:23))
         /\ ((0 < y:5 /\ y:5 = phi_tmp___2:31)
               \/ (y:5 <= 0 /\ 0 = phi_tmp___2:31)))}	
<Unique State Name, 65> -> <Unique State Name, 61>	Base relation: 
{__cost := (__cost:102 + 1)
 y := (y:103 + -1)
 when (0 < y:103 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}	
<Unique State Name, 65> -> <Unique State Name, 97>	Base relation: 
{return := havoc:109
 return@pos := type_err:110
 return@width := type_err:111
 when y:103 <= 0}	
<Unique State Name, 84> -> <Unique State Name, 29>	Base relation: 
{x := param0:80
 y := param1:83}	
<Unique State Name, 45> -> <Unique State Name, 101>	Base relation: 
{}	
<Unique State Name, 25> -> <Unique State Name, 98>	Base relation: 
{return := havoc:63
 return@pos := type_err:66
 return@width := type_err:67}	
<Unique State Name, 49> -> <Unique State Name, 45>	Base relation: 
{__cost := (__cost:102 + 1)
 y := (y:103 + -1)
 when (0 < y:103 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}	
<Unique State Name, 49> -> <Unique State Name, 83>	Base relation: 
{when y:103 <= 0}	
#################################################################
           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:102 + 1)
 x := (x:101 + -1)
 y := (y:103 + 2)
 when (0 < x:101 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':177) = (1)*(__cost:102) + 1
           (y':179) = (1)*(y:103) + 2*1
           (x':178) = (1)*(x:101) + (-1)*1
           }
          pre:
            [|__cost:102>=0; x:101-1>=0|]
          post:
            [|x':178>=0; __cost':177-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':177
   x := x':178
   y := y':179
   when ((!(0 <= K:190) \/ mid___cost:194 = (__cost:102 + K:190))
           /\ (!(0 <= K:190) \/ mid_y:192 = (y:103 + (2 * K:190)))
           /\ (!(0 <= K:190) \/ mid_x:193 = (x:101 + -K:190))
           /\ ((K:190 = 0 /\ y:103 = mid_y:192 /\ x:101 = mid_x:193
                  /\ __cost:102 = mid___cost:194)
                 \/ (1 <= K:190 /\ 0 <= __cost:102 /\ 0 <= (-1 + x:101)
                       /\ 0 <= mid_x:193 /\ 0 <= (-1 + mid___cost:194)))
           /\ K:191 = 0 /\ mid_y:192 = y':179 /\ mid_x:193 = x':178
           /\ mid___cost:194 = __cost':177 /\ 0 = K:191
           /\ (K:190 + K:191) = K:189 /\ 0 <= K:189)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:102 + 1)
 y := (y:103 + -1)
 when (0 < y:103 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':177) = (1)*(__cost:102) + 1
           (y':179) = (1)*(y:103) + (-1)*1
           }
          pre:
            [|__cost:102>=0; y:103-1>=0|]
          post:
            [|y':179>=0; __cost':177-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':177
   y := y':179
   when ((!(0 <= K:211) \/ mid___cost:214 = (__cost:102 + K:211))
           /\ (!(0 <= K:211) \/ mid_y:213 = (y:103 + -K:211))
           /\ ((K:211 = 0 /\ y:103 = mid_y:213 /\ __cost:102 = mid___cost:214)
                 \/ (1 <= K:211 /\ 0 <= __cost:102 /\ 0 <= (-1 + y:103)
                       /\ 0 <= mid_y:213 /\ 0 <= (-1 + mid___cost:214)))
           /\ K:212 = 0 /\ mid_y:213 = y':179 /\ mid___cost:214 = __cost':177
           /\ 0 = K:212 /\ (K:211 + K:212) = K:210 /\ 0 <= K:210)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:102 + 1)
 y := (y:103 + -1)
 when (y:103 <= 0 /\ y:103 <= 0 /\ 0 < y:103 /\ 0 <= __cost:102
         /\ 0 <= (__cost:102 + 1))}
**** alpha hat: 
  {<Split [true
            }
          pre:
            bottom
          post:
            bottom
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':177
   y := y':179
   when (K:227 = 0 /\ y:103 = mid_y:229 /\ __cost:102 = mid___cost:230
           /\ K:228 = 0 /\ mid_y:229 = y':179 /\ mid___cost:230 = __cost':177
           /\ 0 = K:228 /\ (K:227 + K:228) = K:226 /\ 0 <= K:226)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  28  31  


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


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:80
       param1 := param1:83
       param0@pos := type_err:88
       param1@pos := type_err:89
       param0@width := type_err:90
       param1@width := type_err:91}    )
    ,
    Var(28)
  )
  ,
  Weight(Base relation: 
    {return := havoc:63
     return@pos := type_err:66
     return@width := type_err:67}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=28: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := __cost':220
       x := x':201
       y := y':219
       when ((!(0 <= K:195) \/ mid___cost:196 = (__cost:102 + K:195))
               /\ (!(0 <= K:195) \/ mid_y:197 = (param1:83 + (2 * K:195)))
               /\ (!(0 <= K:195) \/ mid_x:198 = (param0:80 + -K:195))
               /\ ((K:195 = 0 /\ param1:83 = mid_y:197
                      /\ param0:80 = mid_x:198 /\ __cost:102 = mid___cost:196)
                     \/ (1 <= K:195 /\ 0 <= __cost:102
                           /\ 0 <= (-1 + param0:80) /\ 0 <= mid_x:198
                           /\ 0 <= (-1 + mid___cost:196))) /\ K:199 = 0
               /\ mid_y:197 = y':200 /\ mid_x:198 = x':201
               /\ mid___cost:196 = __cost':202 /\ 0 = K:199
               /\ (K:195 + K:199) = K:203 /\ 0 <= K:203 /\ x':201 <= 0
               /\ (!(0 <= K:215) \/ mid___cost:216 = (__cost':202 + K:215))
               /\ (!(0 <= K:215) \/ mid_y:217 = (y':200 + -K:215))
               /\ ((K:215 = 0 /\ y':200 = mid_y:217
                      /\ __cost':202 = mid___cost:216)
                     \/ (1 <= K:215 /\ 0 <= __cost':202 /\ 0 <= (-1 + y':200)
                           /\ 0 <= mid_y:217 /\ 0 <= (-1 + mid___cost:216)))
               /\ K:218 = 0 /\ mid_y:217 = y':219
               /\ mid___cost:216 = __cost':220 /\ 0 = K:218
               /\ (K:215 + K:218) = K:221 /\ 0 <= K:221 /\ y':219 <= 0)}    )
    ,
    Var(31)
  )
  ,
  Weight(Base relation: 
    {__cost := __cost':177
     y := y':179
     return := havoc:231
     return@pos := type_err:232
     return@width := type_err:233
     when (K:227 = 0 /\ y:103 = mid_y:229 /\ __cost:102 = mid___cost:230
             /\ K:228 = 0 /\ mid_y:229 = y':179
             /\ mid___cost:230 = __cost':177 /\ 0 = K:228
             /\ (K:227 + K:228) = K:226 /\ 0 <= K:226 /\ y':179 <= 0
             /\ y':179 <= 0 /\ y':179 <= 0)}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=31: 
Weight(Base relation: 
  {return := havoc:169
   return@pos := type_err:172
   return@width := type_err:173})



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



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:80
         param1 := param1:83
         param0@pos := type_err:88
         param1@pos := type_err:89
         param0@width := type_err:90
         param1@width := type_err:91}      )
      ,
      Var(28)
    )
    ,
    Weight(Base relation: 
      {return := havoc:63
       return@pos := type_err:66
       return@width := type_err:67}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := __cost':220
         x := x':201
         y := y':219
         when ((!(0 <= K:195) \/ mid___cost:196 = (__cost:102 + K:195))
                 /\ (!(0 <= K:195) \/ mid_y:197 = (param1:83 + (2 * K:195)))
                 /\ (!(0 <= K:195) \/ mid_x:198 = (param0:80 + -K:195))
                 /\ ((K:195 = 0 /\ param1:83 = mid_y:197
                        /\ param0:80 = mid_x:198
                        /\ __cost:102 = mid___cost:196)
                       \/ (1 <= K:195 /\ 0 <= __cost:102
                             /\ 0 <= (-1 + param0:80) /\ 0 <= mid_x:198
                             /\ 0 <= (-1 + mid___cost:196))) /\ K:199 = 0
                 /\ mid_y:197 = y':200 /\ mid_x:198 = x':201
                 /\ mid___cost:196 = __cost':202 /\ 0 = K:199
                 /\ (K:195 + K:199) = K:203 /\ 0 <= K:203 /\ x':201 <= 0
                 /\ (!(0 <= K:215) \/ mid___cost:216 = (__cost':202 + K:215))
                 /\ (!(0 <= K:215) \/ mid_y:217 = (y':200 + -K:215))
                 /\ ((K:215 = 0 /\ y':200 = mid_y:217
                        /\ __cost':202 = mid___cost:216)
                       \/ (1 <= K:215 /\ 0 <= __cost':202
                             /\ 0 <= (-1 + y':200) /\ 0 <= mid_y:217
                             /\ 0 <= (-1 + mid___cost:216))) /\ K:218 = 0
                 /\ mid_y:217 = y':219 /\ mid___cost:216 = __cost':220
                 /\ 0 = K:218 /\ (K:215 + K:218) = K:221 /\ 0 <= K:221
                 /\ y':219 <= 0)}      )
      ,
      Var(31)
    )
    ,
    Weight(Base relation: 
      {__cost := __cost':177
       y := y':179
       return := havoc:231
       return@pos := type_err:232
       return@width := type_err:233
       when (K:227 = 0 /\ y:103 = mid_y:229 /\ __cost:102 = mid___cost:230
               /\ K:228 = 0 /\ mid_y:229 = y':179
               /\ mid___cost:230 = __cost':177 /\ 0 = K:228
               /\ (K:227 + K:228) = K:226 /\ 0 <= K:226 /\ y':179 <= 0
               /\ y':179 <= 0 /\ y':179 <= 0)}    )
  )
)



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

Weight(Base relation: 
  {return := havoc:169
   return@pos := type_err:172
   return@width := type_err:173})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':297
   return := 0
   param0 := havoc:21
   param1 := havoc:22
   return@pos := type_err:308
   param0@pos := type_err:301
   param1@pos := type_err:302
   return@width := type_err:309
   param0@width := type_err:304
   param1@width := type_err:305
   when ((!(0 <= K:276) \/ mid___cost:277 = K:276)
           /\ (!(0 <= K:276) \/ mid_y:278 = (havoc:22 + (2 * K:276)))
           /\ (!(0 <= K:276) \/ mid_x:279 = (havoc:21 + -K:276))
           /\ ((K:276 = 0 /\ havoc:22 = mid_y:278 /\ havoc:21 = mid_x:279
                  /\ 0 = mid___cost:277)
                 \/ (1 <= K:276 /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_x:279
                       /\ 0 <= (-1 + mid___cost:277))) /\ K:280 = 0
           /\ mid_y:278 = y':281 /\ mid_x:279 = x':282
           /\ mid___cost:277 = __cost':283 /\ 0 = K:280
           /\ (K:276 + K:280) = K:284 /\ 0 <= K:284 /\ x':282 <= 0
           /\ (!(0 <= K:285) \/ mid___cost:286 = (__cost':283 + K:285))
           /\ (!(0 <= K:285) \/ mid_y:287 = (y':281 + -K:285))
           /\ ((K:285 = 0 /\ y':281 = mid_y:287
                  /\ __cost':283 = mid___cost:286)
                 \/ (1 <= K:285 /\ 0 <= __cost':283 /\ 0 <= (-1 + y':281)
                       /\ 0 <= mid_y:287 /\ 0 <= (-1 + mid___cost:286)))
           /\ K:288 = 0 /\ mid_y:287 = y':289 /\ mid___cost:286 = __cost':290
           /\ 0 = K:288 /\ (K:285 + K:288) = K:291 /\ 0 <= K:291
           /\ y':289 <= 0 /\ K:292 = 0 /\ y':289 = mid_y:293
           /\ __cost':290 = mid___cost:294 /\ K:295 = 0 /\ mid_y:293 = y':296
           /\ mid___cost:294 = __cost':297 /\ 0 = K:295
           /\ (K:292 + K:295) = K:298 /\ 0 <= K:298 /\ y':296 <= 0
           /\ y':296 <= 0 /\ y':296 <= 0
           /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:306)
                 \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:306))
           /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:307)
                 \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:307)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':344
   return := havoc:349
   param0 := param0:80
   param1 := param1:83
   return@pos := type_err:350
   param0@pos := type_err:88
   param1@pos := type_err:89
   return@width := type_err:351
   param0@width := type_err:90
   param1@width := type_err:91
   when ((!(0 <= K:323) \/ mid___cost:324 = (__cost:102 + K:323))
           /\ (!(0 <= K:323) \/ mid_y:325 = (param1:83 + (2 * K:323)))
           /\ (!(0 <= K:323) \/ mid_x:326 = (param0:80 + -K:323))
           /\ ((K:323 = 0 /\ param1:83 = mid_y:325 /\ param0:80 = mid_x:326
                  /\ __cost:102 = mid___cost:324)
                 \/ (1 <= K:323 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                       /\ 0 <= mid_x:326 /\ 0 <= (-1 + mid___cost:324)))
           /\ K:327 = 0 /\ mid_y:325 = y':328 /\ mid_x:326 = x':329
           /\ mid___cost:324 = __cost':330 /\ 0 = K:327
           /\ (K:323 + K:327) = K:331 /\ 0 <= K:331 /\ x':329 <= 0
           /\ (!(0 <= K:332) \/ mid___cost:333 = (__cost':330 + K:332))
           /\ (!(0 <= K:332) \/ mid_y:334 = (y':328 + -K:332))
           /\ ((K:332 = 0 /\ y':328 = mid_y:334
                  /\ __cost':330 = mid___cost:333)
                 \/ (1 <= K:332 /\ 0 <= __cost':330 /\ 0 <= (-1 + y':328)
                       /\ 0 <= mid_y:334 /\ 0 <= (-1 + mid___cost:333)))
           /\ K:335 = 0 /\ mid_y:334 = y':336 /\ mid___cost:333 = __cost':337
           /\ 0 = K:335 /\ (K:332 + K:335) = K:338 /\ 0 <= K:338
           /\ y':336 <= 0 /\ K:339 = 0 /\ y':336 = mid_y:340
           /\ __cost':337 = mid___cost:341 /\ K:342 = 0 /\ mid_y:340 = y':343
           /\ mid___cost:341 = __cost':344 /\ 0 = K:342
           /\ (K:339 + K:342) = K:345 /\ 0 <= K:345 /\ y':343 <= 0
           /\ y':343 <= 0 /\ y':343 <= 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=28: 
Weight(Base relation: 
  {__cost := __cost':360
   return := havoc:362
   return@pos := type_err:363
   return@width := type_err:364
   when ((!(0 <= K:195) \/ mid___cost:196 = (__cost:102 + K:195))
           /\ (!(0 <= K:195) \/ mid_y:197 = (param1:83 + (2 * K:195)))
           /\ (!(0 <= K:195) \/ mid_x:198 = (param0:80 + -K:195))
           /\ ((K:195 = 0 /\ param1:83 = mid_y:197 /\ param0:80 = mid_x:198
                  /\ __cost:102 = mid___cost:196)
                 \/ (1 <= K:195 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                       /\ 0 <= mid_x:198 /\ 0 <= (-1 + mid___cost:196)))
           /\ K:199 = 0 /\ mid_y:197 = y':200 /\ mid_x:198 = x':201
           /\ mid___cost:196 = __cost':202 /\ 0 = K:199
           /\ (K:195 + K:199) = K:203 /\ 0 <= K:203 /\ x':201 <= 0
           /\ (!(0 <= K:215) \/ mid___cost:216 = (__cost':202 + K:215))
           /\ (!(0 <= K:215) \/ mid_y:217 = (y':200 + -K:215))
           /\ ((K:215 = 0 /\ y':200 = mid_y:217
                  /\ __cost':202 = mid___cost:216)
                 \/ (1 <= K:215 /\ 0 <= __cost':202 /\ 0 <= (-1 + y':200)
                       /\ 0 <= mid_y:217 /\ 0 <= (-1 + mid___cost:216)))
           /\ K:218 = 0 /\ mid_y:217 = y':219 /\ mid___cost:216 = __cost':220
           /\ 0 = K:218 /\ (K:215 + K:218) = K:221 /\ 0 <= K:221
           /\ y':219 <= 0 /\ K:355 = 0 /\ y':219 = mid_y:356
           /\ __cost':220 = mid___cost:357 /\ K:358 = 0 /\ mid_y:356 = y':359
           /\ mid___cost:357 = __cost':360 /\ 0 = K:358
           /\ (K:355 + K:358) = K:361 /\ 0 <= K:361 /\ y':359 <= 0
           /\ y':359 <= 0 /\ y':359 <= 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=31: 
Weight(Base relation: 
  {return := havoc:169
   return@pos := type_err:172
   return@width := type_err:173})


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':297
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:308
 param0@pos := type_err:301
 param1@pos := type_err:302
 return@width := type_err:309
 param0@width := type_err:304
 param1@width := type_err:305
 when ((!(0 <= K:276) \/ mid___cost:277 = K:276)
         /\ (!(0 <= K:276) \/ mid_y:278 = (havoc:22 + (2 * K:276)))
         /\ (!(0 <= K:276) \/ mid_x:279 = (havoc:21 + -K:276))
         /\ ((K:276 = 0 /\ havoc:22 = mid_y:278 /\ havoc:21 = mid_x:279
                /\ 0 = mid___cost:277)
               \/ (1 <= K:276 /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_x:279
                     /\ 0 <= (-1 + mid___cost:277))) /\ K:280 = 0
         /\ mid_y:278 = y':281 /\ mid_x:279 = x':282
         /\ mid___cost:277 = __cost':283 /\ 0 = K:280
         /\ (K:276 + K:280) = K:284 /\ 0 <= K:284 /\ x':282 <= 0
         /\ (!(0 <= K:285) \/ mid___cost:286 = (__cost':283 + K:285))
         /\ (!(0 <= K:285) \/ mid_y:287 = (y':281 + -K:285))
         /\ ((K:285 = 0 /\ y':281 = mid_y:287 /\ __cost':283 = mid___cost:286)
               \/ (1 <= K:285 /\ 0 <= __cost':283 /\ 0 <= (-1 + y':281)
                     /\ 0 <= mid_y:287 /\ 0 <= (-1 + mid___cost:286)))
         /\ K:288 = 0 /\ mid_y:287 = y':289 /\ mid___cost:286 = __cost':290
         /\ 0 = K:288 /\ (K:285 + K:288) = K:291 /\ 0 <= K:291 /\ y':289 <= 0
         /\ K:292 = 0 /\ y':289 = mid_y:293 /\ __cost':290 = mid___cost:294
         /\ K:295 = 0 /\ mid_y:293 = y':296 /\ mid___cost:294 = __cost':297
         /\ 0 = K:295 /\ (K:292 + K:295) = K:298 /\ 0 <= K:298 /\ y':296 <= 0
         /\ y':296 <= 0 /\ y':296 <= 0
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:306)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:306))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:307)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:307)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':344
 return := havoc:349
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:350
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:351
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:323) \/ mid___cost:324 = (__cost:102 + K:323))
         /\ (!(0 <= K:323) \/ mid_y:325 = (param1:83 + (2 * K:323)))
         /\ (!(0 <= K:323) \/ mid_x:326 = (param0:80 + -K:323))
         /\ ((K:323 = 0 /\ param1:83 = mid_y:325 /\ param0:80 = mid_x:326
                /\ __cost:102 = mid___cost:324)
               \/ (1 <= K:323 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= mid_x:326 /\ 0 <= (-1 + mid___cost:324)))
         /\ K:327 = 0 /\ mid_y:325 = y':328 /\ mid_x:326 = x':329
         /\ mid___cost:324 = __cost':330 /\ 0 = K:327
         /\ (K:323 + K:327) = K:331 /\ 0 <= K:331 /\ x':329 <= 0
         /\ (!(0 <= K:332) \/ mid___cost:333 = (__cost':330 + K:332))
         /\ (!(0 <= K:332) \/ mid_y:334 = (y':328 + -K:332))
         /\ ((K:332 = 0 /\ y':328 = mid_y:334 /\ __cost':330 = mid___cost:333)
               \/ (1 <= K:332 /\ 0 <= __cost':330 /\ 0 <= (-1 + y':328)
                     /\ 0 <= mid_y:334 /\ 0 <= (-1 + mid___cost:333)))
         /\ K:335 = 0 /\ mid_y:334 = y':336 /\ mid___cost:333 = __cost':337
         /\ 0 = K:335 /\ (K:332 + K:335) = K:338 /\ 0 <= K:338 /\ y':336 <= 0
         /\ K:339 = 0 /\ y':336 = mid_y:340 /\ __cost':337 = mid___cost:341
         /\ K:342 = 0 /\ mid_y:340 = y':343 /\ mid___cost:341 = __cost':344
         /\ 0 = K:342 /\ (K:339 + K:342) = K:345 /\ 0 <= K:345 /\ y':343 <= 0
         /\ y':343 <= 0 /\ y':343 <= 0)}

Evaluating variable number 28 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':360
 return := havoc:362
 return@pos := type_err:363
 return@width := type_err:364
 when ((!(0 <= K:195) \/ mid___cost:196 = (__cost:102 + K:195))
         /\ (!(0 <= K:195) \/ mid_y:197 = (param1:83 + (2 * K:195)))
         /\ (!(0 <= K:195) \/ mid_x:198 = (param0:80 + -K:195))
         /\ ((K:195 = 0 /\ param1:83 = mid_y:197 /\ param0:80 = mid_x:198
                /\ __cost:102 = mid___cost:196)
               \/ (1 <= K:195 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= mid_x:198 /\ 0 <= (-1 + mid___cost:196)))
         /\ K:199 = 0 /\ mid_y:197 = y':200 /\ mid_x:198 = x':201
         /\ mid___cost:196 = __cost':202 /\ 0 = K:199
         /\ (K:195 + K:199) = K:203 /\ 0 <= K:203 /\ x':201 <= 0
         /\ (!(0 <= K:215) \/ mid___cost:216 = (__cost':202 + K:215))
         /\ (!(0 <= K:215) \/ mid_y:217 = (y':200 + -K:215))
         /\ ((K:215 = 0 /\ y':200 = mid_y:217 /\ __cost':202 = mid___cost:216)
               \/ (1 <= K:215 /\ 0 <= __cost':202 /\ 0 <= (-1 + y':200)
                     /\ 0 <= mid_y:217 /\ 0 <= (-1 + mid___cost:216)))
         /\ K:218 = 0 /\ mid_y:217 = y':219 /\ mid___cost:216 = __cost':220
         /\ 0 = K:218 /\ (K:215 + K:218) = K:221 /\ 0 <= K:221 /\ y':219 <= 0
         /\ K:355 = 0 /\ y':219 = mid_y:356 /\ __cost':220 = mid___cost:357
         /\ K:358 = 0 /\ mid_y:356 = y':359 /\ mid___cost:357 = __cost':360
         /\ 0 = K:358 /\ (K:355 + K:358) = K:361 /\ 0 <= K:361 /\ y':359 <= 0
         /\ y':359 <= 0 /\ y':359 <= 0)}

Evaluating variable number 31 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{return := havoc:169
 return@pos := type_err:172
 return@width := type_err:173}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,84)_g1> -> <__pstate, (Unique State Name,81)_g1>	Base relation: 
{__cost := __cost':220
 x := x':201
 y := y':219
 when ((!(0 <= K:195) \/ mid___cost:196 = (__cost:102 + K:195))
         /\ (!(0 <= K:195) \/ mid_y:197 = (param1:83 + (2 * K:195)))
         /\ (!(0 <= K:195) \/ mid_x:198 = (param0:80 + -K:195))
         /\ ((K:195 = 0 /\ param1:83 = mid_y:197 /\ param0:80 = mid_x:198
                /\ __cost:102 = mid___cost:196)
               \/ (1 <= K:195 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= mid_x:198 /\ 0 <= (-1 + mid___cost:196)))
         /\ K:199 = 0 /\ mid_y:197 = y':200 /\ mid_x:198 = x':201
         /\ mid___cost:196 = __cost':202 /\ 0 = K:199
         /\ (K:195 + K:199) = K:203 /\ 0 <= K:203 /\ x':201 <= 0
         /\ (!(0 <= K:215) \/ mid___cost:216 = (__cost':202 + K:215))
         /\ (!(0 <= K:215) \/ mid_y:217 = (y':200 + -K:215))
         /\ ((K:215 = 0 /\ y':200 = mid_y:217 /\ __cost':202 = mid___cost:216)
               \/ (1 <= K:215 /\ 0 <= __cost':202 /\ 0 <= (-1 + y':200)
                     /\ 0 <= mid_y:217 /\ 0 <= (-1 + mid___cost:216)))
         /\ K:218 = 0 /\ mid_y:217 = y':219 /\ mid___cost:216 = __cost':220
         /\ 0 = K:218 /\ (K:215 + K:218) = K:221 /\ 0 <= K:221 /\ y':219 <= 0)}	
<__pstate, accept> -> <__pstate, (Unique State Name,90)_g1>	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}	
<__pstate, (Unique State Name,90)_g1> -> <__pstate, (Unique State Name,84)_g1>	Base relation: 
{param0 := param0:80
 param1 := param1:83
 param0@pos := type_err:88
 param1@pos := type_err:89
 param0@width := type_err:90
 param1@width := type_err:91}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x56b5780: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x524ccc0: 
	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,81)_g1 , __done )	Base relation: 
{__cost := __cost':473
 x := havoc:21
 y := havoc:22
 x := x':465
 y := y':472
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:455
 param1@pos := type_err:456
 param0@width := type_err:457
 param1@width := type_err:458
 when ((!(0 <= K:459) \/ mid___cost:460 = K:459)
         /\ (!(0 <= K:459) \/ mid_y:461 = (havoc:22 + (2 * K:459)))
         /\ (!(0 <= K:459) \/ mid_x:462 = (havoc:21 + -K:459))
         /\ ((K:459 = 0 /\ havoc:22 = mid_y:461 /\ havoc:21 = mid_x:462
                /\ 0 = mid___cost:460)
               \/ (1 <= K:459 /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_x:462
                     /\ 0 <= (-1 + mid___cost:460))) /\ K:463 = 0
         /\ mid_y:461 = y':464 /\ mid_x:462 = x':465
         /\ mid___cost:460 = __cost':466 /\ 0 = K:463
         /\ (K:459 + K:463) = K:467 /\ 0 <= K:467 /\ x':465 <= 0
         /\ (!(0 <= K:468) \/ mid___cost:469 = (__cost':466 + K:468))
         /\ (!(0 <= K:468) \/ mid_y:470 = (y':464 + -K:468))
         /\ ((K:468 = 0 /\ y':464 = mid_y:470 /\ __cost':466 = mid___cost:469)
               \/ (1 <= K:468 /\ 0 <= __cost':466 /\ 0 <= (-1 + y':464)
                     /\ 0 <= mid_y:470 /\ 0 <= (-1 + mid___cost:469)))
         /\ K:471 = 0 /\ mid_y:470 = y':472 /\ mid___cost:469 = __cost':473
         /\ 0 = K:471 /\ (K:468 + K:471) = K:474 /\ 0 <= K:474 /\ y':472 <= 0)}
    ( __pstate , (Unique State Name,84)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:475
 param1@pos := type_err:476
 param0@width := type_err:477
 param1@width := type_err:478}
    ( __pstate , (Unique State Name,90)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}

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

------------------------------------------------
Procedure summary for fish

Base relation: 
{return := havoc:169
 return@pos := type_err:172
 return@width := type_err:173}

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

Base relation: 
{__cost := __cost':386
 x := havoc:21
 y := havoc:22
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:397
 param0@pos := type_err:390
 param1@pos := type_err:391
 return@width := type_err:398
 param0@width := type_err:393
 param1@width := type_err:394
 when ((!(0 <= K:365) \/ mid___cost:366 = K:365)
         /\ (!(0 <= K:365) \/ mid_y:367 = (havoc:22 + (2 * K:365)))
         /\ (!(0 <= K:365) \/ mid_x:368 = (havoc:21 + -K:365))
         /\ ((K:365 = 0 /\ havoc:22 = mid_y:367 /\ havoc:21 = mid_x:368
                /\ 0 = mid___cost:366)
               \/ (1 <= K:365 /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_x:368
                     /\ 0 <= (-1 + mid___cost:366))) /\ K:369 = 0
         /\ mid_y:367 = y':370 /\ mid_x:368 = x':371
         /\ mid___cost:366 = __cost':372 /\ 0 = K:369
         /\ (K:365 + K:369) = K:373 /\ 0 <= K:373 /\ x':371 <= 0
         /\ (!(0 <= K:374) \/ mid___cost:375 = (__cost':372 + K:374))
         /\ (!(0 <= K:374) \/ mid_y:376 = (y':370 + -K:374))
         /\ ((K:374 = 0 /\ y':370 = mid_y:376 /\ __cost':372 = mid___cost:375)
               \/ (1 <= K:374 /\ 0 <= __cost':372 /\ 0 <= (-1 + y':370)
                     /\ 0 <= mid_y:376 /\ 0 <= (-1 + mid___cost:375)))
         /\ K:377 = 0 /\ mid_y:376 = y':378 /\ mid___cost:375 = __cost':379
         /\ 0 = K:377 /\ (K:374 + K:377) = K:380 /\ 0 <= K:380 /\ y':378 <= 0
         /\ K:381 = 0 /\ y':378 = mid_y:382 /\ __cost':379 = mid___cost:383
         /\ K:384 = 0 /\ mid_y:382 = y':385 /\ mid___cost:383 = __cost':386
         /\ 0 = K:384 /\ (K:381 + K:384) = K:387 /\ 0 <= K:387 /\ y':385 <= 0
         /\ y':385 <= 0 /\ y':385 <= 0
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:395)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:395))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:396)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:396)))}

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

Base relation: 
{__cost := __cost':433
 return := havoc:438
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:439
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:440
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:412) \/ mid___cost:413 = (__cost:102 + K:412))
         /\ (!(0 <= K:412) \/ mid_y:414 = (param1:83 + (2 * K:412)))
         /\ (!(0 <= K:412) \/ mid_x:415 = (param0:80 + -K:412))
         /\ ((K:412 = 0 /\ param1:83 = mid_y:414 /\ param0:80 = mid_x:415
                /\ __cost:102 = mid___cost:413)
               \/ (1 <= K:412 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= mid_x:415 /\ 0 <= (-1 + mid___cost:413)))
         /\ K:416 = 0 /\ mid_y:414 = y':417 /\ mid_x:415 = x':418
         /\ mid___cost:413 = __cost':419 /\ 0 = K:416
         /\ (K:412 + K:416) = K:420 /\ 0 <= K:420 /\ x':418 <= 0
         /\ (!(0 <= K:421) \/ mid___cost:422 = (__cost':419 + K:421))
         /\ (!(0 <= K:421) \/ mid_y:423 = (y':417 + -K:421))
         /\ ((K:421 = 0 /\ y':417 = mid_y:423 /\ __cost':419 = mid___cost:422)
               \/ (1 <= K:421 /\ 0 <= __cost':419 /\ 0 <= (-1 + y':417)
                     /\ 0 <= mid_y:423 /\ 0 <= (-1 + mid___cost:422)))
         /\ K:424 = 0 /\ mid_y:423 = y':425 /\ mid___cost:422 = __cost':426
         /\ 0 = K:424 /\ (K:421 + K:424) = K:427 /\ 0 <= K:427 /\ y':425 <= 0
         /\ K:428 = 0 /\ y':425 = mid_y:429 /\ __cost':426 = mid___cost:430
         /\ K:431 = 0 /\ mid_y:429 = y':432 /\ mid___cost:430 = __cost':433
         /\ 0 = K:431 /\ (K:428 + K:431) = K:434 /\ 0 <= K:434 /\ y':432 <= 0
         /\ y':432 <= 0 /\ y':432 <= 0)}

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

Base relation: 
{__cost := __cost':407
 x := x':201
 y := y':406
 return := havoc:409
 return@pos := type_err:410
 return@width := type_err:411
 when ((!(0 <= K:195) \/ mid___cost:196 = (__cost:102 + K:195))
         /\ (!(0 <= K:195) \/ mid_y:197 = (param1:83 + (2 * K:195)))
         /\ (!(0 <= K:195) \/ mid_x:198 = (param0:80 + -K:195))
         /\ ((K:195 = 0 /\ param1:83 = mid_y:197 /\ param0:80 = mid_x:198
                /\ __cost:102 = mid___cost:196)
               \/ (1 <= K:195 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= mid_x:198 /\ 0 <= (-1 + mid___cost:196)))
         /\ K:199 = 0 /\ mid_y:197 = y':200 /\ mid_x:198 = x':201
         /\ mid___cost:196 = __cost':202 /\ 0 = K:199
         /\ (K:195 + K:199) = K:203 /\ 0 <= K:203 /\ x':201 <= 0
         /\ (!(0 <= K:215) \/ mid___cost:216 = (__cost':202 + K:215))
         /\ (!(0 <= K:215) \/ mid_y:217 = (y':200 + -K:215))
         /\ ((K:215 = 0 /\ y':200 = mid_y:217 /\ __cost':202 = mid___cost:216)
               \/ (1 <= K:215 /\ 0 <= __cost':202 /\ 0 <= (-1 + y':200)
                     /\ 0 <= mid_y:217 /\ 0 <= (-1 + mid___cost:216)))
         /\ K:218 = 0 /\ mid_y:217 = y':219 /\ mid___cost:216 = __cost':220
         /\ 0 = K:218 /\ (K:215 + K:218) = K:221 /\ 0 <= K:221 /\ y':219 <= 0
         /\ K:402 = 0 /\ y':219 = mid_y:403 /\ __cost':220 = mid___cost:404
         /\ K:405 = 0 /\ mid_y:403 = y':406 /\ mid___cost:404 = __cost':407
         /\ 0 = K:405 /\ (K:402 + K:405) = K:408 /\ 0 <= K:408 /\ y':406 <= 0
         /\ y':406 <= 0 /\ y':406 <= 0)}

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

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

Variable bounds at line 28 in run

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

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