/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, 38> -> <Unique State Name, 34>	Base relation: 
{__cost := (__cost:66 + 1)
 y := (y:65 + -1)
 when (0 < y:65 /\ 0 <= __cost:66 /\ 0 <= (__cost:66 + 1))}	
<Unique State Name, 38> -> <Unique State Name, 54>	Base relation: 
{when y:65 <= 0}	
<Unique State Name, 60> -> <Unique State Name, 70>	Base relation: 
{return := havoc:68
 return@pos := type_err:71
 return@width := type_err:72}	
<Unique State Name, 71> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 23> -> <Unique State Name, 69>	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}	
<Unique State Name, 69> -> <Unique State Name, 64 68>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 28> -> <Unique State Name, 53>	Base relation: 
{tmp := havoc:79
 x := (x:63 + -1)
 when 0 < x:63}	
<Unique State Name, 28> -> <Unique State Name, 60>	Base relation: 
{when x:63 <= 0}	
<Unique State Name, 72> -> <Unique State Name, 38>	Base relation: 
{}	
<Unique State Name, 70> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 54> -> <Unique State Name, 24>	Base relation: 
{}	
<Unique State Name, 34> -> <Unique State Name, 72>	Base relation: 
{}	
<Unique State Name, 24> -> <Unique State Name, 73>	Base relation: 
{}	
<Unique State Name, 53> -> <Unique State Name, 34>	Base relation: 
{when tmp:67 = 0}	
<Unique State Name, 53> -> <Unique State Name, 54>	Base relation: 
{__cost := (__cost:66 + 1)
 y := (y:65 + 1)
 when (!(tmp:67 = 0) /\ 0 <= __cost:66 /\ 0 <= (__cost:66 + 1))}	
<Unique State Name, 73> -> <Unique State Name, 28>	Base relation: 
{}	
<Unique State Name, 68> -> <Unique State Name, 71>	Base relation: 
{return := 0
 return@pos := type_err:32
 return@width := type_err:33
 when (((0 < x:4 /\ x:4 = phi_tmp___1:23) \/ (x:4 <= 0 /\ 0 = phi_tmp___1:23))
         /\ ((0 < y:5 /\ y:5 = phi_tmp___2:31)
               \/ (y:5 <= 0 /\ 0 = phi_tmp___2:31)))}	
