/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: 
{__cost := (__cost:103 + 1)
 y := (y:101 + 1)
 when (y:101 < z:102 /\ 0 <= __cost:103 /\ 0 <= (__cost:103 + 1))}	
<Unique State Name, 33> -> <Unique State Name, 44>	Base relation: 
{when z:102 <= y:101}	
<Unique State Name, 75> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 66> -> <Unique State Name, 25>	Base relation: 
{}	
<Unique State Name, 73> -> <Unique State Name, 68 72>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 48> -> <Unique State Name, 44>	Base relation: 
{__cost := (__cost:103 + 1)
 y := (y:101 + -3)
 when (2 < y:101 /\ 0 <= __cost:103 /\ 0 <= (__cost:103 + 1))}	
<Unique State Name, 48> -> <Unique State Name, 74>	Base relation: 
{return := havoc:109
 return@pos := type_err:110
 return@width := type_err:111
 when y:101 <= 2}	
<Unique State Name, 23> -> <Unique State Name, 73>	Base relation: 
{__cost := 0
 y := havoc:21
 z := 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, 74> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 78> -> <Unique State Name, 33>	Base relation: 
{}	
<Unique State Name, 25> -> <Unique State Name, 75>	Base relation: 
{return := havoc:63
 return@pos := type_err:66
 return@width := type_err:67}	
<Unique State Name, 77> -> <Unique State Name, 48>	Base relation: 
{}	
<Unique State Name, 72> -> <Unique State Name, 76>	Base relation: 
{return := 0
 return@pos := type_err:32
 return@width := type_err:33
 when (((y:4 < z:5 /\ (z:5 + -y:4) = phi_tmp___1:23)
          \/ (z:5 <= y:4 /\ 0 = phi_tmp___1:23))
         /\ ((0 < y:4 /\ y:4 = phi_tmp___2:31)
               \/ (y:4 <= 0 /\ 0 = phi_tmp___2:31)))}	
<Unique State Name, 29> -> <Unique State Name, 78>	Base relation: 
{}	
<Unique State Name, 44> -> <Unique State Name, 77>	Base relation: 
{}	
<Unique State Name, 68> -> <Unique State Name, 67>	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, 62> -> <Unique State Name, 29>	Base relation: 
{y := param0:80
 z := param1:83}	
<Unique State Name, 76> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 67> -> <Unique State Name, 62 66>	Base relation: 
{}	MergeFn[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:103 + 1)
 y := (y:101 + 1)
 when (y:101 < z:102 /\ 0 <= __cost:103 /\ 0 <= (__cost:103 + 1))}
