/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, 34>	Base relation: 
{z := (100 + (2 * y:92))
 x := (x:93 + -((y:92 + 1)))
 when y:92 < x:93}	
<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, 38>	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, 38> -> <Unique State Name, 24>	Base relation: 
{when z:94 <= 0}	
<Unique State Name, 38> -> <Unique State Name, 34>	Base relation: 
{__cost := (__cost:95 + 1)
 z := (z:94 + -1)
 when (0 < z:94 /\ 0 <= __cost:95 /\ 0 <= (__cost:95 + 1))}	
<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, 34> -> <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: 
{__cost := (__cost:95 + 1)
 z := (z:94 + -1)
 when (0 < z:94 /\ 0 <= __cost:95 /\ 0 <= (__cost:95 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':142) = (1)*(__cost:95) + 1
           (z':143) = (1)*(z:94) + (-1)*1
           }
          pre:
            [|__cost:95>=0; z:94-1>=0|]
          post:
            [|z':143>=0; __cost':142-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':142
   z := z':143
   when ((!(0 <= K:151) \/ mid___cost:154 = (__cost:95 + K:151))
           /\ (!(0 <= K:151) \/ mid_z:153 = (z:94 + -K:151))
           /\ ((K:151 = 0 /\ z:94 = mid_z:153 /\ __cost:95 = mid___cost:154)
                 \/ (1 <= K:151 /\ 0 <= __cost:95 /\ 0 <= (-1 + z:94)
                       /\ 0 <= mid_z:153 /\ 0 <= (-1 + mid___cost:154)))
           /\ K:152 = 0 /\ mid_z:153 = z':143 /\ mid___cost:154 = __cost':142
           /\ 0 = K:152 /\ (K:151 + K:152) = K:150 /\ 0 <= K:150)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':160
 z := z':159
 x := (x:93 + -((y:92 + 1)))
 when (y:92 < x:93 /\ (!(0 <= K:155) \/ mid___cost:156 = (__cost:95 + K:155))
         /\ (!(0 <= K:155) \/ mid_z:157 = ((100 + (2 * y:92)) + -K:155))
         /\ ((K:155 = 0 /\ (100 + (2 * y:92)) = mid_z:157
                /\ __cost:95 = mid___cost:156)
               \/ (1 <= K:155 /\ 0 <= __cost:95
                     /\ 0 <= (-1 + (100 + (2 * y:92))) /\ 0 <= mid_z:157
                     /\ 0 <= (-1 + mid___cost:156))) /\ K:158 = 0
         /\ mid_z:157 = z':159 /\ mid___cost:156 = __cost':160 /\ 0 = K:158
         /\ (K:155 + K:158) = K:161 /\ 0 <= K:161 /\ z':159 <= 0)}
**** alpha hat: 
  {<Split [!(-__cost:95 <= 0)
            (x':162) = (1)*(x:93) + (-1)*1 + (-1)*y:92
           (__cost':142) = (1)*(__cost:95) + 0
           (z':143) = 100*1 + 2*y:92
           (-x':162) <= (1)*(-x:93) + (-49)*1
           (-x':162) <= (1)*(-x:93) + x:93
           }
          pre:
            [|-__cost:95-1>=0; -y:92-50>=0; -y:92+x:93-1>=0|]
          post:
            [|-2y:92+z':143-100=0; -y:92-50>=0; -__cost':142-1>=0; x':162>=0|]
           (x':162) = (1)*(x:93) + (-1)*1 + (-1)*y:92
          (-__cost':142) <= (1)*(-__cost:95) + 0
          (-x':162) <= (1)*(-x:93) + x:93
          ((-__cost':142 + (-2 * x':162))) <= (1)*((-__cost:95 + (-2 * x:93)))
                                               + (-98)*1
          }
  pre:
    [|-y:92+x:93-1>=0; __cost:95>=0|]
  post:
    [|-2y:92+__cost':142+z':143-100>=0; -z':143>=0; x':162>=0;
      2y:92-z':143+100>=0|]],
[!((-99 + (-2 * y:92)) <= 0)
  (z':143) = 100*1 + 2*y:92
 (x':162) = (1)*(x:93) + (-1)*1 + (-1)*y:92
 (__cost':142) = (1)*(__cost:95) + 0
 (-x':162) <= (1)*(-x:93) + (-49)*1
 (-x':162) <= (1)*(-x:93) + x:93
 } pre:   [|-y:92-50>=0; -y:92+x:93-1>=0|] post:
  [|-2y:92+z':143-100=0; -y:92-50>=0; x':162>=0|]  (z':143) = 0
(x':162) = (1)*(x:93) + (-1)*1 + (-1)*y:92
(__cost':142) = (1)*(__cost:95) + 100*1 + 2*y:92
(x':162) <= (1)*(x:93) + 48*1 (-x':162) <= (1)*(-x:93) + x:93 } pre:
  [|-y:92+x:93-1>=0; __cost:95>=0; y:92+49>=0|] post:
  [|z':143=0; -2y:92+__cost':142-100>=0; x':162>=0; y:92+49>=0|]]>}
**** star transition: 
  {__cost := __cost':142
   z := z':143
   x := x':162
   when ((!(0 <= K:190) \/ mid_x:192 = (x:93 + -K:190 + -((y:92 * K:190))))
           /\ (!(0 <= K:190) \/ mid___cost:194 = __cost:95)
           /\ (!((0 <= K:190 /\ K:190 <= 0)) \/ mid_z:193 = z:94)
           /\ (!(1 <= K:190) \/ mid_z:193 = (100 + z:94 + (2 * y:92) + -z:94))
           /\ (!(0 <= K:190) \/ -mid_x:192 <= (-x:93 + (-49 * K:190)))
           /\ (!(0 <= K:190)
                 \/ -mid_x:192 <= (-x:93 + (1/2 * K:190)
                                     + (1/2 * y:92 * K:190) + (x:93 * K:190)
                                     + (-1/2 * (K:190 * K:190))
                                     + (-1/2 * y:92 * (K:190 * K:190))))
           /\ ((K:190 = 0 /\ x:93 = mid_x:192 /\ z:94 = mid_z:193
                  /\ __cost:95 = mid___cost:194)
                 \/ (1 <= K:190 /\ 0 <= (-1 + -__cost:95)
                       /\ 0 <= (-50 + -y:92) /\ 0 <= (-1 + -y:92 + x:93)
                       /\ (-100 + (-2 * y:92) + mid_z:193) = 0
                       /\ 0 <= (-50 + -y:92) /\ 0 <= (-1 + -mid___cost:194)
                       /\ 0 <= mid_x:192))
           /\ (0 = K:190 \/ !(-__cost:95 <= 0))
           /\ (!(0 <= K:191)
                 \/ x':162 = (mid_x:192 + -K:191 + -((y:92 * K:191))))
           /\ (!(0 <= K:191) \/ -__cost':142 <= -mid___cost:194)
           /\ (!(0 <= K:191)
                 \/ -x':162 <= (-mid_x:192 + (1/2 * K:191)
                                  + (1/2 * y:92 * K:191)
                                  + (mid_x:192 * K:191)
                                  + (-1/2 * (K:191 * K:191))
                                  + (-1/2 * y:92 * (K:191 * K:191))))
           /\ (!(0 <= K:191)
                 \/ (-__cost':142 + (-2 * x':162)) <= ((-mid___cost:194
                                                          + (-2 * mid_x:192))
                                                         + (-98 * K:191)))
           /\ ((K:191 = 0 /\ mid_x:192 = x':162 /\ mid_z:193 = z':143
                  /\ mid___cost:194 = __cost':142)
                 \/ (1 <= K:191 /\ 0 <= (-1 + -y:92 + mid_x:192)
                       /\ 0 <= mid___cost:194
                       /\ 0 <= (-100 + (-2 * y:92) + __cost':142 + z':143)
                       /\ 0 <= -z':143 /\ 0 <= x':162
                       /\ 0 <= (100 + (2 * y:92) + -z':143)))
           /\ (0 = K:191 \/ -mid___cost:194 <= 0) /\ (K:190 + K:191) = K:189
           /\ (!((0 <= K:195 /\ K:195 <= 0)) \/ mid_z:198 = z:94)
           /\ (!(1 <= K:195) \/ mid_z:198 = (100 + z:94 + (2 * y:92) + -z:94))
           /\ (!(0 <= K:195)
                 \/ mid_x:197 = (x:93 + -K:195 + -((y:92 * K:195))))
           /\ (!(0 <= K:195) \/ mid___cost:199 = __cost:95)
           /\ (!(0 <= K:195) \/ -mid_x:197 <= (-x:93 + (-49 * K:195)))
           /\ (!(0 <= K:195)
                 \/ -mid_x:197 <= (-x:93 + (1/2 * K:195)
                                     + (1/2 * y:92 * K:195) + (x:93 * K:195)
                                     + (-1/2 * (K:195 * K:195))
                                     + (-1/2 * y:92 * (K:195 * K:195))))
           /\ ((K:195 = 0 /\ x:93 = mid_x:197 /\ z:94 = mid_z:198
                  /\ __cost:95 = mid___cost:199)
                 \/ (1 <= K:195 /\ 0 <= (-50 + -y:92)
                       /\ 0 <= (-1 + -y:92 + x:93)
                       /\ (-100 + (-2 * y:92) + mid_z:198) = 0
                       /\ 0 <= (-50 + -y:92) /\ 0 <= mid_x:197))
           /\ (0 = K:195 \/ !((-99 + (-2 * y:92)) <= 0))
           /\ (!((0 <= K:196 /\ K:196 <= 0)) \/ z':143 = mid_z:198)
           /\ (!(1 <= K:196) \/ z':143 = 0)
           /\ (!(0 <= K:196)
                 \/ x':162 = (mid_x:197 + -K:196 + -((y:92 * K:196))))
           /\ (!(0 <= K:196)
                 \/ __cost':142 = (mid___cost:199 + (100 * K:196)
                                     + (2 * y:92 * K:196)))
           /\ (!(0 <= K:196) \/ x':162 <= (mid_x:197 + (48 * K:196)))
           /\ (!(0 <= K:196)
                 \/ -x':162 <= (-mid_x:197 + (1/2 * K:196)
                                  + (1/2 * y:92 * K:196)
                                  + (mid_x:197 * K:196)
                                  + (-1/2 * (K:196 * K:196))
                                  + (-1/2 * y:92 * (K:196 * K:196))))
           /\ ((K:196 = 0 /\ mid_x:197 = x':162 /\ mid_z:198 = z':143
                  /\ mid___cost:199 = __cost':142)
                 \/ (1 <= K:196 /\ 0 <= (-1 + -y:92 + mid_x:197)
                       /\ 0 <= mid___cost:199 /\ 0 <= (49 + y:92)
                       /\ z':143 = 0
                       /\ 0 <= (-100 + (-2 * y:92) + __cost':142)
                       /\ 0 <= x':162 /\ 0 <= (49 + y:92)))
           /\ (0 = K:196 \/ (-99 + (-2 * y:92)) <= 0)
           /\ (K:195 + K:196) = K:189 /\ 0 <= K:189)}
}
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':206
   z := z':207
   x := x':205
   y := param1:74
   return := havoc:221
   return@pos := type_err:222
   return@width := type_err:223
   when ((!(0 <= K:200)
            \/ mid_x:201 = (param0:71 + -K:200 + -((param1:74 * K:200))))
           /\ (!(0 <= K:200) \/ mid___cost:202 = __cost:95)
           /\ (!((0 <= K:200 /\ K:200 <= 0)) \/ mid_z:203 = z:94)
           /\ (!(1 <= K:200)
                 \/ mid_z:203 = (100 + z:94 + (2 * param1:74) + -z:94))
           /\ (!(0 <= K:200) \/ -mid_x:201 <= (-param0:71 + (-49 * K:200)))
           /\ (!(0 <= K:200)
                 \/ -mid_x:201 <= (-param0:71 + (1/2 * K:200)
                                     + (1/2 * param1:74 * K:200)
                                     + (param0:71 * K:200)
                                     + (-1/2 * (K:200 * K:200))
                                     + (-1/2 * param1:74 * (K:200 * K:200))))
           /\ ((K:200 = 0 /\ param0:71 = mid_x:201 /\ z:94 = mid_z:203
                  /\ __cost:95 = mid___cost:202)
                 \/ (1 <= K:200 /\ 0 <= (-1 + -__cost:95)
                       /\ 0 <= (-50 + -param1:74)
                       /\ 0 <= (-1 + -param1:74 + param0:71)
                       /\ (-100 + (-2 * param1:74) + mid_z:203) = 0
                       /\ 0 <= (-50 + -param1:74)
                       /\ 0 <= (-1 + -mid___cost:202) /\ 0 <= mid_x:201))
           /\ (0 = K:200 \/ !(-__cost:95 <= 0))
           /\ (!(0 <= K:204)
                 \/ x':205 = (mid_x:201 + -K:204 + -((param1:74 * K:204))))
           /\ (!(0 <= K:204) \/ -__cost':206 <= -mid___cost:202)
           /\ (!(0 <= K:204)
                 \/ -x':205 <= (-mid_x:201 + (1/2 * K:204)
                                  + (1/2 * param1:74 * K:204)
                                  + (mid_x:201 * K:204)
                                  + (-1/2 * (K:204 * K:204))
                                  + (-1/2 * param1:74 * (K:204 * K:204))))
           /\ (!(0 <= K:204)
                 \/ (-__cost':206 + (-2 * x':205)) <= ((-mid___cost:202
                                                          + (-2 * mid_x:201))
                                                         + (-98 * K:204)))
           /\ ((K:204 = 0 /\ mid_x:201 = x':205 /\ mid_z:203 = z':207
                  /\ mid___cost:202 = __cost':206)
                 \/ (1 <= K:204 /\ 0 <= (-1 + -param1:74 + mid_x:201)
                       /\ 0 <= mid___cost:202
                       /\ 0 <= (-100 + (-2 * param1:74) + __cost':206
                                  + z':207) /\ 0 <= -z':207 /\ 0 <= x':205
                       /\ 0 <= (100 + (2 * param1:74) + -z':207)))
           /\ (0 = K:204 \/ -mid___cost:202 <= 0) /\ (K:200 + K:204) = K:208
           /\ (!((0 <= K:209 /\ K:209 <= 0)) \/ mid_z:210 = z:94)
           /\ (!(1 <= K:209)
                 \/ mid_z:210 = (100 + z:94 + (2 * param1:74) + -z:94))
           /\ (!(0 <= K:209)
                 \/ mid_x:211 = (param0:71 + -K:209 + -((param1:74 * K:209))))
           /\ (!(0 <= K:209) \/ mid___cost:212 = __cost:95)
           /\ (!(0 <= K:209) \/ -mid_x:211 <= (-param0:71 + (-49 * K:209)))
           /\ (!(0 <= K:209)
                 \/ -mid_x:211 <= (-param0:71 + (1/2 * K:209)
                                     + (1/2 * param1:74 * K:209)
                                     + (param0:71 * K:209)
                                     + (-1/2 * (K:209 * K:209))
                                     + (-1/2 * param1:74 * (K:209 * K:209))))
           /\ ((K:209 = 0 /\ param0:71 = mid_x:211 /\ z:94 = mid_z:210
                  /\ __cost:95 = mid___cost:212)
                 \/ (1 <= K:209 /\ 0 <= (-50 + -param1:74)
                       /\ 0 <= (-1 + -param1:74 + param0:71)
                       /\ (-100 + (-2 * param1:74) + mid_z:210) = 0
                       /\ 0 <= (-50 + -param1:74) /\ 0 <= mid_x:211))
           /\ (0 = K:209 \/ !((-99 + (-2 * param1:74)) <= 0))
           /\ (!((0 <= K:213 /\ K:213 <= 0)) \/ z':207 = mid_z:210)
           /\ (!(1 <= K:213) \/ z':207 = 0)
           /\ (!(0 <= K:213)
                 \/ x':205 = (mid_x:211 + -K:213 + -((param1:74 * K:213))))
           /\ (!(0 <= K:213)
                 \/ __cost':206 = (mid___cost:212 + (100 * K:213)
                                     + (2 * param1:74 * K:213)))
           /\ (!(0 <= K:213) \/ x':205 <= (mid_x:211 + (48 * K:213)))
           /\ (!(0 <= K:213)
                 \/ -x':205 <= (-mid_x:211 + (1/2 * K:213)
                                  + (1/2 * param1:74 * K:213)
                                  + (mid_x:211 * K:213)
                                  + (-1/2 * (K:213 * K:213))
                                  + (-1/2 * param1:74 * (K:213 * K:213))))
           /\ ((K:213 = 0 /\ mid_x:211 = x':205 /\ mid_z:210 = z':207
                  /\ mid___cost:212 = __cost':206)
                 \/ (1 <= K:213 /\ 0 <= (-1 + -param1:74 + mid_x:211)
                       /\ 0 <= mid___cost:212 /\ 0 <= (49 + param1:74)
                       /\ z':207 = 0
                       /\ 0 <= (-100 + (-2 * param1:74) + __cost':206)
                       /\ 0 <= x':205 /\ 0 <= (49 + param1:74)))
           /\ (0 = K:213 \/ (-99 + (-2 * param1:74)) <= 0)
           /\ (K:209 + K:213) = K:208 /\ 0 <= K:208 /\ x':205 <= 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':206
   return := havoc:221
   return@pos := type_err:222
   return@width := type_err:223
   when ((!(0 <= K:200)
            \/ mid_x:201 = (param0:71 + -K:200 + -((param1:74 * K:200))))
           /\ (!(0 <= K:200) \/ mid___cost:202 = __cost:95)
           /\ (!((0 <= K:200 /\ K:200 <= 0)) \/ mid_z:203 = z:224)
           /\ (!(1 <= K:200)
                 \/ mid_z:203 = (100 + z:224 + (2 * param1:74) + -z:224))
           /\ (!(0 <= K:200) \/ -mid_x:201 <= (-param0:71 + (-49 * K:200)))
           /\ (!(0 <= K:200)
                 \/ -mid_x:201 <= (-param0:71 + (1/2 * K:200)
                                     + (1/2 * param1:74 * K:200)
                                     + (param0:71 * K:200)
                                     + (-1/2 * (K:200 * K:200))
                                     + (-1/2 * param1:74 * (K:200 * K:200))))
           /\ ((K:200 = 0 /\ param0:71 = mid_x:201 /\ z:224 = mid_z:203
                  /\ __cost:95 = mid___cost:202)
                 \/ (1 <= K:200 /\ 0 <= (-1 + -__cost:95)
                       /\ 0 <= (-50 + -param1:74)
                       /\ 0 <= (-1 + -param1:74 + param0:71)
                       /\ (-100 + (-2 * param1:74) + mid_z:203) = 0
                       /\ 0 <= (-50 + -param1:74)
                       /\ 0 <= (-1 + -mid___cost:202) /\ 0 <= mid_x:201))
           /\ (0 = K:200 \/ !(-__cost:95 <= 0))
           /\ (!(0 <= K:204)
                 \/ x':205 = (mid_x:201 + -K:204 + -((param1:74 * K:204))))
           /\ (!(0 <= K:204) \/ -__cost':206 <= -mid___cost:202)
           /\ (!(0 <= K:204)
                 \/ -x':205 <= (-mid_x:201 + (1/2 * K:204)
                                  + (1/2 * param1:74 * K:204)
                                  + (mid_x:201 * K:204)
                                  + (-1/2 * (K:204 * K:204))
                                  + (-1/2 * param1:74 * (K:204 * K:204))))
           /\ (!(0 <= K:204)
                 \/ (-__cost':206 + (-2 * x':205)) <= ((-mid___cost:202
                                                          + (-2 * mid_x:201))
                                                         + (-98 * K:204)))
           /\ ((K:204 = 0 /\ mid_x:201 = x':205 /\ mid_z:203 = z':207
                  /\ mid___cost:202 = __cost':206)
                 \/ (1 <= K:204 /\ 0 <= (-1 + -param1:74 + mid_x:201)
                       /\ 0 <= mid___cost:202
                       /\ 0 <= (-100 + (-2 * param1:74) + __cost':206
                                  + z':207) /\ 0 <= -z':207 /\ 0 <= x':205
                       /\ 0 <= (100 + (2 * param1:74) + -z':207)))
           /\ (0 = K:204 \/ -mid___cost:202 <= 0) /\ (K:200 + K:204) = K:208
           /\ (!((0 <= K:209 /\ K:209 <= 0)) \/ mid_z:210 = z:224)
           /\ (!(1 <= K:209)
                 \/ mid_z:210 = (100 + z:224 + (2 * param1:74) + -z:224))
           /\ (!(0 <= K:209)
                 \/ mid_x:211 = (param0:71 + -K:209 + -((param1:74 * K:209))))
           /\ (!(0 <= K:209) \/ mid___cost:212 = __cost:95)
           /\ (!(0 <= K:209) \/ -mid_x:211 <= (-param0:71 + (-49 * K:209)))
           /\ (!(0 <= K:209)
                 \/ -mid_x:211 <= (-param0:71 + (1/2 * K:209)
                                     + (1/2 * param1:74 * K:209)
                                     + (param0:71 * K:209)
                                     + (-1/2 * (K:209 * K:209))
                                     + (-1/2 * param1:74 * (K:209 * K:209))))
           /\ ((K:209 = 0 /\ param0:71 = mid_x:211 /\ z:224 = mid_z:210
                  /\ __cost:95 = mid___cost:212)
                 \/ (1 <= K:209 /\ 0 <= (-50 + -param1:74)
                       /\ 0 <= (-1 + -param1:74 + param0:71)
                       /\ (-100 + (-2 * param1:74) + mid_z:210) = 0
                       /\ 0 <= (-50 + -param1:74) /\ 0 <= mid_x:211))
           /\ (0 = K:209 \/ !((-99 + (-2 * param1:74)) <= 0))
           /\ (!((0 <= K:213 /\ K:213 <= 0)) \/ z':207 = mid_z:210)
           /\ (!(1 <= K:213) \/ z':207 = 0)
           /\ (!(0 <= K:213)
                 \/ x':205 = (mid_x:211 + -K:213 + -((param1:74 * K:213))))
           /\ (!(0 <= K:213)
                 \/ __cost':206 = (mid___cost:212 + (100 * K:213)
                                     + (2 * param1:74 * K:213)))
           /\ (!(0 <= K:213) \/ x':205 <= (mid_x:211 + (48 * K:213)))
           /\ (!(0 <= K:213)
                 \/ -x':205 <= (-mid_x:211 + (1/2 * K:213)
                                  + (1/2 * param1:74 * K:213)
                                  + (mid_x:211 * K:213)
                                  + (-1/2 * (K:213 * K:213))
                                  + (-1/2 * param1:74 * (K:213 * K:213))))
           /\ ((K:213 = 0 /\ mid_x:211 = x':205 /\ mid_z:210 = z':207
                  /\ mid___cost:212 = __cost':206)
                 \/ (1 <= K:213 /\ 0 <= (-1 + -param1:74 + mid_x:211)
                       /\ 0 <= mid___cost:212 /\ 0 <= (49 + param1:74)
                       /\ z':207 = 0
                       /\ 0 <= (-100 + (-2 * param1:74) + __cost':206)
                       /\ 0 <= x':205 /\ 0 <= (49 + param1:74)))
           /\ (0 = K:213 \/ (-99 + (-2 * param1:74)) <= 0)
           /\ (K:209 + K:213) = K:208 /\ 0 <= K:208 /\ x':205 <= param1:74)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':253
   return := 0
   param0 := havoc:20
   param1 := havoc:21
   return@pos := type_err:269
   param0@pos := type_err:263
   param1@pos := type_err:264
   return@width := type_err:270
   param0@width := type_err:266
   param1@width := type_err:267
   when (0 <= havoc:21
           /\ (!(0 <= K:246)
                 \/ mid_x:247 = (havoc:20 + -K:246 + -((havoc:21 * K:246))))
           /\ (!(0 <= K:246) \/ mid___cost:248 = 0)
           /\ (!((0 <= K:246 /\ K:246 <= 0)) \/ mid_z:249 = z:250)
           /\ (!(1 <= K:246)
                 \/ mid_z:249 = (100 + z:250 + (2 * havoc:21) + -z:250))
           /\ (!(0 <= K:246) \/ -mid_x:247 <= (-havoc:20 + (-49 * K:246)))
           /\ (!(0 <= K:246)
                 \/ -mid_x:247 <= (-havoc:20 + (1/2 * K:246)
                                     + (1/2 * havoc:21 * K:246)
                                     + (havoc:20 * K:246)
                                     + (-1/2 * (K:246 * K:246))
                                     + (-1/2 * havoc:21 * (K:246 * K:246))))
           /\ K:246 = 0 /\ havoc:20 = mid_x:247 /\ z:250 = mid_z:249
           /\ 0 = mid___cost:248 /\ 0 = K:246
           /\ (!(0 <= K:251)
                 \/ x':252 = (mid_x:247 + -K:251 + -((havoc:21 * K:251))))
           /\ (!(0 <= K:251) \/ -__cost':253 <= -mid___cost:248)
           /\ (!(0 <= K:251)
                 \/ -x':252 <= (-mid_x:247 + (1/2 * K:251)
                                  + (1/2 * havoc:21 * K:251)
                                  + (mid_x:247 * K:251)
                                  + (-1/2 * (K:251 * K:251))
                                  + (-1/2 * havoc:21 * (K:251 * K:251))))
           /\ (!(0 <= K:251)
                 \/ (-__cost':253 + (-2 * x':252)) <= ((-mid___cost:248
                                                          + (-2 * mid_x:247))
                                                         + (-98 * K:251)))
           /\ ((K:251 = 0 /\ mid_x:247 = x':252 /\ mid_z:249 = z':254
                  /\ mid___cost:248 = __cost':253)
                 \/ (1 <= K:251 /\ 0 <= (-1 + -havoc:21 + mid_x:247)
                       /\ 0 <= mid___cost:248
                       /\ 0 <= (-100 + (-2 * havoc:21) + __cost':253 + z':254)
                       /\ 0 <= -z':254 /\ 0 <= x':252
                       /\ 0 <= (100 + (2 * havoc:21) + -z':254)))
           /\ (0 = K:251 \/ -mid___cost:248 <= 0) /\ (K:246 + K:251) = K:255
           /\ (!((0 <= K:256 /\ K:256 <= 0)) \/ mid_z:257 = z:250)
           /\ (!(1 <= K:256)
                 \/ mid_z:257 = (100 + z:250 + (2 * havoc:21) + -z:250))
           /\ (!(0 <= K:256)
                 \/ mid_x:258 = (havoc:20 + -K:256 + -((havoc:21 * K:256))))
           /\ (!(0 <= K:256) \/ mid___cost:259 = 0)
           /\ (!(0 <= K:256) \/ -mid_x:258 <= (-havoc:20 + (-49 * K:256)))
           /\ (!(0 <= K:256)
                 \/ -mid_x:258 <= (-havoc:20 + (1/2 * K:256)
                                     + (1/2 * havoc:21 * K:256)
                                     + (havoc:20 * K:256)
                                     + (-1/2 * (K:256 * K:256))
                                     + (-1/2 * havoc:21 * (K:256 * K:256))))
           /\ ((K:256 = 0 /\ havoc:20 = mid_x:258 /\ z:250 = mid_z:257
                  /\ 0 = mid___cost:259)
                 \/ (1 <= K:256 /\ 0 <= (-50 + -havoc:21)
                       /\ 0 <= (-1 + -havoc:21 + havoc:20)
                       /\ (-100 + (-2 * havoc:21) + mid_z:257) = 0
                       /\ 0 <= (-50 + -havoc:21) /\ 0 <= mid_x:258))
           /\ (0 = K:256 \/ !((-99 + (-2 * havoc:21)) <= 0))
           /\ (!((0 <= K:260 /\ K:260 <= 0)) \/ z':254 = mid_z:257)
           /\ (!(1 <= K:260) \/ z':254 = 0)
           /\ (!(0 <= K:260)
                 \/ x':252 = (mid_x:258 + -K:260 + -((havoc:21 * K:260))))
           /\ (!(0 <= K:260)
                 \/ __cost':253 = (mid___cost:259 + (100 * K:260)
                                     + (2 * havoc:21 * K:260)))
           /\ (!(0 <= K:260) \/ x':252 <= (mid_x:258 + (48 * K:260)))
           /\ (!(0 <= K:260)
                 \/ -x':252 <= (-mid_x:258 + (1/2 * K:260)
                                  + (1/2 * havoc:21 * K:260)
                                  + (mid_x:258 * K:260)
                                  + (-1/2 * (K:260 * K:260))
                                  + (-1/2 * havoc:21 * (K:260 * K:260))))
           /\ ((K:260 = 0 /\ mid_x:258 = x':252 /\ mid_z:257 = z':254
                  /\ mid___cost:259 = __cost':253)
                 \/ (1 <= K:260 /\ 0 <= (-1 + -havoc:21 + mid_x:258)
                       /\ 0 <= mid___cost:259 /\ 0 <= (49 + havoc:21)
                       /\ z':254 = 0
                       /\ 0 <= (-100 + (-2 * havoc:21) + __cost':253)
                       /\ 0 <= x':252 /\ 0 <= (49 + havoc:21)))
           /\ (0 = K:260 \/ (-99 + (-2 * havoc:21)) <= 0)
           /\ (K:256 + K:260) = K:255 /\ 0 <= K:255 /\ x':252 <= havoc:21
           /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:268)
                 \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:268)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':278
   return := havoc:289
   param0 := param0:71
   param1 := param1:74
   return@pos := type_err:290
   param0@pos := type_err:79
   param1@pos := type_err:80
   return@width := type_err:291
   param0@width := type_err:81
   param1@width := type_err:82
   when ((!(0 <= K:271)
            \/ mid_x:272 = (param0:71 + -K:271 + -((param1:74 * K:271))))
           /\ (!(0 <= K:271) \/ mid___cost:273 = __cost:95)
           /\ (!((0 <= K:271 /\ K:271 <= 0)) \/ mid_z:274 = z:275)
           /\ (!(1 <= K:271)
                 \/ mid_z:274 = (100 + z:275 + (2 * param1:74) + -z:275))
           /\ (!(0 <= K:271) \/ -mid_x:272 <= (-param0:71 + (-49 * K:271)))
           /\ (!(0 <= K:271)
                 \/ -mid_x:272 <= (-param0:71 + (1/2 * K:271)
                                     + (1/2 * param1:74 * K:271)
                                     + (param0:71 * K:271)
                                     + (-1/2 * (K:271 * K:271))
                                     + (-1/2 * param1:74 * (K:271 * K:271))))
           /\ ((K:271 = 0 /\ param0:71 = mid_x:272 /\ z:275 = mid_z:274
                  /\ __cost:95 = mid___cost:273)
                 \/ (1 <= K:271 /\ 0 <= (-1 + -__cost:95)
                       /\ 0 <= (-50 + -param1:74)
                       /\ 0 <= (-1 + -param1:74 + param0:71)
                       /\ (-100 + (-2 * param1:74) + mid_z:274) = 0
                       /\ 0 <= (-50 + -param1:74)
                       /\ 0 <= (-1 + -mid___cost:273) /\ 0 <= mid_x:272))
           /\ (0 = K:271 \/ !(-__cost:95 <= 0))
           /\ (!(0 <= K:276)
                 \/ x':277 = (mid_x:272 + -K:276 + -((param1:74 * K:276))))
           /\ (!(0 <= K:276) \/ -__cost':278 <= -mid___cost:273)
           /\ (!(0 <= K:276)
                 \/ -x':277 <= (-mid_x:272 + (1/2 * K:276)
                                  + (1/2 * param1:74 * K:276)
                                  + (mid_x:272 * K:276)
                                  + (-1/2 * (K:276 * K:276))
                                  + (-1/2 * param1:74 * (K:276 * K:276))))
           /\ (!(0 <= K:276)
                 \/ (-__cost':278 + (-2 * x':277)) <= ((-mid___cost:273
                                                          + (-2 * mid_x:272))
                                                         + (-98 * K:276)))
           /\ ((K:276 = 0 /\ mid_x:272 = x':277 /\ mid_z:274 = z':279
                  /\ mid___cost:273 = __cost':278)
                 \/ (1 <= K:276 /\ 0 <= (-1 + -param1:74 + mid_x:272)
                       /\ 0 <= mid___cost:273
                       /\ 0 <= (-100 + (-2 * param1:74) + __cost':278
                                  + z':279) /\ 0 <= -z':279 /\ 0 <= x':277
                       /\ 0 <= (100 + (2 * param1:74) + -z':279)))
           /\ (0 = K:276 \/ -mid___cost:273 <= 0) /\ (K:271 + K:276) = K:280
           /\ (!((0 <= K:281 /\ K:281 <= 0)) \/ mid_z:282 = z:275)
           /\ (!(1 <= K:281)
                 \/ mid_z:282 = (100 + z:275 + (2 * param1:74) + -z:275))
           /\ (!(0 <= K:281)
                 \/ mid_x:283 = (param0:71 + -K:281 + -((param1:74 * K:281))))
           /\ (!(0 <= K:281) \/ mid___cost:284 = __cost:95)
           /\ (!(0 <= K:281) \/ -mid_x:283 <= (-param0:71 + (-49 * K:281)))
           /\ (!(0 <= K:281)
                 \/ -mid_x:283 <= (-param0:71 + (1/2 * K:281)
                                     + (1/2 * param1:74 * K:281)
                                     + (param0:71 * K:281)
                                     + (-1/2 * (K:281 * K:281))
                                     + (-1/2 * param1:74 * (K:281 * K:281))))
           /\ ((K:281 = 0 /\ param0:71 = mid_x:283 /\ z:275 = mid_z:282
                  /\ __cost:95 = mid___cost:284)
                 \/ (1 <= K:281 /\ 0 <= (-50 + -param1:74)
                       /\ 0 <= (-1 + -param1:74 + param0:71)
                       /\ (-100 + (-2 * param1:74) + mid_z:282) = 0
                       /\ 0 <= (-50 + -param1:74) /\ 0 <= mid_x:283))
           /\ (0 = K:281 \/ !((-99 + (-2 * param1:74)) <= 0))
           /\ (!((0 <= K:285 /\ K:285 <= 0)) \/ z':279 = mid_z:282)
           /\ (!(1 <= K:285) \/ z':279 = 0)
           /\ (!(0 <= K:285)
                 \/ x':277 = (mid_x:283 + -K:285 + -((param1:74 * K:285))))
           /\ (!(0 <= K:285)
                 \/ __cost':278 = (mid___cost:284 + (100 * K:285)
                                     + (2 * param1:74 * K:285)))
           /\ (!(0 <= K:285) \/ x':277 <= (mid_x:283 + (48 * K:285)))
           /\ (!(0 <= K:285)
                 \/ -x':277 <= (-mid_x:283 + (1/2 * K:285)
                                  + (1/2 * param1:74 * K:285)
                                  + (mid_x:283 * K:285)
                                  + (-1/2 * (K:285 * K:285))
                                  + (-1/2 * param1:74 * (K:285 * K:285))))
           /\ ((K:285 = 0 /\ mid_x:283 = x':277 /\ mid_z:282 = z':279
                  /\ mid___cost:284 = __cost':278)
                 \/ (1 <= K:285 /\ 0 <= (-1 + -param1:74 + mid_x:283)
                       /\ 0 <= mid___cost:284 /\ 0 <= (49 + param1:74)
                       /\ z':279 = 0
                       /\ 0 <= (-100 + (-2 * param1:74) + __cost':278)
                       /\ 0 <= x':277 /\ 0 <= (49 + param1:74)))
           /\ (0 = K:285 \/ (-99 + (-2 * param1:74)) <= 0)
           /\ (K:281 + K:285) = K:280 /\ 0 <= K:280 /\ x':277 <= param1:74)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=20: 
Weight(Base relation: 
  {__cost := __cost':206
   return := havoc:221
   return@pos := type_err:222
   return@width := type_err:223
   when ((!(0 <= K:200)
            \/ mid_x:201 = (param0:71 + -K:200 + -((param1:74 * K:200))))
           /\ (!(0 <= K:200) \/ mid___cost:202 = __cost:95)
           /\ (!((0 <= K:200 /\ K:200 <= 0)) \/ mid_z:203 = z:224)
           /\ (!(1 <= K:200)
                 \/ mid_z:203 = (100 + z:224 + (2 * param1:74) + -z:224))
           /\ (!(0 <= K:200) \/ -mid_x:201 <= (-param0:71 + (-49 * K:200)))
           /\ (!(0 <= K:200)
                 \/ -mid_x:201 <= (-param0:71 + (1/2 * K:200)
                                     + (1/2 * param1:74 * K:200)
                                     + (param0:71 * K:200)
                                     + (-1/2 * (K:200 * K:200))
                                     + (-1/2 * param1:74 * (K:200 * K:200))))
           /\ ((K:200 = 0 /\ param0:71 = mid_x:201 /\ z:224 = mid_z:203
                  /\ __cost:95 = mid___cost:202)
                 \/ (1 <= K:200 /\ 0 <= (-1 + -__cost:95)
                       /\ 0 <= (-50 + -param1:74)
                       /\ 0 <= (-1 + -param1:74 + param0:71)
                       /\ (-100 + (-2 * param1:74) + mid_z:203) = 0
                       /\ 0 <= (-50 + -param1:74)
                       /\ 0 <= (-1 + -mid___cost:202) /\ 0 <= mid_x:201))
           /\ (0 = K:200 \/ !(-__cost:95 <= 0))
           /\ (!(0 <= K:204)
                 \/ x':205 = (mid_x:201 + -K:204 + -((param1:74 * K:204))))
           /\ (!(0 <= K:204) \/ -__cost':206 <= -mid___cost:202)
           /\ (!(0 <= K:204)
                 \/ -x':205 <= (-mid_x:201 + (1/2 * K:204)
                                  + (1/2 * param1:74 * K:204)
                                  + (mid_x:201 * K:204)
                                  + (-1/2 * (K:204 * K:204))
                                  + (-1/2 * param1:74 * (K:204 * K:204))))
           /\ (!(0 <= K:204)
                 \/ (-__cost':206 + (-2 * x':205)) <= ((-mid___cost:202
                                                          + (-2 * mid_x:201))
                                                         + (-98 * K:204)))
           /\ ((K:204 = 0 /\ mid_x:201 = x':205 /\ mid_z:203 = z':207
                  /\ mid___cost:202 = __cost':206)
                 \/ (1 <= K:204 /\ 0 <= (-1 + -param1:74 + mid_x:201)
                       /\ 0 <= mid___cost:202
                       /\ 0 <= (-100 + (-2 * param1:74) + __cost':206
                                  + z':207) /\ 0 <= -z':207 /\ 0 <= x':205
                       /\ 0 <= (100 + (2 * param1:74) + -z':207)))
           /\ (0 = K:204 \/ -mid___cost:202 <= 0) /\ (K:200 + K:204) = K:208
           /\ (!((0 <= K:209 /\ K:209 <= 0)) \/ mid_z:210 = z:224)
           /\ (!(1 <= K:209)
                 \/ mid_z:210 = (100 + z:224 + (2 * param1:74) + -z:224))
           /\ (!(0 <= K:209)
                 \/ mid_x:211 = (param0:71 + -K:209 + -((param1:74 * K:209))))
           /\ (!(0 <= K:209) \/ mid___cost:212 = __cost:95)
           /\ (!(0 <= K:209) \/ -mid_x:211 <= (-param0:71 + (-49 * K:209)))
           /\ (!(0 <= K:209)
                 \/ -mid_x:211 <= (-param0:71 + (1/2 * K:209)
                                     + (1/2 * param1:74 * K:209)
                                     + (param0:71 * K:209)
                                     + (-1/2 * (K:209 * K:209))
                                     + (-1/2 * param1:74 * (K:209 * K:209))))
           /\ ((K:209 = 0 /\ param0:71 = mid_x:211 /\ z:224 = mid_z:210
                  /\ __cost:95 = mid___cost:212)
                 \/ (1 <= K:209 /\ 0 <= (-50 + -param1:74)
                       /\ 0 <= (-1 + -param1:74 + param0:71)
                       /\ (-100 + (-2 * param1:74) + mid_z:210) = 0
                       /\ 0 <= (-50 + -param1:74) /\ 0 <= mid_x:211))
           /\ (0 = K:209 \/ !((-99 + (-2 * param1:74)) <= 0))
           /\ (!((0 <= K:213 /\ K:213 <= 0)) \/ z':207 = mid_z:210)
           /\ (!(1 <= K:213) \/ z':207 = 0)
           /\ (!(0 <= K:213)
                 \/ x':205 = (mid_x:211 + -K:213 + -((param1:74 * K:213))))
           /\ (!(0 <= K:213)
                 \/ __cost':206 = (mid___cost:212 + (100 * K:213)
                                     + (2 * param1:74 * K:213)))
           /\ (!(0 <= K:213) \/ x':205 <= (mid_x:211 + (48 * K:213)))
           /\ (!(0 <= K:213)
                 \/ -x':205 <= (-mid_x:211 + (1/2 * K:213)
                                  + (1/2 * param1:74 * K:213)
                                  + (mid_x:211 * K:213)
                                  + (-1/2 * (K:213 * K:213))
                                  + (-1/2 * param1:74 * (K:213 * K:213))))
           /\ ((K:213 = 0 /\ mid_x:211 = x':205 /\ mid_z:210 = z':207
                  /\ mid___cost:212 = __cost':206)
                 \/ (1 <= K:213 /\ 0 <= (-1 + -param1:74 + mid_x:211)
                       /\ 0 <= mid___cost:212 /\ 0 <= (49 + param1:74)
                       /\ z':207 = 0
                       /\ 0 <= (-100 + (-2 * param1:74) + __cost':206)
                       /\ 0 <= x':205 /\ 0 <= (49 + param1:74)))
           /\ (0 = K:213 \/ (-99 + (-2 * param1:74)) <= 0)
           /\ (K:209 + K:213) = K:208 /\ 0 <= K:208 /\ x':205 <= 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':253
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:269
 param0@pos := type_err:263
 param1@pos := type_err:264
 return@width := type_err:270
 param0@width := type_err:266
 param1@width := type_err:267
 when (0 <= havoc:21
         /\ (!(0 <= K:246)
               \/ mid_x:247 = (havoc:20 + -K:246 + -((havoc:21 * K:246))))
         /\ (!(0 <= K:246) \/ mid___cost:248 = 0)
         /\ (!((0 <= K:246 /\ K:246 <= 0)) \/ mid_z:249 = z:250)
         /\ (!(1 <= K:246)
               \/ mid_z:249 = (100 + z:250 + (2 * havoc:21) + -z:250))
         /\ (!(0 <= K:246) \/ -mid_x:247 <= (-havoc:20 + (-49 * K:246)))
         /\ (!(0 <= K:246)
               \/ -mid_x:247 <= (-havoc:20 + (1/2 * K:246)
                                   + (1/2 * havoc:21 * K:246)
                                   + (havoc:20 * K:246)
                                   + (-1/2 * (K:246 * K:246))
                                   + (-1/2 * havoc:21 * (K:246 * K:246))))
         /\ K:246 = 0 /\ havoc:20 = mid_x:247 /\ z:250 = mid_z:249
         /\ 0 = mid___cost:248 /\ 0 = K:246
         /\ (!(0 <= K:251)
               \/ x':252 = (mid_x:247 + -K:251 + -((havoc:21 * K:251))))
         /\ (!(0 <= K:251) \/ -__cost':253 <= -mid___cost:248)
         /\ (!(0 <= K:251)
               \/ -x':252 <= (-mid_x:247 + (1/2 * K:251)
                                + (1/2 * havoc:21 * K:251)
                                + (mid_x:247 * K:251)
                                + (-1/2 * (K:251 * K:251))
                                + (-1/2 * havoc:21 * (K:251 * K:251))))
         /\ (!(0 <= K:251)
               \/ (-__cost':253 + (-2 * x':252)) <= ((-mid___cost:248
                                                        + (-2 * mid_x:247))
                                                       + (-98 * K:251)))
         /\ ((K:251 = 0 /\ mid_x:247 = x':252 /\ mid_z:249 = z':254
                /\ mid___cost:248 = __cost':253)
               \/ (1 <= K:251 /\ 0 <= (-1 + -havoc:21 + mid_x:247)
                     /\ 0 <= mid___cost:248
                     /\ 0 <= (-100 + (-2 * havoc:21) + __cost':253 + z':254)
                     /\ 0 <= -z':254 /\ 0 <= x':252
                     /\ 0 <= (100 + (2 * havoc:21) + -z':254)))
         /\ (0 = K:251 \/ -mid___cost:248 <= 0) /\ (K:246 + K:251) = K:255
         /\ (!((0 <= K:256 /\ K:256 <= 0)) \/ mid_z:257 = z:250)
         /\ (!(1 <= K:256)
               \/ mid_z:257 = (100 + z:250 + (2 * havoc:21) + -z:250))
         /\ (!(0 <= K:256)
               \/ mid_x:258 = (havoc:20 + -K:256 + -((havoc:21 * K:256))))
         /\ (!(0 <= K:256) \/ mid___cost:259 = 0)
         /\ (!(0 <= K:256) \/ -mid_x:258 <= (-havoc:20 + (-49 * K:256)))
         /\ (!(0 <= K:256)
               \/ -mid_x:258 <= (-havoc:20 + (1/2 * K:256)
                                   + (1/2 * havoc:21 * K:256)
                                   + (havoc:20 * K:256)
                                   + (-1/2 * (K:256 * K:256))
                                   + (-1/2 * havoc:21 * (K:256 * K:256))))
         /\ ((K:256 = 0 /\ havoc:20 = mid_x:258 /\ z:250 = mid_z:257
                /\ 0 = mid___cost:259)
               \/ (1 <= K:256 /\ 0 <= (-50 + -havoc:21)
                     /\ 0 <= (-1 + -havoc:21 + havoc:20)
                     /\ (-100 + (-2 * havoc:21) + mid_z:257) = 0
                     /\ 0 <= (-50 + -havoc:21) /\ 0 <= mid_x:258))
         /\ (0 = K:256 \/ !((-99 + (-2 * havoc:21)) <= 0))
         /\ (!((0 <= K:260 /\ K:260 <= 0)) \/ z':254 = mid_z:257)
         /\ (!(1 <= K:260) \/ z':254 = 0)
         /\ (!(0 <= K:260)
               \/ x':252 = (mid_x:258 + -K:260 + -((havoc:21 * K:260))))
         /\ (!(0 <= K:260)
               \/ __cost':253 = (mid___cost:259 + (100 * K:260)
                                   + (2 * havoc:21 * K:260)))
         /\ (!(0 <= K:260) \/ x':252 <= (mid_x:258 + (48 * K:260)))
         /\ (!(0 <= K:260)
               \/ -x':252 <= (-mid_x:258 + (1/2 * K:260)
                                + (1/2 * havoc:21 * K:260)
                                + (mid_x:258 * K:260)
                                + (-1/2 * (K:260 * K:260))
                                + (-1/2 * havoc:21 * (K:260 * K:260))))
         /\ ((K:260 = 0 /\ mid_x:258 = x':252 /\ mid_z:257 = z':254
                /\ mid___cost:259 = __cost':253)
               \/ (1 <= K:260 /\ 0 <= (-1 + -havoc:21 + mid_x:258)
                     /\ 0 <= mid___cost:259 /\ 0 <= (49 + havoc:21)
                     /\ z':254 = 0
                     /\ 0 <= (-100 + (-2 * havoc:21) + __cost':253)
                     /\ 0 <= x':252 /\ 0 <= (49 + havoc:21)))
         /\ (0 = K:260 \/ (-99 + (-2 * havoc:21)) <= 0)
         /\ (K:256 + K:260) = K:255 /\ 0 <= K:255 /\ x':252 <= havoc:21
         /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:268)
               \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:268)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':278
 return := havoc:289
 param0 := param0:71
 param1 := param1:74
 return@pos := type_err:290
 param0@pos := type_err:79
 param1@pos := type_err:80
 return@width := type_err:291
 param0@width := type_err:81
 param1@width := type_err:82
 when ((!(0 <= K:271)
          \/ mid_x:272 = (param0:71 + -K:271 + -((param1:74 * K:271))))
         /\ (!(0 <= K:271) \/ mid___cost:273 = __cost:95)
         /\ (!((0 <= K:271 /\ K:271 <= 0)) \/ mid_z:274 = z:275)
         /\ (!(1 <= K:271)
               \/ mid_z:274 = (100 + z:275 + (2 * param1:74) + -z:275))
         /\ (!(0 <= K:271) \/ -mid_x:272 <= (-param0:71 + (-49 * K:271)))
         /\ (!(0 <= K:271)
               \/ -mid_x:272 <= (-param0:71 + (1/2 * K:271)
                                   + (1/2 * param1:74 * K:271)
                                   + (param0:71 * K:271)
                                   + (-1/2 * (K:271 * K:271))
                                   + (-1/2 * param1:74 * (K:271 * K:271))))
         /\ ((K:271 = 0 /\ param0:71 = mid_x:272 /\ z:275 = mid_z:274
                /\ __cost:95 = mid___cost:273)
               \/ (1 <= K:271 /\ 0 <= (-1 + -__cost:95)
                     /\ 0 <= (-50 + -param1:74)
                     /\ 0 <= (-1 + -param1:74 + param0:71)
                     /\ (-100 + (-2 * param1:74) + mid_z:274) = 0
                     /\ 0 <= (-50 + -param1:74)
                     /\ 0 <= (-1 + -mid___cost:273) /\ 0 <= mid_x:272))
         /\ (0 = K:271 \/ !(-__cost:95 <= 0))
         /\ (!(0 <= K:276)
               \/ x':277 = (mid_x:272 + -K:276 + -((param1:74 * K:276))))
         /\ (!(0 <= K:276) \/ -__cost':278 <= -mid___cost:273)
         /\ (!(0 <= K:276)
               \/ -x':277 <= (-mid_x:272 + (1/2 * K:276)
                                + (1/2 * param1:74 * K:276)
                                + (mid_x:272 * K:276)
                                + (-1/2 * (K:276 * K:276))
                                + (-1/2 * param1:74 * (K:276 * K:276))))
         /\ (!(0 <= K:276)
               \/ (-__cost':278 + (-2 * x':277)) <= ((-mid___cost:273
                                                        + (-2 * mid_x:272))
                                                       + (-98 * K:276)))
         /\ ((K:276 = 0 /\ mid_x:272 = x':277 /\ mid_z:274 = z':279
                /\ mid___cost:273 = __cost':278)
               \/ (1 <= K:276 /\ 0 <= (-1 + -param1:74 + mid_x:272)
                     /\ 0 <= mid___cost:273
                     /\ 0 <= (-100 + (-2 * param1:74) + __cost':278 + z':279)
                     /\ 0 <= -z':279 /\ 0 <= x':277
                     /\ 0 <= (100 + (2 * param1:74) + -z':279)))
         /\ (0 = K:276 \/ -mid___cost:273 <= 0) /\ (K:271 + K:276) = K:280
         /\ (!((0 <= K:281 /\ K:281 <= 0)) \/ mid_z:282 = z:275)
         /\ (!(1 <= K:281)
               \/ mid_z:282 = (100 + z:275 + (2 * param1:74) + -z:275))
         /\ (!(0 <= K:281)
               \/ mid_x:283 = (param0:71 + -K:281 + -((param1:74 * K:281))))
         /\ (!(0 <= K:281) \/ mid___cost:284 = __cost:95)
         /\ (!(0 <= K:281) \/ -mid_x:283 <= (-param0:71 + (-49 * K:281)))
         /\ (!(0 <= K:281)
               \/ -mid_x:283 <= (-param0:71 + (1/2 * K:281)
                                   + (1/2 * param1:74 * K:281)
                                   + (param0:71 * K:281)
                                   + (-1/2 * (K:281 * K:281))
                                   + (-1/2 * param1:74 * (K:281 * K:281))))
         /\ ((K:281 = 0 /\ param0:71 = mid_x:283 /\ z:275 = mid_z:282
                /\ __cost:95 = mid___cost:284)
               \/ (1 <= K:281 /\ 0 <= (-50 + -param1:74)
                     /\ 0 <= (-1 + -param1:74 + param0:71)
                     /\ (-100 + (-2 * param1:74) + mid_z:282) = 0
                     /\ 0 <= (-50 + -param1:74) /\ 0 <= mid_x:283))
         /\ (0 = K:281 \/ !((-99 + (-2 * param1:74)) <= 0))
         /\ (!((0 <= K:285 /\ K:285 <= 0)) \/ z':279 = mid_z:282)
         /\ (!(1 <= K:285) \/ z':279 = 0)
         /\ (!(0 <= K:285)
               \/ x':277 = (mid_x:283 + -K:285 + -((param1:74 * K:285))))
         /\ (!(0 <= K:285)
               \/ __cost':278 = (mid___cost:284 + (100 * K:285)
                                   + (2 * param1:74 * K:285)))
         /\ (!(0 <= K:285) \/ x':277 <= (mid_x:283 + (48 * K:285)))
         /\ (!(0 <= K:285)
               \/ -x':277 <= (-mid_x:283 + (1/2 * K:285)
                                + (1/2 * param1:74 * K:285)
                                + (mid_x:283 * K:285)
                                + (-1/2 * (K:285 * K:285))
                                + (-1/2 * param1:74 * (K:285 * K:285))))
         /\ ((K:285 = 0 /\ mid_x:283 = x':277 /\ mid_z:282 = z':279
                /\ mid___cost:284 = __cost':278)
               \/ (1 <= K:285 /\ 0 <= (-1 + -param1:74 + mid_x:283)
                     /\ 0 <= mid___cost:284 /\ 0 <= (49 + param1:74)
                     /\ z':279 = 0
                     /\ 0 <= (-100 + (-2 * param1:74) + __cost':278)
                     /\ 0 <= x':277 /\ 0 <= (49 + param1:74)))
         /\ (0 = K:285 \/ (-99 + (-2 * param1:74)) <= 0)
         /\ (K:281 + K:285) = K:280 /\ 0 <= K:280 /\ x':277 <= param1:74)}

Evaluating variable number 20 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':206
 return := havoc:221
 return@pos := type_err:222
 return@width := type_err:223
 when ((!(0 <= K:200)
          \/ mid_x:201 = (param0:71 + -K:200 + -((param1:74 * K:200))))
         /\ (!(0 <= K:200) \/ mid___cost:202 = __cost:95)
         /\ (!((0 <= K:200 /\ K:200 <= 0)) \/ mid_z:203 = z:224)
         /\ (!(1 <= K:200)
               \/ mid_z:203 = (100 + z:224 + (2 * param1:74) + -z:224))
         /\ (!(0 <= K:200) \/ -mid_x:201 <= (-param0:71 + (-49 * K:200)))
         /\ (!(0 <= K:200)
               \/ -mid_x:201 <= (-param0:71 + (1/2 * K:200)
                                   + (1/2 * param1:74 * K:200)
                                   + (param0:71 * K:200)
                                   + (-1/2 * (K:200 * K:200))
                                   + (-1/2 * param1:74 * (K:200 * K:200))))
         /\ ((K:200 = 0 /\ param0:71 = mid_x:201 /\ z:224 = mid_z:203
                /\ __cost:95 = mid___cost:202)
               \/ (1 <= K:200 /\ 0 <= (-1 + -__cost:95)
                     /\ 0 <= (-50 + -param1:74)
                     /\ 0 <= (-1 + -param1:74 + param0:71)
                     /\ (-100 + (-2 * param1:74) + mid_z:203) = 0
                     /\ 0 <= (-50 + -param1:74)
                     /\ 0 <= (-1 + -mid___cost:202) /\ 0 <= mid_x:201))
         /\ (0 = K:200 \/ !(-__cost:95 <= 0))
         /\ (!(0 <= K:204)
               \/ x':205 = (mid_x:201 + -K:204 + -((param1:74 * K:204))))
         /\ (!(0 <= K:204) \/ -__cost':206 <= -mid___cost:202)
         /\ (!(0 <= K:204)
               \/ -x':205 <= (-mid_x:201 + (1/2 * K:204)
                                + (1/2 * param1:74 * K:204)
                                + (mid_x:201 * K:204)
                                + (-1/2 * (K:204 * K:204))
                                + (-1/2 * param1:74 * (K:204 * K:204))))
         /\ (!(0 <= K:204)
               \/ (-__cost':206 + (-2 * x':205)) <= ((-mid___cost:202
                                                        + (-2 * mid_x:201))
                                                       + (-98 * K:204)))
         /\ ((K:204 = 0 /\ mid_x:201 = x':205 /\ mid_z:203 = z':207
                /\ mid___cost:202 = __cost':206)
               \/ (1 <= K:204 /\ 0 <= (-1 + -param1:74 + mid_x:201)
                     /\ 0 <= mid___cost:202
                     /\ 0 <= (-100 + (-2 * param1:74) + __cost':206 + z':207)
                     /\ 0 <= -z':207 /\ 0 <= x':205
                     /\ 0 <= (100 + (2 * param1:74) + -z':207)))
         /\ (0 = K:204 \/ -mid___cost:202 <= 0) /\ (K:200 + K:204) = K:208
         /\ (!((0 <= K:209 /\ K:209 <= 0)) \/ mid_z:210 = z:224)
         /\ (!(1 <= K:209)
               \/ mid_z:210 = (100 + z:224 + (2 * param1:74) + -z:224))
         /\ (!(0 <= K:209)
               \/ mid_x:211 = (param0:71 + -K:209 + -((param1:74 * K:209))))
         /\ (!(0 <= K:209) \/ mid___cost:212 = __cost:95)
         /\ (!(0 <= K:209) \/ -mid_x:211 <= (-param0:71 + (-49 * K:209)))
         /\ (!(0 <= K:209)
               \/ -mid_x:211 <= (-param0:71 + (1/2 * K:209)
                                   + (1/2 * param1:74 * K:209)
                                   + (param0:71 * K:209)
                                   + (-1/2 * (K:209 * K:209))
                                   + (-1/2 * param1:74 * (K:209 * K:209))))
         /\ ((K:209 = 0 /\ param0:71 = mid_x:211 /\ z:224 = mid_z:210
                /\ __cost:95 = mid___cost:212)
               \/ (1 <= K:209 /\ 0 <= (-50 + -param1:74)
                     /\ 0 <= (-1 + -param1:74 + param0:71)
                     /\ (-100 + (-2 * param1:74) + mid_z:210) = 0
                     /\ 0 <= (-50 + -param1:74) /\ 0 <= mid_x:211))
         /\ (0 = K:209 \/ !((-99 + (-2 * param1:74)) <= 0))
         /\ (!((0 <= K:213 /\ K:213 <= 0)) \/ z':207 = mid_z:210)
         /\ (!(1 <= K:213) \/ z':207 = 0)
         /\ (!(0 <= K:213)
               \/ x':205 = (mid_x:211 + -K:213 + -((param1:74 * K:213))))
         /\ (!(0 <= K:213)
               \/ __cost':206 = (mid___cost:212 + (100 * K:213)
                                   + (2 * param1:74 * K:213)))
         /\ (!(0 <= K:213) \/ x':205 <= (mid_x:211 + (48 * K:213)))
         /\ (!(0 <= K:213)
               \/ -x':205 <= (-mid_x:211 + (1/2 * K:213)
                                + (1/2 * param1:74 * K:213)
                                + (mid_x:211 * K:213)
                                + (-1/2 * (K:213 * K:213))
                                + (-1/2 * param1:74 * (K:213 * K:213))))
         /\ ((K:213 = 0 /\ mid_x:211 = x':205 /\ mid_z:210 = z':207
                /\ mid___cost:212 = __cost':206)
               \/ (1 <= K:213 /\ 0 <= (-1 + -param1:74 + mid_x:211)
                     /\ 0 <= mid___cost:212 /\ 0 <= (49 + param1:74)
                     /\ z':207 = 0
                     /\ 0 <= (-100 + (-2 * param1:74) + __cost':206)
                     /\ 0 <= x':205 /\ 0 <= (49 + param1:74)))
         /\ (0 = K:213 \/ (-99 + (-2 * param1:74)) <= 0)
         /\ (K:209 + K:213) = K:208 /\ 0 <= K:208 /\ x':205 <= 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 0x4a47420: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x4a4acb0: 
	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:338
 param1@pos := type_err:339
 param0@width := type_err:340
 param1@width := type_err:341
 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 0x4ca9940: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x4a4a370: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
================================================
Procedure Summaries

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

Base relation: 
{__cost := __cost':299
 x := havoc:20
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:315
 param0@pos := type_err:309
 param1@pos := type_err:310
 return@width := type_err:316
 param0@width := type_err:312
 param1@width := type_err:313
 when (0 <= havoc:21
         /\ (!(0 <= K:292)
               \/ mid_x:293 = (havoc:20 + -K:292 + -((havoc:21 * K:292))))
         /\ (!(0 <= K:292) \/ mid___cost:294 = 0)
         /\ (!((0 <= K:292 /\ K:292 <= 0)) \/ mid_z:295 = z:296)
         /\ (!(1 <= K:292)
               \/ mid_z:295 = (100 + z:296 + (2 * havoc:21) + -z:296))
         /\ (!(0 <= K:292) \/ -mid_x:293 <= (-havoc:20 + (-49 * K:292)))
         /\ (!(0 <= K:292)
               \/ -mid_x:293 <= (-havoc:20 + (1/2 * K:292)
                                   + (1/2 * havoc:21 * K:292)
                                   + (havoc:20 * K:292)
                                   + (-1/2 * (K:292 * K:292))
                                   + (-1/2 * havoc:21 * (K:292 * K:292))))
         /\ K:292 = 0 /\ havoc:20 = mid_x:293 /\ z:296 = mid_z:295
         /\ 0 = mid___cost:294 /\ 0 = K:292
         /\ (!(0 <= K:297)
               \/ x':298 = (mid_x:293 + -K:297 + -((havoc:21 * K:297))))
         /\ (!(0 <= K:297) \/ -__cost':299 <= -mid___cost:294)
         /\ (!(0 <= K:297)
               \/ -x':298 <= (-mid_x:293 + (1/2 * K:297)
                                + (1/2 * havoc:21 * K:297)
                                + (mid_x:293 * K:297)
                                + (-1/2 * (K:297 * K:297))
                                + (-1/2 * havoc:21 * (K:297 * K:297))))
         /\ (!(0 <= K:297)
               \/ (-__cost':299 + (-2 * x':298)) <= ((-mid___cost:294
                                                        + (-2 * mid_x:293))
                                                       + (-98 * K:297)))
         /\ ((K:297 = 0 /\ mid_x:293 = x':298 /\ mid_z:295 = z':300
                /\ mid___cost:294 = __cost':299)
               \/ (1 <= K:297 /\ 0 <= (-1 + -havoc:21 + mid_x:293)
                     /\ 0 <= mid___cost:294
                     /\ 0 <= (-100 + (-2 * havoc:21) + __cost':299 + z':300)
                     /\ 0 <= -z':300 /\ 0 <= x':298
                     /\ 0 <= (100 + (2 * havoc:21) + -z':300)))
         /\ (0 = K:297 \/ -mid___cost:294 <= 0) /\ (K:292 + K:297) = K:301
         /\ (!((0 <= K:302 /\ K:302 <= 0)) \/ mid_z:303 = z:296)
         /\ (!(1 <= K:302)
               \/ mid_z:303 = (100 + z:296 + (2 * havoc:21) + -z:296))
         /\ (!(0 <= K:302)
               \/ mid_x:304 = (havoc:20 + -K:302 + -((havoc:21 * K:302))))
         /\ (!(0 <= K:302) \/ mid___cost:305 = 0)
         /\ (!(0 <= K:302) \/ -mid_x:304 <= (-havoc:20 + (-49 * K:302)))
         /\ (!(0 <= K:302)
               \/ -mid_x:304 <= (-havoc:20 + (1/2 * K:302)
                                   + (1/2 * havoc:21 * K:302)
                                   + (havoc:20 * K:302)
                                   + (-1/2 * (K:302 * K:302))
                                   + (-1/2 * havoc:21 * (K:302 * K:302))))
         /\ ((K:302 = 0 /\ havoc:20 = mid_x:304 /\ z:296 = mid_z:303
                /\ 0 = mid___cost:305)
               \/ (1 <= K:302 /\ 0 <= (-50 + -havoc:21)
                     /\ 0 <= (-1 + -havoc:21 + havoc:20)
                     /\ (-100 + (-2 * havoc:21) + mid_z:303) = 0
                     /\ 0 <= (-50 + -havoc:21) /\ 0 <= mid_x:304))
         /\ (0 = K:302 \/ !((-99 + (-2 * havoc:21)) <= 0))
         /\ (!((0 <= K:306 /\ K:306 <= 0)) \/ z':300 = mid_z:303)
         /\ (!(1 <= K:306) \/ z':300 = 0)
         /\ (!(0 <= K:306)
               \/ x':298 = (mid_x:304 + -K:306 + -((havoc:21 * K:306))))
         /\ (!(0 <= K:306)
               \/ __cost':299 = (mid___cost:305 + (100 * K:306)
                                   + (2 * havoc:21 * K:306)))
         /\ (!(0 <= K:306) \/ x':298 <= (mid_x:304 + (48 * K:306)))
         /\ (!(0 <= K:306)
               \/ -x':298 <= (-mid_x:304 + (1/2 * K:306)
                                + (1/2 * havoc:21 * K:306)
                                + (mid_x:304 * K:306)
                                + (-1/2 * (K:306 * K:306))
                                + (-1/2 * havoc:21 * (K:306 * K:306))))
         /\ ((K:306 = 0 /\ mid_x:304 = x':298 /\ mid_z:303 = z':300
                /\ mid___cost:305 = __cost':299)
               \/ (1 <= K:306 /\ 0 <= (-1 + -havoc:21 + mid_x:304)
                     /\ 0 <= mid___cost:305 /\ 0 <= (49 + havoc:21)
                     /\ z':300 = 0
                     /\ 0 <= (-100 + (-2 * havoc:21) + __cost':299)
                     /\ 0 <= x':298 /\ 0 <= (49 + havoc:21)))
         /\ (0 = K:306 \/ (-99 + (-2 * havoc:21)) <= 0)
         /\ (K:302 + K:306) = K:301 /\ 0 <= K:301 /\ x':298 <= havoc:21
         /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:314)
               \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:314)))}

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

Base relation: 
{__cost := __cost':324
 return := havoc:335
 param0 := param0:71
 param1 := param1:74
 return@pos := type_err:336
 param0@pos := type_err:79
 param1@pos := type_err:80
 return@width := type_err:337
 param0@width := type_err:81
 param1@width := type_err:82
 when ((!(0 <= K:317)
          \/ mid_x:318 = (param0:71 + -K:317 + -((param1:74 * K:317))))
         /\ (!(0 <= K:317) \/ mid___cost:319 = __cost:95)
         /\ (!((0 <= K:317 /\ K:317 <= 0)) \/ mid_z:320 = z:321)
         /\ (!(1 <= K:317)
               \/ mid_z:320 = (100 + z:321 + (2 * param1:74) + -z:321))
         /\ (!(0 <= K:317) \/ -mid_x:318 <= (-param0:71 + (-49 * K:317)))
         /\ (!(0 <= K:317)
               \/ -mid_x:318 <= (-param0:71 + (1/2 * K:317)
                                   + (1/2 * param1:74 * K:317)
                                   + (param0:71 * K:317)
                                   + (-1/2 * (K:317 * K:317))
                                   + (-1/2 * param1:74 * (K:317 * K:317))))
         /\ ((K:317 = 0 /\ param0:71 = mid_x:318 /\ z:321 = mid_z:320
                /\ __cost:95 = mid___cost:319)
               \/ (1 <= K:317 /\ 0 <= (-1 + -__cost:95)
                     /\ 0 <= (-50 + -param1:74)
                     /\ 0 <= (-1 + -param1:74 + param0:71)
                     /\ (-100 + (-2 * param1:74) + mid_z:320) = 0
                     /\ 0 <= (-50 + -param1:74)
                     /\ 0 <= (-1 + -mid___cost:319) /\ 0 <= mid_x:318))
         /\ (0 = K:317 \/ !(-__cost:95 <= 0))
         /\ (!(0 <= K:322)
               \/ x':323 = (mid_x:318 + -K:322 + -((param1:74 * K:322))))
         /\ (!(0 <= K:322) \/ -__cost':324 <= -mid___cost:319)
         /\ (!(0 <= K:322)
               \/ -x':323 <= (-mid_x:318 + (1/2 * K:322)
                                + (1/2 * param1:74 * K:322)
                                + (mid_x:318 * K:322)
                                + (-1/2 * (K:322 * K:322))
                                + (-1/2 * param1:74 * (K:322 * K:322))))
         /\ (!(0 <= K:322)
               \/ (-__cost':324 + (-2 * x':323)) <= ((-mid___cost:319
                                                        + (-2 * mid_x:318))
                                                       + (-98 * K:322)))
         /\ ((K:322 = 0 /\ mid_x:318 = x':323 /\ mid_z:320 = z':325
                /\ mid___cost:319 = __cost':324)
               \/ (1 <= K:322 /\ 0 <= (-1 + -param1:74 + mid_x:318)
                     /\ 0 <= mid___cost:319
                     /\ 0 <= (-100 + (-2 * param1:74) + __cost':324 + z':325)
                     /\ 0 <= -z':325 /\ 0 <= x':323
                     /\ 0 <= (100 + (2 * param1:74) + -z':325)))
         /\ (0 = K:322 \/ -mid___cost:319 <= 0) /\ (K:317 + K:322) = K:326
         /\ (!((0 <= K:327 /\ K:327 <= 0)) \/ mid_z:328 = z:321)
         /\ (!(1 <= K:327)
               \/ mid_z:328 = (100 + z:321 + (2 * param1:74) + -z:321))
         /\ (!(0 <= K:327)
               \/ mid_x:329 = (param0:71 + -K:327 + -((param1:74 * K:327))))
         /\ (!(0 <= K:327) \/ mid___cost:330 = __cost:95)
         /\ (!(0 <= K:327) \/ -mid_x:329 <= (-param0:71 + (-49 * K:327)))
         /\ (!(0 <= K:327)
               \/ -mid_x:329 <= (-param0:71 + (1/2 * K:327)
                                   + (1/2 * param1:74 * K:327)
                                   + (param0:71 * K:327)
                                   + (-1/2 * (K:327 * K:327))
                                   + (-1/2 * param1:74 * (K:327 * K:327))))
         /\ ((K:327 = 0 /\ param0:71 = mid_x:329 /\ z:321 = mid_z:328
                /\ __cost:95 = mid___cost:330)
               \/ (1 <= K:327 /\ 0 <= (-50 + -param1:74)
                     /\ 0 <= (-1 + -param1:74 + param0:71)
                     /\ (-100 + (-2 * param1:74) + mid_z:328) = 0
                     /\ 0 <= (-50 + -param1:74) /\ 0 <= mid_x:329))
         /\ (0 = K:327 \/ !((-99 + (-2 * param1:74)) <= 0))
         /\ (!((0 <= K:331 /\ K:331 <= 0)) \/ z':325 = mid_z:328)
         /\ (!(1 <= K:331) \/ z':325 = 0)
         /\ (!(0 <= K:331)
               \/ x':323 = (mid_x:329 + -K:331 + -((param1:74 * K:331))))
         /\ (!(0 <= K:331)
               \/ __cost':324 = (mid___cost:330 + (100 * K:331)
                                   + (2 * param1:74 * K:331)))
         /\ (!(0 <= K:331) \/ x':323 <= (mid_x:329 + (48 * K:331)))
         /\ (!(0 <= K:331)
               \/ -x':323 <= (-mid_x:329 + (1/2 * K:331)
                                + (1/2 * param1:74 * K:331)
                                + (mid_x:329 * K:331)
                                + (-1/2 * (K:331 * K:331))
                                + (-1/2 * param1:74 * (K:331 * K:331))))
         /\ ((K:331 = 0 /\ mid_x:329 = x':323 /\ mid_z:328 = z':325
                /\ mid___cost:330 = __cost':324)
               \/ (1 <= K:331 /\ 0 <= (-1 + -param1:74 + mid_x:329)
                     /\ 0 <= mid___cost:330 /\ 0 <= (49 + param1:74)
                     /\ z':325 = 0
                     /\ 0 <= (-100 + (-2 * param1:74) + __cost':324)
                     /\ 0 <= x':323 /\ 0 <= (49 + param1:74)))
         /\ (0 = K:331 \/ (-99 + (-2 * param1:74)) <= 0)
         /\ (K:327 + K:331) = K:326 /\ 0 <= K:326 /\ x':323 <= param1:74)}

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

Base relation: 
{__cost := __cost':206
 z := z':207
 x := x':205
 y := param1:74
 return := havoc:221
 return@pos := type_err:222
 return@width := type_err:223
 when ((!(0 <= K:200)
          \/ mid_x:201 = (param0:71 + -K:200 + -((param1:74 * K:200))))
         /\ (!(0 <= K:200) \/ mid___cost:202 = __cost:95)
         /\ (!((0 <= K:200 /\ K:200 <= 0)) \/ mid_z:203 = z:94)
         /\ (!(1 <= K:200)
               \/ mid_z:203 = (100 + z:94 + (2 * param1:74) + -z:94))
         /\ (!(0 <= K:200) \/ -mid_x:201 <= (-param0:71 + (-49 * K:200)))
         /\ (!(0 <= K:200)
               \/ -mid_x:201 <= (-param0:71 + (1/2 * K:200)
                                   + (1/2 * param1:74 * K:200)
                                   + (param0:71 * K:200)
                                   + (-1/2 * (K:200 * K:200))
                                   + (-1/2 * param1:74 * (K:200 * K:200))))
         /\ ((K:200 = 0 /\ param0:71 = mid_x:201 /\ z:94 = mid_z:203
                /\ __cost:95 = mid___cost:202)
               \/ (1 <= K:200 /\ 0 <= (-1 + -__cost:95)
                     /\ 0 <= (-50 + -param1:74)
                     /\ 0 <= (-1 + -param1:74 + param0:71)
                     /\ (-100 + (-2 * param1:74) + mid_z:203) = 0
                     /\ 0 <= (-50 + -param1:74)
                     /\ 0 <= (-1 + -mid___cost:202) /\ 0 <= mid_x:201))
         /\ (0 = K:200 \/ !(-__cost:95 <= 0))
         /\ (!(0 <= K:204)
               \/ x':205 = (mid_x:201 + -K:204 + -((param1:74 * K:204))))
         /\ (!(0 <= K:204) \/ -__cost':206 <= -mid___cost:202)
         /\ (!(0 <= K:204)
               \/ -x':205 <= (-mid_x:201 + (1/2 * K:204)
                                + (1/2 * param1:74 * K:204)
                                + (mid_x:201 * K:204)
                                + (-1/2 * (K:204 * K:204))
                                + (-1/2 * param1:74 * (K:204 * K:204))))
         /\ (!(0 <= K:204)
               \/ (-__cost':206 + (-2 * x':205)) <= ((-mid___cost:202
                                                        + (-2 * mid_x:201))
                                                       + (-98 * K:204)))
         /\ ((K:204 = 0 /\ mid_x:201 = x':205 /\ mid_z:203 = z':207
                /\ mid___cost:202 = __cost':206)
               \/ (1 <= K:204 /\ 0 <= (-1 + -param1:74 + mid_x:201)
                     /\ 0 <= mid___cost:202
                     /\ 0 <= (-100 + (-2 * param1:74) + __cost':206 + z':207)
                     /\ 0 <= -z':207 /\ 0 <= x':205
                     /\ 0 <= (100 + (2 * param1:74) + -z':207)))
         /\ (0 = K:204 \/ -mid___cost:202 <= 0) /\ (K:200 + K:204) = K:208
         /\ (!((0 <= K:209 /\ K:209 <= 0)) \/ mid_z:210 = z:94)
         /\ (!(1 <= K:209)
               \/ mid_z:210 = (100 + z:94 + (2 * param1:74) + -z:94))
         /\ (!(0 <= K:209)
               \/ mid_x:211 = (param0:71 + -K:209 + -((param1:74 * K:209))))
         /\ (!(0 <= K:209) \/ mid___cost:212 = __cost:95)
         /\ (!(0 <= K:209) \/ -mid_x:211 <= (-param0:71 + (-49 * K:209)))
         /\ (!(0 <= K:209)
               \/ -mid_x:211 <= (-param0:71 + (1/2 * K:209)
                                   + (1/2 * param1:74 * K:209)
                                   + (param0:71 * K:209)
                                   + (-1/2 * (K:209 * K:209))
                                   + (-1/2 * param1:74 * (K:209 * K:209))))
         /\ ((K:209 = 0 /\ param0:71 = mid_x:211 /\ z:94 = mid_z:210
                /\ __cost:95 = mid___cost:212)
               \/ (1 <= K:209 /\ 0 <= (-50 + -param1:74)
                     /\ 0 <= (-1 + -param1:74 + param0:71)
                     /\ (-100 + (-2 * param1:74) + mid_z:210) = 0
                     /\ 0 <= (-50 + -param1:74) /\ 0 <= mid_x:211))
         /\ (0 = K:209 \/ !((-99 + (-2 * param1:74)) <= 0))
         /\ (!((0 <= K:213 /\ K:213 <= 0)) \/ z':207 = mid_z:210)
         /\ (!(1 <= K:213) \/ z':207 = 0)
         /\ (!(0 <= K:213)
               \/ x':205 = (mid_x:211 + -K:213 + -((param1:74 * K:213))))
         /\ (!(0 <= K:213)
               \/ __cost':206 = (mid___cost:212 + (100 * K:213)
                                   + (2 * param1:74 * K:213)))
         /\ (!(0 <= K:213) \/ x':205 <= (mid_x:211 + (48 * K:213)))
         /\ (!(0 <= K:213)
               \/ -x':205 <= (-mid_x:211 + (1/2 * K:213)
                                + (1/2 * param1:74 * K:213)
                                + (mid_x:211 * K:213)
                                + (-1/2 * (K:213 * K:213))
                                + (-1/2 * param1:74 * (K:213 * K:213))))
         /\ ((K:213 = 0 /\ mid_x:211 = x':205 /\ mid_z:210 = z':207
                /\ mid___cost:212 = __cost':206)
               \/ (1 <= K:213 /\ 0 <= (-1 + -param1:74 + mid_x:211)
                     /\ 0 <= mid___cost:212 /\ 0 <= (49 + param1:74)
                     /\ z':207 = 0
                     /\ 0 <= (-100 + (-2 * param1:74) + __cost':206)
                     /\ 0 <= x':205 /\ 0 <= (49 + param1:74)))
         /\ (0 = K:213 \/ (-99 + (-2 * param1:74)) <= 0)
         /\ (K:209 + K:213) = K:208 /\ 0 <= K:208 /\ x':205 <= param1:74)}

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

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

Variable bounds at line 24 in run

min(__cost, max((98 + (-2 * y) + __cost + (2 * x)), (100 + (2 * y)))) <= __cost
__cost is o(1)

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