/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, 39>	Base relation: 
{n := (n:101 + 1)
 y := (y:102 + 1000)
 when n:101 < 0}	
<Unique State Name, 33> -> <Unique State Name, 72>	Base relation: 
{return := havoc:109
 return@pos := type_err:110
 return@width := type_err:111
 when 0 <= n:101}	
<Unique State Name, 73> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 64> -> <Unique State Name, 25>	Base relation: 
{}	
<Unique State Name, 71> -> <Unique State Name, 66 70>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 75> -> <Unique State Name, 43>	Base relation: 
{}	
<Unique State Name, 23> -> <Unique State Name, 71>	Base relation: 
{__cost := 0
 n := 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, 43> -> <Unique State Name, 29>	Base relation: 
{when y:102 < 100}	
<Unique State Name, 43> -> <Unique State Name, 39>	Base relation: 
{__cost := (__cost:103 + 1)
 y := (y:102 + -100)
 when (100 <= y:102 /\ 0 <= __cost:103 /\ 0 <= (__cost:103 + 1))}	
<Unique State Name, 76> -> <Unique State Name, 33>	Base relation: 
{}	
<Unique State Name, 25> -> <Unique State Name, 73>	Base relation: 
{return := havoc:63
 return@pos := type_err:66
 return@width := type_err:67}	
<Unique State Name, 72> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 70> -> <Unique State Name, 74>	Base relation: 
{return := 0
 return@pos := type_err:32
 return@width := type_err:33
 when (((n:4 < y:5 /\ (y:5 + -n:4) = phi_tmp___1:23)
          \/ (y:5 <= n:4 /\ 0 = phi_tmp___1:23))
         /\ ((n:4 < 0 /\ -n:4 = phi_tmp___2:31)
               \/ (0 <= n:4 /\ 0 = phi_tmp___2:31)))}	
<Unique State Name, 29> -> <Unique State Name, 76>	Base relation: 
{}	
<Unique State Name, 39> -> <Unique State Name, 75>	Base relation: 
{}	
<Unique State Name, 66> -> <Unique State Name, 65>	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, 60> -> <Unique State Name, 29>	Base relation: 
{n := param0:80
 y := param1:83}	
<Unique State Name, 74> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 65> -> <Unique State Name, 60 64>	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:102 + -100)
 when (100 <= y:102 /\ 0 <= __cost:103 /\ 0 <= (__cost:103 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':151) = (1)*(__cost:103) + 1
           (y':152) = (1)*(y:102) + (-100)*1
           }
          pre:
            [|y:102-100>=0; __cost:103>=0|]
          post:
            [|y':152>=0; __cost':151-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':151
   y := y':152
   when ((!(0 <= K:160) \/ mid___cost:163 = (__cost:103 + K:160))
           /\ (!(0 <= K:160) \/ mid_y:162 = (y:102 + (-100 * K:160)))
           /\ ((K:160 = 0 /\ y:102 = mid_y:162 /\ __cost:103 = mid___cost:163)
                 \/ (1 <= K:160 /\ 0 <= (-100 + y:102) /\ 0 <= __cost:103
                       /\ 0 <= mid_y:162 /\ 0 <= (-1 + mid___cost:163)))
           /\ K:161 = 0 /\ mid_y:162 = y':152 /\ mid___cost:163 = __cost':151
           /\ 0 = K:161 /\ (K:160 + K:161) = K:159 /\ 0 <= K:159)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':169
 n := (n:101 + 1)
 y := y':168
 when (n:101 < 0 /\ (!(0 <= K:164) \/ mid___cost:165 = (__cost:103 + K:164))
         /\ (!(0 <= K:164) \/ mid_y:166 = ((y:102 + 1000) + (-100 * K:164)))
         /\ ((K:164 = 0 /\ (y:102 + 1000) = mid_y:166
                /\ __cost:103 = mid___cost:165)
               \/ (1 <= K:164 /\ 0 <= (-100 + (y:102 + 1000))
                     /\ 0 <= __cost:103 /\ 0 <= mid_y:166
                     /\ 0 <= (-1 + mid___cost:165))) /\ K:167 = 0
         /\ mid_y:166 = y':168 /\ mid___cost:165 = __cost':169 /\ 0 = K:167
         /\ (K:164 + K:167) = K:170 /\ 0 <= K:170 /\ y':168 < 100)}
**** alpha hat: 
  {<Split [!(-__cost:103 <= 0)
            (__cost':151) = (1)*(__cost:103) + 0
           (y':152) = (1)*(y:102) + 1000*1
           (n':171) = (1)*(n:101) + 1
           }
          pre:
            [|-__cost:103-1>=0; -n:101-1>=0; -y:102-901>=0|]
          post:
            [|-__cost':151-1>=0; -y':152+99>=0; -n':171>=0|]
           (n':171) = (1)*(n:101) + 1
          ((__cost':151 + (1/100 * y':152))) = (1)*((__cost:103
                                                       + (1/100 * y:102)))
                                                + 10*1
          (y':152) <= (1)*(y:102) + 1000*1
          }
  pre:
    [|-n:101-1>=0; __cost:103>=0|]
  post:
    [|-n':171>=0; -y':152+99>=0; __cost':151>=0|]],
[!((-900 + -y:102) <= 0)
  (y':152) = (1)*(y:102) + 1000*1
 (__cost':151) = (1)*(__cost:103) + 0
 (n':171) = (1)*(n:101) + 1
 } pre:   [|-n:101-1>=0; -y:102-901>=0|] post:
  [|-y':152+99>=0; -n':171>=0|]
 ((__cost':151 + (1/100 * y':152))) = (1)*((__cost:103 + (1/100 * y:102)))
                                       + 10*1 (n':171) = (1)*(n:101) + 1
(y':152) <= (1)*(y:102) + 900*1
(-y':152) <= (1)*(-y:102) + 100*(__cost:103 + (1/100 * y:102)) } pre:
  [|-n:101-1>=0; y:102+900>=0; __cost:103>=0|] post:
  [|-y':152+99>=0; -n':171>=0; __cost':151-1>=0; y':152>=0|]]>}
**** star transition: 
  {__cost := __cost':151
   n := n':171
   y := y':152
   when ((!(0 <= K:195) \/ mid___cost:199 = __cost:103)
           /\ (!(0 <= K:195) \/ mid_y:197 = (y:102 + (1000 * K:195)))
           /\ (!(0 <= K:195) \/ mid_n:198 = (n:101 + K:195))
           /\ ((K:195 = 0 /\ y:102 = mid_y:197 /\ n:101 = mid_n:198
                  /\ __cost:103 = mid___cost:199)
                 \/ (1 <= K:195 /\ 0 <= (-1 + -__cost:103)
                       /\ 0 <= (-1 + -n:101) /\ 0 <= (-901 + -y:102)
                       /\ 0 <= (-1 + -mid___cost:199)
                       /\ 0 <= (99 + -mid_y:197) /\ 0 <= -mid_n:198))
           /\ (0 = K:195 \/ !(-__cost:103 <= 0))
           /\ (!(0 <= K:196) \/ n':171 = (mid_n:198 + K:196))
           /\ (!(0 <= K:196)
                 \/ (__cost':151 + (1/100 * y':152)) = ((mid___cost:199
                                                           + (1/100
                                                                * mid_y:197))
                                                          + (10 * K:196)))
           /\ (!(0 <= K:196) \/ y':152 <= (mid_y:197 + (1000 * K:196)))
           /\ ((K:196 = 0 /\ mid_y:197 = y':152 /\ mid_n:198 = n':171
                  /\ mid___cost:199 = __cost':151)
                 \/ (1 <= K:196 /\ 0 <= (-1 + -mid_n:198)
                       /\ 0 <= mid___cost:199 /\ 0 <= -n':171
                       /\ 0 <= (99 + -y':152) /\ 0 <= __cost':151))
           /\ (0 = K:196 \/ -mid___cost:199 <= 0) /\ (K:195 + K:196) = K:194
           /\ (!(0 <= K:200) \/ mid_y:202 = (y:102 + (1000 * K:200)))
           /\ (!(0 <= K:200) \/ mid___cost:204 = __cost:103)
           /\ (!(0 <= K:200) \/ mid_n:203 = (n:101 + K:200))
           /\ ((K:200 = 0 /\ y:102 = mid_y:202 /\ n:101 = mid_n:203
                  /\ __cost:103 = mid___cost:204)
                 \/ (1 <= K:200 /\ 0 <= (-1 + -n:101) /\ 0 <= (-901 + -y:102)
                       /\ 0 <= (99 + -mid_y:202) /\ 0 <= -mid_n:203))
           /\ (0 = K:200 \/ !((-900 + -y:102) <= 0))
           /\ (!(0 <= K:201)
                 \/ (__cost':151 + (1/100 * y':152)) = ((mid___cost:204
                                                           + (1/100
                                                                * mid_y:202))
                                                          + (10 * K:201)))
           /\ (!(0 <= K:201) \/ n':171 = (mid_n:203 + K:201))
           /\ (!(0 <= K:201) \/ y':152 <= (mid_y:202 + (900 * K:201)))
           /\ (!(0 <= K:201)
                 \/ -y':152 <= (-mid_y:202 + (-500 * K:201)
                                  + (100
                                       * (mid___cost:204
                                            + (1/100 * mid_y:202)) * K:201)
                                  + (500 * (K:201 * K:201))))
           /\ ((K:201 = 0 /\ mid_y:202 = y':152 /\ mid_n:203 = n':171
                  /\ mid___cost:204 = __cost':151)
                 \/ (1 <= K:201 /\ 0 <= (-1 + -mid_n:203)
                       /\ 0 <= (900 + mid_y:202) /\ 0 <= mid___cost:204
                       /\ 0 <= (99 + -y':152) /\ 0 <= -n':171
                       /\ 0 <= (-1 + __cost':151) /\ 0 <= y':152))
           /\ (0 = K:201 \/ (-900 + -mid_y:202) <= 0)
           /\ (K:200 + K:201) = K:194 /\ 0 <= K:194)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  20  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       n := 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 (((n:4 < y:5 /\ (y:5 + -n:4) = phi_tmp___1:23)
              \/ (y:5 <= n:4 /\ 0 = phi_tmp___1:23))
             /\ ((n:4 < 0 /\ -n:4 = phi_tmp___2:31)
                   \/ (0 <= n:4 /\ 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(20)
  )
  ,
  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=20: 
Weight(Base relation: 
  {__cost := __cost':211
   n := n':210
   y := y':212
   return := havoc:226
   return@pos := type_err:227
   return@width := type_err:228
   when ((!(0 <= K:205) \/ mid___cost:206 = __cost:103)
           /\ (!(0 <= K:205) \/ mid_y:207 = (param1:83 + (1000 * K:205)))
           /\ (!(0 <= K:205) \/ mid_n:208 = (param0:80 + K:205))
           /\ ((K:205 = 0 /\ param1:83 = mid_y:207 /\ param0:80 = mid_n:208
                  /\ __cost:103 = mid___cost:206)
                 \/ (1 <= K:205 /\ 0 <= (-1 + -__cost:103)
                       /\ 0 <= (-1 + -param0:80) /\ 0 <= (-901 + -param1:83)
                       /\ 0 <= (-1 + -mid___cost:206)
                       /\ 0 <= (99 + -mid_y:207) /\ 0 <= -mid_n:208))
           /\ (0 = K:205 \/ !(-__cost:103 <= 0))
           /\ (!(0 <= K:209) \/ n':210 = (mid_n:208 + K:209))
           /\ (!(0 <= K:209)
                 \/ (__cost':211 + (1/100 * y':212)) = ((mid___cost:206
                                                           + (1/100
                                                                * mid_y:207))
                                                          + (10 * K:209)))
           /\ (!(0 <= K:209) \/ y':212 <= (mid_y:207 + (1000 * K:209)))
           /\ ((K:209 = 0 /\ mid_y:207 = y':212 /\ mid_n:208 = n':210
                  /\ mid___cost:206 = __cost':211)
                 \/ (1 <= K:209 /\ 0 <= (-1 + -mid_n:208)
                       /\ 0 <= mid___cost:206 /\ 0 <= -n':210
                       /\ 0 <= (99 + -y':212) /\ 0 <= __cost':211))
           /\ (0 = K:209 \/ -mid___cost:206 <= 0) /\ (K:205 + K:209) = K:213
           /\ (!(0 <= K:214) \/ mid_y:215 = (param1:83 + (1000 * K:214)))
           /\ (!(0 <= K:214) \/ mid___cost:216 = __cost:103)
           /\ (!(0 <= K:214) \/ mid_n:217 = (param0:80 + K:214))
           /\ ((K:214 = 0 /\ param1:83 = mid_y:215 /\ param0:80 = mid_n:217
                  /\ __cost:103 = mid___cost:216)
                 \/ (1 <= K:214 /\ 0 <= (-1 + -param0:80)
                       /\ 0 <= (-901 + -param1:83) /\ 0 <= (99 + -mid_y:215)
                       /\ 0 <= -mid_n:217))
           /\ (0 = K:214 \/ !((-900 + -param1:83) <= 0))
           /\ (!(0 <= K:218)
                 \/ (__cost':211 + (1/100 * y':212)) = ((mid___cost:216
                                                           + (1/100
                                                                * mid_y:215))
                                                          + (10 * K:218)))
           /\ (!(0 <= K:218) \/ n':210 = (mid_n:217 + K:218))
           /\ (!(0 <= K:218) \/ y':212 <= (mid_y:215 + (900 * K:218)))
           /\ (!(0 <= K:218)
                 \/ -y':212 <= (-mid_y:215 + (-500 * K:218)
                                  + (100
                                       * (mid___cost:216
                                            + (1/100 * mid_y:215)) * K:218)
                                  + (500 * (K:218 * K:218))))
           /\ ((K:218 = 0 /\ mid_y:215 = y':212 /\ mid_n:217 = n':210
                  /\ mid___cost:216 = __cost':211)
                 \/ (1 <= K:218 /\ 0 <= (-1 + -mid_n:217)
                       /\ 0 <= (900 + mid_y:215) /\ 0 <= mid___cost:216
                       /\ 0 <= (99 + -y':212) /\ 0 <= -n':210
                       /\ 0 <= (-1 + __cost':211) /\ 0 <= y':212))
           /\ (0 = K:218 \/ (-900 + -mid_y:215) <= 0)
           /\ (K:214 + K:218) = K:213 /\ 0 <= K:213 /\ 0 <= n':210)})



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



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

Weight(Base relation: 
  {__cost := __cost':211
   return := havoc:226
   return@pos := type_err:227
   return@width := type_err:228
   when ((!(0 <= K:205) \/ mid___cost:206 = __cost:103)
           /\ (!(0 <= K:205) \/ mid_y:207 = (param1:83 + (1000 * K:205)))
           /\ (!(0 <= K:205) \/ mid_n:208 = (param0:80 + K:205))
           /\ ((K:205 = 0 /\ param1:83 = mid_y:207 /\ param0:80 = mid_n:208
                  /\ __cost:103 = mid___cost:206)
                 \/ (1 <= K:205 /\ 0 <= (-1 + -__cost:103)
                       /\ 0 <= (-1 + -param0:80) /\ 0 <= (-901 + -param1:83)
                       /\ 0 <= (-1 + -mid___cost:206)
                       /\ 0 <= (99 + -mid_y:207) /\ 0 <= -mid_n:208))
           /\ (0 = K:205 \/ !(-__cost:103 <= 0))
           /\ (!(0 <= K:209) \/ n':210 = (mid_n:208 + K:209))
           /\ (!(0 <= K:209)
                 \/ (__cost':211 + (1/100 * y':212)) = ((mid___cost:206
                                                           + (1/100
                                                                * mid_y:207))
                                                          + (10 * K:209)))
           /\ (!(0 <= K:209) \/ y':212 <= (mid_y:207 + (1000 * K:209)))
           /\ ((K:209 = 0 /\ mid_y:207 = y':212 /\ mid_n:208 = n':210
                  /\ mid___cost:206 = __cost':211)
                 \/ (1 <= K:209 /\ 0 <= (-1 + -mid_n:208)
                       /\ 0 <= mid___cost:206 /\ 0 <= -n':210
                       /\ 0 <= (99 + -y':212) /\ 0 <= __cost':211))
           /\ (0 = K:209 \/ -mid___cost:206 <= 0) /\ (K:205 + K:209) = K:213
           /\ (!(0 <= K:214) \/ mid_y:215 = (param1:83 + (1000 * K:214)))
           /\ (!(0 <= K:214) \/ mid___cost:216 = __cost:103)
           /\ (!(0 <= K:214) \/ mid_n:217 = (param0:80 + K:214))
           /\ ((K:214 = 0 /\ param1:83 = mid_y:215 /\ param0:80 = mid_n:217
                  /\ __cost:103 = mid___cost:216)
                 \/ (1 <= K:214 /\ 0 <= (-1 + -param0:80)
                       /\ 0 <= (-901 + -param1:83) /\ 0 <= (99 + -mid_y:215)
                       /\ 0 <= -mid_n:217))
           /\ (0 = K:214 \/ !((-900 + -param1:83) <= 0))
           /\ (!(0 <= K:218)
                 \/ (__cost':211 + (1/100 * y':212)) = ((mid___cost:216
                                                           + (1/100
                                                                * mid_y:215))
                                                          + (10 * K:218)))
           /\ (!(0 <= K:218) \/ n':210 = (mid_n:217 + K:218))
           /\ (!(0 <= K:218) \/ y':212 <= (mid_y:215 + (900 * K:218)))
           /\ (!(0 <= K:218)
                 \/ -y':212 <= (-mid_y:215 + (-500 * K:218)
                                  + (100
                                       * (mid___cost:216
                                            + (1/100 * mid_y:215)) * K:218)
                                  + (500 * (K:218 * K:218))))
           /\ ((K:218 = 0 /\ mid_y:215 = y':212 /\ mid_n:217 = n':210
                  /\ mid___cost:216 = __cost':211)
                 \/ (1 <= K:218 /\ 0 <= (-1 + -mid_n:217)
                       /\ 0 <= (900 + mid_y:215) /\ 0 <= mid___cost:216
                       /\ 0 <= (99 + -y':212) /\ 0 <= -n':210
                       /\ 0 <= (-1 + __cost':211) /\ 0 <= y':212))
           /\ (0 = K:218 \/ (-900 + -mid_y:215) <= 0)
           /\ (K:214 + K:218) = K:213 /\ 0 <= K:213 /\ 0 <= n':210)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':255
   return := 0
   param0 := havoc:21
   param1 := havoc:22
   return@pos := type_err:272
   param0@pos := type_err:265
   param1@pos := type_err:266
   return@width := type_err:273
   param0@width := type_err:268
   param1@width := type_err:269
   when ((!(0 <= K:249) \/ mid___cost:250 = 0)
           /\ (!(0 <= K:249) \/ mid_y:251 = (havoc:22 + (1000 * K:249)))
           /\ (!(0 <= K:249) \/ mid_n:252 = (havoc:21 + K:249)) /\ K:249 = 0
           /\ havoc:22 = mid_y:251 /\ havoc:21 = mid_n:252
           /\ 0 = mid___cost:250 /\ 0 = K:249
           /\ (!(0 <= K:253) \/ n':254 = (mid_n:252 + K:253))
           /\ (!(0 <= K:253)
                 \/ (__cost':255 + (1/100 * y':256)) = ((mid___cost:250
                                                           + (1/100
                                                                * mid_y:251))
                                                          + (10 * K:253)))
           /\ (!(0 <= K:253) \/ y':256 <= (mid_y:251 + (1000 * K:253)))
           /\ ((K:253 = 0 /\ mid_y:251 = y':256 /\ mid_n:252 = n':254
                  /\ mid___cost:250 = __cost':255)
                 \/ (1 <= K:253 /\ 0 <= (-1 + -mid_n:252)
                       /\ 0 <= mid___cost:250 /\ 0 <= -n':254
                       /\ 0 <= (99 + -y':256) /\ 0 <= __cost':255))
           /\ (0 = K:253 \/ -mid___cost:250 <= 0) /\ (K:249 + K:253) = K:257
           /\ (!(0 <= K:258) \/ mid_y:259 = (havoc:22 + (1000 * K:258)))
           /\ (!(0 <= K:258) \/ mid___cost:260 = 0)
           /\ (!(0 <= K:258) \/ mid_n:261 = (havoc:21 + K:258))
           /\ ((K:258 = 0 /\ havoc:22 = mid_y:259 /\ havoc:21 = mid_n:261
                  /\ 0 = mid___cost:260)
                 \/ (1 <= K:258 /\ 0 <= (-1 + -havoc:21)
                       /\ 0 <= (-901 + -havoc:22) /\ 0 <= (99 + -mid_y:259)
                       /\ 0 <= -mid_n:261))
           /\ (0 = K:258 \/ !((-900 + -havoc:22) <= 0))
           /\ (!(0 <= K:262)
                 \/ (__cost':255 + (1/100 * y':256)) = ((mid___cost:260
                                                           + (1/100
                                                                * mid_y:259))
                                                          + (10 * K:262)))
           /\ (!(0 <= K:262) \/ n':254 = (mid_n:261 + K:262))
           /\ (!(0 <= K:262) \/ y':256 <= (mid_y:259 + (900 * K:262)))
           /\ (!(0 <= K:262)
                 \/ -y':256 <= (-mid_y:259 + (-500 * K:262)
                                  + (100
                                       * (mid___cost:260
                                            + (1/100 * mid_y:259)) * K:262)
                                  + (500 * (K:262 * K:262))))
           /\ ((K:262 = 0 /\ mid_y:259 = y':256 /\ mid_n:261 = n':254
                  /\ mid___cost:260 = __cost':255)
                 \/ (1 <= K:262 /\ 0 <= (-1 + -mid_n:261)
                       /\ 0 <= (900 + mid_y:259) /\ 0 <= mid___cost:260
                       /\ 0 <= (99 + -y':256) /\ 0 <= -n':254
                       /\ 0 <= (-1 + __cost':255) /\ 0 <= y':256))
           /\ (0 = K:262 \/ (-900 + -mid_y:259) <= 0)
           /\ (K:258 + K:262) = K:257 /\ 0 <= K:257 /\ 0 <= n':254
           /\ ((havoc:21 < havoc:22
                  /\ (havoc:22 + -havoc:21) = phi_tmp___1:270)
                 \/ (havoc:22 <= havoc:21 /\ 0 = phi_tmp___1:270))
           /\ ((havoc:21 < 0 /\ -havoc:21 = phi_tmp___2:271)
                 \/ (0 <= havoc:21 /\ 0 = phi_tmp___2:271)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':280
   return := havoc:291
   param0 := param0:80
   param1 := param1:83
   return@pos := type_err:292
   param0@pos := type_err:88
   param1@pos := type_err:89
   return@width := type_err:293
   param0@width := type_err:90
   param1@width := type_err:91
   when ((!(0 <= K:274) \/ mid___cost:275 = __cost:103)
           /\ (!(0 <= K:274) \/ mid_y:276 = (param1:83 + (1000 * K:274)))
           /\ (!(0 <= K:274) \/ mid_n:277 = (param0:80 + K:274))
           /\ ((K:274 = 0 /\ param1:83 = mid_y:276 /\ param0:80 = mid_n:277
                  /\ __cost:103 = mid___cost:275)
                 \/ (1 <= K:274 /\ 0 <= (-1 + -__cost:103)
                       /\ 0 <= (-1 + -param0:80) /\ 0 <= (-901 + -param1:83)
                       /\ 0 <= (-1 + -mid___cost:275)
                       /\ 0 <= (99 + -mid_y:276) /\ 0 <= -mid_n:277))
           /\ (0 = K:274 \/ !(-__cost:103 <= 0))
           /\ (!(0 <= K:278) \/ n':279 = (mid_n:277 + K:278))
           /\ (!(0 <= K:278)
                 \/ (__cost':280 + (1/100 * y':281)) = ((mid___cost:275
                                                           + (1/100
                                                                * mid_y:276))
                                                          + (10 * K:278)))
           /\ (!(0 <= K:278) \/ y':281 <= (mid_y:276 + (1000 * K:278)))
           /\ ((K:278 = 0 /\ mid_y:276 = y':281 /\ mid_n:277 = n':279
                  /\ mid___cost:275 = __cost':280)
                 \/ (1 <= K:278 /\ 0 <= (-1 + -mid_n:277)
                       /\ 0 <= mid___cost:275 /\ 0 <= -n':279
                       /\ 0 <= (99 + -y':281) /\ 0 <= __cost':280))
           /\ (0 = K:278 \/ -mid___cost:275 <= 0) /\ (K:274 + K:278) = K:282
           /\ (!(0 <= K:283) \/ mid_y:284 = (param1:83 + (1000 * K:283)))
           /\ (!(0 <= K:283) \/ mid___cost:285 = __cost:103)
           /\ (!(0 <= K:283) \/ mid_n:286 = (param0:80 + K:283))
           /\ ((K:283 = 0 /\ param1:83 = mid_y:284 /\ param0:80 = mid_n:286
                  /\ __cost:103 = mid___cost:285)
                 \/ (1 <= K:283 /\ 0 <= (-1 + -param0:80)
                       /\ 0 <= (-901 + -param1:83) /\ 0 <= (99 + -mid_y:284)
                       /\ 0 <= -mid_n:286))
           /\ (0 = K:283 \/ !((-900 + -param1:83) <= 0))
           /\ (!(0 <= K:287)
                 \/ (__cost':280 + (1/100 * y':281)) = ((mid___cost:285
                                                           + (1/100
                                                                * mid_y:284))
                                                          + (10 * K:287)))
           /\ (!(0 <= K:287) \/ n':279 = (mid_n:286 + K:287))
           /\ (!(0 <= K:287) \/ y':281 <= (mid_y:284 + (900 * K:287)))
           /\ (!(0 <= K:287)
                 \/ -y':281 <= (-mid_y:284 + (-500 * K:287)
                                  + (100
                                       * (mid___cost:285
                                            + (1/100 * mid_y:284)) * K:287)
                                  + (500 * (K:287 * K:287))))
           /\ ((K:287 = 0 /\ mid_y:284 = y':281 /\ mid_n:286 = n':279
                  /\ mid___cost:285 = __cost':280)
                 \/ (1 <= K:287 /\ 0 <= (-1 + -mid_n:286)
                       /\ 0 <= (900 + mid_y:284) /\ 0 <= mid___cost:285
                       /\ 0 <= (99 + -y':281) /\ 0 <= -n':279
                       /\ 0 <= (-1 + __cost':280) /\ 0 <= y':281))
           /\ (0 = K:287 \/ (-900 + -mid_y:284) <= 0)
           /\ (K:283 + K:287) = K:282 /\ 0 <= K:282 /\ 0 <= n':279)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=20: 
Weight(Base relation: 
  {__cost := __cost':211
   return := havoc:226
   return@pos := type_err:227
   return@width := type_err:228
   when ((!(0 <= K:205) \/ mid___cost:206 = __cost:103)
           /\ (!(0 <= K:205) \/ mid_y:207 = (param1:83 + (1000 * K:205)))
           /\ (!(0 <= K:205) \/ mid_n:208 = (param0:80 + K:205))
           /\ ((K:205 = 0 /\ param1:83 = mid_y:207 /\ param0:80 = mid_n:208
                  /\ __cost:103 = mid___cost:206)
                 \/ (1 <= K:205 /\ 0 <= (-1 + -__cost:103)
                       /\ 0 <= (-1 + -param0:80) /\ 0 <= (-901 + -param1:83)
                       /\ 0 <= (-1 + -mid___cost:206)
                       /\ 0 <= (99 + -mid_y:207) /\ 0 <= -mid_n:208))
           /\ (0 = K:205 \/ !(-__cost:103 <= 0))
           /\ (!(0 <= K:209) \/ n':210 = (mid_n:208 + K:209))
           /\ (!(0 <= K:209)
                 \/ (__cost':211 + (1/100 * y':212)) = ((mid___cost:206
                                                           + (1/100
                                                                * mid_y:207))
                                                          + (10 * K:209)))
           /\ (!(0 <= K:209) \/ y':212 <= (mid_y:207 + (1000 * K:209)))
           /\ ((K:209 = 0 /\ mid_y:207 = y':212 /\ mid_n:208 = n':210
                  /\ mid___cost:206 = __cost':211)
                 \/ (1 <= K:209 /\ 0 <= (-1 + -mid_n:208)
                       /\ 0 <= mid___cost:206 /\ 0 <= -n':210
                       /\ 0 <= (99 + -y':212) /\ 0 <= __cost':211))
           /\ (0 = K:209 \/ -mid___cost:206 <= 0) /\ (K:205 + K:209) = K:213
           /\ (!(0 <= K:214) \/ mid_y:215 = (param1:83 + (1000 * K:214)))
           /\ (!(0 <= K:214) \/ mid___cost:216 = __cost:103)
           /\ (!(0 <= K:214) \/ mid_n:217 = (param0:80 + K:214))
           /\ ((K:214 = 0 /\ param1:83 = mid_y:215 /\ param0:80 = mid_n:217
                  /\ __cost:103 = mid___cost:216)
                 \/ (1 <= K:214 /\ 0 <= (-1 + -param0:80)
                       /\ 0 <= (-901 + -param1:83) /\ 0 <= (99 + -mid_y:215)
                       /\ 0 <= -mid_n:217))
           /\ (0 = K:214 \/ !((-900 + -param1:83) <= 0))
           /\ (!(0 <= K:218)
                 \/ (__cost':211 + (1/100 * y':212)) = ((mid___cost:216
                                                           + (1/100
                                                                * mid_y:215))
                                                          + (10 * K:218)))
           /\ (!(0 <= K:218) \/ n':210 = (mid_n:217 + K:218))
           /\ (!(0 <= K:218) \/ y':212 <= (mid_y:215 + (900 * K:218)))
           /\ (!(0 <= K:218)
                 \/ -y':212 <= (-mid_y:215 + (-500 * K:218)
                                  + (100
                                       * (mid___cost:216
                                            + (1/100 * mid_y:215)) * K:218)
                                  + (500 * (K:218 * K:218))))
           /\ ((K:218 = 0 /\ mid_y:215 = y':212 /\ mid_n:217 = n':210
                  /\ mid___cost:216 = __cost':211)
                 \/ (1 <= K:218 /\ 0 <= (-1 + -mid_n:217)
                       /\ 0 <= (900 + mid_y:215) /\ 0 <= mid___cost:216
                       /\ 0 <= (99 + -y':212) /\ 0 <= -n':210
                       /\ 0 <= (-1 + __cost':211) /\ 0 <= y':212))
           /\ (0 = K:218 \/ (-900 + -mid_y:215) <= 0)
           /\ (K:214 + K:218) = K:213 /\ 0 <= K:213 /\ 0 <= n':210)})


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':255
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:272
 param0@pos := type_err:265
 param1@pos := type_err:266
 return@width := type_err:273
 param0@width := type_err:268
 param1@width := type_err:269
 when ((!(0 <= K:249) \/ mid___cost:250 = 0)
         /\ (!(0 <= K:249) \/ mid_y:251 = (havoc:22 + (1000 * K:249)))
         /\ (!(0 <= K:249) \/ mid_n:252 = (havoc:21 + K:249)) /\ K:249 = 0
         /\ havoc:22 = mid_y:251 /\ havoc:21 = mid_n:252
         /\ 0 = mid___cost:250 /\ 0 = K:249
         /\ (!(0 <= K:253) \/ n':254 = (mid_n:252 + K:253))
         /\ (!(0 <= K:253)
               \/ (__cost':255 + (1/100 * y':256)) = ((mid___cost:250
                                                         + (1/100 * mid_y:251))
                                                        + (10 * K:253)))
         /\ (!(0 <= K:253) \/ y':256 <= (mid_y:251 + (1000 * K:253)))
         /\ ((K:253 = 0 /\ mid_y:251 = y':256 /\ mid_n:252 = n':254
                /\ mid___cost:250 = __cost':255)
               \/ (1 <= K:253 /\ 0 <= (-1 + -mid_n:252)
                     /\ 0 <= mid___cost:250 /\ 0 <= -n':254
                     /\ 0 <= (99 + -y':256) /\ 0 <= __cost':255))
         /\ (0 = K:253 \/ -mid___cost:250 <= 0) /\ (K:249 + K:253) = K:257
         /\ (!(0 <= K:258) \/ mid_y:259 = (havoc:22 + (1000 * K:258)))
         /\ (!(0 <= K:258) \/ mid___cost:260 = 0)
         /\ (!(0 <= K:258) \/ mid_n:261 = (havoc:21 + K:258))
         /\ ((K:258 = 0 /\ havoc:22 = mid_y:259 /\ havoc:21 = mid_n:261
                /\ 0 = mid___cost:260)
               \/ (1 <= K:258 /\ 0 <= (-1 + -havoc:21)
                     /\ 0 <= (-901 + -havoc:22) /\ 0 <= (99 + -mid_y:259)
                     /\ 0 <= -mid_n:261))
         /\ (0 = K:258 \/ !((-900 + -havoc:22) <= 0))
         /\ (!(0 <= K:262)
               \/ (__cost':255 + (1/100 * y':256)) = ((mid___cost:260
                                                         + (1/100 * mid_y:259))
                                                        + (10 * K:262)))
         /\ (!(0 <= K:262) \/ n':254 = (mid_n:261 + K:262))
         /\ (!(0 <= K:262) \/ y':256 <= (mid_y:259 + (900 * K:262)))
         /\ (!(0 <= K:262)
               \/ -y':256 <= (-mid_y:259 + (-500 * K:262)
                                + (100
                                     * (mid___cost:260 + (1/100 * mid_y:259))
                                     * K:262) + (500 * (K:262 * K:262))))
         /\ ((K:262 = 0 /\ mid_y:259 = y':256 /\ mid_n:261 = n':254
                /\ mid___cost:260 = __cost':255)
               \/ (1 <= K:262 /\ 0 <= (-1 + -mid_n:261)
                     /\ 0 <= (900 + mid_y:259) /\ 0 <= mid___cost:260
                     /\ 0 <= (99 + -y':256) /\ 0 <= -n':254
                     /\ 0 <= (-1 + __cost':255) /\ 0 <= y':256))
         /\ (0 = K:262 \/ (-900 + -mid_y:259) <= 0)
         /\ (K:258 + K:262) = K:257 /\ 0 <= K:257 /\ 0 <= n':254
         /\ ((havoc:21 < havoc:22 /\ (havoc:22 + -havoc:21) = phi_tmp___1:270)
               \/ (havoc:22 <= havoc:21 /\ 0 = phi_tmp___1:270))
         /\ ((havoc:21 < 0 /\ -havoc:21 = phi_tmp___2:271)
               \/ (0 <= havoc:21 /\ 0 = phi_tmp___2:271)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':280
 return := havoc:291
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:292
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:293
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:274) \/ mid___cost:275 = __cost:103)
         /\ (!(0 <= K:274) \/ mid_y:276 = (param1:83 + (1000 * K:274)))
         /\ (!(0 <= K:274) \/ mid_n:277 = (param0:80 + K:274))
         /\ ((K:274 = 0 /\ param1:83 = mid_y:276 /\ param0:80 = mid_n:277
                /\ __cost:103 = mid___cost:275)
               \/ (1 <= K:274 /\ 0 <= (-1 + -__cost:103)
                     /\ 0 <= (-1 + -param0:80) /\ 0 <= (-901 + -param1:83)
                     /\ 0 <= (-1 + -mid___cost:275) /\ 0 <= (99 + -mid_y:276)
                     /\ 0 <= -mid_n:277))
         /\ (0 = K:274 \/ !(-__cost:103 <= 0))
         /\ (!(0 <= K:278) \/ n':279 = (mid_n:277 + K:278))
         /\ (!(0 <= K:278)
               \/ (__cost':280 + (1/100 * y':281)) = ((mid___cost:275
                                                         + (1/100 * mid_y:276))
                                                        + (10 * K:278)))
         /\ (!(0 <= K:278) \/ y':281 <= (mid_y:276 + (1000 * K:278)))
         /\ ((K:278 = 0 /\ mid_y:276 = y':281 /\ mid_n:277 = n':279
                /\ mid___cost:275 = __cost':280)
               \/ (1 <= K:278 /\ 0 <= (-1 + -mid_n:277)
                     /\ 0 <= mid___cost:275 /\ 0 <= -n':279
                     /\ 0 <= (99 + -y':281) /\ 0 <= __cost':280))
         /\ (0 = K:278 \/ -mid___cost:275 <= 0) /\ (K:274 + K:278) = K:282
         /\ (!(0 <= K:283) \/ mid_y:284 = (param1:83 + (1000 * K:283)))
         /\ (!(0 <= K:283) \/ mid___cost:285 = __cost:103)
         /\ (!(0 <= K:283) \/ mid_n:286 = (param0:80 + K:283))
         /\ ((K:283 = 0 /\ param1:83 = mid_y:284 /\ param0:80 = mid_n:286
                /\ __cost:103 = mid___cost:285)
               \/ (1 <= K:283 /\ 0 <= (-1 + -param0:80)
                     /\ 0 <= (-901 + -param1:83) /\ 0 <= (99 + -mid_y:284)
                     /\ 0 <= -mid_n:286))
         /\ (0 = K:283 \/ !((-900 + -param1:83) <= 0))
         /\ (!(0 <= K:287)
               \/ (__cost':280 + (1/100 * y':281)) = ((mid___cost:285
                                                         + (1/100 * mid_y:284))
                                                        + (10 * K:287)))
         /\ (!(0 <= K:287) \/ n':279 = (mid_n:286 + K:287))
         /\ (!(0 <= K:287) \/ y':281 <= (mid_y:284 + (900 * K:287)))
         /\ (!(0 <= K:287)
               \/ -y':281 <= (-mid_y:284 + (-500 * K:287)
                                + (100
                                     * (mid___cost:285 + (1/100 * mid_y:284))
                                     * K:287) + (500 * (K:287 * K:287))))
         /\ ((K:287 = 0 /\ mid_y:284 = y':281 /\ mid_n:286 = n':279
                /\ mid___cost:285 = __cost':280)
               \/ (1 <= K:287 /\ 0 <= (-1 + -mid_n:286)
                     /\ 0 <= (900 + mid_y:284) /\ 0 <= mid___cost:285
                     /\ 0 <= (99 + -y':281) /\ 0 <= -n':279
                     /\ 0 <= (-1 + __cost':280) /\ 0 <= y':281))
         /\ (0 = K:287 \/ (-900 + -mid_y:284) <= 0)
         /\ (K:283 + K:287) = K:282 /\ 0 <= K:282 /\ 0 <= n':279)}

Evaluating variable number 20 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':211
 return := havoc:226
 return@pos := type_err:227
 return@width := type_err:228
 when ((!(0 <= K:205) \/ mid___cost:206 = __cost:103)
         /\ (!(0 <= K:205) \/ mid_y:207 = (param1:83 + (1000 * K:205)))
         /\ (!(0 <= K:205) \/ mid_n:208 = (param0:80 + K:205))
         /\ ((K:205 = 0 /\ param1:83 = mid_y:207 /\ param0:80 = mid_n:208
                /\ __cost:103 = mid___cost:206)
               \/ (1 <= K:205 /\ 0 <= (-1 + -__cost:103)
                     /\ 0 <= (-1 + -param0:80) /\ 0 <= (-901 + -param1:83)
                     /\ 0 <= (-1 + -mid___cost:206) /\ 0 <= (99 + -mid_y:207)
                     /\ 0 <= -mid_n:208))
         /\ (0 = K:205 \/ !(-__cost:103 <= 0))
         /\ (!(0 <= K:209) \/ n':210 = (mid_n:208 + K:209))
         /\ (!(0 <= K:209)
               \/ (__cost':211 + (1/100 * y':212)) = ((mid___cost:206
                                                         + (1/100 * mid_y:207))
                                                        + (10 * K:209)))
         /\ (!(0 <= K:209) \/ y':212 <= (mid_y:207 + (1000 * K:209)))
         /\ ((K:209 = 0 /\ mid_y:207 = y':212 /\ mid_n:208 = n':210
                /\ mid___cost:206 = __cost':211)
               \/ (1 <= K:209 /\ 0 <= (-1 + -mid_n:208)
                     /\ 0 <= mid___cost:206 /\ 0 <= -n':210
                     /\ 0 <= (99 + -y':212) /\ 0 <= __cost':211))
         /\ (0 = K:209 \/ -mid___cost:206 <= 0) /\ (K:205 + K:209) = K:213
         /\ (!(0 <= K:214) \/ mid_y:215 = (param1:83 + (1000 * K:214)))
         /\ (!(0 <= K:214) \/ mid___cost:216 = __cost:103)
         /\ (!(0 <= K:214) \/ mid_n:217 = (param0:80 + K:214))
         /\ ((K:214 = 0 /\ param1:83 = mid_y:215 /\ param0:80 = mid_n:217
                /\ __cost:103 = mid___cost:216)
               \/ (1 <= K:214 /\ 0 <= (-1 + -param0:80)
                     /\ 0 <= (-901 + -param1:83) /\ 0 <= (99 + -mid_y:215)
                     /\ 0 <= -mid_n:217))
         /\ (0 = K:214 \/ !((-900 + -param1:83) <= 0))
         /\ (!(0 <= K:218)
               \/ (__cost':211 + (1/100 * y':212)) = ((mid___cost:216
                                                         + (1/100 * mid_y:215))
                                                        + (10 * K:218)))
         /\ (!(0 <= K:218) \/ n':210 = (mid_n:217 + K:218))
         /\ (!(0 <= K:218) \/ y':212 <= (mid_y:215 + (900 * K:218)))
         /\ (!(0 <= K:218)
               \/ -y':212 <= (-mid_y:215 + (-500 * K:218)
                                + (100
                                     * (mid___cost:216 + (1/100 * mid_y:215))
                                     * K:218) + (500 * (K:218 * K:218))))
         /\ ((K:218 = 0 /\ mid_y:215 = y':212 /\ mid_n:217 = n':210
                /\ mid___cost:216 = __cost':211)
               \/ (1 <= K:218 /\ 0 <= (-1 + -mid_n:217)
                     /\ 0 <= (900 + mid_y:215) /\ 0 <= mid___cost:216
                     /\ 0 <= (99 + -y':212) /\ 0 <= -n':210
                     /\ 0 <= (-1 + __cost':211) /\ 0 <= y':212))
         /\ (0 = K:218 \/ (-900 + -mid_y:215) <= 0)
         /\ (K:214 + K:218) = K:213 /\ 0 <= K:213 /\ 0 <= n':210)}

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

NumRnds: 1

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

Weights on states: 
__pstate 0x4df14b0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x61f4da0: 
	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,60)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:339
 param1@pos := type_err:340
 param0@width := type_err:341
 param1@width := type_err:342}
    ( __pstate , (Unique State Name,66)_g1 , __done )	Base relation: 
{__cost := 0
 n := 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 0x6527080: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x61df470: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
================================================
Procedure Summaries

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

Base relation: 
{__cost := __cost':300
 n := havoc:21
 y := havoc:22
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:317
 param0@pos := type_err:310
 param1@pos := type_err:311
 return@width := type_err:318
 param0@width := type_err:313
 param1@width := type_err:314
 when ((!(0 <= K:294) \/ mid___cost:295 = 0)
         /\ (!(0 <= K:294) \/ mid_y:296 = (havoc:22 + (1000 * K:294)))
         /\ (!(0 <= K:294) \/ mid_n:297 = (havoc:21 + K:294)) /\ K:294 = 0
         /\ havoc:22 = mid_y:296 /\ havoc:21 = mid_n:297
         /\ 0 = mid___cost:295 /\ 0 = K:294
         /\ (!(0 <= K:298) \/ n':299 = (mid_n:297 + K:298))
         /\ (!(0 <= K:298)
               \/ (__cost':300 + (1/100 * y':301)) = ((mid___cost:295
                                                         + (1/100 * mid_y:296))
                                                        + (10 * K:298)))
         /\ (!(0 <= K:298) \/ y':301 <= (mid_y:296 + (1000 * K:298)))
         /\ ((K:298 = 0 /\ mid_y:296 = y':301 /\ mid_n:297 = n':299
                /\ mid___cost:295 = __cost':300)
               \/ (1 <= K:298 /\ 0 <= (-1 + -mid_n:297)
                     /\ 0 <= mid___cost:295 /\ 0 <= -n':299
                     /\ 0 <= (99 + -y':301) /\ 0 <= __cost':300))
         /\ (0 = K:298 \/ -mid___cost:295 <= 0) /\ (K:294 + K:298) = K:302
         /\ (!(0 <= K:303) \/ mid_y:304 = (havoc:22 + (1000 * K:303)))
         /\ (!(0 <= K:303) \/ mid___cost:305 = 0)
         /\ (!(0 <= K:303) \/ mid_n:306 = (havoc:21 + K:303))
         /\ ((K:303 = 0 /\ havoc:22 = mid_y:304 /\ havoc:21 = mid_n:306
                /\ 0 = mid___cost:305)
               \/ (1 <= K:303 /\ 0 <= (-1 + -havoc:21)
                     /\ 0 <= (-901 + -havoc:22) /\ 0 <= (99 + -mid_y:304)
                     /\ 0 <= -mid_n:306))
         /\ (0 = K:303 \/ !((-900 + -havoc:22) <= 0))
         /\ (!(0 <= K:307)
               \/ (__cost':300 + (1/100 * y':301)) = ((mid___cost:305
                                                         + (1/100 * mid_y:304))
                                                        + (10 * K:307)))
         /\ (!(0 <= K:307) \/ n':299 = (mid_n:306 + K:307))
         /\ (!(0 <= K:307) \/ y':301 <= (mid_y:304 + (900 * K:307)))
         /\ (!(0 <= K:307)
               \/ -y':301 <= (-mid_y:304 + (-500 * K:307)
                                + (100
                                     * (mid___cost:305 + (1/100 * mid_y:304))
                                     * K:307) + (500 * (K:307 * K:307))))
         /\ ((K:307 = 0 /\ mid_y:304 = y':301 /\ mid_n:306 = n':299
                /\ mid___cost:305 = __cost':300)
               \/ (1 <= K:307 /\ 0 <= (-1 + -mid_n:306)
                     /\ 0 <= (900 + mid_y:304) /\ 0 <= mid___cost:305
                     /\ 0 <= (99 + -y':301) /\ 0 <= -n':299
                     /\ 0 <= (-1 + __cost':300) /\ 0 <= y':301))
         /\ (0 = K:307 \/ (-900 + -mid_y:304) <= 0)
         /\ (K:303 + K:307) = K:302 /\ 0 <= K:302 /\ 0 <= n':299
         /\ ((havoc:21 < havoc:22 /\ (havoc:22 + -havoc:21) = phi_tmp___1:315)
               \/ (havoc:22 <= havoc:21 /\ 0 = phi_tmp___1:315))
         /\ ((havoc:21 < 0 /\ -havoc:21 = phi_tmp___2:316)
               \/ (0 <= havoc:21 /\ 0 = phi_tmp___2:316)))}

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

Base relation: 
{__cost := __cost':325
 return := havoc:336
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:337
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:338
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:319) \/ mid___cost:320 = __cost:103)
         /\ (!(0 <= K:319) \/ mid_y:321 = (param1:83 + (1000 * K:319)))
         /\ (!(0 <= K:319) \/ mid_n:322 = (param0:80 + K:319))
         /\ ((K:319 = 0 /\ param1:83 = mid_y:321 /\ param0:80 = mid_n:322
                /\ __cost:103 = mid___cost:320)
               \/ (1 <= K:319 /\ 0 <= (-1 + -__cost:103)
                     /\ 0 <= (-1 + -param0:80) /\ 0 <= (-901 + -param1:83)
                     /\ 0 <= (-1 + -mid___cost:320) /\ 0 <= (99 + -mid_y:321)
                     /\ 0 <= -mid_n:322))
         /\ (0 = K:319 \/ !(-__cost:103 <= 0))
         /\ (!(0 <= K:323) \/ n':324 = (mid_n:322 + K:323))
         /\ (!(0 <= K:323)
               \/ (__cost':325 + (1/100 * y':326)) = ((mid___cost:320
                                                         + (1/100 * mid_y:321))
                                                        + (10 * K:323)))
         /\ (!(0 <= K:323) \/ y':326 <= (mid_y:321 + (1000 * K:323)))
         /\ ((K:323 = 0 /\ mid_y:321 = y':326 /\ mid_n:322 = n':324
                /\ mid___cost:320 = __cost':325)
               \/ (1 <= K:323 /\ 0 <= (-1 + -mid_n:322)
                     /\ 0 <= mid___cost:320 /\ 0 <= -n':324
                     /\ 0 <= (99 + -y':326) /\ 0 <= __cost':325))
         /\ (0 = K:323 \/ -mid___cost:320 <= 0) /\ (K:319 + K:323) = K:327
         /\ (!(0 <= K:328) \/ mid_y:329 = (param1:83 + (1000 * K:328)))
         /\ (!(0 <= K:328) \/ mid___cost:330 = __cost:103)
         /\ (!(0 <= K:328) \/ mid_n:331 = (param0:80 + K:328))
         /\ ((K:328 = 0 /\ param1:83 = mid_y:329 /\ param0:80 = mid_n:331
                /\ __cost:103 = mid___cost:330)
               \/ (1 <= K:328 /\ 0 <= (-1 + -param0:80)
                     /\ 0 <= (-901 + -param1:83) /\ 0 <= (99 + -mid_y:329)
                     /\ 0 <= -mid_n:331))
         /\ (0 = K:328 \/ !((-900 + -param1:83) <= 0))
         /\ (!(0 <= K:332)
               \/ (__cost':325 + (1/100 * y':326)) = ((mid___cost:330
                                                         + (1/100 * mid_y:329))
                                                        + (10 * K:332)))
         /\ (!(0 <= K:332) \/ n':324 = (mid_n:331 + K:332))
         /\ (!(0 <= K:332) \/ y':326 <= (mid_y:329 + (900 * K:332)))
         /\ (!(0 <= K:332)
               \/ -y':326 <= (-mid_y:329 + (-500 * K:332)
                                + (100
                                     * (mid___cost:330 + (1/100 * mid_y:329))
                                     * K:332) + (500 * (K:332 * K:332))))
         /\ ((K:332 = 0 /\ mid_y:329 = y':326 /\ mid_n:331 = n':324
                /\ mid___cost:330 = __cost':325)
               \/ (1 <= K:332 /\ 0 <= (-1 + -mid_n:331)
                     /\ 0 <= (900 + mid_y:329) /\ 0 <= mid___cost:330
                     /\ 0 <= (99 + -y':326) /\ 0 <= -n':324
                     /\ 0 <= (-1 + __cost':325) /\ 0 <= y':326))
         /\ (0 = K:332 \/ (-900 + -mid_y:329) <= 0)
         /\ (K:328 + K:332) = K:327 /\ 0 <= K:327 /\ 0 <= n':324)}

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

Base relation: 
{__cost := __cost':211
 n := n':210
 y := y':212
 return := havoc:226
 return@pos := type_err:227
 return@width := type_err:228
 when ((!(0 <= K:205) \/ mid___cost:206 = __cost:103)
         /\ (!(0 <= K:205) \/ mid_y:207 = (param1:83 + (1000 * K:205)))
         /\ (!(0 <= K:205) \/ mid_n:208 = (param0:80 + K:205))
         /\ ((K:205 = 0 /\ param1:83 = mid_y:207 /\ param0:80 = mid_n:208
                /\ __cost:103 = mid___cost:206)
               \/ (1 <= K:205 /\ 0 <= (-1 + -__cost:103)
                     /\ 0 <= (-1 + -param0:80) /\ 0 <= (-901 + -param1:83)
                     /\ 0 <= (-1 + -mid___cost:206) /\ 0 <= (99 + -mid_y:207)
                     /\ 0 <= -mid_n:208))
         /\ (0 = K:205 \/ !(-__cost:103 <= 0))
         /\ (!(0 <= K:209) \/ n':210 = (mid_n:208 + K:209))
         /\ (!(0 <= K:209)
               \/ (__cost':211 + (1/100 * y':212)) = ((mid___cost:206
                                                         + (1/100 * mid_y:207))
                                                        + (10 * K:209)))
         /\ (!(0 <= K:209) \/ y':212 <= (mid_y:207 + (1000 * K:209)))
         /\ ((K:209 = 0 /\ mid_y:207 = y':212 /\ mid_n:208 = n':210
                /\ mid___cost:206 = __cost':211)
               \/ (1 <= K:209 /\ 0 <= (-1 + -mid_n:208)
                     /\ 0 <= mid___cost:206 /\ 0 <= -n':210
                     /\ 0 <= (99 + -y':212) /\ 0 <= __cost':211))
         /\ (0 = K:209 \/ -mid___cost:206 <= 0) /\ (K:205 + K:209) = K:213
         /\ (!(0 <= K:214) \/ mid_y:215 = (param1:83 + (1000 * K:214)))
         /\ (!(0 <= K:214) \/ mid___cost:216 = __cost:103)
         /\ (!(0 <= K:214) \/ mid_n:217 = (param0:80 + K:214))
         /\ ((K:214 = 0 /\ param1:83 = mid_y:215 /\ param0:80 = mid_n:217
                /\ __cost:103 = mid___cost:216)
               \/ (1 <= K:214 /\ 0 <= (-1 + -param0:80)
                     /\ 0 <= (-901 + -param1:83) /\ 0 <= (99 + -mid_y:215)
                     /\ 0 <= -mid_n:217))
         /\ (0 = K:214 \/ !((-900 + -param1:83) <= 0))
         /\ (!(0 <= K:218)
               \/ (__cost':211 + (1/100 * y':212)) = ((mid___cost:216
                                                         + (1/100 * mid_y:215))
                                                        + (10 * K:218)))
         /\ (!(0 <= K:218) \/ n':210 = (mid_n:217 + K:218))
         /\ (!(0 <= K:218) \/ y':212 <= (mid_y:215 + (900 * K:218)))
         /\ (!(0 <= K:218)
               \/ -y':212 <= (-mid_y:215 + (-500 * K:218)
                                + (100
                                     * (mid___cost:216 + (1/100 * mid_y:215))
                                     * K:218) + (500 * (K:218 * K:218))))
         /\ ((K:218 = 0 /\ mid_y:215 = y':212 /\ mid_n:217 = n':210
                /\ mid___cost:216 = __cost':211)
               \/ (1 <= K:218 /\ 0 <= (-1 + -mid_n:217)
                     /\ 0 <= (900 + mid_y:215) /\ 0 <= mid___cost:216
                     /\ 0 <= (99 + -y':212) /\ 0 <= -n':210
                     /\ 0 <= (-1 + __cost':211) /\ 0 <= y':212))
         /\ (0 = K:218 \/ (-900 + -mid_y:215) <= 0)
         /\ (K:214 + K:218) = K:213 /\ 0 <= K:213 /\ 0 <= n':210)}

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

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

Variable bounds at line 20 in run

min(min(max((1 + __cost), (-99/100 + (1/100 * y) + __cost + (-10 * n))),
        max((__cost + -n), (-99/100 + (1/100 * y) + __cost + (-10 * n)))),
    __cost) <= __cost
__cost is o(1)
__cost <= max(max(((1/100 * y) + __cost + (-10 * n)),
                  min(((1/100 * y) + __cost + (-10 * n)),
                      (__cost + (-5 * n) + (((1/100 * y) + __cost) * -n)
                         + (5 * (-n * -n))))),
              __cost)
__cost is O(n)

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