/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, 34> -> <Unique State Name, 45>	Base relation: 
{__cost := (__cost:63 + 1)
 tmp := havoc:71
 when (0 < n:62 /\ 0 <= __cost:63 /\ 0 <= (__cost:63 + 1))}	
<Unique State Name, 34> -> <Unique State Name, 52>	Base relation: 
{when n:62 <= 0}	
<Unique State Name, 17> -> <Unique State Name, 68>	Base relation: 
{return := havoc:41
 return@pos := type_err:44
 return@width := type_err:45}	
<Unique State Name, 15> -> <Unique State Name, 66>	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
<Unique State Name, 21> -> <Unique State Name, 71>	Base relation: 
{}	
<Unique State Name, 52> -> <Unique State Name, 21>	Base relation: 
{}	
<Unique State Name, 65> -> <Unique State Name, 69>	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, 63> -> <Unique State Name, 62>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
<Unique State Name, 69> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 61> -> <Unique State Name, 17>	Base relation: 
{}	
<Unique State Name, 67> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 45> -> <Unique State Name, 30>	Base relation: 
{n := (n:62 + -1)
 when tmp:65 = 0}	
<Unique State Name, 45> -> <Unique State Name, 52>	Base relation: 
{when !(tmp:65 = 0)}	
<Unique State Name, 68> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 70> -> <Unique State Name, 34>	Base relation: 
{}	
<Unique State Name, 62> -> <Unique State Name, 59 61>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 59> -> <Unique State Name, 21>	Base relation: 
{n := param0:53}	
<Unique State Name, 71> -> <Unique State Name, 25>	Base relation: 
{}	
<Unique State Name, 66> -> <Unique State Name, 63 65>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 30> -> <Unique State Name, 70>	Base relation: 
{when 0 <= n:62}	
<Unique State Name, 25> -> <Unique State Name, 30>	Base relation: 
{n := (n:62 + -1)
 when 0 < n:62}	
<Unique State Name, 25> -> <Unique State Name, 67>	Base relation: 
{return := havoc:72
 return@pos := type_err:73
 return@width := type_err:74
 when n:62 <= 0}	
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:63 + 1)
 tmp := havoc:117
 n := (n:62 + -1)
 when (0 <= n:62 /\ 0 < n:62 /\ 0 <= __cost:63 /\ 0 <= (__cost:63 + 1)
         /\ havoc:117 = 0)}
