/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, 53> -> <Unique State Name, 50 52>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 15> -> <Unique State Name, 53>	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
<Unique State Name, 56> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 46> -> <Unique State Name, 22>	Base relation: 
{flag := 1
 n := param0:53}	
<Unique State Name, 22> -> <Unique State Name, 57>	Base relation: 
{when (flag:62 <= 1 /\ 0 <= flag:62)}	
<Unique State Name, 48> -> <Unique State Name, 17>	Base relation: 
{}	
<Unique State Name, 54> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 49> -> <Unique State Name, 46 48>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 57> -> <Unique State Name, 26>	Base relation: 
{}	
<Unique State Name, 17> -> <Unique State Name, 55>	Base relation: 
{return := havoc:41
 return@pos := type_err:44
 return@width := type_err:45}	
<Unique State Name, 50> -> <Unique State Name, 49>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
<Unique State Name, 52> -> <Unique State Name, 56>	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, 26> -> <Unique State Name, 22>	Base relation: 
{__cost := (__cost:63 + 1)
 flag := phi_flag:75
 n := phi_n:76
 when (0 < flag:62 /\ 0 <= __cost:63 /\ 0 <= (__cost:63 + 1)
         /\ ((0 < n:64 /\ 1 = phi_flag:75 /\ (n:64 + -1) = phi_n:76)
               \/ (n:64 <= 0 /\ 0 = phi_flag:75 /\ n:64 = phi_n:76)))}	
<Unique State Name, 26> -> <Unique State Name, 54>	Base relation: 
{return := havoc:72
 return@pos := type_err:73
 return@width := type_err:74
 when flag:62 <= 0}	
<Unique State Name, 55> -> <Unique State Name, >	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:63 + 1)
 flag := phi_flag:122
 n := phi_n:123
 when (flag:62 <= 1 /\ 0 <= flag:62 /\ 0 < flag:62 /\ 0 <= __cost:63
         /\ 0 <= (__cost:63 + 1)
         /\ ((0 < n:64 /\ 1 = phi_flag:122 /\ (n:64 + -1) = phi_n:123)
               \/ (n:64 <= 0 /\ 0 = phi_flag:122 /\ n:64 = phi_n:123)))}
