/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, 28> -> <Unique State Name, 37>	Base relation: 
{__cost := (__cost:94 + 1)
 z := y:92
 x := (x:93 + -((y:92 + 1)))
 when (y:92 < x:93 /\ 0 <= __cost:94 /\ 0 <= (__cost:94 + 1))}	
<Unique State Name, 28> -> <Unique State Name, 67>	Base relation: 
{return := havoc:101
 return@pos := type_err:102
 return@width := type_err:103
 when x:93 <= y:92}	
<Unique State Name, 68> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 59> -> <Unique State Name, 20>	Base relation: 
{}	
<Unique State Name, 66> -> <Unique State Name, 61 65>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 70> -> <Unique State Name, 41>	Base relation: 
{}	
<Unique State Name, 18> -> <Unique State Name, 66>	Base relation: 
{__cost := 0
 x := havoc:20
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:25
 param1@pos := type_err:27
 param0@width := type_err:26
 param1@width := type_err:28
 when 0 <= havoc:21}	
<Unique State Name, 41> -> <Unique State Name, 24>	Base relation: 
{when z:95 <= 0}	
<Unique State Name, 41> -> <Unique State Name, 37>	Base relation: 
{z := (z:95 + -1)
 when 0 < z:95}	
<Unique State Name, 71> -> <Unique State Name, 28>	Base relation: 
{}	
<Unique State Name, 20> -> <Unique State Name, 68>	Base relation: 
{return := havoc:54
 return@pos := type_err:57
 return@width := type_err:58}	
<Unique State Name, 67> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 65> -> <Unique State Name, 69>	Base relation: 
{return := 0
 return@pos := type_err:29
 return@width := type_err:30
 when ((0 < x:5 /\ x:5 = phi_tmp___1:22) \/ (x:5 <= 0 /\ 0 = phi_tmp___1:22))}	
<Unique State Name, 24> -> <Unique State Name, 71>	Base relation: 
{}	
<Unique State Name, 37> -> <Unique State Name, 70>	Base relation: 
{}	
<Unique State Name, 61> -> <Unique State Name, 60>	Base relation: 
{param0 := param0:71
 param1 := param1:74
 param0@pos := type_err:79
 param1@pos := type_err:80
 param0@width := type_err:81
 param1@width := type_err:82}	
<Unique State Name, 55> -> <Unique State Name, 24>	Base relation: 
{x := param0:71
 y := param1:74}	
<Unique State Name, 69> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 60> -> <Unique State Name, 55 59>	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: 
{z := (z:95 + -1)
 when 0 < z:95}
