/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, 26> -> <Unique State Name, 31>	Base relation: 
{flag := 0
 when 0 < flag:64}	
<Unique State Name, 26> -> <Unique State Name, 61>	Base relation: 
{return := havoc:72
 return@pos := type_err:73
 return@width := type_err:74
 when flag:64 <= 0}	
<Unique State Name, 62> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 55> -> <Unique State Name, 17>	Base relation: 
{}	
<Unique State Name, 60> -> <Unique State Name, 57 59>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 64> -> <Unique State Name, 35>	Base relation: 
{}	
<Unique State Name, 15> -> <Unique State Name, 60>	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
<Unique State Name, 35> -> <Unique State Name, 22>	Base relation: 
{when n:65 <= 0}	
<Unique State Name, 35> -> <Unique State Name, 31>	Base relation: 
{__cost := (__cost:66 + 1)
 flag := 1
 n := (n:65 + -1)
 when (0 < n:65 /\ 0 <= __cost:66 /\ 0 <= (__cost:66 + 1))}	
<Unique State Name, 65> -> <Unique State Name, 26>	Base relation: 
{}	
<Unique State Name, 17> -> <Unique State Name, 62>	Base relation: 
{return := 0
 return@pos := type_err:54
 return@width := type_err:55}	
<Unique State Name, 61> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 59> -> <Unique State Name, 63>	Base relation: 
{return := 0
 return@pos := type_err:19
 return@width := type_err:20
 when ((0 < n:2 /\ n:2 = phi_tmp___0:14) \/ (n:2 <= 0 /\ 0 = phi_tmp___0:14))}	
<Unique State Name, 22> -> <Unique State Name, 65>	Base relation: 
{when (flag:64 <= 1 /\ 0 <= flag:64)}	
<Unique State Name, 31> -> <Unique State Name, 64>	Base relation: 
{when (flag:64 <= 1 /\ 0 <= flag:64)}	
<Unique State Name, 57> -> <Unique State Name, 56>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:56
 param0@width := type_err:57}	
<Unique State Name, 53> -> <Unique State Name, 22>	Base relation: 
{flag := 1
 n := param0:53}	