**** alpha hat: 
  {<Split [-n:64 < 0
            (__cost':124) = (1)*(__cost:63) + 1
           (flag':125) = 1
           (n':126) = (1)*(n:64) + (-1)*1
           }
          pre:
            [|flag:62-1=0; __cost:63>=0; n:64-1>=0|]
          post:
            [|flag':125-1=0; n':126>=0; __cost':124-1>=0|]
           (n':126) = (1)*(n:64) + 0
          (flag':125) = 0
          (__cost':124) = (1)*(__cost:63) + 1
          }
  pre:
    [|flag:62-1=0; -n:64>=0; __cost:63>=0|]
  post:
    [|flag':125=0; -n':126>=0; __cost':124-1>=0|]],
[!(n:64 <= 0)
  (__cost':124) = (1)*(__cost:63) + 1
 (flag':125) = 1
 (n':126) = (1)*(n:64) + (-1)*1
 } pre:   [|flag:62-1=0; __cost:63>=0; n:64-1>=0|] post:
  [|flag':125-1=0; n':126>=0; __cost':124-1>=0|]  (n':126) = (1)*(n:64) + 0
(flag':125) = 0 (__cost':124) = (1)*(__cost:63) + 1 } pre:
  [|flag:62-1=0; -n:64>=0; __cost:63>=0|] post:
  [|flag':125=0; -n':126>=0; __cost':124-1>=0|]]>}
**** star transition: 
  {__cost := __cost':124
   flag := flag':125
   n := n':126
   when ((!(0 <= K:152) \/ mid___cost:156 = (__cost:63 + K:152))
           /\ (!((0 <= K:152 /\ K:152 <= 0)) \/ mid_flag:155 = flag:62)
           /\ (!(1 <= K:152) \/ mid_flag:155 = 1)
           /\ (!(0 <= K:152) \/ mid_n:154 = (n:64 + -K:152))
           /\ ((K:152 = 0 /\ n:64 = mid_n:154 /\ flag:62 = mid_flag:155
                  /\ __cost:63 = mid___cost:156)
                 \/ (1 <= K:152 /\ (-1 + flag:62) = 0 /\ 0 <= __cost:63
                       /\ 0 <= (-1 + n:64) /\ (-1 + mid_flag:155) = 0
                       /\ 0 <= mid_n:154 /\ 0 <= (-1 + mid___cost:156)))
           /\ (0 = K:152 \/ -n:64 < 0)
           /\ (!(0 <= K:153) \/ n':126 = mid_n:154)
           /\ (!((0 <= K:153 /\ K:153 <= 0)) \/ flag':125 = mid_flag:155)
           /\ (!(1 <= K:153) \/ flag':125 = 0)
           /\ (!(0 <= K:153) \/ __cost':124 = (mid___cost:156 + K:153))
           /\ ((K:153 = 0 /\ mid_n:154 = n':126 /\ mid_flag:155 = flag':125
                  /\ mid___cost:156 = __cost':124)
                 \/ (1 <= K:153 /\ (-1 + mid_flag:155) = 0 /\ 0 <= -mid_n:154
                       /\ 0 <= mid___cost:156 /\ flag':125 = 0
                       /\ 0 <= -n':126 /\ 0 <= (-1 + __cost':124)))
           /\ (0 = K:153 \/ !(-mid_n:154 < 0)) /\ (K:152 + K:153) = K:151
           /\ (!(0 <= K:157) \/ mid___cost:161 = (__cost:63 + K:157))
           /\ (!((0 <= K:157 /\ K:157 <= 0)) \/ mid_flag:160 = flag:62)
           /\ (!(1 <= K:157) \/ mid_flag:160 = 1)
           /\ (!(0 <= K:157) \/ mid_n:159 = (n:64 + -K:157))
           /\ ((K:157 = 0 /\ n:64 = mid_n:159 /\ flag:62 = mid_flag:160
                  /\ __cost:63 = mid___cost:161)
                 \/ (1 <= K:157 /\ (-1 + flag:62) = 0 /\ 0 <= __cost:63
                       /\ 0 <= (-1 + n:64) /\ (-1 + mid_flag:160) = 0
                       /\ 0 <= mid_n:159 /\ 0 <= (-1 + mid___cost:161)))
           /\ (0 = K:157 \/ !(n:64 <= 0))
           /\ (!(0 <= K:158) \/ n':126 = mid_n:159)
           /\ (!((0 <= K:158 /\ K:158 <= 0)) \/ flag':125 = mid_flag:160)
           /\ (!(1 <= K:158) \/ flag':125 = 0)
           /\ (!(0 <= K:158) \/ __cost':124 = (mid___cost:161 + K:158))
           /\ ((K:158 = 0 /\ mid_n:159 = n':126 /\ mid_flag:160 = flag':125
                  /\ mid___cost:161 = __cost':124)
                 \/ (1 <= K:158 /\ (-1 + mid_flag:160) = 0 /\ 0 <= -mid_n:159
                       /\ 0 <= mid___cost:161 /\ flag':125 = 0
                       /\ 0 <= -n':126 /\ 0 <= (-1 + __cost':124)))
           /\ (0 = K:158 \/ mid_n:159 <= 0) /\ (K:157 + K:158) = K:151
           /\ 0 <= K:151)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  19  


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:54
       param0@width := type_err:55}    )
    ,
    Var(19)
  )
  ,
  Weight(Base relation: 
    {return := havoc:41
     return@pos := type_err:44
     return@width := type_err:45}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=19: 
Weight(Base relation: 
  {__cost := __cost':169
   flag := flag':168
   n := n':167
   return := havoc:176
   return@pos := type_err:177
   return@width := type_err:178
   when ((!(0 <= K:162) \/ mid___cost:163 = (__cost:63 + K:162))
           /\ (!((0 <= K:162 /\ K:162 <= 0)) \/ mid_flag:164 = 1)
           /\ (!(1 <= K:162) \/ mid_flag:164 = 1)
           /\ (!(0 <= K:162) \/ mid_n:165 = (param0:53 + -K:162))
           /\ ((K:162 = 0 /\ param0:53 = mid_n:165 /\ 1 = mid_flag:164
                  /\ __cost:63 = mid___cost:163)
                 \/ (1 <= K:162 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                       /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:164) = 0
                       /\ 0 <= mid_n:165 /\ 0 <= (-1 + mid___cost:163)))
           /\ (0 = K:162 \/ -param0:53 < 0)
           /\ (!(0 <= K:166) \/ n':167 = mid_n:165)
           /\ (!((0 <= K:166 /\ K:166 <= 0)) \/ flag':168 = mid_flag:164)
           /\ (!(1 <= K:166) \/ flag':168 = 0)
           /\ (!(0 <= K:166) \/ __cost':169 = (mid___cost:163 + K:166))
           /\ ((K:166 = 0 /\ mid_n:165 = n':167 /\ mid_flag:164 = flag':168
                  /\ mid___cost:163 = __cost':169)
                 \/ (1 <= K:166 /\ (-1 + mid_flag:164) = 0 /\ 0 <= -mid_n:165
                       /\ 0 <= mid___cost:163 /\ flag':168 = 0
                       /\ 0 <= -n':167 /\ 0 <= (-1 + __cost':169)))
           /\ (0 = K:166 \/ !(-mid_n:165 < 0)) /\ (K:162 + K:166) = K:170
           /\ (!(0 <= K:171) \/ mid___cost:172 = (__cost:63 + K:171))
           /\ (!((0 <= K:171 /\ K:171 <= 0)) \/ mid_flag:173 = 1)
           /\ (!(1 <= K:171) \/ mid_flag:173 = 1)
           /\ (!(0 <= K:171) \/ mid_n:174 = (param0:53 + -K:171))
           /\ ((K:171 = 0 /\ param0:53 = mid_n:174 /\ 1 = mid_flag:173
                  /\ __cost:63 = mid___cost:172)
                 \/ (1 <= K:171 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                       /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:173) = 0
                       /\ 0 <= mid_n:174 /\ 0 <= (-1 + mid___cost:172)))
           /\ (0 = K:171 \/ !(param0:53 <= 0))
           /\ (!(0 <= K:175) \/ n':167 = mid_n:174)
           /\ (!((0 <= K:175 /\ K:175 <= 0)) \/ flag':168 = mid_flag:173)
           /\ (!(1 <= K:175) \/ flag':168 = 0)
           /\ (!(0 <= K:175) \/ __cost':169 = (mid___cost:172 + K:175))
           /\ ((K:175 = 0 /\ mid_n:174 = n':167 /\ mid_flag:173 = flag':168
                  /\ mid___cost:172 = __cost':169)
                 \/ (1 <= K:175 /\ (-1 + mid_flag:173) = 0 /\ 0 <= -mid_n:174
                       /\ 0 <= mid___cost:172 /\ flag':168 = 0
                       /\ 0 <= -n':167 /\ 0 <= (-1 + __cost':169)))
           /\ (0 = K:175 \/ mid_n:174 <= 0) /\ (K:171 + K:175) = K:170
           /\ 0 <= K:170 /\ flag':168 <= 1 /\ 0 <= flag':168
           /\ flag':168 <= 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:54
         param0@width := type_err:55}      )
      ,
      Var(19)
    )
    ,
    Weight(Base relation: 
      {return := havoc:41
       return@pos := type_err:44
       return@width := type_err:45}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':169
   return := havoc:176
   return@pos := type_err:177
   return@width := type_err:178
   when ((!(0 <= K:162) \/ mid___cost:163 = (__cost:63 + K:162))
           /\ (!((0 <= K:162 /\ K:162 <= 0)) \/ mid_flag:164 = 1)
           /\ (!(1 <= K:162) \/ mid_flag:164 = 1)
           /\ (!(0 <= K:162) \/ mid_n:165 = (param0:53 + -K:162))
           /\ ((K:162 = 0 /\ param0:53 = mid_n:165 /\ 1 = mid_flag:164
                  /\ __cost:63 = mid___cost:163)
                 \/ (1 <= K:162 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                       /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:164) = 0
                       /\ 0 <= mid_n:165 /\ 0 <= (-1 + mid___cost:163)))
           /\ (0 = K:162 \/ -param0:53 < 0)
           /\ (!(0 <= K:166) \/ n':167 = mid_n:165)
           /\ (!((0 <= K:166 /\ K:166 <= 0)) \/ flag':168 = mid_flag:164)
           /\ (!(1 <= K:166) \/ flag':168 = 0)
           /\ (!(0 <= K:166) \/ __cost':169 = (mid___cost:163 + K:166))
           /\ ((K:166 = 0 /\ mid_n:165 = n':167 /\ mid_flag:164 = flag':168
                  /\ mid___cost:163 = __cost':169)
                 \/ (1 <= K:166 /\ (-1 + mid_flag:164) = 0 /\ 0 <= -mid_n:165
                       /\ 0 <= mid___cost:163 /\ flag':168 = 0
                       /\ 0 <= -n':167 /\ 0 <= (-1 + __cost':169)))
           /\ (0 = K:166 \/ !(-mid_n:165 < 0)) /\ (K:162 + K:166) = K:170
           /\ (!(0 <= K:171) \/ mid___cost:172 = (__cost:63 + K:171))
           /\ (!((0 <= K:171 /\ K:171 <= 0)) \/ mid_flag:173 = 1)
           /\ (!(1 <= K:171) \/ mid_flag:173 = 1)
           /\ (!(0 <= K:171) \/ mid_n:174 = (param0:53 + -K:171))
           /\ ((K:171 = 0 /\ param0:53 = mid_n:174 /\ 1 = mid_flag:173
                  /\ __cost:63 = mid___cost:172)
                 \/ (1 <= K:171 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                       /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:173) = 0
                       /\ 0 <= mid_n:174 /\ 0 <= (-1 + mid___cost:172)))
           /\ (0 = K:171 \/ !(param0:53 <= 0))
           /\ (!(0 <= K:175) \/ n':167 = mid_n:174)
           /\ (!((0 <= K:175 /\ K:175 <= 0)) \/ flag':168 = mid_flag:173)
           /\ (!(1 <= K:175) \/ flag':168 = 0)
           /\ (!(0 <= K:175) \/ __cost':169 = (mid___cost:172 + K:175))
           /\ ((K:175 = 0 /\ mid_n:174 = n':167 /\ mid_flag:173 = flag':168
                  /\ mid___cost:172 = __cost':169)
                 \/ (1 <= K:175 /\ (-1 + mid_flag:173) = 0 /\ 0 <= -mid_n:174
                       /\ 0 <= mid___cost:172 /\ flag':168 = 0
                       /\ 0 <= -n':167 /\ 0 <= (-1 + __cost':169)))
           /\ (0 = K:175 \/ mid_n:174 <= 0) /\ (K:171 + K:175) = K:170
           /\ 0 <= K:170 /\ flag':168 <= 1 /\ 0 <= flag':168
           /\ flag':168 <= 0)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':206
   return := 0
   param0 := havoc:13
   return@pos := type_err:219
   param0@pos := type_err:215
   return@width := type_err:220
   param0@width := type_err:217
   when ((!(0 <= K:199) \/ mid___cost:200 = K:199)
           /\ (!((0 <= K:199 /\ K:199 <= 0)) \/ mid_flag:201 = 1)
           /\ (!(1 <= K:199) \/ mid_flag:201 = 1)
           /\ (!(0 <= K:199) \/ mid_n:202 = (havoc:13 + -K:199))
           /\ ((K:199 = 0 /\ havoc:13 = mid_n:202 /\ 1 = mid_flag:201
                  /\ 0 = mid___cost:200)
                 \/ (1 <= K:199 /\ (-1 + 1) = 0 /\ 0 <= (-1 + havoc:13)
                       /\ (-1 + mid_flag:201) = 0 /\ 0 <= mid_n:202
                       /\ 0 <= (-1 + mid___cost:200)))
           /\ (0 = K:199 \/ -havoc:13 < 0)
           /\ (!(0 <= K:203) \/ n':204 = mid_n:202)
           /\ (!((0 <= K:203 /\ K:203 <= 0)) \/ flag':205 = mid_flag:201)
           /\ (!(1 <= K:203) \/ flag':205 = 0)
           /\ (!(0 <= K:203) \/ __cost':206 = (mid___cost:200 + K:203))
           /\ ((K:203 = 0 /\ mid_n:202 = n':204 /\ mid_flag:201 = flag':205
                  /\ mid___cost:200 = __cost':206)
                 \/ (1 <= K:203 /\ (-1 + mid_flag:201) = 0 /\ 0 <= -mid_n:202
                       /\ 0 <= mid___cost:200 /\ flag':205 = 0
                       /\ 0 <= -n':204 /\ 0 <= (-1 + __cost':206)))
           /\ (0 = K:203 \/ !(-mid_n:202 < 0)) /\ (K:199 + K:203) = K:207
           /\ (!(0 <= K:208) \/ mid___cost:209 = K:208)
           /\ (!((0 <= K:208 /\ K:208 <= 0)) \/ mid_flag:210 = 1)
           /\ (!(1 <= K:208) \/ mid_flag:210 = 1)
           /\ (!(0 <= K:208) \/ mid_n:211 = (havoc:13 + -K:208))
           /\ ((K:208 = 0 /\ havoc:13 = mid_n:211 /\ 1 = mid_flag:210
                  /\ 0 = mid___cost:209)
                 \/ (1 <= K:208 /\ (-1 + 1) = 0 /\ 0 <= (-1 + havoc:13)
                       /\ (-1 + mid_flag:210) = 0 /\ 0 <= mid_n:211
                       /\ 0 <= (-1 + mid___cost:209)))
           /\ (0 = K:208 \/ !(havoc:13 <= 0))
           /\ (!(0 <= K:212) \/ n':204 = mid_n:211)
           /\ (!((0 <= K:212 /\ K:212 <= 0)) \/ flag':205 = mid_flag:210)
           /\ (!(1 <= K:212) \/ flag':205 = 0)
           /\ (!(0 <= K:212) \/ __cost':206 = (mid___cost:209 + K:212))
           /\ ((K:212 = 0 /\ mid_n:211 = n':204 /\ mid_flag:210 = flag':205
                  /\ mid___cost:209 = __cost':206)
                 \/ (1 <= K:212 /\ (-1 + mid_flag:210) = 0 /\ 0 <= -mid_n:211
                       /\ 0 <= mid___cost:209 /\ flag':205 = 0
                       /\ 0 <= -n':204 /\ 0 <= (-1 + __cost':206)))
           /\ (0 = K:212 \/ mid_n:211 <= 0) /\ (K:208 + K:212) = K:207
           /\ 0 <= K:207 /\ flag':205 <= 1 /\ 0 <= flag':205
           /\ flag':205 <= 0
           /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:218)
                 \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:218)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':228
   return := havoc:238
   param0 := param0:53
   return@pos := type_err:239
   param0@pos := type_err:54
   return@width := type_err:240
   param0@width := type_err:55
   when ((!(0 <= K:221) \/ mid___cost:222 = (__cost:63 + K:221))
           /\ (!((0 <= K:221 /\ K:221 <= 0)) \/ mid_flag:223 = 1)
           /\ (!(1 <= K:221) \/ mid_flag:223 = 1)
           /\ (!(0 <= K:221) \/ mid_n:224 = (param0:53 + -K:221))
           /\ ((K:221 = 0 /\ param0:53 = mid_n:224 /\ 1 = mid_flag:223
                  /\ __cost:63 = mid___cost:222)
                 \/ (1 <= K:221 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                       /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:223) = 0
                       /\ 0 <= mid_n:224 /\ 0 <= (-1 + mid___cost:222)))
           /\ (0 = K:221 \/ -param0:53 < 0)
           /\ (!(0 <= K:225) \/ n':226 = mid_n:224)
           /\ (!((0 <= K:225 /\ K:225 <= 0)) \/ flag':227 = mid_flag:223)
           /\ (!(1 <= K:225) \/ flag':227 = 0)
           /\ (!(0 <= K:225) \/ __cost':228 = (mid___cost:222 + K:225))
           /\ ((K:225 = 0 /\ mid_n:224 = n':226 /\ mid_flag:223 = flag':227
                  /\ mid___cost:222 = __cost':228)
                 \/ (1 <= K:225 /\ (-1 + mid_flag:223) = 0 /\ 0 <= -mid_n:224
                       /\ 0 <= mid___cost:222 /\ flag':227 = 0
                       /\ 0 <= -n':226 /\ 0 <= (-1 + __cost':228)))
           /\ (0 = K:225 \/ !(-mid_n:224 < 0)) /\ (K:221 + K:225) = K:229
           /\ (!(0 <= K:230) \/ mid___cost:231 = (__cost:63 + K:230))
           /\ (!((0 <= K:230 /\ K:230 <= 0)) \/ mid_flag:232 = 1)
           /\ (!(1 <= K:230) \/ mid_flag:232 = 1)
           /\ (!(0 <= K:230) \/ mid_n:233 = (param0:53 + -K:230))
           /\ ((K:230 = 0 /\ param0:53 = mid_n:233 /\ 1 = mid_flag:232
                  /\ __cost:63 = mid___cost:231)
                 \/ (1 <= K:230 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                       /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:232) = 0
                       /\ 0 <= mid_n:233 /\ 0 <= (-1 + mid___cost:231)))
           /\ (0 = K:230 \/ !(param0:53 <= 0))
           /\ (!(0 <= K:234) \/ n':226 = mid_n:233)
           /\ (!((0 <= K:234 /\ K:234 <= 0)) \/ flag':227 = mid_flag:232)
           /\ (!(1 <= K:234) \/ flag':227 = 0)
           /\ (!(0 <= K:234) \/ __cost':228 = (mid___cost:231 + K:234))
           /\ ((K:234 = 0 /\ mid_n:233 = n':226 /\ mid_flag:232 = flag':227
                  /\ mid___cost:231 = __cost':228)
                 \/ (1 <= K:234 /\ (-1 + mid_flag:232) = 0 /\ 0 <= -mid_n:233
                       /\ 0 <= mid___cost:231 /\ flag':227 = 0
                       /\ 0 <= -n':226 /\ 0 <= (-1 + __cost':228)))
           /\ (0 = K:234 \/ mid_n:233 <= 0) /\ (K:230 + K:234) = K:229
           /\ 0 <= K:229 /\ flag':227 <= 1 /\ 0 <= flag':227
           /\ flag':227 <= 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=19: 
Weight(Base relation: 
  {__cost := __cost':169
   return := havoc:176
   return@pos := type_err:177
   return@width := type_err:178
   when ((!(0 <= K:162) \/ mid___cost:163 = (__cost:63 + K:162))
           /\ (!((0 <= K:162 /\ K:162 <= 0)) \/ mid_flag:164 = 1)
           /\ (!(1 <= K:162) \/ mid_flag:164 = 1)
           /\ (!(0 <= K:162) \/ mid_n:165 = (param0:53 + -K:162))
           /\ ((K:162 = 0 /\ param0:53 = mid_n:165 /\ 1 = mid_flag:164
                  /\ __cost:63 = mid___cost:163)
                 \/ (1 <= K:162 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                       /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:164) = 0
                       /\ 0 <= mid_n:165 /\ 0 <= (-1 + mid___cost:163)))
           /\ (0 = K:162 \/ -param0:53 < 0)
           /\ (!(0 <= K:166) \/ n':167 = mid_n:165)
           /\ (!((0 <= K:166 /\ K:166 <= 0)) \/ flag':168 = mid_flag:164)
           /\ (!(1 <= K:166) \/ flag':168 = 0)
           /\ (!(0 <= K:166) \/ __cost':169 = (mid___cost:163 + K:166))
           /\ ((K:166 = 0 /\ mid_n:165 = n':167 /\ mid_flag:164 = flag':168
                  /\ mid___cost:163 = __cost':169)
                 \/ (1 <= K:166 /\ (-1 + mid_flag:164) = 0 /\ 0 <= -mid_n:165
                       /\ 0 <= mid___cost:163 /\ flag':168 = 0
                       /\ 0 <= -n':167 /\ 0 <= (-1 + __cost':169)))
           /\ (0 = K:166 \/ !(-mid_n:165 < 0)) /\ (K:162 + K:166) = K:170
           /\ (!(0 <= K:171) \/ mid___cost:172 = (__cost:63 + K:171))
           /\ (!((0 <= K:171 /\ K:171 <= 0)) \/ mid_flag:173 = 1)
           /\ (!(1 <= K:171) \/ mid_flag:173 = 1)
           /\ (!(0 <= K:171) \/ mid_n:174 = (param0:53 + -K:171))
           /\ ((K:171 = 0 /\ param0:53 = mid_n:174 /\ 1 = mid_flag:173
                  /\ __cost:63 = mid___cost:172)
                 \/ (1 <= K:171 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                       /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:173) = 0
                       /\ 0 <= mid_n:174 /\ 0 <= (-1 + mid___cost:172)))
           /\ (0 = K:171 \/ !(param0:53 <= 0))
           /\ (!(0 <= K:175) \/ n':167 = mid_n:174)
           /\ (!((0 <= K:175 /\ K:175 <= 0)) \/ flag':168 = mid_flag:173)
           /\ (!(1 <= K:175) \/ flag':168 = 0)
           /\ (!(0 <= K:175) \/ __cost':169 = (mid___cost:172 + K:175))
           /\ ((K:175 = 0 /\ mid_n:174 = n':167 /\ mid_flag:173 = flag':168
                  /\ mid___cost:172 = __cost':169)
                 \/ (1 <= K:175 /\ (-1 + mid_flag:173) = 0 /\ 0 <= -mid_n:174
                       /\ 0 <= mid___cost:172 /\ flag':168 = 0
                       /\ 0 <= -n':167 /\ 0 <= (-1 + __cost':169)))
           /\ (0 = K:175 \/ mid_n:174 <= 0) /\ (K:171 + K:175) = K:170
           /\ 0 <= K:170 /\ flag':168 <= 1 /\ 0 <= flag':168
           /\ flag':168 <= 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':206
 return := 0
 param0 := havoc:13
 return@pos := type_err:219
 param0@pos := type_err:215
 return@width := type_err:220
 param0@width := type_err:217
 when ((!(0 <= K:199) \/ mid___cost:200 = K:199)
         /\ (!((0 <= K:199 /\ K:199 <= 0)) \/ mid_flag:201 = 1)
         /\ (!(1 <= K:199) \/ mid_flag:201 = 1)
         /\ (!(0 <= K:199) \/ mid_n:202 = (havoc:13 + -K:199))
         /\ ((K:199 = 0 /\ havoc:13 = mid_n:202 /\ 1 = mid_flag:201
                /\ 0 = mid___cost:200)
               \/ (1 <= K:199 /\ (-1 + 1) = 0 /\ 0 <= (-1 + havoc:13)
                     /\ (-1 + mid_flag:201) = 0 /\ 0 <= mid_n:202
                     /\ 0 <= (-1 + mid___cost:200)))
         /\ (0 = K:199 \/ -havoc:13 < 0)
         /\ (!(0 <= K:203) \/ n':204 = mid_n:202)
         /\ (!((0 <= K:203 /\ K:203 <= 0)) \/ flag':205 = mid_flag:201)
         /\ (!(1 <= K:203) \/ flag':205 = 0)
         /\ (!(0 <= K:203) \/ __cost':206 = (mid___cost:200 + K:203))
         /\ ((K:203 = 0 /\ mid_n:202 = n':204 /\ mid_flag:201 = flag':205
                /\ mid___cost:200 = __cost':206)
               \/ (1 <= K:203 /\ (-1 + mid_flag:201) = 0 /\ 0 <= -mid_n:202
                     /\ 0 <= mid___cost:200 /\ flag':205 = 0 /\ 0 <= -n':204
                     /\ 0 <= (-1 + __cost':206)))
         /\ (0 = K:203 \/ !(-mid_n:202 < 0)) /\ (K:199 + K:203) = K:207
         /\ (!(0 <= K:208) \/ mid___cost:209 = K:208)
         /\ (!((0 <= K:208 /\ K:208 <= 0)) \/ mid_flag:210 = 1)
         /\ (!(1 <= K:208) \/ mid_flag:210 = 1)
         /\ (!(0 <= K:208) \/ mid_n:211 = (havoc:13 + -K:208))
         /\ ((K:208 = 0 /\ havoc:13 = mid_n:211 /\ 1 = mid_flag:210
                /\ 0 = mid___cost:209)
               \/ (1 <= K:208 /\ (-1 + 1) = 0 /\ 0 <= (-1 + havoc:13)
                     /\ (-1 + mid_flag:210) = 0 /\ 0 <= mid_n:211
                     /\ 0 <= (-1 + mid___cost:209)))
         /\ (0 = K:208 \/ !(havoc:13 <= 0))
         /\ (!(0 <= K:212) \/ n':204 = mid_n:211)
         /\ (!((0 <= K:212 /\ K:212 <= 0)) \/ flag':205 = mid_flag:210)
         /\ (!(1 <= K:212) \/ flag':205 = 0)
         /\ (!(0 <= K:212) \/ __cost':206 = (mid___cost:209 + K:212))
         /\ ((K:212 = 0 /\ mid_n:211 = n':204 /\ mid_flag:210 = flag':205
                /\ mid___cost:209 = __cost':206)
               \/ (1 <= K:212 /\ (-1 + mid_flag:210) = 0 /\ 0 <= -mid_n:211
                     /\ 0 <= mid___cost:209 /\ flag':205 = 0 /\ 0 <= -n':204
                     /\ 0 <= (-1 + __cost':206)))
         /\ (0 = K:212 \/ mid_n:211 <= 0) /\ (K:208 + K:212) = K:207
         /\ 0 <= K:207 /\ flag':205 <= 1 /\ 0 <= flag':205 /\ flag':205 <= 0
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:218)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:218)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':228
 return := havoc:238
 param0 := param0:53
 return@pos := type_err:239
 param0@pos := type_err:54
 return@width := type_err:240
 param0@width := type_err:55
 when ((!(0 <= K:221) \/ mid___cost:222 = (__cost:63 + K:221))
         /\ (!((0 <= K:221 /\ K:221 <= 0)) \/ mid_flag:223 = 1)
         /\ (!(1 <= K:221) \/ mid_flag:223 = 1)
         /\ (!(0 <= K:221) \/ mid_n:224 = (param0:53 + -K:221))
         /\ ((K:221 = 0 /\ param0:53 = mid_n:224 /\ 1 = mid_flag:223
                /\ __cost:63 = mid___cost:222)
               \/ (1 <= K:221 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                     /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:223) = 0
                     /\ 0 <= mid_n:224 /\ 0 <= (-1 + mid___cost:222)))
         /\ (0 = K:221 \/ -param0:53 < 0)
         /\ (!(0 <= K:225) \/ n':226 = mid_n:224)
         /\ (!((0 <= K:225 /\ K:225 <= 0)) \/ flag':227 = mid_flag:223)
         /\ (!(1 <= K:225) \/ flag':227 = 0)
         /\ (!(0 <= K:225) \/ __cost':228 = (mid___cost:222 + K:225))
         /\ ((K:225 = 0 /\ mid_n:224 = n':226 /\ mid_flag:223 = flag':227
                /\ mid___cost:222 = __cost':228)
               \/ (1 <= K:225 /\ (-1 + mid_flag:223) = 0 /\ 0 <= -mid_n:224
                     /\ 0 <= mid___cost:222 /\ flag':227 = 0 /\ 0 <= -n':226
                     /\ 0 <= (-1 + __cost':228)))
         /\ (0 = K:225 \/ !(-mid_n:224 < 0)) /\ (K:221 + K:225) = K:229
         /\ (!(0 <= K:230) \/ mid___cost:231 = (__cost:63 + K:230))
         /\ (!((0 <= K:230 /\ K:230 <= 0)) \/ mid_flag:232 = 1)
         /\ (!(1 <= K:230) \/ mid_flag:232 = 1)
         /\ (!(0 <= K:230) \/ mid_n:233 = (param0:53 + -K:230))
         /\ ((K:230 = 0 /\ param0:53 = mid_n:233 /\ 1 = mid_flag:232
                /\ __cost:63 = mid___cost:231)
               \/ (1 <= K:230 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                     /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:232) = 0
                     /\ 0 <= mid_n:233 /\ 0 <= (-1 + mid___cost:231)))
         /\ (0 = K:230 \/ !(param0:53 <= 0))
         /\ (!(0 <= K:234) \/ n':226 = mid_n:233)
         /\ (!((0 <= K:234 /\ K:234 <= 0)) \/ flag':227 = mid_flag:232)
         /\ (!(1 <= K:234) \/ flag':227 = 0)
         /\ (!(0 <= K:234) \/ __cost':228 = (mid___cost:231 + K:234))
         /\ ((K:234 = 0 /\ mid_n:233 = n':226 /\ mid_flag:232 = flag':227
                /\ mid___cost:231 = __cost':228)
               \/ (1 <= K:234 /\ (-1 + mid_flag:232) = 0 /\ 0 <= -mid_n:233
                     /\ 0 <= mid___cost:231 /\ flag':227 = 0 /\ 0 <= -n':226
                     /\ 0 <= (-1 + __cost':228)))
         /\ (0 = K:234 \/ mid_n:233 <= 0) /\ (K:230 + K:234) = K:229
         /\ 0 <= K:229 /\ flag':227 <= 1 /\ 0 <= flag':227 /\ flag':227 <= 0)}

Evaluating variable number 19 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':169
 return := havoc:176
 return@pos := type_err:177
 return@width := type_err:178
 when ((!(0 <= K:162) \/ mid___cost:163 = (__cost:63 + K:162))
         /\ (!((0 <= K:162 /\ K:162 <= 0)) \/ mid_flag:164 = 1)
         /\ (!(1 <= K:162) \/ mid_flag:164 = 1)
         /\ (!(0 <= K:162) \/ mid_n:165 = (param0:53 + -K:162))
         /\ ((K:162 = 0 /\ param0:53 = mid_n:165 /\ 1 = mid_flag:164
                /\ __cost:63 = mid___cost:163)
               \/ (1 <= K:162 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                     /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:164) = 0
                     /\ 0 <= mid_n:165 /\ 0 <= (-1 + mid___cost:163)))
         /\ (0 = K:162 \/ -param0:53 < 0)
         /\ (!(0 <= K:166) \/ n':167 = mid_n:165)
         /\ (!((0 <= K:166 /\ K:166 <= 0)) \/ flag':168 = mid_flag:164)
         /\ (!(1 <= K:166) \/ flag':168 = 0)
         /\ (!(0 <= K:166) \/ __cost':169 = (mid___cost:163 + K:166))
         /\ ((K:166 = 0 /\ mid_n:165 = n':167 /\ mid_flag:164 = flag':168
                /\ mid___cost:163 = __cost':169)
               \/ (1 <= K:166 /\ (-1 + mid_flag:164) = 0 /\ 0 <= -mid_n:165
                     /\ 0 <= mid___cost:163 /\ flag':168 = 0 /\ 0 <= -n':167
                     /\ 0 <= (-1 + __cost':169)))
         /\ (0 = K:166 \/ !(-mid_n:165 < 0)) /\ (K:162 + K:166) = K:170
         /\ (!(0 <= K:171) \/ mid___cost:172 = (__cost:63 + K:171))
         /\ (!((0 <= K:171 /\ K:171 <= 0)) \/ mid_flag:173 = 1)
         /\ (!(1 <= K:171) \/ mid_flag:173 = 1)
         /\ (!(0 <= K:171) \/ mid_n:174 = (param0:53 + -K:171))
         /\ ((K:171 = 0 /\ param0:53 = mid_n:174 /\ 1 = mid_flag:173
                /\ __cost:63 = mid___cost:172)
               \/ (1 <= K:171 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                     /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:173) = 0
                     /\ 0 <= mid_n:174 /\ 0 <= (-1 + mid___cost:172)))
         /\ (0 = K:171 \/ !(param0:53 <= 0))
         /\ (!(0 <= K:175) \/ n':167 = mid_n:174)
         /\ (!((0 <= K:175 /\ K:175 <= 0)) \/ flag':168 = mid_flag:173)
         /\ (!(1 <= K:175) \/ flag':168 = 0)
         /\ (!(0 <= K:175) \/ __cost':169 = (mid___cost:172 + K:175))
         /\ ((K:175 = 0 /\ mid_n:174 = n':167 /\ mid_flag:173 = flag':168
                /\ mid___cost:172 = __cost':169)
               \/ (1 <= K:175 /\ (-1 + mid_flag:173) = 0 /\ 0 <= -mid_n:174
                     /\ 0 <= mid___cost:172 /\ flag':168 = 0 /\ 0 <= -n':167
                     /\ 0 <= (-1 + __cost':169)))
         /\ (0 = K:175 \/ mid_n:174 <= 0) /\ (K:171 + K:175) = K:170
         /\ 0 <= K:170 /\ flag':168 <= 1 /\ 0 <= flag':168 /\ flag':168 <= 0)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,50)_g1> -> <__pstate, (Unique State Name,46)_g1>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
<__pstate, accept> -> <__pstate, (Unique State Name,50)_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: 
__done 0x3e17550: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x335c650: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
##### ANS
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}
    ( __pstate , (Unique State Name,46)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:283
 param0@width := type_err:284}
    ( __pstate , (Unique State Name,50)_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: 
__done 0x334b3a0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x3cf6200: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
================================================
Procedure Summaries

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

Base relation: 
{__cost := __cost':248
 n := havoc:13
 return := 0
 param0 := havoc:13
 return@pos := type_err:261
 param0@pos := type_err:257
 return@width := type_err:262
 param0@width := type_err:259
 when ((!(0 <= K:241) \/ mid___cost:242 = K:241)
         /\ (!((0 <= K:241 /\ K:241 <= 0)) \/ mid_flag:243 = 1)
         /\ (!(1 <= K:241) \/ mid_flag:243 = 1)
         /\ (!(0 <= K:241) \/ mid_n:244 = (havoc:13 + -K:241))
         /\ ((K:241 = 0 /\ havoc:13 = mid_n:244 /\ 1 = mid_flag:243
                /\ 0 = mid___cost:242)
               \/ (1 <= K:241 /\ (-1 + 1) = 0 /\ 0 <= (-1 + havoc:13)
                     /\ (-1 + mid_flag:243) = 0 /\ 0 <= mid_n:244
                     /\ 0 <= (-1 + mid___cost:242)))
         /\ (0 = K:241 \/ -havoc:13 < 0)
         /\ (!(0 <= K:245) \/ n':246 = mid_n:244)
         /\ (!((0 <= K:245 /\ K:245 <= 0)) \/ flag':247 = mid_flag:243)
         /\ (!(1 <= K:245) \/ flag':247 = 0)
         /\ (!(0 <= K:245) \/ __cost':248 = (mid___cost:242 + K:245))
         /\ ((K:245 = 0 /\ mid_n:244 = n':246 /\ mid_flag:243 = flag':247
                /\ mid___cost:242 = __cost':248)
               \/ (1 <= K:245 /\ (-1 + mid_flag:243) = 0 /\ 0 <= -mid_n:244
                     /\ 0 <= mid___cost:242 /\ flag':247 = 0 /\ 0 <= -n':246
                     /\ 0 <= (-1 + __cost':248)))
         /\ (0 = K:245 \/ !(-mid_n:244 < 0)) /\ (K:241 + K:245) = K:249
         /\ (!(0 <= K:250) \/ mid___cost:251 = K:250)
         /\ (!((0 <= K:250 /\ K:250 <= 0)) \/ mid_flag:252 = 1)
         /\ (!(1 <= K:250) \/ mid_flag:252 = 1)
         /\ (!(0 <= K:250) \/ mid_n:253 = (havoc:13 + -K:250))
         /\ ((K:250 = 0 /\ havoc:13 = mid_n:253 /\ 1 = mid_flag:252
                /\ 0 = mid___cost:251)
               \/ (1 <= K:250 /\ (-1 + 1) = 0 /\ 0 <= (-1 + havoc:13)
                     /\ (-1 + mid_flag:252) = 0 /\ 0 <= mid_n:253
                     /\ 0 <= (-1 + mid___cost:251)))
         /\ (0 = K:250 \/ !(havoc:13 <= 0))
         /\ (!(0 <= K:254) \/ n':246 = mid_n:253)
         /\ (!((0 <= K:254 /\ K:254 <= 0)) \/ flag':247 = mid_flag:252)
         /\ (!(1 <= K:254) \/ flag':247 = 0)
         /\ (!(0 <= K:254) \/ __cost':248 = (mid___cost:251 + K:254))
         /\ ((K:254 = 0 /\ mid_n:253 = n':246 /\ mid_flag:252 = flag':247
                /\ mid___cost:251 = __cost':248)
               \/ (1 <= K:254 /\ (-1 + mid_flag:252) = 0 /\ 0 <= -mid_n:253
                     /\ 0 <= mid___cost:251 /\ flag':247 = 0 /\ 0 <= -n':246
                     /\ 0 <= (-1 + __cost':248)))
         /\ (0 = K:254 \/ mid_n:253 <= 0) /\ (K:250 + K:254) = K:249
         /\ 0 <= K:249 /\ flag':247 <= 1 /\ 0 <= flag':247 /\ flag':247 <= 0
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:260)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:260)))}

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

Base relation: 
{__cost := __cost':270
 return := havoc:280
 param0 := param0:53
 return@pos := type_err:281
 param0@pos := type_err:54
 return@width := type_err:282
 param0@width := type_err:55
 when ((!(0 <= K:263) \/ mid___cost:264 = (__cost:63 + K:263))
         /\ (!((0 <= K:263 /\ K:263 <= 0)) \/ mid_flag:265 = 1)
         /\ (!(1 <= K:263) \/ mid_flag:265 = 1)
         /\ (!(0 <= K:263) \/ mid_n:266 = (param0:53 + -K:263))
         /\ ((K:263 = 0 /\ param0:53 = mid_n:266 /\ 1 = mid_flag:265
                /\ __cost:63 = mid___cost:264)
               \/ (1 <= K:263 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                     /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:265) = 0
                     /\ 0 <= mid_n:266 /\ 0 <= (-1 + mid___cost:264)))
         /\ (0 = K:263 \/ -param0:53 < 0)
         /\ (!(0 <= K:267) \/ n':268 = mid_n:266)
         /\ (!((0 <= K:267 /\ K:267 <= 0)) \/ flag':269 = mid_flag:265)
         /\ (!(1 <= K:267) \/ flag':269 = 0)
         /\ (!(0 <= K:267) \/ __cost':270 = (mid___cost:264 + K:267))
         /\ ((K:267 = 0 /\ mid_n:266 = n':268 /\ mid_flag:265 = flag':269
                /\ mid___cost:264 = __cost':270)
               \/ (1 <= K:267 /\ (-1 + mid_flag:265) = 0 /\ 0 <= -mid_n:266
                     /\ 0 <= mid___cost:264 /\ flag':269 = 0 /\ 0 <= -n':268
                     /\ 0 <= (-1 + __cost':270)))
         /\ (0 = K:267 \/ !(-mid_n:266 < 0)) /\ (K:263 + K:267) = K:271
         /\ (!(0 <= K:272) \/ mid___cost:273 = (__cost:63 + K:272))
         /\ (!((0 <= K:272 /\ K:272 <= 0)) \/ mid_flag:274 = 1)
         /\ (!(1 <= K:272) \/ mid_flag:274 = 1)
         /\ (!(0 <= K:272) \/ mid_n:275 = (param0:53 + -K:272))
         /\ ((K:272 = 0 /\ param0:53 = mid_n:275 /\ 1 = mid_flag:274
                /\ __cost:63 = mid___cost:273)
               \/ (1 <= K:272 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                     /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:274) = 0
                     /\ 0 <= mid_n:275 /\ 0 <= (-1 + mid___cost:273)))
         /\ (0 = K:272 \/ !(param0:53 <= 0))
         /\ (!(0 <= K:276) \/ n':268 = mid_n:275)
         /\ (!((0 <= K:276 /\ K:276 <= 0)) \/ flag':269 = mid_flag:274)
         /\ (!(1 <= K:276) \/ flag':269 = 0)
         /\ (!(0 <= K:276) \/ __cost':270 = (mid___cost:273 + K:276))
         /\ ((K:276 = 0 /\ mid_n:275 = n':268 /\ mid_flag:274 = flag':269
                /\ mid___cost:273 = __cost':270)
               \/ (1 <= K:276 /\ (-1 + mid_flag:274) = 0 /\ 0 <= -mid_n:275
                     /\ 0 <= mid___cost:273 /\ flag':269 = 0 /\ 0 <= -n':268
                     /\ 0 <= (-1 + __cost':270)))
         /\ (0 = K:276 \/ mid_n:275 <= 0) /\ (K:272 + K:276) = K:271
         /\ 0 <= K:271 /\ flag':269 <= 1 /\ 0 <= flag':269 /\ flag':269 <= 0)}

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

Base relation: 
{__cost := __cost':169
 flag := flag':168
 n := n':167
 return := havoc:176
 return@pos := type_err:177
 return@width := type_err:178
 when ((!(0 <= K:162) \/ mid___cost:163 = (__cost:63 + K:162))
         /\ (!((0 <= K:162 /\ K:162 <= 0)) \/ mid_flag:164 = 1)
         /\ (!(1 <= K:162) \/ mid_flag:164 = 1)
         /\ (!(0 <= K:162) \/ mid_n:165 = (param0:53 + -K:162))
         /\ ((K:162 = 0 /\ param0:53 = mid_n:165 /\ 1 = mid_flag:164
                /\ __cost:63 = mid___cost:163)
               \/ (1 <= K:162 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                     /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:164) = 0
                     /\ 0 <= mid_n:165 /\ 0 <= (-1 + mid___cost:163)))
         /\ (0 = K:162 \/ -param0:53 < 0)
         /\ (!(0 <= K:166) \/ n':167 = mid_n:165)
         /\ (!((0 <= K:166 /\ K:166 <= 0)) \/ flag':168 = mid_flag:164)
         /\ (!(1 <= K:166) \/ flag':168 = 0)
         /\ (!(0 <= K:166) \/ __cost':169 = (mid___cost:163 + K:166))
         /\ ((K:166 = 0 /\ mid_n:165 = n':167 /\ mid_flag:164 = flag':168
                /\ mid___cost:163 = __cost':169)
               \/ (1 <= K:166 /\ (-1 + mid_flag:164) = 0 /\ 0 <= -mid_n:165
                     /\ 0 <= mid___cost:163 /\ flag':168 = 0 /\ 0 <= -n':167
                     /\ 0 <= (-1 + __cost':169)))
         /\ (0 = K:166 \/ !(-mid_n:165 < 0)) /\ (K:162 + K:166) = K:170
         /\ (!(0 <= K:171) \/ mid___cost:172 = (__cost:63 + K:171))
         /\ (!((0 <= K:171 /\ K:171 <= 0)) \/ mid_flag:173 = 1)
         /\ (!(1 <= K:171) \/ mid_flag:173 = 1)
         /\ (!(0 <= K:171) \/ mid_n:174 = (param0:53 + -K:171))
         /\ ((K:171 = 0 /\ param0:53 = mid_n:174 /\ 1 = mid_flag:173
                /\ __cost:63 = mid___cost:172)
               \/ (1 <= K:171 /\ (-1 + 1) = 0 /\ 0 <= __cost:63
                     /\ 0 <= (-1 + param0:53) /\ (-1 + mid_flag:173) = 0
                     /\ 0 <= mid_n:174 /\ 0 <= (-1 + mid___cost:172)))
         /\ (0 = K:171 \/ !(param0:53 <= 0))
         /\ (!(0 <= K:175) \/ n':167 = mid_n:174)
         /\ (!((0 <= K:175 /\ K:175 <= 0)) \/ flag':168 = mid_flag:173)
         /\ (!(1 <= K:175) \/ flag':168 = 0)
         /\ (!(0 <= K:175) \/ __cost':169 = (mid___cost:172 + K:175))
         /\ ((K:175 = 0 /\ mid_n:174 = n':167 /\ mid_flag:173 = flag':168
                /\ mid___cost:172 = __cost':169)
               \/ (1 <= K:175 /\ (-1 + mid_flag:173) = 0 /\ 0 <= -mid_n:174
                     /\ 0 <= mid___cost:172 /\ flag':168 = 0 /\ 0 <= -n':167
                     /\ 0 <= (-1 + __cost':169)))
         /\ (0 = K:175 \/ mid_n:174 <= 0) /\ (K:171 + K:175) = K:170
         /\ 0 <= K:170 /\ flag':168 <= 1 /\ 0 <= flag':168 /\ flag':168 <= 0)}

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

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

Variable bounds at line 22 in run

(1 + n + __cost) <= __cost
__cost is o(n)

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