<Unique State Name, 64> -> <Unique State Name, 24>	Base relation: 
{x := param0:75
 y := param1:78}	
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:66 + 1)
 y := (y:65 + -1)
 when (0 < y:65 /\ 0 <= __cost:66 /\ 0 <= (__cost:66 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':135) = (1)*(__cost:66) + 1
           (y':136) = (1)*(y:65) + (-1)*1
           }
          pre:
            [|__cost:66>=0; y:65-1>=0|]
          post:
            [|y':136>=0; __cost':135-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':135
   y := y':136
   when ((!(0 <= K:144) \/ mid___cost:147 = (__cost:66 + K:144))
           /\ (!(0 <= K:144) \/ mid_y:146 = (y:65 + -K:144))
           /\ ((K:144 = 0 /\ y:65 = mid_y:146 /\ __cost:66 = mid___cost:147)
                 \/ (1 <= K:144 /\ 0 <= __cost:66 /\ 0 <= (-1 + y:65)
                       /\ 0 <= mid_y:146 /\ 0 <= (-1 + mid___cost:147)))
           /\ K:145 = 0 /\ mid_y:146 = y':136 /\ mid___cost:147 = __cost':135
           /\ 0 = K:145 /\ (K:144 + K:145) = K:143 /\ 0 <= K:143)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := phi___cost:157
 tmp := havoc:79
 x := (x:63 + -1)
 y := phi_y:158
 when (0 < x:63
         /\ ((!(havoc:79 = 0) /\ 0 <= __cost:66 /\ 0 <= (__cost:66 + 1)
                /\ (__cost:66 + 1) = phi___cost:157 /\ (y:65 + 1) = phi_y:158)
               \/ (havoc:79 = 0
                     /\ (!(0 <= K:159)
                           \/ mid___cost:160 = (__cost:66 + K:159))
                     /\ (!(0 <= K:159) \/ mid_y:161 = (y:65 + -K:159))
                     /\ ((K:159 = 0 /\ y:65 = mid_y:161
                            /\ __cost:66 = mid___cost:160)
                           \/ (1 <= K:159 /\ 0 <= __cost:66
                                 /\ 0 <= (-1 + y:65) /\ 0 <= mid_y:161
                                 /\ 0 <= (-1 + mid___cost:160))) /\ K:162 = 0
                     /\ mid_y:161 = y':163 /\ mid___cost:160 = __cost':164
                     /\ 0 = K:162 /\ (K:159 + K:162) = K:165 /\ 0 <= K:165
                     /\ y':163 <= 0 /\ __cost':164 = phi___cost:157
                     /\ y':163 = phi_y:158)))}
**** alpha hat: 
  {<Split [!(-__cost:66 <= 0)
            (x':167) = (1)*(x:63) + (-1)*1
           (tmp':166) = 0
           (__cost':135) = (1)*(__cost:66) + 0
           (y':136) = (1)*(y:65) + 0
           }
          pre:
            [|-__cost:66-1>=0; -y:65>=0; x:63-1>=0|]
          post:
            [|tmp':166=0; -y':136>=0; -__cost':135-1>=0; x':167>=0|]
           (x':167) = (1)*(x:63) + (-1)*1
          ((__cost':135 + y':136)) <= (1)*((__cost:66 + y:65)) + 2*1
          ((-__cost':135 + y':136)) <= (1)*((-__cost:66 + y:65)) + 0
          ((-__cost':135 + -y':136)) <= (1)*((-__cost:66 + -y:65)) + 0
          }
  pre:
    [|__cost:66>=0; x:63-1>=0|]
  post:
    [|__cost':135>=0; x':167>=0|]],
[!((-1 + -__cost:66) <= 0)
  (x':167) = (1)*(x:63) + (-1)*1
 (tmp':166) = 0
 (__cost':135) = (1)*(__cost:66) + 0
 (y':136) = (1)*(y:65) + 0
 } pre:   [|-__cost:66-2>=0; -y:65>=0; x:63-1>=0|] post:
  [|tmp':166=0; -y':136>=0; -__cost':135-2>=0; x':167>=0|]
 (x':167) = (1)*(x:63) + (-1)*1
((__cost':135 + y':136)) <= (1)*((__cost:66 + y:65)) + 2*1
((-__cost':135 + y':136)) <= (1)*((-__cost:66 + y:65)) + 0
((-__cost':135 + -y':136)) <= (1)*((-__cost:66 + -y:65)) + 0 } pre:
  [|__cost:66+1>=0; x:63-1>=0|] post:
  [|__cost':135+1>=0; x':167>=0|]]>}
**** star transition: 
  {__cost := __cost':135
   tmp := tmp':166
   x := x':167
   y := y':136
   when ((!(0 <= K:195) \/ mid_x:198 = (x:63 + -K:195))
           /\ (!((0 <= K:195 /\ K:195 <= 0)) \/ mid_tmp:199 = tmp:67)
           /\ (!(1 <= K:195) \/ mid_tmp:199 = 0)
           /\ (!(0 <= K:195) \/ mid___cost:200 = __cost:66)
           /\ (!(0 <= K:195) \/ mid_y:197 = y:65)
           /\ ((K:195 = 0 /\ y:65 = mid_y:197 /\ x:63 = mid_x:198
                  /\ tmp:67 = mid_tmp:199 /\ __cost:66 = mid___cost:200)
                 \/ (1 <= K:195 /\ 0 <= (-1 + -__cost:66) /\ 0 <= -y:65
                       /\ 0 <= (-1 + x:63) /\ mid_tmp:199 = 0
                       /\ 0 <= -mid_y:197 /\ 0 <= (-1 + -mid___cost:200)
                       /\ 0 <= mid_x:198))
           /\ (0 = K:195 \/ !(-__cost:66 <= 0))
           /\ (!(0 <= K:196) \/ x':167 = (mid_x:198 + -K:196))
           /\ (!(0 <= K:196)
                 \/ (__cost':135 + y':136) <= ((mid___cost:200 + mid_y:197)
                                                 + (2 * K:196)))
           /\ (!(0 <= K:196)
                 \/ (-__cost':135 + y':136) <= (-mid___cost:200 + mid_y:197))
           /\ (!(0 <= K:196)
                 \/ (-__cost':135 + -y':136) <= (-mid___cost:200 + -mid_y:197))
           /\ ((K:196 = 0 /\ mid_y:197 = y':136 /\ mid_x:198 = x':167
                  /\ mid_tmp:199 = tmp':166 /\ mid___cost:200 = __cost':135)
                 \/ (1 <= K:196 /\ 0 <= mid___cost:200
                       /\ 0 <= (-1 + mid_x:198) /\ 0 <= __cost':135
                       /\ 0 <= x':167))
           /\ (0 = K:196 \/ -mid___cost:200 <= 0) /\ (K:195 + K:196) = K:194
           /\ (!(0 <= K:201) \/ mid_x:204 = (x:63 + -K:201))
           /\ (!((0 <= K:201 /\ K:201 <= 0)) \/ mid_tmp:205 = tmp:67)
           /\ (!(1 <= K:201) \/ mid_tmp:205 = 0)
           /\ (!(0 <= K:201) \/ mid___cost:206 = __cost:66)
           /\ (!(0 <= K:201) \/ mid_y:203 = y:65)
           /\ ((K:201 = 0 /\ y:65 = mid_y:203 /\ x:63 = mid_x:204
                  /\ tmp:67 = mid_tmp:205 /\ __cost:66 = mid___cost:206)
                 \/ (1 <= K:201 /\ 0 <= (-2 + -__cost:66) /\ 0 <= -y:65
                       /\ 0 <= (-1 + x:63) /\ mid_tmp:205 = 0
                       /\ 0 <= -mid_y:203 /\ 0 <= (-2 + -mid___cost:206)
                       /\ 0 <= mid_x:204))
           /\ (0 = K:201 \/ !((-1 + -__cost:66) <= 0))
           /\ (!(0 <= K:202) \/ x':167 = (mid_x:204 + -K:202))
           /\ (!(0 <= K:202)
                 \/ (__cost':135 + y':136) <= ((mid___cost:206 + mid_y:203)
                                                 + (2 * K:202)))
           /\ (!(0 <= K:202)
                 \/ (-__cost':135 + y':136) <= (-mid___cost:206 + mid_y:203))
           /\ (!(0 <= K:202)
                 \/ (-__cost':135 + -y':136) <= (-mid___cost:206 + -mid_y:203))
           /\ ((K:202 = 0 /\ mid_y:203 = y':136 /\ mid_x:204 = x':167
                  /\ mid_tmp:205 = tmp':166 /\ mid___cost:206 = __cost':135)
                 \/ (1 <= K:202 /\ 0 <= (1 + mid___cost:206)
                       /\ 0 <= (-1 + mid_x:204) /\ 0 <= (1 + __cost':135)
                       /\ 0 <= x':167))
           /\ (0 = K:202 \/ (-1 + -mid___cost:206) <= 0)
           /\ (K:201 + K:202) = K:194 /\ 0 <= K:194)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  14  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       x := havoc:21
       y := havoc:22
       param0 := havoc:21
       param1 := havoc:22
       param0@pos := type_err:27
       param1@pos := type_err:29
       param0@width := type_err:28
       param1@width := type_err:30}    )
    ,
    Var(14)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:32
     return@width := type_err:33
     when (((0 < x:4 /\ x:4 = phi_tmp___1:23)
              \/ (x:4 <= 0 /\ 0 = phi_tmp___1:23))
             /\ ((0 < y:5 /\ y:5 = phi_tmp___2:31)
                   \/ (y:5 <= 0 /\ 0 = phi_tmp___2:31)))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=14: 
Weight(Base relation: 
  {__cost := __cost':214
   tmp := tmp':216
   x := x':213
   y := y':215
   return := havoc:224
   return@pos := type_err:225
   return@width := type_err:226
   when ((!(0 <= K:207) \/ mid_x:208 = (param0:75 + -K:207))
           /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:67)
           /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
           /\ (!(0 <= K:207) \/ mid___cost:210 = __cost:66)
           /\ (!(0 <= K:207) \/ mid_y:211 = param1:78)
           /\ ((K:207 = 0 /\ param1:78 = mid_y:211 /\ param0:75 = mid_x:208
                  /\ tmp:67 = mid_tmp:209 /\ __cost:66 = mid___cost:210)
                 \/ (1 <= K:207 /\ 0 <= (-1 + -__cost:66) /\ 0 <= -param1:78
                       /\ 0 <= (-1 + param0:75) /\ mid_tmp:209 = 0
                       /\ 0 <= -mid_y:211 /\ 0 <= (-1 + -mid___cost:210)
                       /\ 0 <= mid_x:208))
           /\ (0 = K:207 \/ !(-__cost:66 <= 0))
           /\ (!(0 <= K:212) \/ x':213 = (mid_x:208 + -K:212))
           /\ (!(0 <= K:212)
                 \/ (__cost':214 + y':215) <= ((mid___cost:210 + mid_y:211)
                                                 + (2 * K:212)))
           /\ (!(0 <= K:212)
                 \/ (-__cost':214 + y':215) <= (-mid___cost:210 + mid_y:211))
           /\ (!(0 <= K:212)
                 \/ (-__cost':214 + -y':215) <= (-mid___cost:210 + -mid_y:211))
           /\ ((K:212 = 0 /\ mid_y:211 = y':215 /\ mid_x:208 = x':213
                  /\ mid_tmp:209 = tmp':216 /\ mid___cost:210 = __cost':214)
                 \/ (1 <= K:212 /\ 0 <= mid___cost:210
                       /\ 0 <= (-1 + mid_x:208) /\ 0 <= __cost':214
                       /\ 0 <= x':213))
           /\ (0 = K:212 \/ -mid___cost:210 <= 0) /\ (K:207 + K:212) = K:217
           /\ (!(0 <= K:218) \/ mid_x:219 = (param0:75 + -K:218))
           /\ (!((0 <= K:218 /\ K:218 <= 0)) \/ mid_tmp:220 = tmp:67)
           /\ (!(1 <= K:218) \/ mid_tmp:220 = 0)
           /\ (!(0 <= K:218) \/ mid___cost:221 = __cost:66)
           /\ (!(0 <= K:218) \/ mid_y:222 = param1:78)
           /\ ((K:218 = 0 /\ param1:78 = mid_y:222 /\ param0:75 = mid_x:219
                  /\ tmp:67 = mid_tmp:220 /\ __cost:66 = mid___cost:221)
                 \/ (1 <= K:218 /\ 0 <= (-2 + -__cost:66) /\ 0 <= -param1:78
                       /\ 0 <= (-1 + param0:75) /\ mid_tmp:220 = 0
                       /\ 0 <= -mid_y:222 /\ 0 <= (-2 + -mid___cost:221)
                       /\ 0 <= mid_x:219))
           /\ (0 = K:218 \/ !((-1 + -__cost:66) <= 0))
           /\ (!(0 <= K:223) \/ x':213 = (mid_x:219 + -K:223))
           /\ (!(0 <= K:223)
                 \/ (__cost':214 + y':215) <= ((mid___cost:221 + mid_y:222)
                                                 + (2 * K:223)))
           /\ (!(0 <= K:223)
                 \/ (-__cost':214 + y':215) <= (-mid___cost:221 + mid_y:222))
           /\ (!(0 <= K:223)
                 \/ (-__cost':214 + -y':215) <= (-mid___cost:221 + -mid_y:222))
           /\ ((K:223 = 0 /\ mid_y:222 = y':215 /\ mid_x:219 = x':213
                  /\ mid_tmp:220 = tmp':216 /\ mid___cost:221 = __cost':214)
                 \/ (1 <= K:223 /\ 0 <= (1 + mid___cost:221)
                       /\ 0 <= (-1 + mid_x:219) /\ 0 <= (1 + __cost':214)
                       /\ 0 <= x':213))
           /\ (0 = K:223 \/ (-1 + -mid___cost:221) <= 0)
           /\ (K:218 + K:223) = K:217 /\ 0 <= K:217 /\ x':213 <= 0)})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := 0
         x := havoc:21
         y := havoc:22
         param0 := havoc:21
         param1 := havoc:22
         param0@pos := type_err:27
         param1@pos := type_err:29
         param0@width := type_err:28
         param1@width := type_err:30}      )
      ,
      Var(14)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:32
       return@width := type_err:33
       when (((0 < x:4 /\ x:4 = phi_tmp___1:23)
                \/ (x:4 <= 0 /\ 0 = phi_tmp___1:23))
               /\ ((0 < y:5 /\ y:5 = phi_tmp___2:31)
                     \/ (y:5 <= 0 /\ 0 = phi_tmp___2:31)))}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':214
   return := havoc:224
   return@pos := type_err:225
   return@width := type_err:226
   when ((!(0 <= K:207) \/ mid_x:208 = (param0:75 + -K:207))
           /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:245)
           /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
           /\ (!(0 <= K:207) \/ mid___cost:210 = __cost:66)
           /\ (!(0 <= K:207) \/ mid_y:211 = param1:78)
           /\ ((K:207 = 0 /\ param1:78 = mid_y:211 /\ param0:75 = mid_x:208
                  /\ tmp:245 = mid_tmp:209 /\ __cost:66 = mid___cost:210)
                 \/ (1 <= K:207 /\ 0 <= (-1 + -__cost:66) /\ 0 <= -param1:78
                       /\ 0 <= (-1 + param0:75) /\ mid_tmp:209 = 0
                       /\ 0 <= -mid_y:211 /\ 0 <= (-1 + -mid___cost:210)
                       /\ 0 <= mid_x:208))
           /\ (0 = K:207 \/ !(-__cost:66 <= 0))
           /\ (!(0 <= K:212) \/ x':213 = (mid_x:208 + -K:212))
           /\ (!(0 <= K:212)
                 \/ (__cost':214 + y':215) <= ((mid___cost:210 + mid_y:211)
                                                 + (2 * K:212)))
           /\ (!(0 <= K:212)
                 \/ (-__cost':214 + y':215) <= (-mid___cost:210 + mid_y:211))
           /\ (!(0 <= K:212)
                 \/ (-__cost':214 + -y':215) <= (-mid___cost:210 + -mid_y:211))
           /\ ((K:212 = 0 /\ mid_y:211 = y':215 /\ mid_x:208 = x':213
                  /\ mid_tmp:209 = tmp':216 /\ mid___cost:210 = __cost':214)
                 \/ (1 <= K:212 /\ 0 <= mid___cost:210
                       /\ 0 <= (-1 + mid_x:208) /\ 0 <= __cost':214
                       /\ 0 <= x':213))
           /\ (0 = K:212 \/ -mid___cost:210 <= 0) /\ (K:207 + K:212) = K:217
           /\ (!(0 <= K:218) \/ mid_x:219 = (param0:75 + -K:218))
           /\ (!((0 <= K:218 /\ K:218 <= 0)) \/ mid_tmp:220 = tmp:245)
           /\ (!(1 <= K:218) \/ mid_tmp:220 = 0)
           /\ (!(0 <= K:218) \/ mid___cost:221 = __cost:66)
           /\ (!(0 <= K:218) \/ mid_y:222 = param1:78)
           /\ ((K:218 = 0 /\ param1:78 = mid_y:222 /\ param0:75 = mid_x:219
                  /\ tmp:245 = mid_tmp:220 /\ __cost:66 = mid___cost:221)
                 \/ (1 <= K:218 /\ 0 <= (-2 + -__cost:66) /\ 0 <= -param1:78
                       /\ 0 <= (-1 + param0:75) /\ mid_tmp:220 = 0
                       /\ 0 <= -mid_y:222 /\ 0 <= (-2 + -mid___cost:221)
                       /\ 0 <= mid_x:219))
           /\ (0 = K:218 \/ !((-1 + -__cost:66) <= 0))
           /\ (!(0 <= K:223) \/ x':213 = (mid_x:219 + -K:223))
           /\ (!(0 <= K:223)
                 \/ (__cost':214 + y':215) <= ((mid___cost:221 + mid_y:222)
                                                 + (2 * K:223)))
           /\ (!(0 <= K:223)
                 \/ (-__cost':214 + y':215) <= (-mid___cost:221 + mid_y:222))
           /\ (!(0 <= K:223)
                 \/ (-__cost':214 + -y':215) <= (-mid___cost:221 + -mid_y:222))
           /\ ((K:223 = 0 /\ mid_y:222 = y':215 /\ mid_x:219 = x':213
                  /\ mid_tmp:220 = tmp':216 /\ mid___cost:221 = __cost':214)
                 \/ (1 <= K:223 /\ 0 <= (1 + mid___cost:221)
                       /\ 0 <= (-1 + mid_x:219) /\ 0 <= (1 + __cost':214)
                       /\ 0 <= x':213))
           /\ (0 = K:223 \/ (-1 + -mid___cost:221) <= 0)
           /\ (K:218 + K:223) = K:217 /\ 0 <= K:217 /\ x':213 <= 0)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':254
   return := 0
   param0 := havoc:21
   param1 := havoc:22
   return@pos := type_err:269
   param0@pos := type_err:27
   param1@pos := type_err:29
   return@width := type_err:270
   param0@width := type_err:28
   param1@width := type_err:30
   when ((!(0 <= K:246) \/ mid_x:247 = (havoc:21 + -K:246))
           /\ (!((0 <= K:246 /\ K:246 <= 0)) \/ mid_tmp:248 = tmp:249)
           /\ (!(1 <= K:246) \/ mid_tmp:248 = 0)
           /\ (!(0 <= K:246) \/ mid___cost:250 = 0)
           /\ (!(0 <= K:246) \/ mid_y:251 = havoc:22) /\ K:246 = 0
           /\ havoc:22 = mid_y:251 /\ havoc:21 = mid_x:247
           /\ tmp:249 = mid_tmp:248 /\ 0 = mid___cost:250 /\ 0 = K:246
           /\ (!(0 <= K:252) \/ x':253 = (mid_x:247 + -K:252))
           /\ (!(0 <= K:252)
                 \/ (__cost':254 + y':255) <= ((mid___cost:250 + mid_y:251)
                                                 + (2 * K:252)))
           /\ (!(0 <= K:252)
                 \/ (-__cost':254 + y':255) <= (-mid___cost:250 + mid_y:251))
           /\ (!(0 <= K:252)
                 \/ (-__cost':254 + -y':255) <= (-mid___cost:250 + -mid_y:251))
           /\ ((K:252 = 0 /\ mid_y:251 = y':255 /\ mid_x:247 = x':253
                  /\ mid_tmp:248 = tmp':256 /\ mid___cost:250 = __cost':254)
                 \/ (1 <= K:252 /\ 0 <= mid___cost:250
                       /\ 0 <= (-1 + mid_x:247) /\ 0 <= __cost':254
                       /\ 0 <= x':253))
           /\ (0 = K:252 \/ -mid___cost:250 <= 0) /\ (K:246 + K:252) = K:257
           /\ (!(0 <= K:258) \/ mid_x:259 = (havoc:21 + -K:258))
           /\ (!((0 <= K:258 /\ K:258 <= 0)) \/ mid_tmp:260 = tmp:249)
           /\ (!(1 <= K:258) \/ mid_tmp:260 = 0)
           /\ (!(0 <= K:258) \/ mid___cost:261 = 0)
           /\ (!(0 <= K:258) \/ mid_y:262 = havoc:22) /\ K:258 = 0
           /\ havoc:22 = mid_y:262 /\ havoc:21 = mid_x:259
           /\ tmp:249 = mid_tmp:260 /\ 0 = mid___cost:261 /\ 0 = K:258
           /\ (!(0 <= K:263) \/ x':253 = (mid_x:259 + -K:263))
           /\ (!(0 <= K:263)
                 \/ (__cost':254 + y':255) <= ((mid___cost:261 + mid_y:262)
                                                 + (2 * K:263)))
           /\ (!(0 <= K:263)
                 \/ (-__cost':254 + y':255) <= (-mid___cost:261 + mid_y:262))
           /\ (!(0 <= K:263)
                 \/ (-__cost':254 + -y':255) <= (-mid___cost:261 + -mid_y:262))
           /\ ((K:263 = 0 /\ mid_y:262 = y':255 /\ mid_x:259 = x':253
                  /\ mid_tmp:260 = tmp':256 /\ mid___cost:261 = __cost':254)
                 \/ (1 <= K:263 /\ 0 <= (1 + mid___cost:261)
                       /\ 0 <= (-1 + mid_x:259) /\ 0 <= (1 + __cost':254)
                       /\ 0 <= x':253))
           /\ (0 = K:263 \/ (-1 + -mid___cost:261) <= 0)
           /\ (K:258 + K:263) = K:257 /\ 0 <= K:257 /\ x':253 <= 0
           /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:267)
                 \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:267))
           /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:268)
                 \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:268)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=14: 
Weight(Base relation: 
  {__cost := __cost':214
   return := havoc:224
   return@pos := type_err:225
   return@width := type_err:226
   when ((!(0 <= K:207) \/ mid_x:208 = (param0:75 + -K:207))
           /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:245)
           /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
           /\ (!(0 <= K:207) \/ mid___cost:210 = __cost:66)
           /\ (!(0 <= K:207) \/ mid_y:211 = param1:78)
           /\ ((K:207 = 0 /\ param1:78 = mid_y:211 /\ param0:75 = mid_x:208
                  /\ tmp:245 = mid_tmp:209 /\ __cost:66 = mid___cost:210)
                 \/ (1 <= K:207 /\ 0 <= (-1 + -__cost:66) /\ 0 <= -param1:78
                       /\ 0 <= (-1 + param0:75) /\ mid_tmp:209 = 0
                       /\ 0 <= -mid_y:211 /\ 0 <= (-1 + -mid___cost:210)
                       /\ 0 <= mid_x:208))
           /\ (0 = K:207 \/ !(-__cost:66 <= 0))
           /\ (!(0 <= K:212) \/ x':213 = (mid_x:208 + -K:212))
           /\ (!(0 <= K:212)
                 \/ (__cost':214 + y':215) <= ((mid___cost:210 + mid_y:211)
                                                 + (2 * K:212)))
           /\ (!(0 <= K:212)
                 \/ (-__cost':214 + y':215) <= (-mid___cost:210 + mid_y:211))
           /\ (!(0 <= K:212)
                 \/ (-__cost':214 + -y':215) <= (-mid___cost:210 + -mid_y:211))
           /\ ((K:212 = 0 /\ mid_y:211 = y':215 /\ mid_x:208 = x':213
                  /\ mid_tmp:209 = tmp':216 /\ mid___cost:210 = __cost':214)
                 \/ (1 <= K:212 /\ 0 <= mid___cost:210
                       /\ 0 <= (-1 + mid_x:208) /\ 0 <= __cost':214
                       /\ 0 <= x':213))
           /\ (0 = K:212 \/ -mid___cost:210 <= 0) /\ (K:207 + K:212) = K:217
           /\ (!(0 <= K:218) \/ mid_x:219 = (param0:75 + -K:218))
           /\ (!((0 <= K:218 /\ K:218 <= 0)) \/ mid_tmp:220 = tmp:245)
           /\ (!(1 <= K:218) \/ mid_tmp:220 = 0)
           /\ (!(0 <= K:218) \/ mid___cost:221 = __cost:66)
           /\ (!(0 <= K:218) \/ mid_y:222 = param1:78)
           /\ ((K:218 = 0 /\ param1:78 = mid_y:222 /\ param0:75 = mid_x:219
                  /\ tmp:245 = mid_tmp:220 /\ __cost:66 = mid___cost:221)
                 \/ (1 <= K:218 /\ 0 <= (-2 + -__cost:66) /\ 0 <= -param1:78
                       /\ 0 <= (-1 + param0:75) /\ mid_tmp:220 = 0
                       /\ 0 <= -mid_y:222 /\ 0 <= (-2 + -mid___cost:221)
                       /\ 0 <= mid_x:219))
           /\ (0 = K:218 \/ !((-1 + -__cost:66) <= 0))
           /\ (!(0 <= K:223) \/ x':213 = (mid_x:219 + -K:223))
           /\ (!(0 <= K:223)
                 \/ (__cost':214 + y':215) <= ((mid___cost:221 + mid_y:222)
                                                 + (2 * K:223)))
           /\ (!(0 <= K:223)
                 \/ (-__cost':214 + y':215) <= (-mid___cost:221 + mid_y:222))
           /\ (!(0 <= K:223)
                 \/ (-__cost':214 + -y':215) <= (-mid___cost:221 + -mid_y:222))
           /\ ((K:223 = 0 /\ mid_y:222 = y':215 /\ mid_x:219 = x':213
                  /\ mid_tmp:220 = tmp':216 /\ mid___cost:221 = __cost':214)
                 \/ (1 <= K:223 /\ 0 <= (1 + mid___cost:221)
                       /\ 0 <= (-1 + mid_x:219) /\ 0 <= (1 + __cost':214)
                       /\ 0 <= x':213))
           /\ (0 = K:223 \/ (-1 + -mid___cost:221) <= 0)
           /\ (K:218 + K:223) = K:217 /\ 0 <= K:217 /\ x':213 <= 0)})


Step 5: =========================================================
[Newton] Running Newton
-------------------------------------------------------------------------------
Round 0:
Evaluating variable number 6 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':254
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:269
 param0@pos := type_err:27
 param1@pos := type_err:29
 return@width := type_err:270
 param0@width := type_err:28
 param1@width := type_err:30
 when ((!(0 <= K:246) \/ mid_x:247 = (havoc:21 + -K:246))
         /\ (!((0 <= K:246 /\ K:246 <= 0)) \/ mid_tmp:248 = tmp:249)
         /\ (!(1 <= K:246) \/ mid_tmp:248 = 0)
         /\ (!(0 <= K:246) \/ mid___cost:250 = 0)
         /\ (!(0 <= K:246) \/ mid_y:251 = havoc:22) /\ K:246 = 0
         /\ havoc:22 = mid_y:251 /\ havoc:21 = mid_x:247
         /\ tmp:249 = mid_tmp:248 /\ 0 = mid___cost:250 /\ 0 = K:246
         /\ (!(0 <= K:252) \/ x':253 = (mid_x:247 + -K:252))
         /\ (!(0 <= K:252)
               \/ (__cost':254 + y':255) <= ((mid___cost:250 + mid_y:251)
                                               + (2 * K:252)))
         /\ (!(0 <= K:252)
               \/ (-__cost':254 + y':255) <= (-mid___cost:250 + mid_y:251))
         /\ (!(0 <= K:252)
               \/ (-__cost':254 + -y':255) <= (-mid___cost:250 + -mid_y:251))
         /\ ((K:252 = 0 /\ mid_y:251 = y':255 /\ mid_x:247 = x':253
                /\ mid_tmp:248 = tmp':256 /\ mid___cost:250 = __cost':254)
               \/ (1 <= K:252 /\ 0 <= mid___cost:250 /\ 0 <= (-1 + mid_x:247)
                     /\ 0 <= __cost':254 /\ 0 <= x':253))
         /\ (0 = K:252 \/ -mid___cost:250 <= 0) /\ (K:246 + K:252) = K:257
         /\ (!(0 <= K:258) \/ mid_x:259 = (havoc:21 + -K:258))
         /\ (!((0 <= K:258 /\ K:258 <= 0)) \/ mid_tmp:260 = tmp:249)
         /\ (!(1 <= K:258) \/ mid_tmp:260 = 0)
         /\ (!(0 <= K:258) \/ mid___cost:261 = 0)
         /\ (!(0 <= K:258) \/ mid_y:262 = havoc:22) /\ K:258 = 0
         /\ havoc:22 = mid_y:262 /\ havoc:21 = mid_x:259
         /\ tmp:249 = mid_tmp:260 /\ 0 = mid___cost:261 /\ 0 = K:258
         /\ (!(0 <= K:263) \/ x':253 = (mid_x:259 + -K:263))
         /\ (!(0 <= K:263)
               \/ (__cost':254 + y':255) <= ((mid___cost:261 + mid_y:262)
                                               + (2 * K:263)))
         /\ (!(0 <= K:263)
               \/ (-__cost':254 + y':255) <= (-mid___cost:261 + mid_y:262))
         /\ (!(0 <= K:263)
               \/ (-__cost':254 + -y':255) <= (-mid___cost:261 + -mid_y:262))
         /\ ((K:263 = 0 /\ mid_y:262 = y':255 /\ mid_x:259 = x':253
                /\ mid_tmp:260 = tmp':256 /\ mid___cost:261 = __cost':254)
               \/ (1 <= K:263 /\ 0 <= (1 + mid___cost:261)
                     /\ 0 <= (-1 + mid_x:259) /\ 0 <= (1 + __cost':254)
                     /\ 0 <= x':253))
         /\ (0 = K:263 \/ (-1 + -mid___cost:261) <= 0)
         /\ (K:258 + K:263) = K:257 /\ 0 <= K:257 /\ x':253 <= 0
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:267)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:267))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:268)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:268)))}

Evaluating variable number 14 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':214
 return := havoc:224
 return@pos := type_err:225
 return@width := type_err:226
 when ((!(0 <= K:207) \/ mid_x:208 = (param0:75 + -K:207))
         /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:245)
         /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
         /\ (!(0 <= K:207) \/ mid___cost:210 = __cost:66)
         /\ (!(0 <= K:207) \/ mid_y:211 = param1:78)
         /\ ((K:207 = 0 /\ param1:78 = mid_y:211 /\ param0:75 = mid_x:208
                /\ tmp:245 = mid_tmp:209 /\ __cost:66 = mid___cost:210)
               \/ (1 <= K:207 /\ 0 <= (-1 + -__cost:66) /\ 0 <= -param1:78
                     /\ 0 <= (-1 + param0:75) /\ mid_tmp:209 = 0
                     /\ 0 <= -mid_y:211 /\ 0 <= (-1 + -mid___cost:210)
                     /\ 0 <= mid_x:208)) /\ (0 = K:207 \/ !(-__cost:66 <= 0))
         /\ (!(0 <= K:212) \/ x':213 = (mid_x:208 + -K:212))
         /\ (!(0 <= K:212)
               \/ (__cost':214 + y':215) <= ((mid___cost:210 + mid_y:211)
                                               + (2 * K:212)))
         /\ (!(0 <= K:212)
               \/ (-__cost':214 + y':215) <= (-mid___cost:210 + mid_y:211))
         /\ (!(0 <= K:212)
               \/ (-__cost':214 + -y':215) <= (-mid___cost:210 + -mid_y:211))
         /\ ((K:212 = 0 /\ mid_y:211 = y':215 /\ mid_x:208 = x':213
                /\ mid_tmp:209 = tmp':216 /\ mid___cost:210 = __cost':214)
               \/ (1 <= K:212 /\ 0 <= mid___cost:210 /\ 0 <= (-1 + mid_x:208)
                     /\ 0 <= __cost':214 /\ 0 <= x':213))
         /\ (0 = K:212 \/ -mid___cost:210 <= 0) /\ (K:207 + K:212) = K:217
         /\ (!(0 <= K:218) \/ mid_x:219 = (param0:75 + -K:218))
         /\ (!((0 <= K:218 /\ K:218 <= 0)) \/ mid_tmp:220 = tmp:245)
         /\ (!(1 <= K:218) \/ mid_tmp:220 = 0)
         /\ (!(0 <= K:218) \/ mid___cost:221 = __cost:66)
         /\ (!(0 <= K:218) \/ mid_y:222 = param1:78)
         /\ ((K:218 = 0 /\ param1:78 = mid_y:222 /\ param0:75 = mid_x:219
                /\ tmp:245 = mid_tmp:220 /\ __cost:66 = mid___cost:221)
               \/ (1 <= K:218 /\ 0 <= (-2 + -__cost:66) /\ 0 <= -param1:78
                     /\ 0 <= (-1 + param0:75) /\ mid_tmp:220 = 0
                     /\ 0 <= -mid_y:222 /\ 0 <= (-2 + -mid___cost:221)
                     /\ 0 <= mid_x:219))
         /\ (0 = K:218 \/ !((-1 + -__cost:66) <= 0))
         /\ (!(0 <= K:223) \/ x':213 = (mid_x:219 + -K:223))
         /\ (!(0 <= K:223)
               \/ (__cost':214 + y':215) <= ((mid___cost:221 + mid_y:222)
                                               + (2 * K:223)))
         /\ (!(0 <= K:223)
               \/ (-__cost':214 + y':215) <= (-mid___cost:221 + mid_y:222))
         /\ (!(0 <= K:223)
               \/ (-__cost':214 + -y':215) <= (-mid___cost:221 + -mid_y:222))
         /\ ((K:223 = 0 /\ mid_y:222 = y':215 /\ mid_x:219 = x':213
                /\ mid_tmp:220 = tmp':216 /\ mid___cost:221 = __cost':214)
               \/ (1 <= K:223 /\ 0 <= (1 + mid___cost:221)
                     /\ 0 <= (-1 + mid_x:219) /\ 0 <= (1 + __cost':214)
                     /\ 0 <= x':213))
         /\ (0 = K:223 \/ (-1 + -mid___cost:221) <= 0)
         /\ (K:218 + K:223) = K:217 /\ 0 <= K:217 /\ x':213 <= 0)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, accept> -> <__pstate, (Unique State Name,64)_g1>	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x5ae2500: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x5b00100: 
	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,64)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}

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

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

Base relation: 
{__cost := __cost':279
 x := havoc:21
 y := havoc:22
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:294
 param0@pos := type_err:27
 param1@pos := type_err:29
 return@width := type_err:295
 param0@width := type_err:28
 param1@width := type_err:30
 when ((!(0 <= K:271) \/ mid_x:272 = (havoc:21 + -K:271))
         /\ (!((0 <= K:271 /\ K:271 <= 0)) \/ mid_tmp:273 = tmp:274)
         /\ (!(1 <= K:271) \/ mid_tmp:273 = 0)
         /\ (!(0 <= K:271) \/ mid___cost:275 = 0)
         /\ (!(0 <= K:271) \/ mid_y:276 = havoc:22) /\ K:271 = 0
         /\ havoc:22 = mid_y:276 /\ havoc:21 = mid_x:272
         /\ tmp:274 = mid_tmp:273 /\ 0 = mid___cost:275 /\ 0 = K:271
         /\ (!(0 <= K:277) \/ x':278 = (mid_x:272 + -K:277))
         /\ (!(0 <= K:277)
               \/ (__cost':279 + y':280) <= ((mid___cost:275 + mid_y:276)
                                               + (2 * K:277)))
         /\ (!(0 <= K:277)
               \/ (-__cost':279 + y':280) <= (-mid___cost:275 + mid_y:276))
         /\ (!(0 <= K:277)
               \/ (-__cost':279 + -y':280) <= (-mid___cost:275 + -mid_y:276))
         /\ ((K:277 = 0 /\ mid_y:276 = y':280 /\ mid_x:272 = x':278
                /\ mid_tmp:273 = tmp':281 /\ mid___cost:275 = __cost':279)
               \/ (1 <= K:277 /\ 0 <= mid___cost:275 /\ 0 <= (-1 + mid_x:272)
                     /\ 0 <= __cost':279 /\ 0 <= x':278))
         /\ (0 = K:277 \/ -mid___cost:275 <= 0) /\ (K:271 + K:277) = K:282
         /\ (!(0 <= K:283) \/ mid_x:284 = (havoc:21 + -K:283))
         /\ (!((0 <= K:283 /\ K:283 <= 0)) \/ mid_tmp:285 = tmp:274)
         /\ (!(1 <= K:283) \/ mid_tmp:285 = 0)
         /\ (!(0 <= K:283) \/ mid___cost:286 = 0)
         /\ (!(0 <= K:283) \/ mid_y:287 = havoc:22) /\ K:283 = 0
         /\ havoc:22 = mid_y:287 /\ havoc:21 = mid_x:284
         /\ tmp:274 = mid_tmp:285 /\ 0 = mid___cost:286 /\ 0 = K:283
         /\ (!(0 <= K:288) \/ x':278 = (mid_x:284 + -K:288))
         /\ (!(0 <= K:288)
               \/ (__cost':279 + y':280) <= ((mid___cost:286 + mid_y:287)
                                               + (2 * K:288)))
         /\ (!(0 <= K:288)
               \/ (-__cost':279 + y':280) <= (-mid___cost:286 + mid_y:287))
         /\ (!(0 <= K:288)
               \/ (-__cost':279 + -y':280) <= (-mid___cost:286 + -mid_y:287))
         /\ ((K:288 = 0 /\ mid_y:287 = y':280 /\ mid_x:284 = x':278
                /\ mid_tmp:285 = tmp':281 /\ mid___cost:286 = __cost':279)
               \/ (1 <= K:288 /\ 0 <= (1 + mid___cost:286)
                     /\ 0 <= (-1 + mid_x:284) /\ 0 <= (1 + __cost':279)
                     /\ 0 <= x':278))
         /\ (0 = K:288 \/ (-1 + -mid___cost:286) <= 0)
         /\ (K:283 + K:288) = K:282 /\ 0 <= K:282 /\ x':278 <= 0
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:292)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:292))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:293)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:293)))}

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

Base relation: 
{__cost := __cost':214
 tmp := tmp':216
 x := x':213
 y := y':215
 return := havoc:224
 return@pos := type_err:225
 return@width := type_err:226
 when ((!(0 <= K:207) \/ mid_x:208 = (param0:75 + -K:207))
         /\ (!((0 <= K:207 /\ K:207 <= 0)) \/ mid_tmp:209 = tmp:67)
         /\ (!(1 <= K:207) \/ mid_tmp:209 = 0)
         /\ (!(0 <= K:207) \/ mid___cost:210 = __cost:66)
         /\ (!(0 <= K:207) \/ mid_y:211 = param1:78)
         /\ ((K:207 = 0 /\ param1:78 = mid_y:211 /\ param0:75 = mid_x:208
                /\ tmp:67 = mid_tmp:209 /\ __cost:66 = mid___cost:210)
               \/ (1 <= K:207 /\ 0 <= (-1 + -__cost:66) /\ 0 <= -param1:78
                     /\ 0 <= (-1 + param0:75) /\ mid_tmp:209 = 0
                     /\ 0 <= -mid_y:211 /\ 0 <= (-1 + -mid___cost:210)
                     /\ 0 <= mid_x:208)) /\ (0 = K:207 \/ !(-__cost:66 <= 0))
         /\ (!(0 <= K:212) \/ x':213 = (mid_x:208 + -K:212))
         /\ (!(0 <= K:212)
               \/ (__cost':214 + y':215) <= ((mid___cost:210 + mid_y:211)
                                               + (2 * K:212)))
         /\ (!(0 <= K:212)
               \/ (-__cost':214 + y':215) <= (-mid___cost:210 + mid_y:211))
         /\ (!(0 <= K:212)
               \/ (-__cost':214 + -y':215) <= (-mid___cost:210 + -mid_y:211))
         /\ ((K:212 = 0 /\ mid_y:211 = y':215 /\ mid_x:208 = x':213
                /\ mid_tmp:209 = tmp':216 /\ mid___cost:210 = __cost':214)
               \/ (1 <= K:212 /\ 0 <= mid___cost:210 /\ 0 <= (-1 + mid_x:208)
                     /\ 0 <= __cost':214 /\ 0 <= x':213))
         /\ (0 = K:212 \/ -mid___cost:210 <= 0) /\ (K:207 + K:212) = K:217
         /\ (!(0 <= K:218) \/ mid_x:219 = (param0:75 + -K:218))
         /\ (!((0 <= K:218 /\ K:218 <= 0)) \/ mid_tmp:220 = tmp:67)
         /\ (!(1 <= K:218) \/ mid_tmp:220 = 0)
         /\ (!(0 <= K:218) \/ mid___cost:221 = __cost:66)
         /\ (!(0 <= K:218) \/ mid_y:222 = param1:78)
         /\ ((K:218 = 0 /\ param1:78 = mid_y:222 /\ param0:75 = mid_x:219
                /\ tmp:67 = mid_tmp:220 /\ __cost:66 = mid___cost:221)
               \/ (1 <= K:218 /\ 0 <= (-2 + -__cost:66) /\ 0 <= -param1:78
                     /\ 0 <= (-1 + param0:75) /\ mid_tmp:220 = 0
                     /\ 0 <= -mid_y:222 /\ 0 <= (-2 + -mid___cost:221)
                     /\ 0 <= mid_x:219))
         /\ (0 = K:218 \/ !((-1 + -__cost:66) <= 0))
         /\ (!(0 <= K:223) \/ x':213 = (mid_x:219 + -K:223))
         /\ (!(0 <= K:223)
               \/ (__cost':214 + y':215) <= ((mid___cost:221 + mid_y:222)
                                               + (2 * K:223)))
         /\ (!(0 <= K:223)
               \/ (-__cost':214 + y':215) <= (-mid___cost:221 + mid_y:222))
         /\ (!(0 <= K:223)
               \/ (-__cost':214 + -y':215) <= (-mid___cost:221 + -mid_y:222))
         /\ ((K:223 = 0 /\ mid_y:222 = y':215 /\ mid_x:219 = x':213
                /\ mid_tmp:220 = tmp':216 /\ mid___cost:221 = __cost':214)
               \/ (1 <= K:223 /\ 0 <= (1 + mid___cost:221)
                     /\ 0 <= (-1 + mid_x:219) /\ 0 <= (1 + __cost':214)
                     /\ 0 <= x':213))
         /\ (0 = K:223 \/ (-1 + -mid___cost:221) <= 0)
         /\ (K:218 + K:223) = K:217 /\ 0 <= K:217 /\ x':213 <= 0)}

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

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

Variable bounds at line 21 in start

min(__cost, __cost) <= __cost
__cost is o(1)

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