<Unique State Name, 63> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 56> -> <Unique State Name, 53 55>	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:66 + 1)
 flag := 1
 n := (n:65 + -1)
 when (flag:64 <= 1 /\ 0 <= flag:64 /\ 0 < n:65 /\ 0 <= __cost:66
         /\ 0 <= (__cost:66 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':158) = (1)*(__cost:66) + 1
           (flag':159) = 1
           (n':160) = (1)*(n:65) + (-1)*1
           (flag':159) <= (1)*(flag:64) + 1
           (-flag':159) <= (1)*(-flag:64) + 0
           }
          pre:
            [|-flag:64+1>=0; flag:64>=0; __cost:66>=0; n:65-1>=0|]
          post:
            [|flag':159-1=0; n':160>=0; __cost':158-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':158
   flag := flag':159
   n := n':160
   when ((!(0 <= K:171) \/ mid___cost:175 = (__cost:66 + K:171))
           /\ (!((0 <= K:171 /\ K:171 <= 0)) \/ mid_flag:174 = flag:64)
           /\ (!(1 <= K:171) \/ mid_flag:174 = 1)
           /\ (!(0 <= K:171) \/ mid_n:173 = (n:65 + -K:171))
           /\ (!(0 <= K:171) \/ mid_flag:174 <= (flag:64 + K:171))
           /\ (!(0 <= K:171) \/ -mid_flag:174 <= -flag:64)
           /\ ((K:171 = 0 /\ n:65 = mid_n:173 /\ flag:64 = mid_flag:174
                  /\ __cost:66 = mid___cost:175)
                 \/ (1 <= K:171 /\ 0 <= (1 + -flag:64) /\ 0 <= flag:64
                       /\ 0 <= __cost:66 /\ 0 <= (-1 + n:65)
                       /\ (-1 + mid_flag:174) = 0 /\ 0 <= mid_n:173
                       /\ 0 <= (-1 + mid___cost:175))) /\ K:172 = 0
           /\ mid_n:173 = n':160 /\ mid_flag:174 = flag':159
           /\ mid___cost:175 = __cost':158 /\ 0 = K:172
           /\ (K:171 + K:172) = K:170 /\ 0 <= K:170)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':192
 flag := flag':191
 n := n':190
 when (flag:64 <= 1 /\ 0 <= flag:64 /\ 0 < flag:64
         /\ (!(0 <= K:185) \/ mid___cost:186 = (__cost:66 + K:185))
         /\ (!((0 <= K:185 /\ K:185 <= 0)) \/ mid_flag:187 = 0)
         /\ (!(1 <= K:185) \/ mid_flag:187 = 1)
         /\ (!(0 <= K:185) \/ mid_n:188 = (n:65 + -K:185))
         /\ (!(0 <= K:185) \/ mid_flag:187 <= K:185)
         /\ (!(0 <= K:185) \/ -mid_flag:187 <= 0)
         /\ ((K:185 = 0 /\ n:65 = mid_n:188 /\ 0 = mid_flag:187
                /\ __cost:66 = mid___cost:186)
               \/ (1 <= K:185 /\ 0 <= __cost:66 /\ 0 <= (-1 + n:65)
                     /\ (-1 + mid_flag:187) = 0 /\ 0 <= mid_n:188
                     /\ 0 <= (-1 + mid___cost:186))) /\ K:189 = 0
         /\ mid_n:188 = n':190 /\ mid_flag:187 = flag':191
         /\ mid___cost:186 = __cost':192 /\ 0 = K:189
         /\ (K:185 + K:189) = K:193 /\ 0 <= K:193 /\ flag':191 <= 1
         /\ 0 <= flag':191 /\ n':190 <= 0)}
**** alpha hat: 
  {<Split [(1 + -n:65) <= 0
            (n':160) = 0
           (__cost':158) = (1)*(n:65) + (1)*(__cost:66) + 0
           (flag':159) = 1
           (n':160) <= (1)*(n:65) + (-1)*1
           }
          pre:
            [|flag:64-1=0; n:65-1>=0; __cost:66>=0|]
          post:
            [|flag':159-1=0; n':160=0; __cost':158-1>=0|]
           (flag':159) = 0
          (n':160) = (1)*(n:65) + 0
          (__cost':158) = (1)*(__cost:66) + 0
          }
  pre:
    [|flag:64-1=0; -n:65>=0|]
  post:
    [|flag':159=0; -n':160>=0|]],
[!(-__cost:66 <= 0)
  (n':160) = (1)*(n:65) + 0
 (flag':159) = 0
 (__cost':158) = (1)*(__cost:66) + 0
 } pre:   [|flag:64-1=0; -__cost:66-1>=0; -n:65>=0|] post:
  [|flag':159=0; -n':160>=0; -__cost':158-1>=0|]
 ((__cost':158 + n':160)) = (1)*((__cost:66 + n:65)) + 0
((flag':159 + n':160)) <= (1)*((flag:64 + n:65)) + (-1)*1
(flag':159) <= (1)*(flag:64) + 0 (-flag':159) <= (1)*(-flag:64) + 1 } pre:
  [|flag:64-1=0; __cost:66>=0|] post:
  [|-flag':159+1>=0; -flag':159+__cost':158>=0; -n':160>=0; flag':159>=0|]]>}
**** star transition: 
  {__cost := __cost':158
   flag := flag':159
   n := n':160
   when ((!((0 <= K:217 /\ K:217 <= 0)) \/ mid_n:219 = n:65)
           /\ (!(1 <= K:217) \/ mid_n:219 = 0)
           /\ (!((0 <= K:217 /\ K:217 <= 0)) \/ mid___cost:221 = __cost:66)
           /\ (!(1 <= K:217) \/ mid___cost:221 = (n:65 + __cost:66))
           /\ (!((0 <= K:217 /\ K:217 <= 0)) \/ mid_flag:220 = flag:64)
           /\ (!(1 <= K:217) \/ mid_flag:220 = 1)
           /\ (!(0 <= K:217) \/ mid_n:219 <= (n:65 + -K:217))
           /\ ((K:217 = 0 /\ n:65 = mid_n:219 /\ flag:64 = mid_flag:220
                  /\ __cost:66 = mid___cost:221)
                 \/ (1 <= K:217 /\ (-1 + flag:64) = 0 /\ 0 <= (-1 + n:65)
                       /\ 0 <= __cost:66 /\ (-1 + mid_flag:220) = 0
                       /\ mid_n:219 = 0 /\ 0 <= (-1 + mid___cost:221)))
           /\ (0 = K:217 \/ (1 + -n:65) <= 0)
           /\ (!((0 <= K:218 /\ K:218 <= 0)) \/ flag':159 = mid_flag:220)
           /\ (!(1 <= K:218) \/ flag':159 = 0)
           /\ (!(0 <= K:218) \/ n':160 = mid_n:219)
           /\ (!(0 <= K:218) \/ __cost':158 = mid___cost:221)
           /\ ((K:218 = 0 /\ mid_n:219 = n':160 /\ mid_flag:220 = flag':159
                  /\ mid___cost:221 = __cost':158)
                 \/ (1 <= K:218 /\ (-1 + mid_flag:220) = 0 /\ 0 <= -mid_n:219
                       /\ flag':159 = 0 /\ 0 <= -n':160))
           /\ (0 = K:218 \/ !((1 + -mid_n:219) <= 0))
           /\ (K:217 + K:218) = K:216 /\ (!(0 <= K:222) \/ mid_n:224 = n:65)
           /\ (!((0 <= K:222 /\ K:222 <= 0)) \/ mid_flag:225 = flag:64)
           /\ (!(1 <= K:222) \/ mid_flag:225 = 0)
           /\ (!(0 <= K:222) \/ mid___cost:226 = __cost:66)
           /\ ((K:222 = 0 /\ n:65 = mid_n:224 /\ flag:64 = mid_flag:225
                  /\ __cost:66 = mid___cost:226)
                 \/ (1 <= K:222 /\ (-1 + flag:64) = 0
                       /\ 0 <= (-1 + -__cost:66) /\ 0 <= -n:65
                       /\ mid_flag:225 = 0 /\ 0 <= -mid_n:224
                       /\ 0 <= (-1 + -mid___cost:226)))
           /\ (0 = K:222 \/ !(-__cost:66 <= 0))
           /\ (!(0 <= K:223)
                 \/ (__cost':158 + n':160) = (mid___cost:226 + mid_n:224))
           /\ (!(0 <= K:223)
                 \/ (flag':159 + n':160) <= ((mid_flag:225 + mid_n:224)
                                               + -K:223))
           /\ (!(0 <= K:223) \/ flag':159 <= mid_flag:225)
           /\ (!(0 <= K:223) \/ -flag':159 <= (-mid_flag:225 + K:223))
           /\ ((K:223 = 0 /\ mid_n:224 = n':160 /\ mid_flag:225 = flag':159
                  /\ mid___cost:226 = __cost':158)
                 \/ (1 <= K:223 /\ (-1 + mid_flag:225) = 0
                       /\ 0 <= mid___cost:226 /\ 0 <= (1 + -flag':159)
                       /\ 0 <= (-flag':159 + __cost':158) /\ 0 <= -n':160
                       /\ 0 <= flag':159))
           /\ (0 = K:223 \/ -mid___cost:226 <= 0) /\ (K:222 + K:223) = K:216
           /\ 0 <= K:216)}
}
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:13
       param0 := havoc:13
       param0@pos := type_err:17
       param0@width := type_err:18}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:19
     return@width := type_err:20
     when ((0 < n:2 /\ n:2 = phi_tmp___0:14)
             \/ (n:2 <= 0 /\ 0 = phi_tmp___0:14))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:53
       param0@pos := type_err:56
       param0@width := type_err:57}    )
    ,
    Var(20)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:54
     return@width := type_err:55}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=20: 
Weight(Base relation: 
  {__cost := __cost':234
   flag := flag':232
   n := n':233
   return := havoc:259
   return@pos := type_err:260
   return@width := type_err:261
   when ((!((0 <= K:227 /\ K:227 <= 0)) \/ mid_n:228 = param0:53)
           /\ (!(1 <= K:227) \/ mid_n:228 = 0)
           /\ (!((0 <= K:227 /\ K:227 <= 0)) \/ mid___cost:229 = __cost:66)
           /\ (!(1 <= K:227) \/ mid___cost:229 = (param0:53 + __cost:66))
           /\ (!((0 <= K:227 /\ K:227 <= 0)) \/ mid_flag:230 = 1)
           /\ (!(1 <= K:227) \/ mid_flag:230 = 1)
           /\ (!(0 <= K:227) \/ mid_n:228 <= (param0:53 + -K:227))
           /\ ((K:227 = 0 /\ param0:53 = mid_n:228 /\ 1 = mid_flag:230
                  /\ __cost:66 = mid___cost:229)
                 \/ (1 <= K:227 /\ (-1 + 1) = 0 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= __cost:66 /\ (-1 + mid_flag:230) = 0
                       /\ mid_n:228 = 0 /\ 0 <= (-1 + mid___cost:229)))
           /\ (0 = K:227 \/ (1 + -param0:53) <= 0)
           /\ (!((0 <= K:231 /\ K:231 <= 0)) \/ flag':232 = mid_flag:230)
           /\ (!(1 <= K:231) \/ flag':232 = 0)
           /\ (!(0 <= K:231) \/ n':233 = mid_n:228)
           /\ (!(0 <= K:231) \/ __cost':234 = mid___cost:229)
           /\ ((K:231 = 0 /\ mid_n:228 = n':233 /\ mid_flag:230 = flag':232
                  /\ mid___cost:229 = __cost':234)
                 \/ (1 <= K:231 /\ (-1 + mid_flag:230) = 0 /\ 0 <= -mid_n:228
                       /\ flag':232 = 0 /\ 0 <= -n':233))
           /\ (0 = K:231 \/ !((1 + -mid_n:228) <= 0))
           /\ (K:227 + K:231) = K:235
           /\ (!(0 <= K:236) \/ mid_n:237 = param0:53)
           /\ (!((0 <= K:236 /\ K:236 <= 0)) \/ mid_flag:238 = 1)
           /\ (!(1 <= K:236) \/ mid_flag:238 = 0)
           /\ (!(0 <= K:236) \/ mid___cost:239 = __cost:66)
           /\ ((K:236 = 0 /\ param0:53 = mid_n:237 /\ 1 = mid_flag:238
                  /\ __cost:66 = mid___cost:239)
                 \/ (1 <= K:236 /\ (-1 + 1) = 0 /\ 0 <= (-1 + -__cost:66)
                       /\ 0 <= -param0:53 /\ mid_flag:238 = 0
                       /\ 0 <= -mid_n:237 /\ 0 <= (-1 + -mid___cost:239)))
           /\ (0 = K:236 \/ !(-__cost:66 <= 0))
           /\ (!(0 <= K:240)
                 \/ (__cost':234 + n':233) = (mid___cost:239 + mid_n:237))
           /\ (!(0 <= K:240)
                 \/ (flag':232 + n':233) <= ((mid_flag:238 + mid_n:237)
                                               + -K:240))
           /\ (!(0 <= K:240) \/ flag':232 <= mid_flag:238)
           /\ (!(0 <= K:240) \/ -flag':232 <= (-mid_flag:238 + K:240))
           /\ ((K:240 = 0 /\ mid_n:237 = n':233 /\ mid_flag:238 = flag':232
                  /\ mid___cost:239 = __cost':234)
                 \/ (1 <= K:240 /\ (-1 + mid_flag:238) = 0
                       /\ 0 <= mid___cost:239 /\ 0 <= (1 + -flag':232)
                       /\ 0 <= (-flag':232 + __cost':234) /\ 0 <= -n':233
                       /\ 0 <= flag':232))
           /\ (0 = K:240 \/ -mid___cost:239 <= 0) /\ (K:236 + K:240) = K:235
           /\ 0 <= K:235 /\ flag':232 <= 1 /\ 0 <= flag':232
           /\ flag':232 <= 0)})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := 0
         n := havoc:13
         param0 := havoc:13
         param0@pos := type_err:17
         param0@width := type_err:18}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:19
       return@width := type_err:20
       when ((0 < n:2 /\ n:2 = phi_tmp___0:14)
               \/ (n:2 <= 0 /\ 0 = phi_tmp___0:14))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:53
         param0@pos := type_err:56
         param0@width := type_err:57}      )
      ,
      Var(20)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:54
       return@width := type_err:55}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':234
   return := havoc:259
   return@pos := type_err:260
   return@width := type_err:261
   when ((!((0 <= K:227 /\ K:227 <= 0)) \/ mid_n:228 = param0:53)
           /\ (!(1 <= K:227) \/ mid_n:228 = 0)
           /\ (!((0 <= K:227 /\ K:227 <= 0)) \/ mid___cost:229 = __cost:66)
           /\ (!(1 <= K:227) \/ mid___cost:229 = (param0:53 + __cost:66))
           /\ (!((0 <= K:227 /\ K:227 <= 0)) \/ mid_flag:230 = 1)
           /\ (!(1 <= K:227) \/ mid_flag:230 = 1)
           /\ (!(0 <= K:227) \/ mid_n:228 <= (param0:53 + -K:227))
           /\ ((K:227 = 0 /\ param0:53 = mid_n:228 /\ 1 = mid_flag:230
                  /\ __cost:66 = mid___cost:229)
                 \/ (1 <= K:227 /\ (-1 + 1) = 0 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= __cost:66 /\ (-1 + mid_flag:230) = 0
                       /\ mid_n:228 = 0 /\ 0 <= (-1 + mid___cost:229)))
           /\ (0 = K:227 \/ (1 + -param0:53) <= 0)
           /\ (!((0 <= K:231 /\ K:231 <= 0)) \/ flag':232 = mid_flag:230)
           /\ (!(1 <= K:231) \/ flag':232 = 0)
           /\ (!(0 <= K:231) \/ n':233 = mid_n:228)
           /\ (!(0 <= K:231) \/ __cost':234 = mid___cost:229)
           /\ ((K:231 = 0 /\ mid_n:228 = n':233 /\ mid_flag:230 = flag':232
                  /\ mid___cost:229 = __cost':234)
                 \/ (1 <= K:231 /\ (-1 + mid_flag:230) = 0 /\ 0 <= -mid_n:228
                       /\ flag':232 = 0 /\ 0 <= -n':233))
           /\ (0 = K:231 \/ !((1 + -mid_n:228) <= 0))
           /\ (K:227 + K:231) = K:235
           /\ (!(0 <= K:236) \/ mid_n:237 = param0:53)
           /\ (!((0 <= K:236 /\ K:236 <= 0)) \/ mid_flag:238 = 1)
           /\ (!(1 <= K:236) \/ mid_flag:238 = 0)
           /\ (!(0 <= K:236) \/ mid___cost:239 = __cost:66)
           /\ ((K:236 = 0 /\ param0:53 = mid_n:237 /\ 1 = mid_flag:238
                  /\ __cost:66 = mid___cost:239)
                 \/ (1 <= K:236 /\ (-1 + 1) = 0 /\ 0 <= (-1 + -__cost:66)
                       /\ 0 <= -param0:53 /\ mid_flag:238 = 0
                       /\ 0 <= -mid_n:237 /\ 0 <= (-1 + -mid___cost:239)))
           /\ (0 = K:236 \/ !(-__cost:66 <= 0))
           /\ (!(0 <= K:240)
                 \/ (__cost':234 + n':233) = (mid___cost:239 + mid_n:237))
           /\ (!(0 <= K:240)
                 \/ (flag':232 + n':233) <= ((mid_flag:238 + mid_n:237)
                                               + -K:240))
           /\ (!(0 <= K:240) \/ flag':232 <= mid_flag:238)
           /\ (!(0 <= K:240) \/ -flag':232 <= (-mid_flag:238 + K:240))
           /\ ((K:240 = 0 /\ mid_n:237 = n':233 /\ mid_flag:238 = flag':232
                  /\ mid___cost:239 = __cost':234)
                 \/ (1 <= K:240 /\ (-1 + mid_flag:238) = 0
                       /\ 0 <= mid___cost:239 /\ 0 <= (1 + -flag':232)
                       /\ 0 <= (-flag':232 + __cost':234) /\ 0 <= -n':233
                       /\ 0 <= flag':232))
           /\ (0 = K:240 \/ -mid___cost:239 <= 0) /\ (K:236 + K:240) = K:235
           /\ 0 <= K:235 /\ flag':232 <= 1 /\ 0 <= flag':232
           /\ flag':232 <= 0)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':288
   return := 0
   param0 := havoc:13
   return@pos := type_err:300
   param0@pos := type_err:296
   return@width := type_err:301
   param0@width := type_err:298
   when ((!((0 <= K:281 /\ K:281 <= 0)) \/ mid_n:282 = havoc:13)
           /\ (!(1 <= K:281) \/ mid_n:282 = 0)
           /\ (!((0 <= K:281 /\ K:281 <= 0)) \/ mid___cost:283 = 0)
           /\ (!(1 <= K:281) \/ mid___cost:283 = havoc:13)
           /\ (!((0 <= K:281 /\ K:281 <= 0)) \/ mid_flag:284 = 1)
           /\ (!(1 <= K:281) \/ mid_flag:284 = 1)
           /\ (!(0 <= K:281) \/ mid_n:282 <= (havoc:13 + -K:281))
           /\ ((K:281 = 0 /\ havoc:13 = mid_n:282 /\ 1 = mid_flag:284
                  /\ 0 = mid___cost:283)
                 \/ (1 <= K:281 /\ (-1 + 1) = 0 /\ 0 <= (-1 + havoc:13)
                       /\ (-1 + mid_flag:284) = 0 /\ mid_n:282 = 0
                       /\ 0 <= (-1 + mid___cost:283)))
           /\ (0 = K:281 \/ (1 + -havoc:13) <= 0)
           /\ (!((0 <= K:285 /\ K:285 <= 0)) \/ flag':286 = mid_flag:284)
           /\ (!(1 <= K:285) \/ flag':286 = 0)
           /\ (!(0 <= K:285) \/ n':287 = mid_n:282)
           /\ (!(0 <= K:285) \/ __cost':288 = mid___cost:283)
           /\ ((K:285 = 0 /\ mid_n:282 = n':287 /\ mid_flag:284 = flag':286
                  /\ mid___cost:283 = __cost':288)
                 \/ (1 <= K:285 /\ (-1 + mid_flag:284) = 0 /\ 0 <= -mid_n:282
                       /\ flag':286 = 0 /\ 0 <= -n':287))
           /\ (0 = K:285 \/ !((1 + -mid_n:282) <= 0))
           /\ (K:281 + K:285) = K:289
           /\ (!(0 <= K:290) \/ mid_n:291 = havoc:13)
           /\ (!((0 <= K:290 /\ K:290 <= 0)) \/ mid_flag:292 = 1)
           /\ (!(1 <= K:290) \/ mid_flag:292 = 0)
           /\ (!(0 <= K:290) \/ mid___cost:293 = 0) /\ K:290 = 0
           /\ havoc:13 = mid_n:291 /\ 1 = mid_flag:292 /\ 0 = mid___cost:293
           /\ 0 = K:290
           /\ (!(0 <= K:294)
                 \/ (__cost':288 + n':287) = (mid___cost:293 + mid_n:291))
           /\ (!(0 <= K:294)
                 \/ (flag':286 + n':287) <= ((mid_flag:292 + mid_n:291)
                                               + -K:294))
           /\ (!(0 <= K:294) \/ flag':286 <= mid_flag:292)
           /\ (!(0 <= K:294) \/ -flag':286 <= (-mid_flag:292 + K:294))
           /\ ((K:294 = 0 /\ mid_n:291 = n':287 /\ mid_flag:292 = flag':286
                  /\ mid___cost:293 = __cost':288)
                 \/ (1 <= K:294 /\ (-1 + mid_flag:292) = 0
                       /\ 0 <= mid___cost:293 /\ 0 <= (1 + -flag':286)
                       /\ 0 <= (-flag':286 + __cost':288) /\ 0 <= -n':287
                       /\ 0 <= flag':286))
           /\ (0 = K:294 \/ -mid___cost:293 <= 0) /\ (K:290 + K:294) = K:289
           /\ 0 <= K:289 /\ flag':286 <= 1 /\ 0 <= flag':286
           /\ flag':286 <= 0
           /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:299)
                 \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:299)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':309
   return := 0
   param0 := param0:53
   return@pos := type_err:319
   param0@pos := type_err:56
   return@width := type_err:320
   param0@width := type_err:57
   when ((!((0 <= K:302 /\ K:302 <= 0)) \/ mid_n:303 = param0:53)
           /\ (!(1 <= K:302) \/ mid_n:303 = 0)
           /\ (!((0 <= K:302 /\ K:302 <= 0)) \/ mid___cost:304 = __cost:66)
           /\ (!(1 <= K:302) \/ mid___cost:304 = (param0:53 + __cost:66))
           /\ (!((0 <= K:302 /\ K:302 <= 0)) \/ mid_flag:305 = 1)
           /\ (!(1 <= K:302) \/ mid_flag:305 = 1)
           /\ (!(0 <= K:302) \/ mid_n:303 <= (param0:53 + -K:302))
           /\ ((K:302 = 0 /\ param0:53 = mid_n:303 /\ 1 = mid_flag:305
                  /\ __cost:66 = mid___cost:304)
                 \/ (1 <= K:302 /\ (-1 + 1) = 0 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= __cost:66 /\ (-1 + mid_flag:305) = 0
                       /\ mid_n:303 = 0 /\ 0 <= (-1 + mid___cost:304)))
           /\ (0 = K:302 \/ (1 + -param0:53) <= 0)
           /\ (!((0 <= K:306 /\ K:306 <= 0)) \/ flag':307 = mid_flag:305)
           /\ (!(1 <= K:306) \/ flag':307 = 0)
           /\ (!(0 <= K:306) \/ n':308 = mid_n:303)
           /\ (!(0 <= K:306) \/ __cost':309 = mid___cost:304)
           /\ ((K:306 = 0 /\ mid_n:303 = n':308 /\ mid_flag:305 = flag':307
                  /\ mid___cost:304 = __cost':309)
                 \/ (1 <= K:306 /\ (-1 + mid_flag:305) = 0 /\ 0 <= -mid_n:303
                       /\ flag':307 = 0 /\ 0 <= -n':308))
           /\ (0 = K:306 \/ !((1 + -mid_n:303) <= 0))
           /\ (K:302 + K:306) = K:310
           /\ (!(0 <= K:311) \/ mid_n:312 = param0:53)
           /\ (!((0 <= K:311 /\ K:311 <= 0)) \/ mid_flag:313 = 1)
           /\ (!(1 <= K:311) \/ mid_flag:313 = 0)
           /\ (!(0 <= K:311) \/ mid___cost:314 = __cost:66)
           /\ ((K:311 = 0 /\ param0:53 = mid_n:312 /\ 1 = mid_flag:313
                  /\ __cost:66 = mid___cost:314)
                 \/ (1 <= K:311 /\ (-1 + 1) = 0 /\ 0 <= (-1 + -__cost:66)
                       /\ 0 <= -param0:53 /\ mid_flag:313 = 0
                       /\ 0 <= -mid_n:312 /\ 0 <= (-1 + -mid___cost:314)))
           /\ (0 = K:311 \/ !(-__cost:66 <= 0))
           /\ (!(0 <= K:315)
                 \/ (__cost':309 + n':308) = (mid___cost:314 + mid_n:312))
           /\ (!(0 <= K:315)
                 \/ (flag':307 + n':308) <= ((mid_flag:313 + mid_n:312)
                                               + -K:315))
           /\ (!(0 <= K:315) \/ flag':307 <= mid_flag:313)
           /\ (!(0 <= K:315) \/ -flag':307 <= (-mid_flag:313 + K:315))
           /\ ((K:315 = 0 /\ mid_n:312 = n':308 /\ mid_flag:313 = flag':307
                  /\ mid___cost:314 = __cost':309)
                 \/ (1 <= K:315 /\ (-1 + mid_flag:313) = 0
                       /\ 0 <= mid___cost:314 /\ 0 <= (1 + -flag':307)
                       /\ 0 <= (-flag':307 + __cost':309) /\ 0 <= -n':308
                       /\ 0 <= flag':307))
           /\ (0 = K:315 \/ -mid___cost:314 <= 0) /\ (K:311 + K:315) = K:310
           /\ 0 <= K:310 /\ flag':307 <= 1 /\ 0 <= flag':307
           /\ flag':307 <= 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=20: 
Weight(Base relation: 
  {__cost := __cost':234
   return := havoc:259
   return@pos := type_err:260
   return@width := type_err:261
   when ((!((0 <= K:227 /\ K:227 <= 0)) \/ mid_n:228 = param0:53)
           /\ (!(1 <= K:227) \/ mid_n:228 = 0)
           /\ (!((0 <= K:227 /\ K:227 <= 0)) \/ mid___cost:229 = __cost:66)
           /\ (!(1 <= K:227) \/ mid___cost:229 = (param0:53 + __cost:66))
           /\ (!((0 <= K:227 /\ K:227 <= 0)) \/ mid_flag:230 = 1)
           /\ (!(1 <= K:227) \/ mid_flag:230 = 1)
           /\ (!(0 <= K:227) \/ mid_n:228 <= (param0:53 + -K:227))
           /\ ((K:227 = 0 /\ param0:53 = mid_n:228 /\ 1 = mid_flag:230
                  /\ __cost:66 = mid___cost:229)
                 \/ (1 <= K:227 /\ (-1 + 1) = 0 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= __cost:66 /\ (-1 + mid_flag:230) = 0
                       /\ mid_n:228 = 0 /\ 0 <= (-1 + mid___cost:229)))
           /\ (0 = K:227 \/ (1 + -param0:53) <= 0)
           /\ (!((0 <= K:231 /\ K:231 <= 0)) \/ flag':232 = mid_flag:230)
           /\ (!(1 <= K:231) \/ flag':232 = 0)
           /\ (!(0 <= K:231) \/ n':233 = mid_n:228)
           /\ (!(0 <= K:231) \/ __cost':234 = mid___cost:229)
           /\ ((K:231 = 0 /\ mid_n:228 = n':233 /\ mid_flag:230 = flag':232
                  /\ mid___cost:229 = __cost':234)
                 \/ (1 <= K:231 /\ (-1 + mid_flag:230) = 0 /\ 0 <= -mid_n:228
                       /\ flag':232 = 0 /\ 0 <= -n':233))
           /\ (0 = K:231 \/ !((1 + -mid_n:228) <= 0))
           /\ (K:227 + K:231) = K:235
           /\ (!(0 <= K:236) \/ mid_n:237 = param0:53)
           /\ (!((0 <= K:236 /\ K:236 <= 0)) \/ mid_flag:238 = 1)
           /\ (!(1 <= K:236) \/ mid_flag:238 = 0)
           /\ (!(0 <= K:236) \/ mid___cost:239 = __cost:66)
           /\ ((K:236 = 0 /\ param0:53 = mid_n:237 /\ 1 = mid_flag:238
                  /\ __cost:66 = mid___cost:239)
                 \/ (1 <= K:236 /\ (-1 + 1) = 0 /\ 0 <= (-1 + -__cost:66)
                       /\ 0 <= -param0:53 /\ mid_flag:238 = 0
                       /\ 0 <= -mid_n:237 /\ 0 <= (-1 + -mid___cost:239)))
           /\ (0 = K:236 \/ !(-__cost:66 <= 0))
           /\ (!(0 <= K:240)
                 \/ (__cost':234 + n':233) = (mid___cost:239 + mid_n:237))
           /\ (!(0 <= K:240)
                 \/ (flag':232 + n':233) <= ((mid_flag:238 + mid_n:237)
                                               + -K:240))
           /\ (!(0 <= K:240) \/ flag':232 <= mid_flag:238)
           /\ (!(0 <= K:240) \/ -flag':232 <= (-mid_flag:238 + K:240))
           /\ ((K:240 = 0 /\ mid_n:237 = n':233 /\ mid_flag:238 = flag':232
                  /\ mid___cost:239 = __cost':234)
                 \/ (1 <= K:240 /\ (-1 + mid_flag:238) = 0
                       /\ 0 <= mid___cost:239 /\ 0 <= (1 + -flag':232)
                       /\ 0 <= (-flag':232 + __cost':234) /\ 0 <= -n':233
                       /\ 0 <= flag':232))
           /\ (0 = K:240 \/ -mid___cost:239 <= 0) /\ (K:236 + K:240) = K:235
           /\ 0 <= K:235 /\ flag':232 <= 1 /\ 0 <= flag':232
           /\ flag':232 <= 0)})


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':288
 return := 0
 param0 := havoc:13
 return@pos := type_err:300
 param0@pos := type_err:296
 return@width := type_err:301
 param0@width := type_err:298
 when ((!((0 <= K:281 /\ K:281 <= 0)) \/ mid_n:282 = havoc:13)
         /\ (!(1 <= K:281) \/ mid_n:282 = 0)
         /\ (!((0 <= K:281 /\ K:281 <= 0)) \/ mid___cost:283 = 0)
         /\ (!(1 <= K:281) \/ mid___cost:283 = havoc:13)
         /\ (!((0 <= K:281 /\ K:281 <= 0)) \/ mid_flag:284 = 1)
         /\ (!(1 <= K:281) \/ mid_flag:284 = 1)
         /\ (!(0 <= K:281) \/ mid_n:282 <= (havoc:13 + -K:281))
         /\ ((K:281 = 0 /\ havoc:13 = mid_n:282 /\ 1 = mid_flag:284
                /\ 0 = mid___cost:283)
               \/ (1 <= K:281 /\ (-1 + 1) = 0 /\ 0 <= (-1 + havoc:13)
                     /\ (-1 + mid_flag:284) = 0 /\ mid_n:282 = 0
                     /\ 0 <= (-1 + mid___cost:283)))
         /\ (0 = K:281 \/ (1 + -havoc:13) <= 0)
         /\ (!((0 <= K:285 /\ K:285 <= 0)) \/ flag':286 = mid_flag:284)
         /\ (!(1 <= K:285) \/ flag':286 = 0)
         /\ (!(0 <= K:285) \/ n':287 = mid_n:282)
         /\ (!(0 <= K:285) \/ __cost':288 = mid___cost:283)
         /\ ((K:285 = 0 /\ mid_n:282 = n':287 /\ mid_flag:284 = flag':286
                /\ mid___cost:283 = __cost':288)
               \/ (1 <= K:285 /\ (-1 + mid_flag:284) = 0 /\ 0 <= -mid_n:282
                     /\ flag':286 = 0 /\ 0 <= -n':287))
         /\ (0 = K:285 \/ !((1 + -mid_n:282) <= 0))
         /\ (K:281 + K:285) = K:289
         /\ (!(0 <= K:290) \/ mid_n:291 = havoc:13)
         /\ (!((0 <= K:290 /\ K:290 <= 0)) \/ mid_flag:292 = 1)
         /\ (!(1 <= K:290) \/ mid_flag:292 = 0)
         /\ (!(0 <= K:290) \/ mid___cost:293 = 0) /\ K:290 = 0
         /\ havoc:13 = mid_n:291 /\ 1 = mid_flag:292 /\ 0 = mid___cost:293
         /\ 0 = K:290
         /\ (!(0 <= K:294)
               \/ (__cost':288 + n':287) = (mid___cost:293 + mid_n:291))
         /\ (!(0 <= K:294)
               \/ (flag':286 + n':287) <= ((mid_flag:292 + mid_n:291)
                                             + -K:294))
         /\ (!(0 <= K:294) \/ flag':286 <= mid_flag:292)
         /\ (!(0 <= K:294) \/ -flag':286 <= (-mid_flag:292 + K:294))
         /\ ((K:294 = 0 /\ mid_n:291 = n':287 /\ mid_flag:292 = flag':286
                /\ mid___cost:293 = __cost':288)
               \/ (1 <= K:294 /\ (-1 + mid_flag:292) = 0
                     /\ 0 <= mid___cost:293 /\ 0 <= (1 + -flag':286)
                     /\ 0 <= (-flag':286 + __cost':288) /\ 0 <= -n':287
                     /\ 0 <= flag':286))
         /\ (0 = K:294 \/ -mid___cost:293 <= 0) /\ (K:290 + K:294) = K:289
         /\ 0 <= K:289 /\ flag':286 <= 1 /\ 0 <= flag':286 /\ flag':286 <= 0
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:299)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:299)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':309
 return := 0
 param0 := param0:53
 return@pos := type_err:319
 param0@pos := type_err:56
 return@width := type_err:320
 param0@width := type_err:57
 when ((!((0 <= K:302 /\ K:302 <= 0)) \/ mid_n:303 = param0:53)
         /\ (!(1 <= K:302) \/ mid_n:303 = 0)
         /\ (!((0 <= K:302 /\ K:302 <= 0)) \/ mid___cost:304 = __cost:66)
         /\ (!(1 <= K:302) \/ mid___cost:304 = (param0:53 + __cost:66))
         /\ (!((0 <= K:302 /\ K:302 <= 0)) \/ mid_flag:305 = 1)
         /\ (!(1 <= K:302) \/ mid_flag:305 = 1)
         /\ (!(0 <= K:302) \/ mid_n:303 <= (param0:53 + -K:302))
         /\ ((K:302 = 0 /\ param0:53 = mid_n:303 /\ 1 = mid_flag:305
                /\ __cost:66 = mid___cost:304)
               \/ (1 <= K:302 /\ (-1 + 1) = 0 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= __cost:66 /\ (-1 + mid_flag:305) = 0
                     /\ mid_n:303 = 0 /\ 0 <= (-1 + mid___cost:304)))
         /\ (0 = K:302 \/ (1 + -param0:53) <= 0)
         /\ (!((0 <= K:306 /\ K:306 <= 0)) \/ flag':307 = mid_flag:305)
         /\ (!(1 <= K:306) \/ flag':307 = 0)
         /\ (!(0 <= K:306) \/ n':308 = mid_n:303)
         /\ (!(0 <= K:306) \/ __cost':309 = mid___cost:304)
         /\ ((K:306 = 0 /\ mid_n:303 = n':308 /\ mid_flag:305 = flag':307
                /\ mid___cost:304 = __cost':309)
               \/ (1 <= K:306 /\ (-1 + mid_flag:305) = 0 /\ 0 <= -mid_n:303
                     /\ flag':307 = 0 /\ 0 <= -n':308))
         /\ (0 = K:306 \/ !((1 + -mid_n:303) <= 0))
         /\ (K:302 + K:306) = K:310
         /\ (!(0 <= K:311) \/ mid_n:312 = param0:53)
         /\ (!((0 <= K:311 /\ K:311 <= 0)) \/ mid_flag:313 = 1)
         /\ (!(1 <= K:311) \/ mid_flag:313 = 0)
         /\ (!(0 <= K:311) \/ mid___cost:314 = __cost:66)
         /\ ((K:311 = 0 /\ param0:53 = mid_n:312 /\ 1 = mid_flag:313
                /\ __cost:66 = mid___cost:314)
               \/ (1 <= K:311 /\ (-1 + 1) = 0 /\ 0 <= (-1 + -__cost:66)
                     /\ 0 <= -param0:53 /\ mid_flag:313 = 0
                     /\ 0 <= -mid_n:312 /\ 0 <= (-1 + -mid___cost:314)))
         /\ (0 = K:311 \/ !(-__cost:66 <= 0))
         /\ (!(0 <= K:315)
               \/ (__cost':309 + n':308) = (mid___cost:314 + mid_n:312))
         /\ (!(0 <= K:315)
               \/ (flag':307 + n':308) <= ((mid_flag:313 + mid_n:312)
                                             + -K:315))
         /\ (!(0 <= K:315) \/ flag':307 <= mid_flag:313)
         /\ (!(0 <= K:315) \/ -flag':307 <= (-mid_flag:313 + K:315))
         /\ ((K:315 = 0 /\ mid_n:312 = n':308 /\ mid_flag:313 = flag':307
                /\ mid___cost:314 = __cost':309)
               \/ (1 <= K:315 /\ (-1 + mid_flag:313) = 0
                     /\ 0 <= mid___cost:314 /\ 0 <= (1 + -flag':307)
                     /\ 0 <= (-flag':307 + __cost':309) /\ 0 <= -n':308
                     /\ 0 <= flag':307))
         /\ (0 = K:315 \/ -mid___cost:314 <= 0) /\ (K:311 + K:315) = K:310
         /\ 0 <= K:310 /\ flag':307 <= 1 /\ 0 <= flag':307 /\ flag':307 <= 0)}

Evaluating variable number 20 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':234
 return := havoc:259
 return@pos := type_err:260
 return@width := type_err:261
 when ((!((0 <= K:227 /\ K:227 <= 0)) \/ mid_n:228 = param0:53)
         /\ (!(1 <= K:227) \/ mid_n:228 = 0)
         /\ (!((0 <= K:227 /\ K:227 <= 0)) \/ mid___cost:229 = __cost:66)
         /\ (!(1 <= K:227) \/ mid___cost:229 = (param0:53 + __cost:66))
         /\ (!((0 <= K:227 /\ K:227 <= 0)) \/ mid_flag:230 = 1)
         /\ (!(1 <= K:227) \/ mid_flag:230 = 1)
         /\ (!(0 <= K:227) \/ mid_n:228 <= (param0:53 + -K:227))
         /\ ((K:227 = 0 /\ param0:53 = mid_n:228 /\ 1 = mid_flag:230
                /\ __cost:66 = mid___cost:229)
               \/ (1 <= K:227 /\ (-1 + 1) = 0 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= __cost:66 /\ (-1 + mid_flag:230) = 0
                     /\ mid_n:228 = 0 /\ 0 <= (-1 + mid___cost:229)))
         /\ (0 = K:227 \/ (1 + -param0:53) <= 0)
         /\ (!((0 <= K:231 /\ K:231 <= 0)) \/ flag':232 = mid_flag:230)
         /\ (!(1 <= K:231) \/ flag':232 = 0)
         /\ (!(0 <= K:231) \/ n':233 = mid_n:228)
         /\ (!(0 <= K:231) \/ __cost':234 = mid___cost:229)
         /\ ((K:231 = 0 /\ mid_n:228 = n':233 /\ mid_flag:230 = flag':232
                /\ mid___cost:229 = __cost':234)
               \/ (1 <= K:231 /\ (-1 + mid_flag:230) = 0 /\ 0 <= -mid_n:228
                     /\ flag':232 = 0 /\ 0 <= -n':233))
         /\ (0 = K:231 \/ !((1 + -mid_n:228) <= 0))
         /\ (K:227 + K:231) = K:235
         /\ (!(0 <= K:236) \/ mid_n:237 = param0:53)
         /\ (!((0 <= K:236 /\ K:236 <= 0)) \/ mid_flag:238 = 1)
         /\ (!(1 <= K:236) \/ mid_flag:238 = 0)
         /\ (!(0 <= K:236) \/ mid___cost:239 = __cost:66)
         /\ ((K:236 = 0 /\ param0:53 = mid_n:237 /\ 1 = mid_flag:238
                /\ __cost:66 = mid___cost:239)
               \/ (1 <= K:236 /\ (-1 + 1) = 0 /\ 0 <= (-1 + -__cost:66)
                     /\ 0 <= -param0:53 /\ mid_flag:238 = 0
                     /\ 0 <= -mid_n:237 /\ 0 <= (-1 + -mid___cost:239)))
         /\ (0 = K:236 \/ !(-__cost:66 <= 0))
         /\ (!(0 <= K:240)
               \/ (__cost':234 + n':233) = (mid___cost:239 + mid_n:237))
         /\ (!(0 <= K:240)
               \/ (flag':232 + n':233) <= ((mid_flag:238 + mid_n:237)
                                             + -K:240))
         /\ (!(0 <= K:240) \/ flag':232 <= mid_flag:238)
         /\ (!(0 <= K:240) \/ -flag':232 <= (-mid_flag:238 + K:240))
         /\ ((K:240 = 0 /\ mid_n:237 = n':233 /\ mid_flag:238 = flag':232
                /\ mid___cost:239 = __cost':234)
               \/ (1 <= K:240 /\ (-1 + mid_flag:238) = 0
                     /\ 0 <= mid___cost:239 /\ 0 <= (1 + -flag':232)
                     /\ 0 <= (-flag':232 + __cost':234) /\ 0 <= -n':233
                     /\ 0 <= flag':232))
         /\ (0 = K:240 \/ -mid___cost:239 <= 0) /\ (K:236 + K:240) = K:235
         /\ 0 <= K:235 /\ flag':232 <= 1 /\ 0 <= flag':232 /\ flag':232 <= 0)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,57)_g1> -> <__pstate, (Unique State Name,53)_g1>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:56
 param0@width := type_err:57}	
<__pstate, accept> -> <__pstate, (Unique State Name,57)_g1>	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x6f4b220: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x6f4c620: 
	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,53)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:361
 param0@width := type_err:362}
    ( __pstate , (Unique State Name,57)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}

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

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

Base relation: 
{__cost := __cost':328
 n := havoc:13
 return := 0
 param0 := havoc:13
 return@pos := type_err:340
 param0@pos := type_err:336
 return@width := type_err:341
 param0@width := type_err:338
 when ((!((0 <= K:321 /\ K:321 <= 0)) \/ mid_n:322 = havoc:13)
         /\ (!(1 <= K:321) \/ mid_n:322 = 0)
         /\ (!((0 <= K:321 /\ K:321 <= 0)) \/ mid___cost:323 = 0)
         /\ (!(1 <= K:321) \/ mid___cost:323 = havoc:13)
         /\ (!((0 <= K:321 /\ K:321 <= 0)) \/ mid_flag:324 = 1)
         /\ (!(1 <= K:321) \/ mid_flag:324 = 1)
         /\ (!(0 <= K:321) \/ mid_n:322 <= (havoc:13 + -K:321))
         /\ ((K:321 = 0 /\ havoc:13 = mid_n:322 /\ 1 = mid_flag:324
                /\ 0 = mid___cost:323)
               \/ (1 <= K:321 /\ (-1 + 1) = 0 /\ 0 <= (-1 + havoc:13)
                     /\ (-1 + mid_flag:324) = 0 /\ mid_n:322 = 0
                     /\ 0 <= (-1 + mid___cost:323)))
         /\ (0 = K:321 \/ (1 + -havoc:13) <= 0)
         /\ (!((0 <= K:325 /\ K:325 <= 0)) \/ flag':326 = mid_flag:324)
         /\ (!(1 <= K:325) \/ flag':326 = 0)
         /\ (!(0 <= K:325) \/ n':327 = mid_n:322)
         /\ (!(0 <= K:325) \/ __cost':328 = mid___cost:323)
         /\ ((K:325 = 0 /\ mid_n:322 = n':327 /\ mid_flag:324 = flag':326
                /\ mid___cost:323 = __cost':328)
               \/ (1 <= K:325 /\ (-1 + mid_flag:324) = 0 /\ 0 <= -mid_n:322
                     /\ flag':326 = 0 /\ 0 <= -n':327))
         /\ (0 = K:325 \/ !((1 + -mid_n:322) <= 0))
         /\ (K:321 + K:325) = K:329
         /\ (!(0 <= K:330) \/ mid_n:331 = havoc:13)
         /\ (!((0 <= K:330 /\ K:330 <= 0)) \/ mid_flag:332 = 1)
         /\ (!(1 <= K:330) \/ mid_flag:332 = 0)
         /\ (!(0 <= K:330) \/ mid___cost:333 = 0) /\ K:330 = 0
         /\ havoc:13 = mid_n:331 /\ 1 = mid_flag:332 /\ 0 = mid___cost:333
         /\ 0 = K:330
         /\ (!(0 <= K:334)
               \/ (__cost':328 + n':327) = (mid___cost:333 + mid_n:331))
         /\ (!(0 <= K:334)
               \/ (flag':326 + n':327) <= ((mid_flag:332 + mid_n:331)
                                             + -K:334))
         /\ (!(0 <= K:334) \/ flag':326 <= mid_flag:332)
         /\ (!(0 <= K:334) \/ -flag':326 <= (-mid_flag:332 + K:334))
         /\ ((K:334 = 0 /\ mid_n:331 = n':327 /\ mid_flag:332 = flag':326
                /\ mid___cost:333 = __cost':328)
               \/ (1 <= K:334 /\ (-1 + mid_flag:332) = 0
                     /\ 0 <= mid___cost:333 /\ 0 <= (1 + -flag':326)
                     /\ 0 <= (-flag':326 + __cost':328) /\ 0 <= -n':327
                     /\ 0 <= flag':326))
         /\ (0 = K:334 \/ -mid___cost:333 <= 0) /\ (K:330 + K:334) = K:329
         /\ 0 <= K:329 /\ flag':326 <= 1 /\ 0 <= flag':326 /\ flag':326 <= 0
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:339)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:339)))}

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

Base relation: 
{__cost := __cost':349
 return := 0
 param0 := param0:53
 return@pos := type_err:359
 param0@pos := type_err:56
 return@width := type_err:360
 param0@width := type_err:57
 when ((!((0 <= K:342 /\ K:342 <= 0)) \/ mid_n:343 = param0:53)
         /\ (!(1 <= K:342) \/ mid_n:343 = 0)
         /\ (!((0 <= K:342 /\ K:342 <= 0)) \/ mid___cost:344 = __cost:66)
         /\ (!(1 <= K:342) \/ mid___cost:344 = (param0:53 + __cost:66))
         /\ (!((0 <= K:342 /\ K:342 <= 0)) \/ mid_flag:345 = 1)
         /\ (!(1 <= K:342) \/ mid_flag:345 = 1)
         /\ (!(0 <= K:342) \/ mid_n:343 <= (param0:53 + -K:342))
         /\ ((K:342 = 0 /\ param0:53 = mid_n:343 /\ 1 = mid_flag:345
                /\ __cost:66 = mid___cost:344)
               \/ (1 <= K:342 /\ (-1 + 1) = 0 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= __cost:66 /\ (-1 + mid_flag:345) = 0
                     /\ mid_n:343 = 0 /\ 0 <= (-1 + mid___cost:344)))
         /\ (0 = K:342 \/ (1 + -param0:53) <= 0)
         /\ (!((0 <= K:346 /\ K:346 <= 0)) \/ flag':347 = mid_flag:345)
         /\ (!(1 <= K:346) \/ flag':347 = 0)
         /\ (!(0 <= K:346) \/ n':348 = mid_n:343)
         /\ (!(0 <= K:346) \/ __cost':349 = mid___cost:344)
         /\ ((K:346 = 0 /\ mid_n:343 = n':348 /\ mid_flag:345 = flag':347
                /\ mid___cost:344 = __cost':349)
               \/ (1 <= K:346 /\ (-1 + mid_flag:345) = 0 /\ 0 <= -mid_n:343
                     /\ flag':347 = 0 /\ 0 <= -n':348))
         /\ (0 = K:346 \/ !((1 + -mid_n:343) <= 0))
         /\ (K:342 + K:346) = K:350
         /\ (!(0 <= K:351) \/ mid_n:352 = param0:53)
         /\ (!((0 <= K:351 /\ K:351 <= 0)) \/ mid_flag:353 = 1)
         /\ (!(1 <= K:351) \/ mid_flag:353 = 0)
         /\ (!(0 <= K:351) \/ mid___cost:354 = __cost:66)
         /\ ((K:351 = 0 /\ param0:53 = mid_n:352 /\ 1 = mid_flag:353
                /\ __cost:66 = mid___cost:354)
               \/ (1 <= K:351 /\ (-1 + 1) = 0 /\ 0 <= (-1 + -__cost:66)
                     /\ 0 <= -param0:53 /\ mid_flag:353 = 0
                     /\ 0 <= -mid_n:352 /\ 0 <= (-1 + -mid___cost:354)))
         /\ (0 = K:351 \/ !(-__cost:66 <= 0))
         /\ (!(0 <= K:355)
               \/ (__cost':349 + n':348) = (mid___cost:354 + mid_n:352))
         /\ (!(0 <= K:355)
               \/ (flag':347 + n':348) <= ((mid_flag:353 + mid_n:352)
                                             + -K:355))
         /\ (!(0 <= K:355) \/ flag':347 <= mid_flag:353)
         /\ (!(0 <= K:355) \/ -flag':347 <= (-mid_flag:353 + K:355))
         /\ ((K:355 = 0 /\ mid_n:352 = n':348 /\ mid_flag:353 = flag':347
                /\ mid___cost:354 = __cost':349)
               \/ (1 <= K:355 /\ (-1 + mid_flag:353) = 0
                     /\ 0 <= mid___cost:354 /\ 0 <= (1 + -flag':347)
                     /\ 0 <= (-flag':347 + __cost':349) /\ 0 <= -n':348
                     /\ 0 <= flag':347))
         /\ (0 = K:355 \/ -mid___cost:354 <= 0) /\ (K:351 + K:355) = K:350
         /\ 0 <= K:350 /\ flag':347 <= 1 /\ 0 <= flag':347 /\ flag':347 <= 0)}

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

Base relation: 
{__cost := __cost':234
 flag := flag':232
 n := n':233
 return := havoc:259
 return@pos := type_err:260
 return@width := type_err:261
 when ((!((0 <= K:227 /\ K:227 <= 0)) \/ mid_n:228 = param0:53)
         /\ (!(1 <= K:227) \/ mid_n:228 = 0)
         /\ (!((0 <= K:227 /\ K:227 <= 0)) \/ mid___cost:229 = __cost:66)
         /\ (!(1 <= K:227) \/ mid___cost:229 = (param0:53 + __cost:66))
         /\ (!((0 <= K:227 /\ K:227 <= 0)) \/ mid_flag:230 = 1)
         /\ (!(1 <= K:227) \/ mid_flag:230 = 1)
         /\ (!(0 <= K:227) \/ mid_n:228 <= (param0:53 + -K:227))
         /\ ((K:227 = 0 /\ param0:53 = mid_n:228 /\ 1 = mid_flag:230
                /\ __cost:66 = mid___cost:229)
               \/ (1 <= K:227 /\ (-1 + 1) = 0 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= __cost:66 /\ (-1 + mid_flag:230) = 0
                     /\ mid_n:228 = 0 /\ 0 <= (-1 + mid___cost:229)))
         /\ (0 = K:227 \/ (1 + -param0:53) <= 0)
         /\ (!((0 <= K:231 /\ K:231 <= 0)) \/ flag':232 = mid_flag:230)
         /\ (!(1 <= K:231) \/ flag':232 = 0)
         /\ (!(0 <= K:231) \/ n':233 = mid_n:228)
         /\ (!(0 <= K:231) \/ __cost':234 = mid___cost:229)
         /\ ((K:231 = 0 /\ mid_n:228 = n':233 /\ mid_flag:230 = flag':232
                /\ mid___cost:229 = __cost':234)
               \/ (1 <= K:231 /\ (-1 + mid_flag:230) = 0 /\ 0 <= -mid_n:228
                     /\ flag':232 = 0 /\ 0 <= -n':233))
         /\ (0 = K:231 \/ !((1 + -mid_n:228) <= 0))
         /\ (K:227 + K:231) = K:235
         /\ (!(0 <= K:236) \/ mid_n:237 = param0:53)
         /\ (!((0 <= K:236 /\ K:236 <= 0)) \/ mid_flag:238 = 1)
         /\ (!(1 <= K:236) \/ mid_flag:238 = 0)
         /\ (!(0 <= K:236) \/ mid___cost:239 = __cost:66)
         /\ ((K:236 = 0 /\ param0:53 = mid_n:237 /\ 1 = mid_flag:238
                /\ __cost:66 = mid___cost:239)
               \/ (1 <= K:236 /\ (-1 + 1) = 0 /\ 0 <= (-1 + -__cost:66)
                     /\ 0 <= -param0:53 /\ mid_flag:238 = 0
                     /\ 0 <= -mid_n:237 /\ 0 <= (-1 + -mid___cost:239)))
         /\ (0 = K:236 \/ !(-__cost:66 <= 0))
         /\ (!(0 <= K:240)
               \/ (__cost':234 + n':233) = (mid___cost:239 + mid_n:237))
         /\ (!(0 <= K:240)
               \/ (flag':232 + n':233) <= ((mid_flag:238 + mid_n:237)
                                             + -K:240))
         /\ (!(0 <= K:240) \/ flag':232 <= mid_flag:238)
         /\ (!(0 <= K:240) \/ -flag':232 <= (-mid_flag:238 + K:240))
         /\ ((K:240 = 0 /\ mid_n:237 = n':233 /\ mid_flag:238 = flag':232
                /\ mid___cost:239 = __cost':234)
               \/ (1 <= K:240 /\ (-1 + mid_flag:238) = 0
                     /\ 0 <= mid___cost:239 /\ 0 <= (1 + -flag':232)
                     /\ 0 <= (-flag':232 + __cost':234) /\ 0 <= -n':233
                     /\ 0 <= flag':232))
         /\ (0 = K:240 \/ -mid___cost:239 <= 0) /\ (K:236 + K:240) = K:235
         /\ 0 <= K:235 /\ flag':232 <= 1 /\ 0 <= flag':232 /\ flag':232 <= 0)}

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

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

Variable bounds at line 22 in run

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

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