**** alpha hat: 
  {<Split [true
            (z':148) = (1)*(z:95) + (-1)*1
           }
          pre:
            [|z:95-1>=0|]
          post:
            [|z':148>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {z := z':148
   when ((!(0 <= K:153) \/ mid_z:155 = (z:95 + -K:153))
           /\ ((K:153 = 0 /\ z:95 = mid_z:155)
                 \/ (1 <= K:153 /\ 0 <= (-1 + z:95) /\ 0 <= mid_z:155))
           /\ K:154 = 0 /\ mid_z:155 = z':148 /\ 0 = K:154
           /\ (K:153 + K:154) = K:152 /\ 0 <= K:152)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:94 + 1)
 z := z':159
 x := (x:93 + -((y:92 + 1)))
 when (y:92 < x:93 /\ 0 <= __cost:94 /\ 0 <= (__cost:94 + 1)
         /\ (!(0 <= K:156) \/ mid_z:157 = (y:92 + -K:156))
         /\ ((K:156 = 0 /\ y:92 = mid_z:157)
               \/ (1 <= K:156 /\ 0 <= (-1 + y:92) /\ 0 <= mid_z:157))
         /\ K:158 = 0 /\ mid_z:157 = z':159 /\ 0 = K:158
         /\ (K:156 + K:158) = K:160 /\ 0 <= K:160 /\ z':159 <= 0)}
**** alpha hat: 
  {<Split [!((1 + -y:92) <= 0)
            (x':162) = (1)*(x:93) + (-1)*1 + (-1)*y:92
           (z':148) = y:92
           (__cost':161) = (1)*(__cost:94) + 1
           (-x':162) <= (1)*(-x:93) + 1
           (-x':162) <= (1)*(-x:93) + x:93
           }
          pre:
            [|-y:92>=0; -y:92+x:93-1>=0; __cost:94>=0|]
          post:
            [|-y:92+z':148=0; -y:92>=0; x':162>=0; __cost':161-1>=0|]
           (z':148) = 0
          (x':162) = (1)*(x:93) + (-1)*1 + (-1)*y:92
          (__cost':161) = (1)*(__cost:94) + 1
          (x':162) <= (1)*(x:93) + (-2)*1
          (-x':162) <= (1)*(-x:93) + x:93
          }
  pre:
    [|-y:92+x:93-1>=0; __cost:94>=0; y:92-1>=0|]
  post:
    [|z':148=0; x':162>=0; __cost':161-1>=0; y:92-1>=0|]]>}
**** star transition: 
  {__cost := __cost':161
   z := z':148
   x := x':162
   when ((!(0 <= K:178) \/ mid_x:180 = (x:93 + -K:178 + -((y:92 * K:178))))
           /\ (!((0 <= K:178 /\ K:178 <= 0)) \/ mid_z:181 = z:95)
           /\ (!(1 <= K:178) \/ mid_z:181 = y:92)
           /\ (!(0 <= K:178) \/ mid___cost:182 = (__cost:94 + K:178))
           /\ (!(0 <= K:178) \/ -mid_x:180 <= (-x:93 + K:178))
           /\ (!(0 <= K:178)
                 \/ -mid_x:180 <= (-x:93 + (1/2 * K:178)
                                     + (1/2 * y:92 * K:178) + (x:93 * K:178)
                                     + (-1/2 * (K:178 * K:178))
                                     + (-1/2 * y:92 * (K:178 * K:178))))
           /\ ((K:178 = 0 /\ x:93 = mid_x:180 /\ z:95 = mid_z:181
                  /\ __cost:94 = mid___cost:182)
                 \/ (1 <= K:178 /\ 0 <= -y:92 /\ 0 <= (-1 + -y:92 + x:93)
                       /\ 0 <= __cost:94 /\ (-y:92 + mid_z:181) = 0
                       /\ 0 <= -y:92 /\ 0 <= mid_x:180
                       /\ 0 <= (-1 + mid___cost:182)))
           /\ (0 = K:178 \/ !((1 + -y:92) <= 0))
           /\ (!((0 <= K:179 /\ K:179 <= 0)) \/ z':148 = mid_z:181)
           /\ (!(1 <= K:179) \/ z':148 = 0)
           /\ (!(0 <= K:179)
                 \/ x':162 = (mid_x:180 + -K:179 + -((y:92 * K:179))))
           /\ (!(0 <= K:179) \/ __cost':161 = (mid___cost:182 + K:179))
           /\ (!(0 <= K:179) \/ x':162 <= (mid_x:180 + (-2 * K:179)))
           /\ (!(0 <= K:179)
                 \/ -x':162 <= (-mid_x:180 + (1/2 * K:179)
                                  + (1/2 * y:92 * K:179)
                                  + (mid_x:180 * K:179)
                                  + (-1/2 * (K:179 * K:179))
                                  + (-1/2 * y:92 * (K:179 * K:179))))
           /\ ((K:179 = 0 /\ mid_x:180 = x':162 /\ mid_z:181 = z':148
                  /\ mid___cost:182 = __cost':161)
                 \/ (1 <= K:179 /\ 0 <= (-1 + -y:92 + mid_x:180)
                       /\ 0 <= mid___cost:182 /\ 0 <= (-1 + y:92)
                       /\ z':148 = 0 /\ 0 <= x':162
                       /\ 0 <= (-1 + __cost':161) /\ 0 <= (-1 + y:92)))
           /\ (0 = K:179 \/ (1 + -y:92) <= 0) /\ (K:178 + K:179) = K:177
           /\ 0 <= K:177)}
}
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
       x := havoc:20
       param0 := havoc:20
       param1 := havoc:21
       param0@pos := type_err:25
       param1@pos := type_err:27
       param0@width := type_err:26
       param1@width := type_err:28
       when 0 <= havoc:21}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:29
     return@width := type_err:30
     when ((0 < x:5 /\ x:5 = phi_tmp___1:22)
             \/ (x:5 <= 0 /\ 0 = phi_tmp___1:22))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:71
       param1 := param1:74
       param0@pos := type_err:79
       param1@pos := type_err:80
       param0@width := type_err:81
       param1@width := type_err:82}    )
    ,
    Var(20)
  )
  ,
  Weight(Base relation: 
    {return := havoc:54
     return@pos := type_err:57
     return@width := type_err:58}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=20: 
Weight(Base relation: 
  {__cost := __cost':190
   z := z':188
   x := x':189
   y := param1:74
   return := havoc:197
   return@pos := type_err:198
   return@width := type_err:199
   when ((!(0 <= K:183)
            \/ mid_x:184 = (param0:71 + -K:183 + -((param1:74 * K:183))))
           /\ (!((0 <= K:183 /\ K:183 <= 0)) \/ mid_z:185 = z:95)
           /\ (!(1 <= K:183) \/ mid_z:185 = param1:74)
           /\ (!(0 <= K:183) \/ mid___cost:186 = (__cost:94 + K:183))
           /\ (!(0 <= K:183) \/ -mid_x:184 <= (-param0:71 + K:183))
           /\ (!(0 <= K:183)
                 \/ -mid_x:184 <= (-param0:71 + (1/2 * K:183)
                                     + (1/2 * param1:74 * K:183)
                                     + (param0:71 * K:183)
                                     + (-1/2 * (K:183 * K:183))
                                     + (-1/2 * param1:74 * (K:183 * K:183))))
           /\ ((K:183 = 0 /\ param0:71 = mid_x:184 /\ z:95 = mid_z:185
                  /\ __cost:94 = mid___cost:186)
                 \/ (1 <= K:183 /\ 0 <= -param1:74
                       /\ 0 <= (-1 + -param1:74 + param0:71)
                       /\ 0 <= __cost:94 /\ (-param1:74 + mid_z:185) = 0
                       /\ 0 <= -param1:74 /\ 0 <= mid_x:184
                       /\ 0 <= (-1 + mid___cost:186)))
           /\ (0 = K:183 \/ !((1 + -param1:74) <= 0))
           /\ (!((0 <= K:187 /\ K:187 <= 0)) \/ z':188 = mid_z:185)
           /\ (!(1 <= K:187) \/ z':188 = 0)
           /\ (!(0 <= K:187)
                 \/ x':189 = (mid_x:184 + -K:187 + -((param1:74 * K:187))))
           /\ (!(0 <= K:187) \/ __cost':190 = (mid___cost:186 + K:187))
           /\ (!(0 <= K:187) \/ x':189 <= (mid_x:184 + (-2 * K:187)))
           /\ (!(0 <= K:187)
                 \/ -x':189 <= (-mid_x:184 + (1/2 * K:187)
                                  + (1/2 * param1:74 * K:187)
                                  + (mid_x:184 * K:187)
                                  + (-1/2 * (K:187 * K:187))
                                  + (-1/2 * param1:74 * (K:187 * K:187))))
           /\ ((K:187 = 0 /\ mid_x:184 = x':189 /\ mid_z:185 = z':188
                  /\ mid___cost:186 = __cost':190)
                 \/ (1 <= K:187 /\ 0 <= (-1 + -param1:74 + mid_x:184)
                       /\ 0 <= mid___cost:186 /\ 0 <= (-1 + param1:74)
                       /\ z':188 = 0 /\ 0 <= x':189
                       /\ 0 <= (-1 + __cost':190) /\ 0 <= (-1 + param1:74)))
           /\ (0 = K:187 \/ (1 + -param1:74) <= 0) /\ (K:183 + K:187) = K:191
           /\ 0 <= K:191 /\ x':189 <= param1:74)})



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
         x := havoc:20
         param0 := havoc:20
         param1 := havoc:21
         param0@pos := type_err:25
         param1@pos := type_err:27
         param0@width := type_err:26
         param1@width := type_err:28
         when 0 <= havoc:21}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:29
       return@width := type_err:30
       when ((0 < x:5 /\ x:5 = phi_tmp___1:22)
               \/ (x:5 <= 0 /\ 0 = phi_tmp___1:22))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:71
         param1 := param1:74
         param0@pos := type_err:79
         param1@pos := type_err:80
         param0@width := type_err:81
         param1@width := type_err:82}      )
      ,
      Var(20)
    )
    ,
    Weight(Base relation: 
      {return := havoc:54
       return@pos := type_err:57
       return@width := type_err:58}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':190
   return := havoc:197
   return@pos := type_err:198
   return@width := type_err:199
   when ((!(0 <= K:183)
            \/ mid_x:184 = (param0:71 + -K:183 + -((param1:74 * K:183))))
           /\ (!((0 <= K:183 /\ K:183 <= 0)) \/ mid_z:185 = z:200)
           /\ (!(1 <= K:183) \/ mid_z:185 = param1:74)
           /\ (!(0 <= K:183) \/ mid___cost:186 = (__cost:94 + K:183))
           /\ (!(0 <= K:183) \/ -mid_x:184 <= (-param0:71 + K:183))
           /\ (!(0 <= K:183)
                 \/ -mid_x:184 <= (-param0:71 + (1/2 * K:183)
                                     + (1/2 * param1:74 * K:183)
                                     + (param0:71 * K:183)
                                     + (-1/2 * (K:183 * K:183))
                                     + (-1/2 * param1:74 * (K:183 * K:183))))
           /\ ((K:183 = 0 /\ param0:71 = mid_x:184 /\ z:200 = mid_z:185
                  /\ __cost:94 = mid___cost:186)
                 \/ (1 <= K:183 /\ 0 <= -param1:74
                       /\ 0 <= (-1 + -param1:74 + param0:71)
                       /\ 0 <= __cost:94 /\ (-param1:74 + mid_z:185) = 0
                       /\ 0 <= -param1:74 /\ 0 <= mid_x:184
                       /\ 0 <= (-1 + mid___cost:186)))
           /\ (0 = K:183 \/ !((1 + -param1:74) <= 0))
           /\ (!((0 <= K:187 /\ K:187 <= 0)) \/ z':188 = mid_z:185)
           /\ (!(1 <= K:187) \/ z':188 = 0)
           /\ (!(0 <= K:187)
                 \/ x':189 = (mid_x:184 + -K:187 + -((param1:74 * K:187))))
           /\ (!(0 <= K:187) \/ __cost':190 = (mid___cost:186 + K:187))
           /\ (!(0 <= K:187) \/ x':189 <= (mid_x:184 + (-2 * K:187)))
           /\ (!(0 <= K:187)
                 \/ -x':189 <= (-mid_x:184 + (1/2 * K:187)
                                  + (1/2 * param1:74 * K:187)
                                  + (mid_x:184 * K:187)
                                  + (-1/2 * (K:187 * K:187))
                                  + (-1/2 * param1:74 * (K:187 * K:187))))
           /\ ((K:187 = 0 /\ mid_x:184 = x':189 /\ mid_z:185 = z':188
                  /\ mid___cost:186 = __cost':190)
                 \/ (1 <= K:187 /\ 0 <= (-1 + -param1:74 + mid_x:184)
                       /\ 0 <= mid___cost:186 /\ 0 <= (-1 + param1:74)
                       /\ z':188 = 0 /\ 0 <= x':189
                       /\ 0 <= (-1 + __cost':190) /\ 0 <= (-1 + param1:74)))
           /\ (0 = K:187 \/ (1 + -param1:74) <= 0) /\ (K:183 + K:187) = K:191
           /\ 0 <= K:191 /\ x':189 <= param1:74)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':225
   return := 0
   param0 := havoc:20
   param1 := havoc:21
   return@pos := type_err:235
   param0@pos := type_err:229
   param1@pos := type_err:230
   return@width := type_err:236
   param0@width := type_err:232
   param1@width := type_err:233
   when (0 <= havoc:21
           /\ (!(0 <= K:217)
                 \/ mid_x:218 = (havoc:20 + -K:217 + -((havoc:21 * K:217))))
           /\ (!((0 <= K:217 /\ K:217 <= 0)) \/ mid_z:219 = z:220)
           /\ (!(1 <= K:217) \/ mid_z:219 = havoc:21)
           /\ (!(0 <= K:217) \/ mid___cost:221 = K:217)
           /\ (!(0 <= K:217) \/ -mid_x:218 <= (-havoc:20 + K:217))
           /\ (!(0 <= K:217)
                 \/ -mid_x:218 <= (-havoc:20 + (1/2 * K:217)
                                     + (1/2 * havoc:21 * K:217)
                                     + (havoc:20 * K:217)
                                     + (-1/2 * (K:217 * K:217))
                                     + (-1/2 * havoc:21 * (K:217 * K:217))))
           /\ ((K:217 = 0 /\ havoc:20 = mid_x:218 /\ z:220 = mid_z:219
                  /\ 0 = mid___cost:221)
                 \/ (1 <= K:217 /\ 0 <= -havoc:21
                       /\ 0 <= (-1 + -havoc:21 + havoc:20)
                       /\ (-havoc:21 + mid_z:219) = 0 /\ 0 <= -havoc:21
                       /\ 0 <= mid_x:218 /\ 0 <= (-1 + mid___cost:221)))
           /\ (0 = K:217 \/ !((1 + -havoc:21) <= 0))
           /\ (!((0 <= K:222 /\ K:222 <= 0)) \/ z':223 = mid_z:219)
           /\ (!(1 <= K:222) \/ z':223 = 0)
           /\ (!(0 <= K:222)
                 \/ x':224 = (mid_x:218 + -K:222 + -((havoc:21 * K:222))))
           /\ (!(0 <= K:222) \/ __cost':225 = (mid___cost:221 + K:222))
           /\ (!(0 <= K:222) \/ x':224 <= (mid_x:218 + (-2 * K:222)))
           /\ (!(0 <= K:222)
                 \/ -x':224 <= (-mid_x:218 + (1/2 * K:222)
                                  + (1/2 * havoc:21 * K:222)
                                  + (mid_x:218 * K:222)
                                  + (-1/2 * (K:222 * K:222))
                                  + (-1/2 * havoc:21 * (K:222 * K:222))))
           /\ ((K:222 = 0 /\ mid_x:218 = x':224 /\ mid_z:219 = z':223
                  /\ mid___cost:221 = __cost':225)
                 \/ (1 <= K:222 /\ 0 <= (-1 + -havoc:21 + mid_x:218)
                       /\ 0 <= mid___cost:221 /\ 0 <= (-1 + havoc:21)
                       /\ z':223 = 0 /\ 0 <= x':224
                       /\ 0 <= (-1 + __cost':225) /\ 0 <= (-1 + havoc:21)))
           /\ (0 = K:222 \/ (1 + -havoc:21) <= 0) /\ (K:217 + K:222) = K:226
           /\ 0 <= K:226 /\ x':224 <= havoc:21
           /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:234)
                 \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:234)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':245
   return := havoc:250
   param0 := param0:71
   param1 := param1:74
   return@pos := type_err:251
   param0@pos := type_err:79
   param1@pos := type_err:80
   return@width := type_err:252
   param0@width := type_err:81
   param1@width := type_err:82
   when ((!(0 <= K:237)
            \/ mid_x:238 = (param0:71 + -K:237 + -((param1:74 * K:237))))
           /\ (!((0 <= K:237 /\ K:237 <= 0)) \/ mid_z:239 = z:240)
           /\ (!(1 <= K:237) \/ mid_z:239 = param1:74)
           /\ (!(0 <= K:237) \/ mid___cost:241 = (__cost:94 + K:237))
           /\ (!(0 <= K:237) \/ -mid_x:238 <= (-param0:71 + K:237))
           /\ (!(0 <= K:237)
                 \/ -mid_x:238 <= (-param0:71 + (1/2 * K:237)
                                     + (1/2 * param1:74 * K:237)
                                     + (param0:71 * K:237)
                                     + (-1/2 * (K:237 * K:237))
                                     + (-1/2 * param1:74 * (K:237 * K:237))))
           /\ ((K:237 = 0 /\ param0:71 = mid_x:238 /\ z:240 = mid_z:239
                  /\ __cost:94 = mid___cost:241)
                 \/ (1 <= K:237 /\ 0 <= -param1:74
                       /\ 0 <= (-1 + -param1:74 + param0:71)
                       /\ 0 <= __cost:94 /\ (-param1:74 + mid_z:239) = 0
                       /\ 0 <= -param1:74 /\ 0 <= mid_x:238
                       /\ 0 <= (-1 + mid___cost:241)))
           /\ (0 = K:237 \/ !((1 + -param1:74) <= 0))
           /\ (!((0 <= K:242 /\ K:242 <= 0)) \/ z':243 = mid_z:239)
           /\ (!(1 <= K:242) \/ z':243 = 0)
           /\ (!(0 <= K:242)
                 \/ x':244 = (mid_x:238 + -K:242 + -((param1:74 * K:242))))
           /\ (!(0 <= K:242) \/ __cost':245 = (mid___cost:241 + K:242))
           /\ (!(0 <= K:242) \/ x':244 <= (mid_x:238 + (-2 * K:242)))
           /\ (!(0 <= K:242)
                 \/ -x':244 <= (-mid_x:238 + (1/2 * K:242)
                                  + (1/2 * param1:74 * K:242)
                                  + (mid_x:238 * K:242)
                                  + (-1/2 * (K:242 * K:242))
                                  + (-1/2 * param1:74 * (K:242 * K:242))))
           /\ ((K:242 = 0 /\ mid_x:238 = x':244 /\ mid_z:239 = z':243
                  /\ mid___cost:241 = __cost':245)
                 \/ (1 <= K:242 /\ 0 <= (-1 + -param1:74 + mid_x:238)
                       /\ 0 <= mid___cost:241 /\ 0 <= (-1 + param1:74)
                       /\ z':243 = 0 /\ 0 <= x':244
                       /\ 0 <= (-1 + __cost':245) /\ 0 <= (-1 + param1:74)))
           /\ (0 = K:242 \/ (1 + -param1:74) <= 0) /\ (K:237 + K:242) = K:246
           /\ 0 <= K:246 /\ x':244 <= param1:74)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=20: 
Weight(Base relation: 
  {__cost := __cost':190
   return := havoc:197
   return@pos := type_err:198
   return@width := type_err:199
   when ((!(0 <= K:183)
            \/ mid_x:184 = (param0:71 + -K:183 + -((param1:74 * K:183))))
           /\ (!((0 <= K:183 /\ K:183 <= 0)) \/ mid_z:185 = z:200)
           /\ (!(1 <= K:183) \/ mid_z:185 = param1:74)
           /\ (!(0 <= K:183) \/ mid___cost:186 = (__cost:94 + K:183))
           /\ (!(0 <= K:183) \/ -mid_x:184 <= (-param0:71 + K:183))
           /\ (!(0 <= K:183)
                 \/ -mid_x:184 <= (-param0:71 + (1/2 * K:183)
                                     + (1/2 * param1:74 * K:183)
                                     + (param0:71 * K:183)
                                     + (-1/2 * (K:183 * K:183))
                                     + (-1/2 * param1:74 * (K:183 * K:183))))
           /\ ((K:183 = 0 /\ param0:71 = mid_x:184 /\ z:200 = mid_z:185
                  /\ __cost:94 = mid___cost:186)
                 \/ (1 <= K:183 /\ 0 <= -param1:74
                       /\ 0 <= (-1 + -param1:74 + param0:71)
                       /\ 0 <= __cost:94 /\ (-param1:74 + mid_z:185) = 0
                       /\ 0 <= -param1:74 /\ 0 <= mid_x:184
                       /\ 0 <= (-1 + mid___cost:186)))
           /\ (0 = K:183 \/ !((1 + -param1:74) <= 0))
           /\ (!((0 <= K:187 /\ K:187 <= 0)) \/ z':188 = mid_z:185)
           /\ (!(1 <= K:187) \/ z':188 = 0)
           /\ (!(0 <= K:187)
                 \/ x':189 = (mid_x:184 + -K:187 + -((param1:74 * K:187))))
           /\ (!(0 <= K:187) \/ __cost':190 = (mid___cost:186 + K:187))
           /\ (!(0 <= K:187) \/ x':189 <= (mid_x:184 + (-2 * K:187)))
           /\ (!(0 <= K:187)
                 \/ -x':189 <= (-mid_x:184 + (1/2 * K:187)
                                  + (1/2 * param1:74 * K:187)
                                  + (mid_x:184 * K:187)
                                  + (-1/2 * (K:187 * K:187))
                                  + (-1/2 * param1:74 * (K:187 * K:187))))
           /\ ((K:187 = 0 /\ mid_x:184 = x':189 /\ mid_z:185 = z':188
                  /\ mid___cost:186 = __cost':190)
                 \/ (1 <= K:187 /\ 0 <= (-1 + -param1:74 + mid_x:184)
                       /\ 0 <= mid___cost:186 /\ 0 <= (-1 + param1:74)
                       /\ z':188 = 0 /\ 0 <= x':189
                       /\ 0 <= (-1 + __cost':190) /\ 0 <= (-1 + param1:74)))
           /\ (0 = K:187 \/ (1 + -param1:74) <= 0) /\ (K:183 + K:187) = K:191
           /\ 0 <= K:191 /\ x':189 <= param1:74)})


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':225
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:235
 param0@pos := type_err:229
 param1@pos := type_err:230
 return@width := type_err:236
 param0@width := type_err:232
 param1@width := type_err:233
 when (0 <= havoc:21
         /\ (!(0 <= K:217)
               \/ mid_x:218 = (havoc:20 + -K:217 + -((havoc:21 * K:217))))
         /\ (!((0 <= K:217 /\ K:217 <= 0)) \/ mid_z:219 = z:220)
         /\ (!(1 <= K:217) \/ mid_z:219 = havoc:21)
         /\ (!(0 <= K:217) \/ mid___cost:221 = K:217)
         /\ (!(0 <= K:217) \/ -mid_x:218 <= (-havoc:20 + K:217))
         /\ (!(0 <= K:217)
               \/ -mid_x:218 <= (-havoc:20 + (1/2 * K:217)
                                   + (1/2 * havoc:21 * K:217)
                                   + (havoc:20 * K:217)
                                   + (-1/2 * (K:217 * K:217))
                                   + (-1/2 * havoc:21 * (K:217 * K:217))))
         /\ ((K:217 = 0 /\ havoc:20 = mid_x:218 /\ z:220 = mid_z:219
                /\ 0 = mid___cost:221)
               \/ (1 <= K:217 /\ 0 <= -havoc:21
                     /\ 0 <= (-1 + -havoc:21 + havoc:20)
                     /\ (-havoc:21 + mid_z:219) = 0 /\ 0 <= -havoc:21
                     /\ 0 <= mid_x:218 /\ 0 <= (-1 + mid___cost:221)))
         /\ (0 = K:217 \/ !((1 + -havoc:21) <= 0))
         /\ (!((0 <= K:222 /\ K:222 <= 0)) \/ z':223 = mid_z:219)
         /\ (!(1 <= K:222) \/ z':223 = 0)
         /\ (!(0 <= K:222)
               \/ x':224 = (mid_x:218 + -K:222 + -((havoc:21 * K:222))))
         /\ (!(0 <= K:222) \/ __cost':225 = (mid___cost:221 + K:222))
         /\ (!(0 <= K:222) \/ x':224 <= (mid_x:218 + (-2 * K:222)))
         /\ (!(0 <= K:222)
               \/ -x':224 <= (-mid_x:218 + (1/2 * K:222)
                                + (1/2 * havoc:21 * K:222)
                                + (mid_x:218 * K:222)
                                + (-1/2 * (K:222 * K:222))
                                + (-1/2 * havoc:21 * (K:222 * K:222))))
         /\ ((K:222 = 0 /\ mid_x:218 = x':224 /\ mid_z:219 = z':223
                /\ mid___cost:221 = __cost':225)
               \/ (1 <= K:222 /\ 0 <= (-1 + -havoc:21 + mid_x:218)
                     /\ 0 <= mid___cost:221 /\ 0 <= (-1 + havoc:21)
                     /\ z':223 = 0 /\ 0 <= x':224 /\ 0 <= (-1 + __cost':225)
                     /\ 0 <= (-1 + havoc:21)))
         /\ (0 = K:222 \/ (1 + -havoc:21) <= 0) /\ (K:217 + K:222) = K:226
         /\ 0 <= K:226 /\ x':224 <= havoc:21
         /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:234)
               \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:234)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':245
 return := havoc:250
 param0 := param0:71
 param1 := param1:74
 return@pos := type_err:251
 param0@pos := type_err:79
 param1@pos := type_err:80
 return@width := type_err:252
 param0@width := type_err:81
 param1@width := type_err:82
 when ((!(0 <= K:237)
          \/ mid_x:238 = (param0:71 + -K:237 + -((param1:74 * K:237))))
         /\ (!((0 <= K:237 /\ K:237 <= 0)) \/ mid_z:239 = z:240)
         /\ (!(1 <= K:237) \/ mid_z:239 = param1:74)
         /\ (!(0 <= K:237) \/ mid___cost:241 = (__cost:94 + K:237))
         /\ (!(0 <= K:237) \/ -mid_x:238 <= (-param0:71 + K:237))
         /\ (!(0 <= K:237)
               \/ -mid_x:238 <= (-param0:71 + (1/2 * K:237)
                                   + (1/2 * param1:74 * K:237)
                                   + (param0:71 * K:237)
                                   + (-1/2 * (K:237 * K:237))
                                   + (-1/2 * param1:74 * (K:237 * K:237))))
         /\ ((K:237 = 0 /\ param0:71 = mid_x:238 /\ z:240 = mid_z:239
                /\ __cost:94 = mid___cost:241)
               \/ (1 <= K:237 /\ 0 <= -param1:74
                     /\ 0 <= (-1 + -param1:74 + param0:71) /\ 0 <= __cost:94
                     /\ (-param1:74 + mid_z:239) = 0 /\ 0 <= -param1:74
                     /\ 0 <= mid_x:238 /\ 0 <= (-1 + mid___cost:241)))
         /\ (0 = K:237 \/ !((1 + -param1:74) <= 0))
         /\ (!((0 <= K:242 /\ K:242 <= 0)) \/ z':243 = mid_z:239)
         /\ (!(1 <= K:242) \/ z':243 = 0)
         /\ (!(0 <= K:242)
               \/ x':244 = (mid_x:238 + -K:242 + -((param1:74 * K:242))))
         /\ (!(0 <= K:242) \/ __cost':245 = (mid___cost:241 + K:242))
         /\ (!(0 <= K:242) \/ x':244 <= (mid_x:238 + (-2 * K:242)))
         /\ (!(0 <= K:242)
               \/ -x':244 <= (-mid_x:238 + (1/2 * K:242)
                                + (1/2 * param1:74 * K:242)
                                + (mid_x:238 * K:242)
                                + (-1/2 * (K:242 * K:242))
                                + (-1/2 * param1:74 * (K:242 * K:242))))
         /\ ((K:242 = 0 /\ mid_x:238 = x':244 /\ mid_z:239 = z':243
                /\ mid___cost:241 = __cost':245)
               \/ (1 <= K:242 /\ 0 <= (-1 + -param1:74 + mid_x:238)
                     /\ 0 <= mid___cost:241 /\ 0 <= (-1 + param1:74)
                     /\ z':243 = 0 /\ 0 <= x':244 /\ 0 <= (-1 + __cost':245)
                     /\ 0 <= (-1 + param1:74)))
         /\ (0 = K:242 \/ (1 + -param1:74) <= 0) /\ (K:237 + K:242) = K:246
         /\ 0 <= K:246 /\ x':244 <= param1:74)}

Evaluating variable number 20 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':190
 return := havoc:197
 return@pos := type_err:198
 return@width := type_err:199
 when ((!(0 <= K:183)
          \/ mid_x:184 = (param0:71 + -K:183 + -((param1:74 * K:183))))
         /\ (!((0 <= K:183 /\ K:183 <= 0)) \/ mid_z:185 = z:200)
         /\ (!(1 <= K:183) \/ mid_z:185 = param1:74)
         /\ (!(0 <= K:183) \/ mid___cost:186 = (__cost:94 + K:183))
         /\ (!(0 <= K:183) \/ -mid_x:184 <= (-param0:71 + K:183))
         /\ (!(0 <= K:183)
               \/ -mid_x:184 <= (-param0:71 + (1/2 * K:183)
                                   + (1/2 * param1:74 * K:183)
                                   + (param0:71 * K:183)
                                   + (-1/2 * (K:183 * K:183))
                                   + (-1/2 * param1:74 * (K:183 * K:183))))
         /\ ((K:183 = 0 /\ param0:71 = mid_x:184 /\ z:200 = mid_z:185
                /\ __cost:94 = mid___cost:186)
               \/ (1 <= K:183 /\ 0 <= -param1:74
                     /\ 0 <= (-1 + -param1:74 + param0:71) /\ 0 <= __cost:94
                     /\ (-param1:74 + mid_z:185) = 0 /\ 0 <= -param1:74
                     /\ 0 <= mid_x:184 /\ 0 <= (-1 + mid___cost:186)))
         /\ (0 = K:183 \/ !((1 + -param1:74) <= 0))
         /\ (!((0 <= K:187 /\ K:187 <= 0)) \/ z':188 = mid_z:185)
         /\ (!(1 <= K:187) \/ z':188 = 0)
         /\ (!(0 <= K:187)
               \/ x':189 = (mid_x:184 + -K:187 + -((param1:74 * K:187))))
         /\ (!(0 <= K:187) \/ __cost':190 = (mid___cost:186 + K:187))
         /\ (!(0 <= K:187) \/ x':189 <= (mid_x:184 + (-2 * K:187)))
         /\ (!(0 <= K:187)
               \/ -x':189 <= (-mid_x:184 + (1/2 * K:187)
                                + (1/2 * param1:74 * K:187)
                                + (mid_x:184 * K:187)
                                + (-1/2 * (K:187 * K:187))
                                + (-1/2 * param1:74 * (K:187 * K:187))))
         /\ ((K:187 = 0 /\ mid_x:184 = x':189 /\ mid_z:185 = z':188
                /\ mid___cost:186 = __cost':190)
               \/ (1 <= K:187 /\ 0 <= (-1 + -param1:74 + mid_x:184)
                     /\ 0 <= mid___cost:186 /\ 0 <= (-1 + param1:74)
                     /\ z':188 = 0 /\ 0 <= x':189 /\ 0 <= (-1 + __cost':190)
                     /\ 0 <= (-1 + param1:74)))
         /\ (0 = K:187 \/ (1 + -param1:74) <= 0) /\ (K:183 + K:187) = K:191
         /\ 0 <= K:191 /\ x':189 <= param1:74)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,61)_g1> -> <__pstate, (Unique State Name,55)_g1>	Base relation: 
{param0 := param0:71
 param1 := param1:74
 param0@pos := type_err:79
 param1@pos := type_err:80
 param0@width := type_err:81
 param1@width := type_err:82}	
<__pstate, accept> -> <__pstate, (Unique State Name,61)_g1>	Base relation: 
{__cost := 0
 x := havoc:20
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:25
 param1@pos := type_err:27
 param0@width := type_err:26
 param1@width := type_err:28
 when 0 <= havoc:21}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x463f710: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x4db9860: 
	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,55)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:20
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:289
 param1@pos := type_err:290
 param0@width := type_err:291
 param1@width := type_err:292
 when 0 <= havoc:21}
    ( __pstate , (Unique State Name,61)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:20
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:25
 param1@pos := type_err:27
 param0@width := type_err:26
 param1@width := type_err:28
 when 0 <= havoc:21}

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

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

Base relation: 
{__cost := __cost':261
 x := havoc:20
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:271
 param0@pos := type_err:265
 param1@pos := type_err:266
 return@width := type_err:272
 param0@width := type_err:268
 param1@width := type_err:269
 when (0 <= havoc:21
         /\ (!(0 <= K:253)
               \/ mid_x:254 = (havoc:20 + -K:253 + -((havoc:21 * K:253))))
         /\ (!((0 <= K:253 /\ K:253 <= 0)) \/ mid_z:255 = z:256)
         /\ (!(1 <= K:253) \/ mid_z:255 = havoc:21)
         /\ (!(0 <= K:253) \/ mid___cost:257 = K:253)
         /\ (!(0 <= K:253) \/ -mid_x:254 <= (-havoc:20 + K:253))
         /\ (!(0 <= K:253)
               \/ -mid_x:254 <= (-havoc:20 + (1/2 * K:253)
                                   + (1/2 * havoc:21 * K:253)
                                   + (havoc:20 * K:253)
                                   + (-1/2 * (K:253 * K:253))
                                   + (-1/2 * havoc:21 * (K:253 * K:253))))
         /\ ((K:253 = 0 /\ havoc:20 = mid_x:254 /\ z:256 = mid_z:255
                /\ 0 = mid___cost:257)
               \/ (1 <= K:253 /\ 0 <= -havoc:21
                     /\ 0 <= (-1 + -havoc:21 + havoc:20)
                     /\ (-havoc:21 + mid_z:255) = 0 /\ 0 <= -havoc:21
                     /\ 0 <= mid_x:254 /\ 0 <= (-1 + mid___cost:257)))
         /\ (0 = K:253 \/ !((1 + -havoc:21) <= 0))
         /\ (!((0 <= K:258 /\ K:258 <= 0)) \/ z':259 = mid_z:255)
         /\ (!(1 <= K:258) \/ z':259 = 0)
         /\ (!(0 <= K:258)
               \/ x':260 = (mid_x:254 + -K:258 + -((havoc:21 * K:258))))
         /\ (!(0 <= K:258) \/ __cost':261 = (mid___cost:257 + K:258))
         /\ (!(0 <= K:258) \/ x':260 <= (mid_x:254 + (-2 * K:258)))
         /\ (!(0 <= K:258)
               \/ -x':260 <= (-mid_x:254 + (1/2 * K:258)
                                + (1/2 * havoc:21 * K:258)
                                + (mid_x:254 * K:258)
                                + (-1/2 * (K:258 * K:258))
                                + (-1/2 * havoc:21 * (K:258 * K:258))))
         /\ ((K:258 = 0 /\ mid_x:254 = x':260 /\ mid_z:255 = z':259
                /\ mid___cost:257 = __cost':261)
               \/ (1 <= K:258 /\ 0 <= (-1 + -havoc:21 + mid_x:254)
                     /\ 0 <= mid___cost:257 /\ 0 <= (-1 + havoc:21)
                     /\ z':259 = 0 /\ 0 <= x':260 /\ 0 <= (-1 + __cost':261)
                     /\ 0 <= (-1 + havoc:21)))
         /\ (0 = K:258 \/ (1 + -havoc:21) <= 0) /\ (K:253 + K:258) = K:262
         /\ 0 <= K:262 /\ x':260 <= havoc:21
         /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:270)
               \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:270)))}

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

Base relation: 
{__cost := __cost':281
 return := havoc:286
 param0 := param0:71
 param1 := param1:74
 return@pos := type_err:287
 param0@pos := type_err:79
 param1@pos := type_err:80
 return@width := type_err:288
 param0@width := type_err:81
 param1@width := type_err:82
 when ((!(0 <= K:273)
          \/ mid_x:274 = (param0:71 + -K:273 + -((param1:74 * K:273))))
         /\ (!((0 <= K:273 /\ K:273 <= 0)) \/ mid_z:275 = z:276)
         /\ (!(1 <= K:273) \/ mid_z:275 = param1:74)
         /\ (!(0 <= K:273) \/ mid___cost:277 = (__cost:94 + K:273))
         /\ (!(0 <= K:273) \/ -mid_x:274 <= (-param0:71 + K:273))
         /\ (!(0 <= K:273)
               \/ -mid_x:274 <= (-param0:71 + (1/2 * K:273)
                                   + (1/2 * param1:74 * K:273)
                                   + (param0:71 * K:273)
                                   + (-1/2 * (K:273 * K:273))
                                   + (-1/2 * param1:74 * (K:273 * K:273))))
         /\ ((K:273 = 0 /\ param0:71 = mid_x:274 /\ z:276 = mid_z:275
                /\ __cost:94 = mid___cost:277)
               \/ (1 <= K:273 /\ 0 <= -param1:74
                     /\ 0 <= (-1 + -param1:74 + param0:71) /\ 0 <= __cost:94
                     /\ (-param1:74 + mid_z:275) = 0 /\ 0 <= -param1:74
                     /\ 0 <= mid_x:274 /\ 0 <= (-1 + mid___cost:277)))
         /\ (0 = K:273 \/ !((1 + -param1:74) <= 0))
         /\ (!((0 <= K:278 /\ K:278 <= 0)) \/ z':279 = mid_z:275)
         /\ (!(1 <= K:278) \/ z':279 = 0)
         /\ (!(0 <= K:278)
               \/ x':280 = (mid_x:274 + -K:278 + -((param1:74 * K:278))))
         /\ (!(0 <= K:278) \/ __cost':281 = (mid___cost:277 + K:278))
         /\ (!(0 <= K:278) \/ x':280 <= (mid_x:274 + (-2 * K:278)))
         /\ (!(0 <= K:278)
               \/ -x':280 <= (-mid_x:274 + (1/2 * K:278)
                                + (1/2 * param1:74 * K:278)
                                + (mid_x:274 * K:278)
                                + (-1/2 * (K:278 * K:278))
                                + (-1/2 * param1:74 * (K:278 * K:278))))
         /\ ((K:278 = 0 /\ mid_x:274 = x':280 /\ mid_z:275 = z':279
                /\ mid___cost:277 = __cost':281)
               \/ (1 <= K:278 /\ 0 <= (-1 + -param1:74 + mid_x:274)
                     /\ 0 <= mid___cost:277 /\ 0 <= (-1 + param1:74)
                     /\ z':279 = 0 /\ 0 <= x':280 /\ 0 <= (-1 + __cost':281)
                     /\ 0 <= (-1 + param1:74)))
         /\ (0 = K:278 \/ (1 + -param1:74) <= 0) /\ (K:273 + K:278) = K:282
         /\ 0 <= K:282 /\ x':280 <= param1:74)}

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

Base relation: 
{__cost := __cost':190
 z := z':188
 x := x':189
 y := param1:74
 return := havoc:197
 return@pos := type_err:198
 return@width := type_err:199
 when ((!(0 <= K:183)
          \/ mid_x:184 = (param0:71 + -K:183 + -((param1:74 * K:183))))
         /\ (!((0 <= K:183 /\ K:183 <= 0)) \/ mid_z:185 = z:95)
         /\ (!(1 <= K:183) \/ mid_z:185 = param1:74)
         /\ (!(0 <= K:183) \/ mid___cost:186 = (__cost:94 + K:183))
         /\ (!(0 <= K:183) \/ -mid_x:184 <= (-param0:71 + K:183))
         /\ (!(0 <= K:183)
               \/ -mid_x:184 <= (-param0:71 + (1/2 * K:183)
                                   + (1/2 * param1:74 * K:183)
                                   + (param0:71 * K:183)
                                   + (-1/2 * (K:183 * K:183))
                                   + (-1/2 * param1:74 * (K:183 * K:183))))
         /\ ((K:183 = 0 /\ param0:71 = mid_x:184 /\ z:95 = mid_z:185
                /\ __cost:94 = mid___cost:186)
               \/ (1 <= K:183 /\ 0 <= -param1:74
                     /\ 0 <= (-1 + -param1:74 + param0:71) /\ 0 <= __cost:94
                     /\ (-param1:74 + mid_z:185) = 0 /\ 0 <= -param1:74
                     /\ 0 <= mid_x:184 /\ 0 <= (-1 + mid___cost:186)))
         /\ (0 = K:183 \/ !((1 + -param1:74) <= 0))
         /\ (!((0 <= K:187 /\ K:187 <= 0)) \/ z':188 = mid_z:185)
         /\ (!(1 <= K:187) \/ z':188 = 0)
         /\ (!(0 <= K:187)
               \/ x':189 = (mid_x:184 + -K:187 + -((param1:74 * K:187))))
         /\ (!(0 <= K:187) \/ __cost':190 = (mid___cost:186 + K:187))
         /\ (!(0 <= K:187) \/ x':189 <= (mid_x:184 + (-2 * K:187)))
         /\ (!(0 <= K:187)
               \/ -x':189 <= (-mid_x:184 + (1/2 * K:187)
                                + (1/2 * param1:74 * K:187)
                                + (mid_x:184 * K:187)
                                + (-1/2 * (K:187 * K:187))
                                + (-1/2 * param1:74 * (K:187 * K:187))))
         /\ ((K:187 = 0 /\ mid_x:184 = x':189 /\ mid_z:185 = z':188
                /\ mid___cost:186 = __cost':190)
               \/ (1 <= K:187 /\ 0 <= (-1 + -param1:74 + mid_x:184)
                     /\ 0 <= mid___cost:186 /\ 0 <= (-1 + param1:74)
                     /\ z':188 = 0 /\ 0 <= x':189 /\ 0 <= (-1 + __cost':190)
                     /\ 0 <= (-1 + param1:74)))
         /\ (0 = K:187 \/ (1 + -param1:74) <= 0) /\ (K:183 + K:187) = K:191
         /\ 0 <= K:191 /\ x':189 <= param1:74)}

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

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

Variable bounds at line 20 in run

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

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