**** alpha hat: 
  {<Split [true
            (tmp':119) = 0
           (n':120) = (1)*(n:62) + (-1)*1
           (__cost':118) = (1)*(__cost:63) + 1
           }
          pre:
            [|__cost:63>=0; n:62-1>=0|]
          post:
            [|tmp':119=0; n':120>=0; __cost':118-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':118
   tmp := tmp':119
   n := n':120
   when ((!((0 <= K:131 /\ K:131 <= 0)) \/ mid_tmp:134 = tmp:65)
           /\ (!(1 <= K:131) \/ mid_tmp:134 = 0)
           /\ (!(0 <= K:131) \/ mid_n:133 = (n:62 + -K:131))
           /\ (!(0 <= K:131) \/ mid___cost:135 = (__cost:63 + K:131))
           /\ ((K:131 = 0 /\ n:62 = mid_n:133 /\ tmp:65 = mid_tmp:134
                  /\ __cost:63 = mid___cost:135)
                 \/ (1 <= K:131 /\ 0 <= __cost:63 /\ 0 <= (-1 + n:62)
                       /\ mid_tmp:134 = 0 /\ 0 <= mid_n:133
                       /\ 0 <= (-1 + mid___cost:135))) /\ K:132 = 0
           /\ mid_n:133 = n':120 /\ mid_tmp:134 = tmp':119
           /\ mid___cost:135 = __cost':118 /\ 0 = K:132
           /\ (K:131 + K:132) = K:130 /\ 0 <= K:130)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := phi___cost:147
 tmp := phi_tmp:148
 n := n':141
 when (0 < n:62 /\ (!((0 <= K:136 /\ K:136 <= 0)) \/ mid_tmp:137 = tmp:65)
         /\ (!(1 <= K:136) \/ mid_tmp:137 = 0)
         /\ (!(0 <= K:136) \/ mid_n:138 = ((n:62 + -1) + -K:136))
         /\ (!(0 <= K:136) \/ mid___cost:139 = (__cost:63 + K:136))
         /\ ((K:136 = 0 /\ (n:62 + -1) = mid_n:138 /\ tmp:65 = mid_tmp:137
                /\ __cost:63 = mid___cost:139)
               \/ (1 <= K:136 /\ 0 <= __cost:63 /\ 0 <= (-1 + (n:62 + -1))
                     /\ mid_tmp:137 = 0 /\ 0 <= mid_n:138
                     /\ 0 <= (-1 + mid___cost:139))) /\ K:140 = 0
         /\ mid_n:138 = n':141 /\ mid_tmp:137 = tmp':142
         /\ mid___cost:139 = __cost':143 /\ 0 = K:140
         /\ (K:136 + K:140) = K:144 /\ 0 <= K:144 /\ 0 <= n':141
         /\ ((n':141 <= 0 /\ __cost':143 = phi___cost:147
                /\ tmp':142 = phi_tmp:148)
               \/ (0 < n':141 /\ 0 <= __cost':143 /\ 0 <= (__cost':143 + 1)
                     /\ !(havoc:149 = 0)
                     /\ (__cost':143 + 1) = phi___cost:147
                     /\ havoc:149 = phi_tmp:148)))}
**** alpha hat: 
  {<Split [(2 + -n:62) <= 0
            ((__cost':118 + n':120)) <= (1)*((__cost:63 + n:62)) + 0
           (-__cost':118) <= (1)*(-__cost:63) + (-1)*1
           ((-__cost':118 + -n':120)) <= (1)*((-__cost:63 + -n:62)) + 1
           }
          pre:
            [|__cost:63>=0; n:62-2>=0|]
          post:
            [|__cost':118-1>=0; n':120>=0|]
           (__cost':118) = (1)*(__cost:63) + 0
          (tmp':119) = (1)*(tmp:65) + 0
          (n':120) = 0
          }
  pre:
    [|n:62-1=0|]
  post:
    [|n':120=0|]],
[!(-__cost:63 <= 0)
  (__cost':118) = (1)*(__cost:63) + 0
 (tmp':119) = (1)*(tmp:65) + 0
 (n':120) = 0
 } pre:   [|n:62-1=0; -__cost:63-1>=0|] post:
  [|n':120=0; -__cost':118-1>=0|]
 ((__cost':118 + n':120)) <= (1)*((__cost:63 + n:62)) + 0
(n':120) <= (1)*(n:62) + (-1)*1
((-__cost':118 + -n':120)) <= (1)*((-__cost:63 + -n:62)) + 1 } pre:
  [|__cost:63>=0; n:62-1>=0|] post:
  [|__cost':118>=0; n':120>=0|]]>}
**** star transition: 
  {__cost := __cost':118
   tmp := tmp':119
   n := n':120
   when ((!(0 <= K:169) \/ (mid___cost:173 + mid_n:171) <= (__cost:63 + n:62))
           /\ (!(0 <= K:169) \/ -mid___cost:173 <= (-__cost:63 + -K:169))
           /\ (!(0 <= K:169)
                 \/ (-mid___cost:173 + -mid_n:171) <= ((-__cost:63 + -n:62)
                                                         + K:169))
           /\ ((K:169 = 0 /\ n:62 = mid_n:171 /\ tmp:65 = mid_tmp:172
                  /\ __cost:63 = mid___cost:173)
                 \/ (1 <= K:169 /\ 0 <= __cost:63 /\ 0 <= (-2 + n:62)
                       /\ 0 <= (-1 + mid___cost:173) /\ 0 <= mid_n:171))
           /\ (0 = K:169 \/ (2 + -n:62) <= 0)
           /\ (!(0 <= K:170) \/ __cost':118 = mid___cost:173)
           /\ (!(0 <= K:170) \/ tmp':119 = mid_tmp:172)
           /\ (!((0 <= K:170 /\ K:170 <= 0)) \/ n':120 = mid_n:171)
           /\ (!(1 <= K:170) \/ n':120 = 0)
           /\ ((K:170 = 0 /\ mid_n:171 = n':120 /\ mid_tmp:172 = tmp':119
                  /\ mid___cost:173 = __cost':118)
                 \/ (1 <= K:170 /\ (-1 + mid_n:171) = 0 /\ n':120 = 0))
           /\ (0 = K:170 \/ !((2 + -mid_n:171) <= 0))
           /\ (K:169 + K:170) = K:168
           /\ (!(0 <= K:174) \/ mid___cost:178 = __cost:63)
           /\ (!(0 <= K:174) \/ mid_tmp:177 = tmp:65)
           /\ (!((0 <= K:174 /\ K:174 <= 0)) \/ mid_n:176 = n:62)
           /\ (!(1 <= K:174) \/ mid_n:176 = 0)
           /\ ((K:174 = 0 /\ n:62 = mid_n:176 /\ tmp:65 = mid_tmp:177
                  /\ __cost:63 = mid___cost:178)
                 \/ (1 <= K:174 /\ (-1 + n:62) = 0 /\ 0 <= (-1 + -__cost:63)
                       /\ mid_n:176 = 0 /\ 0 <= (-1 + -mid___cost:178)))
           /\ (0 = K:174 \/ !(-__cost:63 <= 0))
           /\ (!(0 <= K:175)
                 \/ (__cost':118 + n':120) <= (mid___cost:178 + mid_n:176))
           /\ (!(0 <= K:175) \/ n':120 <= (mid_n:176 + -K:175))
           /\ (!(0 <= K:175)
                 \/ (-__cost':118 + -n':120) <= ((-mid___cost:178
                                                    + -mid_n:176) + K:175))
           /\ ((K:175 = 0 /\ mid_n:176 = n':120 /\ mid_tmp:177 = tmp':119
                  /\ mid___cost:178 = __cost':118)
                 \/ (1 <= K:175 /\ 0 <= mid___cost:178
                       /\ 0 <= (-1 + mid_n:176) /\ 0 <= __cost':118
                       /\ 0 <= n':120))
           /\ (0 = K:175 \/ -mid___cost:178 <= 0) /\ (K:174 + K:175) = K:168
           /\ 0 <= K:168)}
}
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:54
       param0@width := type_err:55}    )
    ,
    Var(20)
  )
  ,
  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=20: 
Weight(Base relation: 
  {__cost := __cost':184
   tmp := tmp':185
   n := n':186
   return := havoc:224
   return@pos := type_err:225
   return@width := type_err:226
   when ((!(0 <= K:179)
            \/ (mid___cost:180 + mid_n:181) <= (__cost:63 + param0:53))
           /\ (!(0 <= K:179) \/ -mid___cost:180 <= (-__cost:63 + -K:179))
           /\ (!(0 <= K:179)
                 \/ (-mid___cost:180 + -mid_n:181) <= ((-__cost:63
                                                          + -param0:53)
                                                         + K:179))
           /\ ((K:179 = 0 /\ param0:53 = mid_n:181 /\ tmp:65 = mid_tmp:182
                  /\ __cost:63 = mid___cost:180)
                 \/ (1 <= K:179 /\ 0 <= __cost:63 /\ 0 <= (-2 + param0:53)
                       /\ 0 <= (-1 + mid___cost:180) /\ 0 <= mid_n:181))
           /\ (0 = K:179 \/ (2 + -param0:53) <= 0)
           /\ (!(0 <= K:183) \/ __cost':184 = mid___cost:180)
           /\ (!(0 <= K:183) \/ tmp':185 = mid_tmp:182)
           /\ (!((0 <= K:183 /\ K:183 <= 0)) \/ n':186 = mid_n:181)
           /\ (!(1 <= K:183) \/ n':186 = 0)
           /\ ((K:183 = 0 /\ mid_n:181 = n':186 /\ mid_tmp:182 = tmp':185
                  /\ mid___cost:180 = __cost':184)
                 \/ (1 <= K:183 /\ (-1 + mid_n:181) = 0 /\ n':186 = 0))
           /\ (0 = K:183 \/ !((2 + -mid_n:181) <= 0))
           /\ (K:179 + K:183) = K:187
           /\ (!(0 <= K:188) \/ mid___cost:189 = __cost:63)
           /\ (!(0 <= K:188) \/ mid_tmp:190 = tmp:65)
           /\ (!((0 <= K:188 /\ K:188 <= 0)) \/ mid_n:191 = param0:53)
           /\ (!(1 <= K:188) \/ mid_n:191 = 0)
           /\ ((K:188 = 0 /\ param0:53 = mid_n:191 /\ tmp:65 = mid_tmp:190
                  /\ __cost:63 = mid___cost:189)
                 \/ (1 <= K:188 /\ (-1 + param0:53) = 0
                       /\ 0 <= (-1 + -__cost:63) /\ mid_n:191 = 0
                       /\ 0 <= (-1 + -mid___cost:189)))
           /\ (0 = K:188 \/ !(-__cost:63 <= 0))
           /\ (!(0 <= K:192)
                 \/ (__cost':184 + n':186) <= (mid___cost:189 + mid_n:191))
           /\ (!(0 <= K:192) \/ n':186 <= (mid_n:191 + -K:192))
           /\ (!(0 <= K:192)
                 \/ (-__cost':184 + -n':186) <= ((-mid___cost:189
                                                    + -mid_n:191) + K:192))
           /\ ((K:192 = 0 /\ mid_n:191 = n':186 /\ mid_tmp:190 = tmp':185
                  /\ mid___cost:189 = __cost':184)
                 \/ (1 <= K:192 /\ 0 <= mid___cost:189
                       /\ 0 <= (-1 + mid_n:191) /\ 0 <= __cost':184
                       /\ 0 <= n':186))
           /\ (0 = K:192 \/ -mid___cost:189 <= 0) /\ (K:188 + K:192) = K:187
           /\ 0 <= K:187 /\ n':186 <= 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(20)
    )
    ,
    Weight(Base relation: 
      {return := havoc:41
       return@pos := type_err:44
       return@width := type_err:45}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':184
   return := havoc:224
   return@pos := type_err:225
   return@width := type_err:226
   when ((!(0 <= K:179)
            \/ (mid___cost:180 + mid_n:181) <= (__cost:63 + param0:53))
           /\ (!(0 <= K:179) \/ -mid___cost:180 <= (-__cost:63 + -K:179))
           /\ (!(0 <= K:179)
                 \/ (-mid___cost:180 + -mid_n:181) <= ((-__cost:63
                                                          + -param0:53)
                                                         + K:179))
           /\ ((K:179 = 0 /\ param0:53 = mid_n:181 /\ tmp:227 = mid_tmp:182
                  /\ __cost:63 = mid___cost:180)
                 \/ (1 <= K:179 /\ 0 <= __cost:63 /\ 0 <= (-2 + param0:53)
                       /\ 0 <= (-1 + mid___cost:180) /\ 0 <= mid_n:181))
           /\ (0 = K:179 \/ (2 + -param0:53) <= 0)
           /\ (!(0 <= K:183) \/ __cost':184 = mid___cost:180)
           /\ (!(0 <= K:183) \/ tmp':185 = mid_tmp:182)
           /\ (!((0 <= K:183 /\ K:183 <= 0)) \/ n':186 = mid_n:181)
           /\ (!(1 <= K:183) \/ n':186 = 0)
           /\ ((K:183 = 0 /\ mid_n:181 = n':186 /\ mid_tmp:182 = tmp':185
                  /\ mid___cost:180 = __cost':184)
                 \/ (1 <= K:183 /\ (-1 + mid_n:181) = 0 /\ n':186 = 0))
           /\ (0 = K:183 \/ !((2 + -mid_n:181) <= 0))
           /\ (K:179 + K:183) = K:187
           /\ (!(0 <= K:188) \/ mid___cost:189 = __cost:63)
           /\ (!(0 <= K:188) \/ mid_tmp:190 = tmp:227)
           /\ (!((0 <= K:188 /\ K:188 <= 0)) \/ mid_n:191 = param0:53)
           /\ (!(1 <= K:188) \/ mid_n:191 = 0)
           /\ ((K:188 = 0 /\ param0:53 = mid_n:191 /\ tmp:227 = mid_tmp:190
                  /\ __cost:63 = mid___cost:189)
                 \/ (1 <= K:188 /\ (-1 + param0:53) = 0
                       /\ 0 <= (-1 + -__cost:63) /\ mid_n:191 = 0
                       /\ 0 <= (-1 + -mid___cost:189)))
           /\ (0 = K:188 \/ !(-__cost:63 <= 0))
           /\ (!(0 <= K:192)
                 \/ (__cost':184 + n':186) <= (mid___cost:189 + mid_n:191))
           /\ (!(0 <= K:192) \/ n':186 <= (mid_n:191 + -K:192))
           /\ (!(0 <= K:192)
                 \/ (-__cost':184 + -n':186) <= ((-mid___cost:189
                                                    + -mid_n:191) + K:192))
           /\ ((K:192 = 0 /\ mid_n:191 = n':186 /\ mid_tmp:190 = tmp':185
                  /\ mid___cost:189 = __cost':184)
                 \/ (1 <= K:192 /\ 0 <= mid___cost:189
                       /\ 0 <= (-1 + mid_n:191) /\ 0 <= __cost':184
                       /\ 0 <= n':186))
           /\ (0 = K:192 \/ -mid___cost:189 <= 0) /\ (K:188 + K:192) = K:187
           /\ 0 <= K:187 /\ n':186 <= 0)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':255
   return := 0
   param0 := havoc:13
   return@pos := type_err:270
   param0@pos := type_err:266
   return@width := type_err:271
   param0@width := type_err:268
   when ((!(0 <= K:249) \/ (mid___cost:250 + mid_n:251) <= havoc:13)
           /\ (!(0 <= K:249) \/ -mid___cost:250 <= -K:249)
           /\ (!(0 <= K:249)
                 \/ (-mid___cost:250 + -mid_n:251) <= (-havoc:13 + K:249))
           /\ ((K:249 = 0 /\ havoc:13 = mid_n:251 /\ tmp:252 = mid_tmp:253
                  /\ 0 = mid___cost:250)
                 \/ (1 <= K:249 /\ 0 <= (-2 + havoc:13)
                       /\ 0 <= (-1 + mid___cost:250) /\ 0 <= mid_n:251))
           /\ (0 = K:249 \/ (2 + -havoc:13) <= 0)
           /\ (!(0 <= K:254) \/ __cost':255 = mid___cost:250)
           /\ (!(0 <= K:254) \/ tmp':256 = mid_tmp:253)
           /\ (!((0 <= K:254 /\ K:254 <= 0)) \/ n':257 = mid_n:251)
           /\ (!(1 <= K:254) \/ n':257 = 0)
           /\ ((K:254 = 0 /\ mid_n:251 = n':257 /\ mid_tmp:253 = tmp':256
                  /\ mid___cost:250 = __cost':255)
                 \/ (1 <= K:254 /\ (-1 + mid_n:251) = 0 /\ n':257 = 0))
           /\ (0 = K:254 \/ !((2 + -mid_n:251) <= 0))
           /\ (K:249 + K:254) = K:258
           /\ (!(0 <= K:259) \/ mid___cost:260 = 0)
           /\ (!(0 <= K:259) \/ mid_tmp:261 = tmp:252)
           /\ (!((0 <= K:259 /\ K:259 <= 0)) \/ mid_n:262 = havoc:13)
           /\ (!(1 <= K:259) \/ mid_n:262 = 0) /\ K:259 = 0
           /\ havoc:13 = mid_n:262 /\ tmp:252 = mid_tmp:261
           /\ 0 = mid___cost:260 /\ 0 = K:259
           /\ (!(0 <= K:263)
                 \/ (__cost':255 + n':257) <= (mid___cost:260 + mid_n:262))
           /\ (!(0 <= K:263) \/ n':257 <= (mid_n:262 + -K:263))
           /\ (!(0 <= K:263)
                 \/ (-__cost':255 + -n':257) <= ((-mid___cost:260
                                                    + -mid_n:262) + K:263))
           /\ ((K:263 = 0 /\ mid_n:262 = n':257 /\ mid_tmp:261 = tmp':256
                  /\ mid___cost:260 = __cost':255)
                 \/ (1 <= K:263 /\ 0 <= mid___cost:260
                       /\ 0 <= (-1 + mid_n:262) /\ 0 <= __cost':255
                       /\ 0 <= n':257))
           /\ (0 = K:263 \/ -mid___cost:260 <= 0) /\ (K:259 + K:263) = K:258
           /\ 0 <= K:258 /\ n':257 <= 0
           /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:269)
                 \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:269)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':278
   return := havoc:290
   param0 := param0:53
   return@pos := type_err:291
   param0@pos := type_err:54
   return@width := type_err:292
   param0@width := type_err:55
   when ((!(0 <= K:272)
            \/ (mid___cost:273 + mid_n:274) <= (__cost:63 + param0:53))
           /\ (!(0 <= K:272) \/ -mid___cost:273 <= (-__cost:63 + -K:272))
           /\ (!(0 <= K:272)
                 \/ (-mid___cost:273 + -mid_n:274) <= ((-__cost:63
                                                          + -param0:53)
                                                         + K:272))
           /\ ((K:272 = 0 /\ param0:53 = mid_n:274 /\ tmp:275 = mid_tmp:276
                  /\ __cost:63 = mid___cost:273)
                 \/ (1 <= K:272 /\ 0 <= __cost:63 /\ 0 <= (-2 + param0:53)
                       /\ 0 <= (-1 + mid___cost:273) /\ 0 <= mid_n:274))
           /\ (0 = K:272 \/ (2 + -param0:53) <= 0)
           /\ (!(0 <= K:277) \/ __cost':278 = mid___cost:273)
           /\ (!(0 <= K:277) \/ tmp':279 = mid_tmp:276)
           /\ (!((0 <= K:277 /\ K:277 <= 0)) \/ n':280 = mid_n:274)
           /\ (!(1 <= K:277) \/ n':280 = 0)
           /\ ((K:277 = 0 /\ mid_n:274 = n':280 /\ mid_tmp:276 = tmp':279
                  /\ mid___cost:273 = __cost':278)
                 \/ (1 <= K:277 /\ (-1 + mid_n:274) = 0 /\ n':280 = 0))
           /\ (0 = K:277 \/ !((2 + -mid_n:274) <= 0))
           /\ (K:272 + K:277) = K:281
           /\ (!(0 <= K:282) \/ mid___cost:283 = __cost:63)
           /\ (!(0 <= K:282) \/ mid_tmp:284 = tmp:275)
           /\ (!((0 <= K:282 /\ K:282 <= 0)) \/ mid_n:285 = param0:53)
           /\ (!(1 <= K:282) \/ mid_n:285 = 0)
           /\ ((K:282 = 0 /\ param0:53 = mid_n:285 /\ tmp:275 = mid_tmp:284
                  /\ __cost:63 = mid___cost:283)
                 \/ (1 <= K:282 /\ (-1 + param0:53) = 0
                       /\ 0 <= (-1 + -__cost:63) /\ mid_n:285 = 0
                       /\ 0 <= (-1 + -mid___cost:283)))
           /\ (0 = K:282 \/ !(-__cost:63 <= 0))
           /\ (!(0 <= K:286)
                 \/ (__cost':278 + n':280) <= (mid___cost:283 + mid_n:285))
           /\ (!(0 <= K:286) \/ n':280 <= (mid_n:285 + -K:286))
           /\ (!(0 <= K:286)
                 \/ (-__cost':278 + -n':280) <= ((-mid___cost:283
                                                    + -mid_n:285) + K:286))
           /\ ((K:286 = 0 /\ mid_n:285 = n':280 /\ mid_tmp:284 = tmp':279
                  /\ mid___cost:283 = __cost':278)
                 \/ (1 <= K:286 /\ 0 <= mid___cost:283
                       /\ 0 <= (-1 + mid_n:285) /\ 0 <= __cost':278
                       /\ 0 <= n':280))
           /\ (0 = K:286 \/ -mid___cost:283 <= 0) /\ (K:282 + K:286) = K:281
           /\ 0 <= K:281 /\ n':280 <= 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=20: 
Weight(Base relation: 
  {__cost := __cost':184
   return := havoc:224
   return@pos := type_err:225
   return@width := type_err:226
   when ((!(0 <= K:179)
            \/ (mid___cost:180 + mid_n:181) <= (__cost:63 + param0:53))
           /\ (!(0 <= K:179) \/ -mid___cost:180 <= (-__cost:63 + -K:179))
           /\ (!(0 <= K:179)
                 \/ (-mid___cost:180 + -mid_n:181) <= ((-__cost:63
                                                          + -param0:53)
                                                         + K:179))
           /\ ((K:179 = 0 /\ param0:53 = mid_n:181 /\ tmp:227 = mid_tmp:182
                  /\ __cost:63 = mid___cost:180)
                 \/ (1 <= K:179 /\ 0 <= __cost:63 /\ 0 <= (-2 + param0:53)
                       /\ 0 <= (-1 + mid___cost:180) /\ 0 <= mid_n:181))
           /\ (0 = K:179 \/ (2 + -param0:53) <= 0)
           /\ (!(0 <= K:183) \/ __cost':184 = mid___cost:180)
           /\ (!(0 <= K:183) \/ tmp':185 = mid_tmp:182)
           /\ (!((0 <= K:183 /\ K:183 <= 0)) \/ n':186 = mid_n:181)
           /\ (!(1 <= K:183) \/ n':186 = 0)
           /\ ((K:183 = 0 /\ mid_n:181 = n':186 /\ mid_tmp:182 = tmp':185
                  /\ mid___cost:180 = __cost':184)
                 \/ (1 <= K:183 /\ (-1 + mid_n:181) = 0 /\ n':186 = 0))
           /\ (0 = K:183 \/ !((2 + -mid_n:181) <= 0))
           /\ (K:179 + K:183) = K:187
           /\ (!(0 <= K:188) \/ mid___cost:189 = __cost:63)
           /\ (!(0 <= K:188) \/ mid_tmp:190 = tmp:227)
           /\ (!((0 <= K:188 /\ K:188 <= 0)) \/ mid_n:191 = param0:53)
           /\ (!(1 <= K:188) \/ mid_n:191 = 0)
           /\ ((K:188 = 0 /\ param0:53 = mid_n:191 /\ tmp:227 = mid_tmp:190
                  /\ __cost:63 = mid___cost:189)
                 \/ (1 <= K:188 /\ (-1 + param0:53) = 0
                       /\ 0 <= (-1 + -__cost:63) /\ mid_n:191 = 0
                       /\ 0 <= (-1 + -mid___cost:189)))
           /\ (0 = K:188 \/ !(-__cost:63 <= 0))
           /\ (!(0 <= K:192)
                 \/ (__cost':184 + n':186) <= (mid___cost:189 + mid_n:191))
           /\ (!(0 <= K:192) \/ n':186 <= (mid_n:191 + -K:192))
           /\ (!(0 <= K:192)
                 \/ (-__cost':184 + -n':186) <= ((-mid___cost:189
                                                    + -mid_n:191) + K:192))
           /\ ((K:192 = 0 /\ mid_n:191 = n':186 /\ mid_tmp:190 = tmp':185
                  /\ mid___cost:189 = __cost':184)
                 \/ (1 <= K:192 /\ 0 <= mid___cost:189
                       /\ 0 <= (-1 + mid_n:191) /\ 0 <= __cost':184
                       /\ 0 <= n':186))
           /\ (0 = K:192 \/ -mid___cost:189 <= 0) /\ (K:188 + K:192) = K:187
           /\ 0 <= K:187 /\ n':186 <= 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':255
 return := 0
 param0 := havoc:13
 return@pos := type_err:270
 param0@pos := type_err:266
 return@width := type_err:271
 param0@width := type_err:268
 when ((!(0 <= K:249) \/ (mid___cost:250 + mid_n:251) <= havoc:13)
         /\ (!(0 <= K:249) \/ -mid___cost:250 <= -K:249)
         /\ (!(0 <= K:249)
               \/ (-mid___cost:250 + -mid_n:251) <= (-havoc:13 + K:249))
         /\ ((K:249 = 0 /\ havoc:13 = mid_n:251 /\ tmp:252 = mid_tmp:253
                /\ 0 = mid___cost:250)
               \/ (1 <= K:249 /\ 0 <= (-2 + havoc:13)
                     /\ 0 <= (-1 + mid___cost:250) /\ 0 <= mid_n:251))
         /\ (0 = K:249 \/ (2 + -havoc:13) <= 0)
         /\ (!(0 <= K:254) \/ __cost':255 = mid___cost:250)
         /\ (!(0 <= K:254) \/ tmp':256 = mid_tmp:253)
         /\ (!((0 <= K:254 /\ K:254 <= 0)) \/ n':257 = mid_n:251)
         /\ (!(1 <= K:254) \/ n':257 = 0)
         /\ ((K:254 = 0 /\ mid_n:251 = n':257 /\ mid_tmp:253 = tmp':256
                /\ mid___cost:250 = __cost':255)
               \/ (1 <= K:254 /\ (-1 + mid_n:251) = 0 /\ n':257 = 0))
         /\ (0 = K:254 \/ !((2 + -mid_n:251) <= 0))
         /\ (K:249 + K:254) = K:258 /\ (!(0 <= K:259) \/ mid___cost:260 = 0)
         /\ (!(0 <= K:259) \/ mid_tmp:261 = tmp:252)
         /\ (!((0 <= K:259 /\ K:259 <= 0)) \/ mid_n:262 = havoc:13)
         /\ (!(1 <= K:259) \/ mid_n:262 = 0) /\ K:259 = 0
         /\ havoc:13 = mid_n:262 /\ tmp:252 = mid_tmp:261
         /\ 0 = mid___cost:260 /\ 0 = K:259
         /\ (!(0 <= K:263)
               \/ (__cost':255 + n':257) <= (mid___cost:260 + mid_n:262))
         /\ (!(0 <= K:263) \/ n':257 <= (mid_n:262 + -K:263))
         /\ (!(0 <= K:263)
               \/ (-__cost':255 + -n':257) <= ((-mid___cost:260 + -mid_n:262)
                                                 + K:263))
         /\ ((K:263 = 0 /\ mid_n:262 = n':257 /\ mid_tmp:261 = tmp':256
                /\ mid___cost:260 = __cost':255)
               \/ (1 <= K:263 /\ 0 <= mid___cost:260 /\ 0 <= (-1 + mid_n:262)
                     /\ 0 <= __cost':255 /\ 0 <= n':257))
         /\ (0 = K:263 \/ -mid___cost:260 <= 0) /\ (K:259 + K:263) = K:258
         /\ 0 <= K:258 /\ n':257 <= 0
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:269)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:269)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':278
 return := havoc:290
 param0 := param0:53
 return@pos := type_err:291
 param0@pos := type_err:54
 return@width := type_err:292
 param0@width := type_err:55
 when ((!(0 <= K:272)
          \/ (mid___cost:273 + mid_n:274) <= (__cost:63 + param0:53))
         /\ (!(0 <= K:272) \/ -mid___cost:273 <= (-__cost:63 + -K:272))
         /\ (!(0 <= K:272)
               \/ (-mid___cost:273 + -mid_n:274) <= ((-__cost:63 + -param0:53)
                                                       + K:272))
         /\ ((K:272 = 0 /\ param0:53 = mid_n:274 /\ tmp:275 = mid_tmp:276
                /\ __cost:63 = mid___cost:273)
               \/ (1 <= K:272 /\ 0 <= __cost:63 /\ 0 <= (-2 + param0:53)
                     /\ 0 <= (-1 + mid___cost:273) /\ 0 <= mid_n:274))
         /\ (0 = K:272 \/ (2 + -param0:53) <= 0)
         /\ (!(0 <= K:277) \/ __cost':278 = mid___cost:273)
         /\ (!(0 <= K:277) \/ tmp':279 = mid_tmp:276)
         /\ (!((0 <= K:277 /\ K:277 <= 0)) \/ n':280 = mid_n:274)
         /\ (!(1 <= K:277) \/ n':280 = 0)
         /\ ((K:277 = 0 /\ mid_n:274 = n':280 /\ mid_tmp:276 = tmp':279
                /\ mid___cost:273 = __cost':278)
               \/ (1 <= K:277 /\ (-1 + mid_n:274) = 0 /\ n':280 = 0))
         /\ (0 = K:277 \/ !((2 + -mid_n:274) <= 0))
         /\ (K:272 + K:277) = K:281
         /\ (!(0 <= K:282) \/ mid___cost:283 = __cost:63)
         /\ (!(0 <= K:282) \/ mid_tmp:284 = tmp:275)
         /\ (!((0 <= K:282 /\ K:282 <= 0)) \/ mid_n:285 = param0:53)
         /\ (!(1 <= K:282) \/ mid_n:285 = 0)
         /\ ((K:282 = 0 /\ param0:53 = mid_n:285 /\ tmp:275 = mid_tmp:284
                /\ __cost:63 = mid___cost:283)
               \/ (1 <= K:282 /\ (-1 + param0:53) = 0
                     /\ 0 <= (-1 + -__cost:63) /\ mid_n:285 = 0
                     /\ 0 <= (-1 + -mid___cost:283)))
         /\ (0 = K:282 \/ !(-__cost:63 <= 0))
         /\ (!(0 <= K:286)
               \/ (__cost':278 + n':280) <= (mid___cost:283 + mid_n:285))
         /\ (!(0 <= K:286) \/ n':280 <= (mid_n:285 + -K:286))
         /\ (!(0 <= K:286)
               \/ (-__cost':278 + -n':280) <= ((-mid___cost:283 + -mid_n:285)
                                                 + K:286))
         /\ ((K:286 = 0 /\ mid_n:285 = n':280 /\ mid_tmp:284 = tmp':279
                /\ mid___cost:283 = __cost':278)
               \/ (1 <= K:286 /\ 0 <= mid___cost:283 /\ 0 <= (-1 + mid_n:285)
                     /\ 0 <= __cost':278 /\ 0 <= n':280))
         /\ (0 = K:286 \/ -mid___cost:283 <= 0) /\ (K:282 + K:286) = K:281
         /\ 0 <= K:281 /\ n':280 <= 0)}

Evaluating variable number 20 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':184
 return := havoc:224
 return@pos := type_err:225
 return@width := type_err:226
 when ((!(0 <= K:179)
          \/ (mid___cost:180 + mid_n:181) <= (__cost:63 + param0:53))
         /\ (!(0 <= K:179) \/ -mid___cost:180 <= (-__cost:63 + -K:179))
         /\ (!(0 <= K:179)
               \/ (-mid___cost:180 + -mid_n:181) <= ((-__cost:63 + -param0:53)
                                                       + K:179))
         /\ ((K:179 = 0 /\ param0:53 = mid_n:181 /\ tmp:227 = mid_tmp:182
                /\ __cost:63 = mid___cost:180)
               \/ (1 <= K:179 /\ 0 <= __cost:63 /\ 0 <= (-2 + param0:53)
                     /\ 0 <= (-1 + mid___cost:180) /\ 0 <= mid_n:181))
         /\ (0 = K:179 \/ (2 + -param0:53) <= 0)
         /\ (!(0 <= K:183) \/ __cost':184 = mid___cost:180)
         /\ (!(0 <= K:183) \/ tmp':185 = mid_tmp:182)
         /\ (!((0 <= K:183 /\ K:183 <= 0)) \/ n':186 = mid_n:181)
         /\ (!(1 <= K:183) \/ n':186 = 0)
         /\ ((K:183 = 0 /\ mid_n:181 = n':186 /\ mid_tmp:182 = tmp':185
                /\ mid___cost:180 = __cost':184)
               \/ (1 <= K:183 /\ (-1 + mid_n:181) = 0 /\ n':186 = 0))
         /\ (0 = K:183 \/ !((2 + -mid_n:181) <= 0))
         /\ (K:179 + K:183) = K:187
         /\ (!(0 <= K:188) \/ mid___cost:189 = __cost:63)
         /\ (!(0 <= K:188) \/ mid_tmp:190 = tmp:227)
         /\ (!((0 <= K:188 /\ K:188 <= 0)) \/ mid_n:191 = param0:53)
         /\ (!(1 <= K:188) \/ mid_n:191 = 0)
         /\ ((K:188 = 0 /\ param0:53 = mid_n:191 /\ tmp:227 = mid_tmp:190
                /\ __cost:63 = mid___cost:189)
               \/ (1 <= K:188 /\ (-1 + param0:53) = 0
                     /\ 0 <= (-1 + -__cost:63) /\ mid_n:191 = 0
                     /\ 0 <= (-1 + -mid___cost:189)))
         /\ (0 = K:188 \/ !(-__cost:63 <= 0))
         /\ (!(0 <= K:192)
               \/ (__cost':184 + n':186) <= (mid___cost:189 + mid_n:191))
         /\ (!(0 <= K:192) \/ n':186 <= (mid_n:191 + -K:192))
         /\ (!(0 <= K:192)
               \/ (-__cost':184 + -n':186) <= ((-mid___cost:189 + -mid_n:191)
                                                 + K:192))
         /\ ((K:192 = 0 /\ mid_n:191 = n':186 /\ mid_tmp:190 = tmp':185
                /\ mid___cost:189 = __cost':184)
               \/ (1 <= K:192 /\ 0 <= mid___cost:189 /\ 0 <= (-1 + mid_n:191)
                     /\ 0 <= __cost':184 /\ 0 <= n':186))
         /\ (0 = K:192 \/ -mid___cost:189 <= 0) /\ (K:188 + K:192) = K:187
         /\ 0 <= K:187 /\ n':186 <= 0)}

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

NumRnds: 1

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

Weights on states: 
__done 0x52a7ed0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x5c702e0: 
	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,63)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}
    ( __pstate , (Unique State Name,59)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:337
 param0@width := type_err:338}

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

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

Base relation: 
{__cost := __cost':299
 n := havoc:13
 return := 0
 param0 := havoc:13
 return@pos := type_err:314
 param0@pos := type_err:310
 return@width := type_err:315
 param0@width := type_err:312
 when ((!(0 <= K:293) \/ (mid___cost:294 + mid_n:295) <= havoc:13)
         /\ (!(0 <= K:293) \/ -mid___cost:294 <= -K:293)
         /\ (!(0 <= K:293)
               \/ (-mid___cost:294 + -mid_n:295) <= (-havoc:13 + K:293))
         /\ ((K:293 = 0 /\ havoc:13 = mid_n:295 /\ tmp:296 = mid_tmp:297
                /\ 0 = mid___cost:294)
               \/ (1 <= K:293 /\ 0 <= (-2 + havoc:13)
                     /\ 0 <= (-1 + mid___cost:294) /\ 0 <= mid_n:295))
         /\ (0 = K:293 \/ (2 + -havoc:13) <= 0)
         /\ (!(0 <= K:298) \/ __cost':299 = mid___cost:294)
         /\ (!(0 <= K:298) \/ tmp':300 = mid_tmp:297)
         /\ (!((0 <= K:298 /\ K:298 <= 0)) \/ n':301 = mid_n:295)
         /\ (!(1 <= K:298) \/ n':301 = 0)
         /\ ((K:298 = 0 /\ mid_n:295 = n':301 /\ mid_tmp:297 = tmp':300
                /\ mid___cost:294 = __cost':299)
               \/ (1 <= K:298 /\ (-1 + mid_n:295) = 0 /\ n':301 = 0))
         /\ (0 = K:298 \/ !((2 + -mid_n:295) <= 0))
         /\ (K:293 + K:298) = K:302 /\ (!(0 <= K:303) \/ mid___cost:304 = 0)
         /\ (!(0 <= K:303) \/ mid_tmp:305 = tmp:296)
         /\ (!((0 <= K:303 /\ K:303 <= 0)) \/ mid_n:306 = havoc:13)
         /\ (!(1 <= K:303) \/ mid_n:306 = 0) /\ K:303 = 0
         /\ havoc:13 = mid_n:306 /\ tmp:296 = mid_tmp:305
         /\ 0 = mid___cost:304 /\ 0 = K:303
         /\ (!(0 <= K:307)
               \/ (__cost':299 + n':301) <= (mid___cost:304 + mid_n:306))
         /\ (!(0 <= K:307) \/ n':301 <= (mid_n:306 + -K:307))
         /\ (!(0 <= K:307)
               \/ (-__cost':299 + -n':301) <= ((-mid___cost:304 + -mid_n:306)
                                                 + K:307))
         /\ ((K:307 = 0 /\ mid_n:306 = n':301 /\ mid_tmp:305 = tmp':300
                /\ mid___cost:304 = __cost':299)
               \/ (1 <= K:307 /\ 0 <= mid___cost:304 /\ 0 <= (-1 + mid_n:306)
                     /\ 0 <= __cost':299 /\ 0 <= n':301))
         /\ (0 = K:307 \/ -mid___cost:304 <= 0) /\ (K:303 + K:307) = K:302
         /\ 0 <= K:302 /\ n':301 <= 0
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:313)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:313)))}

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

Base relation: 
{__cost := __cost':322
 return := havoc:334
 param0 := param0:53
 return@pos := type_err:335
 param0@pos := type_err:54
 return@width := type_err:336
 param0@width := type_err:55
 when ((!(0 <= K:316)
          \/ (mid___cost:317 + mid_n:318) <= (__cost:63 + param0:53))
         /\ (!(0 <= K:316) \/ -mid___cost:317 <= (-__cost:63 + -K:316))
         /\ (!(0 <= K:316)
               \/ (-mid___cost:317 + -mid_n:318) <= ((-__cost:63 + -param0:53)
                                                       + K:316))
         /\ ((K:316 = 0 /\ param0:53 = mid_n:318 /\ tmp:319 = mid_tmp:320
                /\ __cost:63 = mid___cost:317)
               \/ (1 <= K:316 /\ 0 <= __cost:63 /\ 0 <= (-2 + param0:53)
                     /\ 0 <= (-1 + mid___cost:317) /\ 0 <= mid_n:318))
         /\ (0 = K:316 \/ (2 + -param0:53) <= 0)
         /\ (!(0 <= K:321) \/ __cost':322 = mid___cost:317)
         /\ (!(0 <= K:321) \/ tmp':323 = mid_tmp:320)
         /\ (!((0 <= K:321 /\ K:321 <= 0)) \/ n':324 = mid_n:318)
         /\ (!(1 <= K:321) \/ n':324 = 0)
         /\ ((K:321 = 0 /\ mid_n:318 = n':324 /\ mid_tmp:320 = tmp':323
                /\ mid___cost:317 = __cost':322)
               \/ (1 <= K:321 /\ (-1 + mid_n:318) = 0 /\ n':324 = 0))
         /\ (0 = K:321 \/ !((2 + -mid_n:318) <= 0))
         /\ (K:316 + K:321) = K:325
         /\ (!(0 <= K:326) \/ mid___cost:327 = __cost:63)
         /\ (!(0 <= K:326) \/ mid_tmp:328 = tmp:319)
         /\ (!((0 <= K:326 /\ K:326 <= 0)) \/ mid_n:329 = param0:53)
         /\ (!(1 <= K:326) \/ mid_n:329 = 0)
         /\ ((K:326 = 0 /\ param0:53 = mid_n:329 /\ tmp:319 = mid_tmp:328
                /\ __cost:63 = mid___cost:327)
               \/ (1 <= K:326 /\ (-1 + param0:53) = 0
                     /\ 0 <= (-1 + -__cost:63) /\ mid_n:329 = 0
                     /\ 0 <= (-1 + -mid___cost:327)))
         /\ (0 = K:326 \/ !(-__cost:63 <= 0))
         /\ (!(0 <= K:330)
               \/ (__cost':322 + n':324) <= (mid___cost:327 + mid_n:329))
         /\ (!(0 <= K:330) \/ n':324 <= (mid_n:329 + -K:330))
         /\ (!(0 <= K:330)
               \/ (-__cost':322 + -n':324) <= ((-mid___cost:327 + -mid_n:329)
                                                 + K:330))
         /\ ((K:330 = 0 /\ mid_n:329 = n':324 /\ mid_tmp:328 = tmp':323
                /\ mid___cost:327 = __cost':322)
               \/ (1 <= K:330 /\ 0 <= mid___cost:327 /\ 0 <= (-1 + mid_n:329)
                     /\ 0 <= __cost':322 /\ 0 <= n':324))
         /\ (0 = K:330 \/ -mid___cost:327 <= 0) /\ (K:326 + K:330) = K:325
         /\ 0 <= K:325 /\ n':324 <= 0)}

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

Base relation: 
{__cost := __cost':184
 tmp := tmp':185
 n := n':186
 return := havoc:224
 return@pos := type_err:225
 return@width := type_err:226
 when ((!(0 <= K:179)
          \/ (mid___cost:180 + mid_n:181) <= (__cost:63 + param0:53))
         /\ (!(0 <= K:179) \/ -mid___cost:180 <= (-__cost:63 + -K:179))
         /\ (!(0 <= K:179)
               \/ (-mid___cost:180 + -mid_n:181) <= ((-__cost:63 + -param0:53)
                                                       + K:179))
         /\ ((K:179 = 0 /\ param0:53 = mid_n:181 /\ tmp:65 = mid_tmp:182
                /\ __cost:63 = mid___cost:180)
               \/ (1 <= K:179 /\ 0 <= __cost:63 /\ 0 <= (-2 + param0:53)
                     /\ 0 <= (-1 + mid___cost:180) /\ 0 <= mid_n:181))
         /\ (0 = K:179 \/ (2 + -param0:53) <= 0)
         /\ (!(0 <= K:183) \/ __cost':184 = mid___cost:180)
         /\ (!(0 <= K:183) \/ tmp':185 = mid_tmp:182)
         /\ (!((0 <= K:183 /\ K:183 <= 0)) \/ n':186 = mid_n:181)
         /\ (!(1 <= K:183) \/ n':186 = 0)
         /\ ((K:183 = 0 /\ mid_n:181 = n':186 /\ mid_tmp:182 = tmp':185
                /\ mid___cost:180 = __cost':184)
               \/ (1 <= K:183 /\ (-1 + mid_n:181) = 0 /\ n':186 = 0))
         /\ (0 = K:183 \/ !((2 + -mid_n:181) <= 0))
         /\ (K:179 + K:183) = K:187
         /\ (!(0 <= K:188) \/ mid___cost:189 = __cost:63)
         /\ (!(0 <= K:188) \/ mid_tmp:190 = tmp:65)
         /\ (!((0 <= K:188 /\ K:188 <= 0)) \/ mid_n:191 = param0:53)
         /\ (!(1 <= K:188) \/ mid_n:191 = 0)
         /\ ((K:188 = 0 /\ param0:53 = mid_n:191 /\ tmp:65 = mid_tmp:190
                /\ __cost:63 = mid___cost:189)
               \/ (1 <= K:188 /\ (-1 + param0:53) = 0
                     /\ 0 <= (-1 + -__cost:63) /\ mid_n:191 = 0
                     /\ 0 <= (-1 + -mid___cost:189)))
         /\ (0 = K:188 \/ !(-__cost:63 <= 0))
         /\ (!(0 <= K:192)
               \/ (__cost':184 + n':186) <= (mid___cost:189 + mid_n:191))
         /\ (!(0 <= K:192) \/ n':186 <= (mid_n:191 + -K:192))
         /\ (!(0 <= K:192)
               \/ (-__cost':184 + -n':186) <= ((-mid___cost:189 + -mid_n:191)
                                                 + K:192))
         /\ ((K:192 = 0 /\ mid_n:191 = n':186 /\ mid_tmp:190 = tmp':185
                /\ mid___cost:189 = __cost':184)
               \/ (1 <= K:192 /\ 0 <= mid___cost:189 /\ 0 <= (-1 + mid_n:191)
                     /\ 0 <= __cost':184 /\ 0 <= n':186))
         /\ (0 = K:192 \/ -mid___cost:189 <= 0) /\ (K:188 + K:192) = K:187
         /\ 0 <= K:187 /\ n':186 <= 0)}

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

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

Variable bounds at line 21 in run

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

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