**** alpha hat: 
  {<Split [true
            (y':179) = (1)*(y:101) + 1
           (__cost':178) = (1)*(__cost:103) + 1
           }
          pre:
            [|-y:101+z:102-1>=0; __cost:103>=0|]
          post:
            [|__cost':178-1>=0; z:102-y':179>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':178
   y := y':179
   when ((!(0 <= K:188) \/ mid_y:190 = (y:101 + K:188))
           /\ (!(0 <= K:188) \/ mid___cost:191 = (__cost:103 + K:188))
           /\ ((K:188 = 0 /\ y:101 = mid_y:190 /\ __cost:103 = mid___cost:191)
                 \/ (1 <= K:188 /\ 0 <= (-1 + -y:101 + z:102)
                       /\ 0 <= __cost:103 /\ 0 <= (-1 + mid___cost:191)
                       /\ 0 <= (z:102 + -mid_y:190))) /\ K:189 = 0
           /\ mid_y:190 = y':179 /\ mid___cost:191 = __cost':178 /\ 0 = K:189
           /\ (K:188 + K:189) = K:187 /\ 0 <= K:187)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:103 + 1)
 y := (y:101 + -3)
 when (2 < y:101 /\ 0 <= __cost:103 /\ 0 <= (__cost:103 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':178) = (1)*(__cost:103) + 1
           (y':179) = (1)*(y:101) + (-3)*1
           }
          pre:
            [|__cost:103>=0; y:101-3>=0|]
          post:
            [|y':179>=0; __cost':178-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':178
   y := y':179
   when ((!(0 <= K:206) \/ mid___cost:209 = (__cost:103 + K:206))
           /\ (!(0 <= K:206) \/ mid_y:208 = (y:101 + (-3 * K:206)))
           /\ ((K:206 = 0 /\ y:101 = mid_y:208 /\ __cost:103 = mid___cost:209)
                 \/ (1 <= K:206 /\ 0 <= __cost:103 /\ 0 <= (-3 + y:101)
                       /\ 0 <= mid_y:208 /\ 0 <= (-1 + mid___cost:209)))
           /\ K:207 = 0 /\ mid_y:208 = y':179 /\ mid___cost:209 = __cost':178
           /\ 0 = K:207 /\ (K:206 + K:207) = K:205 /\ 0 <= K:205)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  22  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       y := havoc:21
       z := 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 (((y:4 < z:5 /\ (z:5 + -y:4) = phi_tmp___1:23)
              \/ (z:5 <= y:4 /\ 0 = phi_tmp___1:23))
             /\ ((0 < y:4 /\ y:4 = phi_tmp___2:31)
                   \/ (y:4 <= 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(22)
  )
  ,
  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=22: 
Weight(Base relation: 
  {__cost := __cost':215
   y := y':214
   z := param1:83
   return := havoc:217
   return@pos := type_err:218
   return@width := type_err:219
   when ((!(0 <= K:192) \/ mid_y:193 = (param0:80 + K:192))
           /\ (!(0 <= K:192) \/ mid___cost:194 = (__cost:103 + K:192))
           /\ ((K:192 = 0 /\ param0:80 = mid_y:193
                  /\ __cost:103 = mid___cost:194)
                 \/ (1 <= K:192 /\ 0 <= (-1 + -param0:80 + param1:83)
                       /\ 0 <= __cost:103 /\ 0 <= (-1 + mid___cost:194)
                       /\ 0 <= (param1:83 + -mid_y:193))) /\ K:195 = 0
           /\ mid_y:193 = y':196 /\ mid___cost:194 = __cost':197 /\ 0 = K:195
           /\ (K:192 + K:195) = K:198 /\ 0 <= K:198 /\ param1:83 <= y':196
           /\ (!(0 <= K:210) \/ mid___cost:211 = (__cost':197 + K:210))
           /\ (!(0 <= K:210) \/ mid_y:212 = (y':196 + (-3 * K:210)))
           /\ ((K:210 = 0 /\ y':196 = mid_y:212
                  /\ __cost':197 = mid___cost:211)
                 \/ (1 <= K:210 /\ 0 <= __cost':197 /\ 0 <= (-3 + y':196)
                       /\ 0 <= mid_y:212 /\ 0 <= (-1 + mid___cost:211)))
           /\ K:213 = 0 /\ mid_y:212 = y':214 /\ mid___cost:211 = __cost':215
           /\ 0 = K:213 /\ (K:210 + K:213) = K:216 /\ 0 <= K:216
           /\ y':214 <= 2)})



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
         y := havoc:21
         z := 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 (((y:4 < z:5 /\ (z:5 + -y:4) = phi_tmp___1:23)
                \/ (z:5 <= y:4 /\ 0 = phi_tmp___1:23))
               /\ ((0 < y:4 /\ y:4 = phi_tmp___2:31)
                     \/ (y:4 <= 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(22)
    )
    ,
    Weight(Base relation: 
      {return := havoc:63
       return@pos := type_err:66
       return@width := type_err:67}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':215
   return := havoc:217
   return@pos := type_err:218
   return@width := type_err:219
   when ((!(0 <= K:192) \/ mid_y:193 = (param0:80 + K:192))
           /\ (!(0 <= K:192) \/ mid___cost:194 = (__cost:103 + K:192))
           /\ ((K:192 = 0 /\ param0:80 = mid_y:193
                  /\ __cost:103 = mid___cost:194)
                 \/ (1 <= K:192 /\ 0 <= (-1 + -param0:80 + param1:83)
                       /\ 0 <= __cost:103 /\ 0 <= (-1 + mid___cost:194)
                       /\ 0 <= (param1:83 + -mid_y:193))) /\ K:195 = 0
           /\ mid_y:193 = y':196 /\ mid___cost:194 = __cost':197 /\ 0 = K:195
           /\ (K:192 + K:195) = K:198 /\ 0 <= K:198 /\ param1:83 <= y':196
           /\ (!(0 <= K:210) \/ mid___cost:211 = (__cost':197 + K:210))
           /\ (!(0 <= K:210) \/ mid_y:212 = (y':196 + (-3 * K:210)))
           /\ ((K:210 = 0 /\ y':196 = mid_y:212
                  /\ __cost':197 = mid___cost:211)
                 \/ (1 <= K:210 /\ 0 <= __cost':197 /\ 0 <= (-3 + y':196)
                       /\ 0 <= mid_y:212 /\ 0 <= (-1 + mid___cost:211)))
           /\ K:213 = 0 /\ mid_y:212 = y':214 /\ mid___cost:211 = __cost':215
           /\ 0 = K:213 /\ (K:210 + K:213) = K:216 /\ 0 <= K:216
           /\ y':214 <= 2)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':252
   return := 0
   param0 := havoc:21
   param1 := havoc:22
   return@pos := type_err:263
   param0@pos := type_err:256
   param1@pos := type_err:257
   return@width := type_err:264
   param0@width := type_err:259
   param1@width := type_err:260
   when ((!(0 <= K:240) \/ mid_y:241 = (havoc:21 + K:240))
           /\ (!(0 <= K:240) \/ mid___cost:242 = K:240)
           /\ ((K:240 = 0 /\ havoc:21 = mid_y:241 /\ 0 = mid___cost:242)
                 \/ (1 <= K:240 /\ 0 <= (-1 + -havoc:21 + havoc:22)
                       /\ 0 <= (-1 + mid___cost:242)
                       /\ 0 <= (havoc:22 + -mid_y:241))) /\ K:243 = 0
           /\ mid_y:241 = y':244 /\ mid___cost:242 = __cost':245 /\ 0 = K:243
           /\ (K:240 + K:243) = K:246 /\ 0 <= K:246 /\ havoc:22 <= y':244
           /\ (!(0 <= K:247) \/ mid___cost:248 = (__cost':245 + K:247))
           /\ (!(0 <= K:247) \/ mid_y:249 = (y':244 + (-3 * K:247)))
           /\ ((K:247 = 0 /\ y':244 = mid_y:249
                  /\ __cost':245 = mid___cost:248)
                 \/ (1 <= K:247 /\ 0 <= __cost':245 /\ 0 <= (-3 + y':244)
                       /\ 0 <= mid_y:249 /\ 0 <= (-1 + mid___cost:248)))
           /\ K:250 = 0 /\ mid_y:249 = y':251 /\ mid___cost:248 = __cost':252
           /\ 0 = K:250 /\ (K:247 + K:250) = K:253 /\ 0 <= K:253
           /\ y':251 <= 2
           /\ ((havoc:21 < havoc:22
                  /\ (havoc:22 + -havoc:21) = phi_tmp___1:261)
                 \/ (havoc:22 <= havoc:21 /\ 0 = phi_tmp___1:261))
           /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___2:262)
                 \/ (havoc:21 <= 0 /\ 0 = phi_tmp___2:262)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':277
   return := havoc:282
   param0 := param0:80
   param1 := param1:83
   return@pos := type_err:283
   param0@pos := type_err:88
   param1@pos := type_err:89
   return@width := type_err:284
   param0@width := type_err:90
   param1@width := type_err:91
   when ((!(0 <= K:265) \/ mid_y:266 = (param0:80 + K:265))
           /\ (!(0 <= K:265) \/ mid___cost:267 = (__cost:103 + K:265))
           /\ ((K:265 = 0 /\ param0:80 = mid_y:266
                  /\ __cost:103 = mid___cost:267)
                 \/ (1 <= K:265 /\ 0 <= (-1 + -param0:80 + param1:83)
                       /\ 0 <= __cost:103 /\ 0 <= (-1 + mid___cost:267)
                       /\ 0 <= (param1:83 + -mid_y:266))) /\ K:268 = 0
           /\ mid_y:266 = y':269 /\ mid___cost:267 = __cost':270 /\ 0 = K:268
           /\ (K:265 + K:268) = K:271 /\ 0 <= K:271 /\ param1:83 <= y':269
           /\ (!(0 <= K:272) \/ mid___cost:273 = (__cost':270 + K:272))
           /\ (!(0 <= K:272) \/ mid_y:274 = (y':269 + (-3 * K:272)))
           /\ ((K:272 = 0 /\ y':269 = mid_y:274
                  /\ __cost':270 = mid___cost:273)
                 \/ (1 <= K:272 /\ 0 <= __cost':270 /\ 0 <= (-3 + y':269)
                       /\ 0 <= mid_y:274 /\ 0 <= (-1 + mid___cost:273)))
           /\ K:275 = 0 /\ mid_y:274 = y':276 /\ mid___cost:273 = __cost':277
           /\ 0 = K:275 /\ (K:272 + K:275) = K:278 /\ 0 <= K:278
           /\ y':276 <= 2)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=22: 
Weight(Base relation: 
  {__cost := __cost':215
   return := havoc:217
   return@pos := type_err:218
   return@width := type_err:219
   when ((!(0 <= K:192) \/ mid_y:193 = (param0:80 + K:192))
           /\ (!(0 <= K:192) \/ mid___cost:194 = (__cost:103 + K:192))
           /\ ((K:192 = 0 /\ param0:80 = mid_y:193
                  /\ __cost:103 = mid___cost:194)
                 \/ (1 <= K:192 /\ 0 <= (-1 + -param0:80 + param1:83)
                       /\ 0 <= __cost:103 /\ 0 <= (-1 + mid___cost:194)
                       /\ 0 <= (param1:83 + -mid_y:193))) /\ K:195 = 0
           /\ mid_y:193 = y':196 /\ mid___cost:194 = __cost':197 /\ 0 = K:195
           /\ (K:192 + K:195) = K:198 /\ 0 <= K:198 /\ param1:83 <= y':196
           /\ (!(0 <= K:210) \/ mid___cost:211 = (__cost':197 + K:210))
           /\ (!(0 <= K:210) \/ mid_y:212 = (y':196 + (-3 * K:210)))
           /\ ((K:210 = 0 /\ y':196 = mid_y:212
                  /\ __cost':197 = mid___cost:211)
                 \/ (1 <= K:210 /\ 0 <= __cost':197 /\ 0 <= (-3 + y':196)
                       /\ 0 <= mid_y:212 /\ 0 <= (-1 + mid___cost:211)))
           /\ K:213 = 0 /\ mid_y:212 = y':214 /\ mid___cost:211 = __cost':215
           /\ 0 = K:213 /\ (K:210 + K:213) = K:216 /\ 0 <= K:216
           /\ y':214 <= 2)})


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':252
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:263
 param0@pos := type_err:256
 param1@pos := type_err:257
 return@width := type_err:264
 param0@width := type_err:259
 param1@width := type_err:260
 when ((!(0 <= K:240) \/ mid_y:241 = (havoc:21 + K:240))
         /\ (!(0 <= K:240) \/ mid___cost:242 = K:240)
         /\ ((K:240 = 0 /\ havoc:21 = mid_y:241 /\ 0 = mid___cost:242)
               \/ (1 <= K:240 /\ 0 <= (-1 + -havoc:21 + havoc:22)
                     /\ 0 <= (-1 + mid___cost:242)
                     /\ 0 <= (havoc:22 + -mid_y:241))) /\ K:243 = 0
         /\ mid_y:241 = y':244 /\ mid___cost:242 = __cost':245 /\ 0 = K:243
         /\ (K:240 + K:243) = K:246 /\ 0 <= K:246 /\ havoc:22 <= y':244
         /\ (!(0 <= K:247) \/ mid___cost:248 = (__cost':245 + K:247))
         /\ (!(0 <= K:247) \/ mid_y:249 = (y':244 + (-3 * K:247)))
         /\ ((K:247 = 0 /\ y':244 = mid_y:249 /\ __cost':245 = mid___cost:248)
               \/ (1 <= K:247 /\ 0 <= __cost':245 /\ 0 <= (-3 + y':244)
                     /\ 0 <= mid_y:249 /\ 0 <= (-1 + mid___cost:248)))
         /\ K:250 = 0 /\ mid_y:249 = y':251 /\ mid___cost:248 = __cost':252
         /\ 0 = K:250 /\ (K:247 + K:250) = K:253 /\ 0 <= K:253 /\ y':251 <= 2
         /\ ((havoc:21 < havoc:22 /\ (havoc:22 + -havoc:21) = phi_tmp___1:261)
               \/ (havoc:22 <= havoc:21 /\ 0 = phi_tmp___1:261))
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___2:262)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___2:262)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':277
 return := havoc:282
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:283
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:284
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:265) \/ mid_y:266 = (param0:80 + K:265))
         /\ (!(0 <= K:265) \/ mid___cost:267 = (__cost:103 + K:265))
         /\ ((K:265 = 0 /\ param0:80 = mid_y:266
                /\ __cost:103 = mid___cost:267)
               \/ (1 <= K:265 /\ 0 <= (-1 + -param0:80 + param1:83)
                     /\ 0 <= __cost:103 /\ 0 <= (-1 + mid___cost:267)
                     /\ 0 <= (param1:83 + -mid_y:266))) /\ K:268 = 0
         /\ mid_y:266 = y':269 /\ mid___cost:267 = __cost':270 /\ 0 = K:268
         /\ (K:265 + K:268) = K:271 /\ 0 <= K:271 /\ param1:83 <= y':269
         /\ (!(0 <= K:272) \/ mid___cost:273 = (__cost':270 + K:272))
         /\ (!(0 <= K:272) \/ mid_y:274 = (y':269 + (-3 * K:272)))
         /\ ((K:272 = 0 /\ y':269 = mid_y:274 /\ __cost':270 = mid___cost:273)
               \/ (1 <= K:272 /\ 0 <= __cost':270 /\ 0 <= (-3 + y':269)
                     /\ 0 <= mid_y:274 /\ 0 <= (-1 + mid___cost:273)))
         /\ K:275 = 0 /\ mid_y:274 = y':276 /\ mid___cost:273 = __cost':277
         /\ 0 = K:275 /\ (K:272 + K:275) = K:278 /\ 0 <= K:278 /\ y':276 <= 2)}

Evaluating variable number 22 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':215
 return := havoc:217
 return@pos := type_err:218
 return@width := type_err:219
 when ((!(0 <= K:192) \/ mid_y:193 = (param0:80 + K:192))
         /\ (!(0 <= K:192) \/ mid___cost:194 = (__cost:103 + K:192))
         /\ ((K:192 = 0 /\ param0:80 = mid_y:193
                /\ __cost:103 = mid___cost:194)
               \/ (1 <= K:192 /\ 0 <= (-1 + -param0:80 + param1:83)
                     /\ 0 <= __cost:103 /\ 0 <= (-1 + mid___cost:194)
                     /\ 0 <= (param1:83 + -mid_y:193))) /\ K:195 = 0
         /\ mid_y:193 = y':196 /\ mid___cost:194 = __cost':197 /\ 0 = K:195
         /\ (K:192 + K:195) = K:198 /\ 0 <= K:198 /\ param1:83 <= y':196
         /\ (!(0 <= K:210) \/ mid___cost:211 = (__cost':197 + K:210))
         /\ (!(0 <= K:210) \/ mid_y:212 = (y':196 + (-3 * K:210)))
         /\ ((K:210 = 0 /\ y':196 = mid_y:212 /\ __cost':197 = mid___cost:211)
               \/ (1 <= K:210 /\ 0 <= __cost':197 /\ 0 <= (-3 + y':196)
                     /\ 0 <= mid_y:212 /\ 0 <= (-1 + mid___cost:211)))
         /\ K:213 = 0 /\ mid_y:212 = y':214 /\ mid___cost:211 = __cost':215
         /\ 0 = K:213 /\ (K:210 + K:213) = K:216 /\ 0 <= K:216 /\ y':214 <= 2)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,68)_g1> -> <__pstate, (Unique State Name,62)_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}	
<__pstate, accept> -> <__pstate, (Unique State Name,68)_g1>	Base relation: 
{__cost := 0
 y := havoc:21
 z := 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}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x5a8bd00: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x5a8b9c0: 
	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,62)_g1 , __done )	Base relation: 
{__cost := 0
 y := havoc:21
 z := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:330
 param1@pos := type_err:331
 param0@width := type_err:332
 param1@width := type_err:333}
    ( __pstate , (Unique State Name,68)_g1 , __done )	Base relation: 
{__cost := 0
 y := havoc:21
 z := 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 0x54a42b0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x5d73fd0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
================================================
Procedure Summaries

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

Base relation: 
{__cost := __cost':297
 y := havoc:21
 z := havoc:22
 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:285) \/ mid_y:286 = (havoc:21 + K:285))
         /\ (!(0 <= K:285) \/ mid___cost:287 = K:285)
         /\ ((K:285 = 0 /\ havoc:21 = mid_y:286 /\ 0 = mid___cost:287)
               \/ (1 <= K:285 /\ 0 <= (-1 + -havoc:21 + havoc:22)
                     /\ 0 <= (-1 + mid___cost:287)
                     /\ 0 <= (havoc:22 + -mid_y:286))) /\ K:288 = 0
         /\ mid_y:286 = y':289 /\ mid___cost:287 = __cost':290 /\ 0 = K:288
         /\ (K:285 + K:288) = K:291 /\ 0 <= K:291 /\ havoc:22 <= y':289
         /\ (!(0 <= K:292) \/ mid___cost:293 = (__cost':290 + K:292))
         /\ (!(0 <= K:292) \/ mid_y:294 = (y':289 + (-3 * K:292)))
         /\ ((K:292 = 0 /\ y':289 = mid_y:294 /\ __cost':290 = mid___cost:293)
               \/ (1 <= K:292 /\ 0 <= __cost':290 /\ 0 <= (-3 + y':289)
                     /\ 0 <= mid_y:294 /\ 0 <= (-1 + mid___cost:293)))
         /\ K:295 = 0 /\ mid_y:294 = y':296 /\ mid___cost:293 = __cost':297
         /\ 0 = K:295 /\ (K:292 + K:295) = K:298 /\ 0 <= K:298 /\ y':296 <= 2
         /\ ((havoc:21 < havoc:22 /\ (havoc:22 + -havoc:21) = phi_tmp___1:306)
               \/ (havoc:22 <= havoc:21 /\ 0 = phi_tmp___1:306))
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___2:307)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___2:307)))}

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

Base relation: 
{__cost := __cost':322
 return := havoc:327
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:328
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:329
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:310) \/ mid_y:311 = (param0:80 + K:310))
         /\ (!(0 <= K:310) \/ mid___cost:312 = (__cost:103 + K:310))
         /\ ((K:310 = 0 /\ param0:80 = mid_y:311
                /\ __cost:103 = mid___cost:312)
               \/ (1 <= K:310 /\ 0 <= (-1 + -param0:80 + param1:83)
                     /\ 0 <= __cost:103 /\ 0 <= (-1 + mid___cost:312)
                     /\ 0 <= (param1:83 + -mid_y:311))) /\ K:313 = 0
         /\ mid_y:311 = y':314 /\ mid___cost:312 = __cost':315 /\ 0 = K:313
         /\ (K:310 + K:313) = K:316 /\ 0 <= K:316 /\ param1:83 <= y':314
         /\ (!(0 <= K:317) \/ mid___cost:318 = (__cost':315 + K:317))
         /\ (!(0 <= K:317) \/ mid_y:319 = (y':314 + (-3 * K:317)))
         /\ ((K:317 = 0 /\ y':314 = mid_y:319 /\ __cost':315 = mid___cost:318)
               \/ (1 <= K:317 /\ 0 <= __cost':315 /\ 0 <= (-3 + y':314)
                     /\ 0 <= mid_y:319 /\ 0 <= (-1 + mid___cost:318)))
         /\ K:320 = 0 /\ mid_y:319 = y':321 /\ mid___cost:318 = __cost':322
         /\ 0 = K:320 /\ (K:317 + K:320) = K:323 /\ 0 <= K:323 /\ y':321 <= 2)}

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

Base relation: 
{__cost := __cost':215
 y := y':214
 z := param1:83
 return := havoc:217
 return@pos := type_err:218
 return@width := type_err:219
 when ((!(0 <= K:192) \/ mid_y:193 = (param0:80 + K:192))
         /\ (!(0 <= K:192) \/ mid___cost:194 = (__cost:103 + K:192))
         /\ ((K:192 = 0 /\ param0:80 = mid_y:193
                /\ __cost:103 = mid___cost:194)
               \/ (1 <= K:192 /\ 0 <= (-1 + -param0:80 + param1:83)
                     /\ 0 <= __cost:103 /\ 0 <= (-1 + mid___cost:194)
                     /\ 0 <= (param1:83 + -mid_y:193))) /\ K:195 = 0
         /\ mid_y:193 = y':196 /\ mid___cost:194 = __cost':197 /\ 0 = K:195
         /\ (K:192 + K:195) = K:198 /\ 0 <= K:198 /\ param1:83 <= y':196
         /\ (!(0 <= K:210) \/ mid___cost:211 = (__cost':197 + K:210))
         /\ (!(0 <= K:210) \/ mid_y:212 = (y':196 + (-3 * K:210)))
         /\ ((K:210 = 0 /\ y':196 = mid_y:212 /\ __cost':197 = mid___cost:211)
               \/ (1 <= K:210 /\ 0 <= __cost':197 /\ 0 <= (-3 + y':196)
                     /\ 0 <= mid_y:212 /\ 0 <= (-1 + mid___cost:211)))
         /\ K:213 = 0 /\ mid_y:212 = y':214 /\ mid___cost:211 = __cost':215
         /\ 0 = K:213 /\ (K:210 + K:213) = K:216 /\ 0 <= K:216 /\ y':214 <= 2)}

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

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

Variable bounds at line 20 in run

min(min(min((__cost + -y + z), __cost),
        max((1 + __cost), (-2/3 + __cost + (1/3 * y)))),
    max((1 + __cost + -y + z), (-2/3 + __cost + -y + (4/3 * z)))) <= __cost
__cost is o(1)
__cost <= max(max(max((__cost + -y + z), __cost), (__cost + (1/3 * y))),
              (__cost + -y + (4/3 * z)))
__cost is O(n)

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