/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, 35> -> <Unique State Name, 46>	Base relation: 
{__cost := (__cost:64 + 1)
 tmp := havoc:72
 when (x:62 < n:63 /\ 0 <= __cost:64 /\ 0 <= (__cost:64 + 1))}	
<Unique State Name, 35> -> <Unique State Name, 53>	Base relation: 
{when n:63 <= x:62}	
<Unique State Name, 17> -> <Unique State Name, 69>	Base relation: 
{return := havoc:41
 return@pos := type_err:44
 return@width := type_err:45}	
<Unique State Name, 15> -> <Unique State Name, 67>	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
<Unique State Name, 22> -> <Unique State Name, 72>	Base relation: 
{when 0 <= x:62}	
<Unique State Name, 53> -> <Unique State Name, 22>	Base relation: 
{}	
<Unique State Name, 66> -> <Unique State Name, 70>	Base relation: 
{return := 0
 return@pos := type_err:19
 return@width := type_err:20
 when ((0 < n:2 /\ n:2 = phi_tmp___0:14) \/ (n:2 <= 0 /\ 0 = phi_tmp___0:14))}	
<Unique State Name, 64> -> <Unique State Name, 63>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
<Unique State Name, 70> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 62> -> <Unique State Name, 17>	Base relation: 
{}	
<Unique State Name, 68> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 46> -> <Unique State Name, 31>	Base relation: 
{x := (x:62 + 1)
 when tmp:66 = 0}	
<Unique State Name, 46> -> <Unique State Name, 53>	Base relation: 
{when !(tmp:66 = 0)}	
<Unique State Name, 69> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 71> -> <Unique State Name, 35>	Base relation: 
{}	
<Unique State Name, 63> -> <Unique State Name, 60 62>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 60> -> <Unique State Name, 22>	Base relation: 
{x := 0
 n := param0:53}	
<Unique State Name, 72> -> <Unique State Name, 26>	Base relation: 
{}	
<Unique State Name, 67> -> <Unique State Name, 64 66>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 31> -> <Unique State Name, 71>	Base relation: 
{when (1 <= n:63 /\ 1 <= x:62)}	
<Unique State Name, 26> -> <Unique State Name, 31>	Base relation: 
{x := (x:62 + 1)
 when x:62 < n:63}	
<Unique State Name, 26> -> <Unique State Name, 68>	Base relation: 
{return := havoc:73
 return@pos := type_err:74
 return@width := type_err:75
 when n:63 <= x:62}	
#################################################################
           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:64 + 1)
 x := (x:62 + 1)
 tmp := havoc:241
 when (1 <= n:63 /\ 1 <= x:62 /\ x:62 < n:63 /\ 0 <= __cost:64
         /\ 0 <= (__cost:64 + 1) /\ havoc:241 = 0)}
**** alpha hat: 
  {<Split [true
            (__cost':242) = (1)*(__cost:64) + 1
           (tmp':244) = 0
           (x':243) = (1)*(x:62) + 1
           }
          pre:
            [|__cost:64>=0; x:62-1>=0; n:63-x:62-1>=0|]
          post:
            [|tmp':244=0; x':243-2>=0; __cost':242-1>=0; n:63-x':243>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':242
   x := x':243
   tmp := tmp':244
   when ((!(0 <= K:256) \/ mid___cost:260 = (__cost:64 + K:256))
           /\ (!((0 <= K:256 /\ K:256 <= 0)) \/ mid_tmp:258 = tmp:66)
           /\ (!(1 <= K:256) \/ mid_tmp:258 = 0)
           /\ (!(0 <= K:256) \/ mid_x:259 = (x:62 + K:256))
           /\ ((K:256 = 0 /\ tmp:66 = mid_tmp:258 /\ x:62 = mid_x:259
                  /\ __cost:64 = mid___cost:260)
                 \/ (1 <= K:256 /\ 0 <= __cost:64 /\ 0 <= (-1 + x:62)
                       /\ 0 <= (-1 + n:63 + -x:62) /\ mid_tmp:258 = 0
                       /\ 0 <= (-2 + mid_x:259) /\ 0 <= (-1 + mid___cost:260)
                       /\ 0 <= (n:63 + -mid_x:259))) /\ K:257 = 0
           /\ mid_tmp:258 = tmp':244 /\ mid_x:259 = x':243
           /\ mid___cost:260 = __cost':242 /\ 0 = K:257
           /\ (K:256 + K:257) = K:255 /\ 0 <= K:255)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := phi___cost:281
 x := x':276
 tmp := phi_tmp:282
 when (0 <= x:62 /\ x:62 < n:63
         /\ (!(0 <= K:270) \/ mid___cost:271 = (__cost:64 + K:270))
         /\ (!((0 <= K:270 /\ K:270 <= 0)) \/ mid_tmp:272 = tmp:66)
         /\ (!(1 <= K:270) \/ mid_tmp:272 = 0)
         /\ (!(0 <= K:270) \/ mid_x:273 = ((x:62 + 1) + K:270))
         /\ ((K:270 = 0 /\ tmp:66 = mid_tmp:272 /\ (x:62 + 1) = mid_x:273
                /\ __cost:64 = mid___cost:271)
               \/ (1 <= K:270 /\ 0 <= __cost:64 /\ 0 <= (-1 + (x:62 + 1))
                     /\ 0 <= (-1 + n:63 + -((x:62 + 1))) /\ mid_tmp:272 = 0
                     /\ 0 <= (-2 + mid_x:273) /\ 0 <= (-1 + mid___cost:271)
                     /\ 0 <= (n:63 + -mid_x:273))) /\ K:274 = 0
         /\ mid_tmp:272 = tmp':275 /\ mid_x:273 = x':276
         /\ mid___cost:271 = __cost':277 /\ 0 = K:274
         /\ (K:270 + K:274) = K:278 /\ 0 <= K:278 /\ 1 <= n:63 /\ 1 <= x':276
         /\ ((n:63 <= x':276 /\ __cost':277 = phi___cost:281
                /\ tmp':275 = phi_tmp:282)
               \/ (x':276 < n:63 /\ 0 <= __cost':277
                     /\ 0 <= (__cost':277 + 1) /\ !(havoc:283 = 0)
                     /\ (__cost':277 + 1) = phi___cost:281
                     /\ havoc:283 = phi_tmp:282)))}
**** alpha hat: 
  {<Split [(2 + x:62 + -n:63) <= 0
            ((-__cost':242 + x':243)) <= (1)*((-__cost:64 + x:62)) + 1
           (__cost':242) <= (1)*(__cost:64) + (-1)*1 + n:63
           (-__cost':242) <= (1)*(-__cost:64) + (-1)*1
           ((__cost':242 + -x':243)) <= (1)*((__cost:64 + -x:62)) + 0
           }
          pre:
            [|-x:62+n:63-2>=0; __cost:64>=0; x:62>=0|]
          post:
            [|-x':243+n:63>=0; n:63-2>=0; __cost':242-1>=0; x':243-1>=0|]
           (x':243) = n:63
          (__cost':242) = (1)*(__cost:64) + 0
          (tmp':244) = (1)*(tmp:66) + 0
          }
  pre:
    [|-x:62+n:63-1=0; x:62>=0|]
  post:
    [|-n:63+x':243=0; n:63-1>=0|]],
[!(-__cost:64 <= 0)
  (x':243) = n:63
 (__cost':242) = (1)*(__cost:64) + 0
 (tmp':244) = (1)*(tmp:66) + 0
 } pre:   [|-x:62+n:63-1=0; -__cost:64-1>=0; x:62>=0|] post:
  [|-n:63+x':243=0; -__cost':242-1>=0; n:63-1>=0|]
 ((-__cost':242 + x':243)) <= (1)*((-__cost:64 + x:62)) + 1
(__cost':242) <= (1)*(__cost:64) + (-1)*1 + n:63
((__cost':242 + -x':243)) <= (1)*((__cost:64 + -x:62)) + 0
(-x':243) <= (1)*(-x:62) + (-1)*1 } pre:
  [|-x:62+n:63-1>=0; __cost:64>=0; x:62>=0|] post:
  [|-x':243+n:63>=0; __cost':242>=0; x':243-1>=0|]]>}
**** star transition: 
  {__cost := __cost':242
   x := x':243
   tmp := tmp':244
   when ((!(0 <= K:307)
            \/ (-mid___cost:311 + mid_x:310) <= ((-__cost:64 + x:62) + K:307))
           /\ (!(0 <= K:307)
                 \/ mid___cost:311 <= (__cost:64 + -K:307 + (n:63 * K:307)))
           /\ (!(0 <= K:307) \/ -mid___cost:311 <= (-__cost:64 + -K:307))
           /\ (!(0 <= K:307)
                 \/ (mid___cost:311 + -mid_x:310) <= (__cost:64 + -x:62))
           /\ ((K:307 = 0 /\ tmp:66 = mid_tmp:309 /\ x:62 = mid_x:310
                  /\ __cost:64 = mid___cost:311)
                 \/ (1 <= K:307 /\ 0 <= (-2 + -x:62 + n:63) /\ 0 <= __cost:64
                       /\ 0 <= x:62 /\ 0 <= (-mid_x:310 + n:63)
                       /\ 0 <= (-2 + n:63) /\ 0 <= (-1 + mid___cost:311)
                       /\ 0 <= (-1 + mid_x:310)))
           /\ (0 = K:307 \/ (2 + x:62 + -n:63) <= 0)
           /\ (!((0 <= K:308 /\ K:308 <= 0)) \/ x':243 = mid_x:310)
           /\ (!(1 <= K:308) \/ x':243 = n:63)
           /\ (!(0 <= K:308) \/ __cost':242 = mid___cost:311)
           /\ (!(0 <= K:308) \/ tmp':244 = mid_tmp:309)
           /\ ((K:308 = 0 /\ mid_tmp:309 = tmp':244 /\ mid_x:310 = x':243
                  /\ mid___cost:311 = __cost':242)
                 \/ (1 <= K:308 /\ (-1 + -mid_x:310 + n:63) = 0
                       /\ 0 <= mid_x:310 /\ (-n:63 + x':243) = 0
                       /\ 0 <= (-1 + n:63)))
           /\ (0 = K:308 \/ !((2 + mid_x:310 + -n:63) <= 0))
           /\ (K:307 + K:308) = K:306
           /\ (!((0 <= K:312 /\ K:312 <= 0)) \/ mid_x:315 = x:62)
           /\ (!(1 <= K:312) \/ mid_x:315 = n:63)
           /\ (!(0 <= K:312) \/ mid___cost:316 = __cost:64)
           /\ (!(0 <= K:312) \/ mid_tmp:314 = tmp:66)
           /\ ((K:312 = 0 /\ tmp:66 = mid_tmp:314 /\ x:62 = mid_x:315
                  /\ __cost:64 = mid___cost:316)
                 \/ (1 <= K:312 /\ (-1 + -x:62 + n:63) = 0
                       /\ 0 <= (-1 + -__cost:64) /\ 0 <= x:62
                       /\ (-n:63 + mid_x:315) = 0
                       /\ 0 <= (-1 + -mid___cost:316) /\ 0 <= (-1 + n:63)))
           /\ (0 = K:312 \/ !(-__cost:64 <= 0))
           /\ (!(0 <= K:313)
                 \/ (-__cost':242 + x':243) <= ((-mid___cost:316 + mid_x:315)
                                                  + K:313))
           /\ (!(0 <= K:313)
                 \/ __cost':242 <= (mid___cost:316 + -K:313 + (n:63 * K:313)))
           /\ (!(0 <= K:313)
                 \/ (__cost':242 + -x':243) <= (mid___cost:316 + -mid_x:315))
           /\ (!(0 <= K:313) \/ -x':243 <= (-mid_x:315 + -K:313))
           /\ ((K:313 = 0 /\ mid_tmp:314 = tmp':244 /\ mid_x:315 = x':243
                  /\ mid___cost:316 = __cost':242)
                 \/ (1 <= K:313 /\ 0 <= (-1 + -mid_x:315 + n:63)
                       /\ 0 <= mid___cost:316 /\ 0 <= mid_x:315
                       /\ 0 <= (-x':243 + n:63) /\ 0 <= __cost':242
                       /\ 0 <= (-1 + x':243)))
           /\ (0 = K:313 \/ -mid___cost:316 <= 0) /\ (K:312 + K:313) = K:306
           /\ 0 <= K:306)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  20  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       n := havoc:13
       param0 := havoc:13
       param0@pos := type_err:17
       param0@width := type_err:18}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:19
     return@width := type_err:20
     when ((0 < n:2 /\ n:2 = phi_tmp___0:14)
             \/ (n:2 <= 0 /\ 0 = phi_tmp___0:14))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:53
       param0@pos := type_err:54
       param0@width := type_err:55}    )
    ,
    Var(20)
  )
  ,
  Weight(Base relation: 
    {return := havoc:41
     return@pos := type_err:44
     return@width := type_err:45}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=20: 
Weight(Base relation: 
  {__cost := __cost':323
   x := x':322
   tmp := tmp':324
   n := param0:53
   return := havoc:362
   return@pos := type_err:363
   return@width := type_err:364
   when ((!(0 <= K:317)
            \/ (-mid___cost:318 + mid_x:319) <= (-__cost:64 + K:317))
           /\ (!(0 <= K:317)
                 \/ mid___cost:318 <= (__cost:64 + -K:317
                                         + (param0:53 * K:317)))
           /\ (!(0 <= K:317) \/ -mid___cost:318 <= (-__cost:64 + -K:317))
           /\ (!(0 <= K:317) \/ (mid___cost:318 + -mid_x:319) <= __cost:64)
           /\ ((K:317 = 0 /\ tmp:66 = mid_tmp:320 /\ 0 = mid_x:319
                  /\ __cost:64 = mid___cost:318)
                 \/ (1 <= K:317 /\ 0 <= (-2 + param0:53) /\ 0 <= __cost:64
                       /\ 0 <= (-mid_x:319 + param0:53)
                       /\ 0 <= (-2 + param0:53) /\ 0 <= (-1 + mid___cost:318)
                       /\ 0 <= (-1 + mid_x:319)))
           /\ (0 = K:317 \/ (2 + -param0:53) <= 0)
           /\ (!((0 <= K:321 /\ K:321 <= 0)) \/ x':322 = mid_x:319)
           /\ (!(1 <= K:321) \/ x':322 = param0:53)
           /\ (!(0 <= K:321) \/ __cost':323 = mid___cost:318)
           /\ (!(0 <= K:321) \/ tmp':324 = mid_tmp:320)
           /\ ((K:321 = 0 /\ mid_tmp:320 = tmp':324 /\ mid_x:319 = x':322
                  /\ mid___cost:318 = __cost':323)
                 \/ (1 <= K:321 /\ (-1 + -mid_x:319 + param0:53) = 0
                       /\ 0 <= mid_x:319 /\ (-param0:53 + x':322) = 0
                       /\ 0 <= (-1 + param0:53)))
           /\ (0 = K:321 \/ !((2 + mid_x:319 + -param0:53) <= 0))
           /\ (K:317 + K:321) = K:325
           /\ (!((0 <= K:326 /\ K:326 <= 0)) \/ mid_x:327 = 0)
           /\ (!(1 <= K:326) \/ mid_x:327 = param0:53)
           /\ (!(0 <= K:326) \/ mid___cost:328 = __cost:64)
           /\ (!(0 <= K:326) \/ mid_tmp:329 = tmp:66)
           /\ ((K:326 = 0 /\ tmp:66 = mid_tmp:329 /\ 0 = mid_x:327
                  /\ __cost:64 = mid___cost:328)
                 \/ (1 <= K:326 /\ (-1 + param0:53) = 0
                       /\ 0 <= (-1 + -__cost:64)
                       /\ (-param0:53 + mid_x:327) = 0
                       /\ 0 <= (-1 + -mid___cost:328)
                       /\ 0 <= (-1 + param0:53)))
           /\ (0 = K:326 \/ !(-__cost:64 <= 0))
           /\ (!(0 <= K:330)
                 \/ (-__cost':323 + x':322) <= ((-mid___cost:328 + mid_x:327)
                                                  + K:330))
           /\ (!(0 <= K:330)
                 \/ __cost':323 <= (mid___cost:328 + -K:330
                                      + (param0:53 * K:330)))
           /\ (!(0 <= K:330)
                 \/ (__cost':323 + -x':322) <= (mid___cost:328 + -mid_x:327))
           /\ (!(0 <= K:330) \/ -x':322 <= (-mid_x:327 + -K:330))
           /\ ((K:330 = 0 /\ mid_tmp:329 = tmp':324 /\ mid_x:327 = x':322
                  /\ mid___cost:328 = __cost':323)
                 \/ (1 <= K:330 /\ 0 <= (-1 + -mid_x:327 + param0:53)
                       /\ 0 <= mid___cost:328 /\ 0 <= mid_x:327
                       /\ 0 <= (-x':322 + param0:53) /\ 0 <= __cost':323
                       /\ 0 <= (-1 + x':322)))
           /\ (0 = K:330 \/ -mid___cost:328 <= 0) /\ (K:326 + K:330) = K:325
           /\ 0 <= K:325 /\ 0 <= x':322 /\ param0:53 <= x':322)})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := 0
         n := havoc:13
         param0 := havoc:13
         param0@pos := type_err:17
         param0@width := type_err:18}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:19
       return@width := type_err:20
       when ((0 < n:2 /\ n:2 = phi_tmp___0:14)
               \/ (n:2 <= 0 /\ 0 = phi_tmp___0:14))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:53
         param0@pos := type_err:54
         param0@width := type_err:55}      )
      ,
      Var(20)
    )
    ,
    Weight(Base relation: 
      {return := havoc:41
       return@pos := type_err:44
       return@width := type_err:45}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':323
   return := havoc:362
   return@pos := type_err:363
   return@width := type_err:364
   when ((!(0 <= K:317)
            \/ (-mid___cost:318 + mid_x:319) <= (-__cost:64 + K:317))
           /\ (!(0 <= K:317)
                 \/ mid___cost:318 <= (__cost:64 + -K:317
                                         + (param0:53 * K:317)))
           /\ (!(0 <= K:317) \/ -mid___cost:318 <= (-__cost:64 + -K:317))
           /\ (!(0 <= K:317) \/ (mid___cost:318 + -mid_x:319) <= __cost:64)
           /\ ((K:317 = 0 /\ tmp:365 = mid_tmp:320 /\ 0 = mid_x:319
                  /\ __cost:64 = mid___cost:318)
                 \/ (1 <= K:317 /\ 0 <= (-2 + param0:53) /\ 0 <= __cost:64
                       /\ 0 <= (-mid_x:319 + param0:53)
                       /\ 0 <= (-2 + param0:53) /\ 0 <= (-1 + mid___cost:318)
                       /\ 0 <= (-1 + mid_x:319)))
           /\ (0 = K:317 \/ (2 + -param0:53) <= 0)
           /\ (!((0 <= K:321 /\ K:321 <= 0)) \/ x':322 = mid_x:319)
           /\ (!(1 <= K:321) \/ x':322 = param0:53)
           /\ (!(0 <= K:321) \/ __cost':323 = mid___cost:318)
           /\ (!(0 <= K:321) \/ tmp':324 = mid_tmp:320)
           /\ ((K:321 = 0 /\ mid_tmp:320 = tmp':324 /\ mid_x:319 = x':322
                  /\ mid___cost:318 = __cost':323)
                 \/ (1 <= K:321 /\ (-1 + -mid_x:319 + param0:53) = 0
                       /\ 0 <= mid_x:319 /\ (-param0:53 + x':322) = 0
                       /\ 0 <= (-1 + param0:53)))
           /\ (0 = K:321 \/ !((2 + mid_x:319 + -param0:53) <= 0))
           /\ (K:317 + K:321) = K:325
           /\ (!((0 <= K:326 /\ K:326 <= 0)) \/ mid_x:327 = 0)
           /\ (!(1 <= K:326) \/ mid_x:327 = param0:53)
           /\ (!(0 <= K:326) \/ mid___cost:328 = __cost:64)
           /\ (!(0 <= K:326) \/ mid_tmp:329 = tmp:365)
           /\ ((K:326 = 0 /\ tmp:365 = mid_tmp:329 /\ 0 = mid_x:327
                  /\ __cost:64 = mid___cost:328)
                 \/ (1 <= K:326 /\ (-1 + param0:53) = 0
                       /\ 0 <= (-1 + -__cost:64)
                       /\ (-param0:53 + mid_x:327) = 0
                       /\ 0 <= (-1 + -mid___cost:328)
                       /\ 0 <= (-1 + param0:53)))
           /\ (0 = K:326 \/ !(-__cost:64 <= 0))
           /\ (!(0 <= K:330)
                 \/ (-__cost':323 + x':322) <= ((-mid___cost:328 + mid_x:327)
                                                  + K:330))
           /\ (!(0 <= K:330)
                 \/ __cost':323 <= (mid___cost:328 + -K:330
                                      + (param0:53 * K:330)))
           /\ (!(0 <= K:330)
                 \/ (__cost':323 + -x':322) <= (mid___cost:328 + -mid_x:327))
           /\ (!(0 <= K:330) \/ -x':322 <= (-mid_x:327 + -K:330))
           /\ ((K:330 = 0 /\ mid_tmp:329 = tmp':324 /\ mid_x:327 = x':322
                  /\ mid___cost:328 = __cost':323)
                 \/ (1 <= K:330 /\ 0 <= (-1 + -mid_x:327 + param0:53)
                       /\ 0 <= mid___cost:328 /\ 0 <= mid_x:327
                       /\ 0 <= (-x':322 + param0:53) /\ 0 <= __cost':323
                       /\ 0 <= (-1 + x':322)))
           /\ (0 = K:330 \/ -mid___cost:328 <= 0) /\ (K:326 + K:330) = K:325
           /\ 0 <= K:325 /\ 0 <= x':322 /\ param0:53 <= x':322)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':394
   return := 0
   param0 := havoc:13
   return@pos := type_err:408
   param0@pos := type_err:404
   return@width := type_err:409
   param0@width := type_err:406
   when ((!(0 <= K:387) \/ (-mid___cost:388 + mid_x:389) <= K:387)
           /\ (!(0 <= K:387)
                 \/ mid___cost:388 <= (-K:387 + (havoc:13 * K:387)))
           /\ (!(0 <= K:387) \/ -mid___cost:388 <= -K:387)
           /\ (!(0 <= K:387) \/ (mid___cost:388 + -mid_x:389) <= 0)
           /\ ((K:387 = 0 /\ tmp:390 = mid_tmp:391 /\ 0 = mid_x:389
                  /\ 0 = mid___cost:388)
                 \/ (1 <= K:387 /\ 0 <= (-2 + havoc:13)
                       /\ 0 <= (-mid_x:389 + havoc:13)
                       /\ 0 <= (-2 + havoc:13) /\ 0 <= (-1 + mid___cost:388)
                       /\ 0 <= (-1 + mid_x:389)))
           /\ (0 = K:387 \/ (2 + -havoc:13) <= 0)
           /\ (!((0 <= K:392 /\ K:392 <= 0)) \/ x':393 = mid_x:389)
           /\ (!(1 <= K:392) \/ x':393 = havoc:13)
           /\ (!(0 <= K:392) \/ __cost':394 = mid___cost:388)
           /\ (!(0 <= K:392) \/ tmp':395 = mid_tmp:391)
           /\ ((K:392 = 0 /\ mid_tmp:391 = tmp':395 /\ mid_x:389 = x':393
                  /\ mid___cost:388 = __cost':394)
                 \/ (1 <= K:392 /\ (-1 + -mid_x:389 + havoc:13) = 0
                       /\ 0 <= mid_x:389 /\ (-havoc:13 + x':393) = 0
                       /\ 0 <= (-1 + havoc:13)))
           /\ (0 = K:392 \/ !((2 + mid_x:389 + -havoc:13) <= 0))
           /\ (K:387 + K:392) = K:396
           /\ (!((0 <= K:397 /\ K:397 <= 0)) \/ mid_x:398 = 0)
           /\ (!(1 <= K:397) \/ mid_x:398 = havoc:13)
           /\ (!(0 <= K:397) \/ mid___cost:399 = 0)
           /\ (!(0 <= K:397) \/ mid_tmp:400 = tmp:390) /\ K:397 = 0
           /\ tmp:390 = mid_tmp:400 /\ 0 = mid_x:398 /\ 0 = mid___cost:399
           /\ 0 = K:397
           /\ (!(0 <= K:401)
                 \/ (-__cost':394 + x':393) <= ((-mid___cost:399 + mid_x:398)
                                                  + K:401))
           /\ (!(0 <= K:401)
                 \/ __cost':394 <= (mid___cost:399 + -K:401
                                      + (havoc:13 * K:401)))
           /\ (!(0 <= K:401)
                 \/ (__cost':394 + -x':393) <= (mid___cost:399 + -mid_x:398))
           /\ (!(0 <= K:401) \/ -x':393 <= (-mid_x:398 + -K:401))
           /\ ((K:401 = 0 /\ mid_tmp:400 = tmp':395 /\ mid_x:398 = x':393
                  /\ mid___cost:399 = __cost':394)
                 \/ (1 <= K:401 /\ 0 <= (-1 + -mid_x:398 + havoc:13)
                       /\ 0 <= mid___cost:399 /\ 0 <= mid_x:398
                       /\ 0 <= (-x':393 + havoc:13) /\ 0 <= __cost':394
                       /\ 0 <= (-1 + x':393)))
           /\ (0 = K:401 \/ -mid___cost:399 <= 0) /\ (K:397 + K:401) = K:396
           /\ 0 <= K:396 /\ 0 <= x':393 /\ havoc:13 <= x':393
           /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:407)
                 \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:407)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':417
   return := havoc:428
   param0 := param0:53
   return@pos := type_err:429
   param0@pos := type_err:54
   return@width := type_err:430
   param0@width := type_err:55
   when ((!(0 <= K:410)
            \/ (-mid___cost:411 + mid_x:412) <= (-__cost:64 + K:410))
           /\ (!(0 <= K:410)
                 \/ mid___cost:411 <= (__cost:64 + -K:410
                                         + (param0:53 * K:410)))
           /\ (!(0 <= K:410) \/ -mid___cost:411 <= (-__cost:64 + -K:410))
           /\ (!(0 <= K:410) \/ (mid___cost:411 + -mid_x:412) <= __cost:64)
           /\ ((K:410 = 0 /\ tmp:413 = mid_tmp:414 /\ 0 = mid_x:412
                  /\ __cost:64 = mid___cost:411)
                 \/ (1 <= K:410 /\ 0 <= (-2 + param0:53) /\ 0 <= __cost:64
                       /\ 0 <= (-mid_x:412 + param0:53)
                       /\ 0 <= (-2 + param0:53) /\ 0 <= (-1 + mid___cost:411)
                       /\ 0 <= (-1 + mid_x:412)))
           /\ (0 = K:410 \/ (2 + -param0:53) <= 0)
           /\ (!((0 <= K:415 /\ K:415 <= 0)) \/ x':416 = mid_x:412)
           /\ (!(1 <= K:415) \/ x':416 = param0:53)
           /\ (!(0 <= K:415) \/ __cost':417 = mid___cost:411)
           /\ (!(0 <= K:415) \/ tmp':418 = mid_tmp:414)
           /\ ((K:415 = 0 /\ mid_tmp:414 = tmp':418 /\ mid_x:412 = x':416
                  /\ mid___cost:411 = __cost':417)
                 \/ (1 <= K:415 /\ (-1 + -mid_x:412 + param0:53) = 0
                       /\ 0 <= mid_x:412 /\ (-param0:53 + x':416) = 0
                       /\ 0 <= (-1 + param0:53)))
           /\ (0 = K:415 \/ !((2 + mid_x:412 + -param0:53) <= 0))
           /\ (K:410 + K:415) = K:419
           /\ (!((0 <= K:420 /\ K:420 <= 0)) \/ mid_x:421 = 0)
           /\ (!(1 <= K:420) \/ mid_x:421 = param0:53)
           /\ (!(0 <= K:420) \/ mid___cost:422 = __cost:64)
           /\ (!(0 <= K:420) \/ mid_tmp:423 = tmp:413)
           /\ ((K:420 = 0 /\ tmp:413 = mid_tmp:423 /\ 0 = mid_x:421
                  /\ __cost:64 = mid___cost:422)
                 \/ (1 <= K:420 /\ (-1 + param0:53) = 0
                       /\ 0 <= (-1 + -__cost:64)
                       /\ (-param0:53 + mid_x:421) = 0
                       /\ 0 <= (-1 + -mid___cost:422)
                       /\ 0 <= (-1 + param0:53)))
           /\ (0 = K:420 \/ !(-__cost:64 <= 0))
           /\ (!(0 <= K:424)
                 \/ (-__cost':417 + x':416) <= ((-mid___cost:422 + mid_x:421)
                                                  + K:424))
           /\ (!(0 <= K:424)
                 \/ __cost':417 <= (mid___cost:422 + -K:424
                                      + (param0:53 * K:424)))
           /\ (!(0 <= K:424)
                 \/ (__cost':417 + -x':416) <= (mid___cost:422 + -mid_x:421))
           /\ (!(0 <= K:424) \/ -x':416 <= (-mid_x:421 + -K:424))
           /\ ((K:424 = 0 /\ mid_tmp:423 = tmp':418 /\ mid_x:421 = x':416
                  /\ mid___cost:422 = __cost':417)
                 \/ (1 <= K:424 /\ 0 <= (-1 + -mid_x:421 + param0:53)
                       /\ 0 <= mid___cost:422 /\ 0 <= mid_x:421
                       /\ 0 <= (-x':416 + param0:53) /\ 0 <= __cost':417
                       /\ 0 <= (-1 + x':416)))
           /\ (0 = K:424 \/ -mid___cost:422 <= 0) /\ (K:420 + K:424) = K:419
           /\ 0 <= K:419 /\ 0 <= x':416 /\ param0:53 <= x':416)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=20: 
Weight(Base relation: 
  {__cost := __cost':323
   return := havoc:362
   return@pos := type_err:363
   return@width := type_err:364
   when ((!(0 <= K:317)
            \/ (-mid___cost:318 + mid_x:319) <= (-__cost:64 + K:317))
           /\ (!(0 <= K:317)
                 \/ mid___cost:318 <= (__cost:64 + -K:317
                                         + (param0:53 * K:317)))
           /\ (!(0 <= K:317) \/ -mid___cost:318 <= (-__cost:64 + -K:317))
           /\ (!(0 <= K:317) \/ (mid___cost:318 + -mid_x:319) <= __cost:64)
           /\ ((K:317 = 0 /\ tmp:365 = mid_tmp:320 /\ 0 = mid_x:319
                  /\ __cost:64 = mid___cost:318)
                 \/ (1 <= K:317 /\ 0 <= (-2 + param0:53) /\ 0 <= __cost:64
                       /\ 0 <= (-mid_x:319 + param0:53)
                       /\ 0 <= (-2 + param0:53) /\ 0 <= (-1 + mid___cost:318)
                       /\ 0 <= (-1 + mid_x:319)))
           /\ (0 = K:317 \/ (2 + -param0:53) <= 0)
           /\ (!((0 <= K:321 /\ K:321 <= 0)) \/ x':322 = mid_x:319)
           /\ (!(1 <= K:321) \/ x':322 = param0:53)
           /\ (!(0 <= K:321) \/ __cost':323 = mid___cost:318)
           /\ (!(0 <= K:321) \/ tmp':324 = mid_tmp:320)
           /\ ((K:321 = 0 /\ mid_tmp:320 = tmp':324 /\ mid_x:319 = x':322
                  /\ mid___cost:318 = __cost':323)
                 \/ (1 <= K:321 /\ (-1 + -mid_x:319 + param0:53) = 0
                       /\ 0 <= mid_x:319 /\ (-param0:53 + x':322) = 0
                       /\ 0 <= (-1 + param0:53)))
           /\ (0 = K:321 \/ !((2 + mid_x:319 + -param0:53) <= 0))
           /\ (K:317 + K:321) = K:325
           /\ (!((0 <= K:326 /\ K:326 <= 0)) \/ mid_x:327 = 0)
           /\ (!(1 <= K:326) \/ mid_x:327 = param0:53)
           /\ (!(0 <= K:326) \/ mid___cost:328 = __cost:64)
           /\ (!(0 <= K:326) \/ mid_tmp:329 = tmp:365)
           /\ ((K:326 = 0 /\ tmp:365 = mid_tmp:329 /\ 0 = mid_x:327
                  /\ __cost:64 = mid___cost:328)
                 \/ (1 <= K:326 /\ (-1 + param0:53) = 0
                       /\ 0 <= (-1 + -__cost:64)
                       /\ (-param0:53 + mid_x:327) = 0
                       /\ 0 <= (-1 + -mid___cost:328)
                       /\ 0 <= (-1 + param0:53)))
           /\ (0 = K:326 \/ !(-__cost:64 <= 0))
           /\ (!(0 <= K:330)
                 \/ (-__cost':323 + x':322) <= ((-mid___cost:328 + mid_x:327)
                                                  + K:330))
           /\ (!(0 <= K:330)
                 \/ __cost':323 <= (mid___cost:328 + -K:330
                                      + (param0:53 * K:330)))
           /\ (!(0 <= K:330)
                 \/ (__cost':323 + -x':322) <= (mid___cost:328 + -mid_x:327))
           /\ (!(0 <= K:330) \/ -x':322 <= (-mid_x:327 + -K:330))
           /\ ((K:330 = 0 /\ mid_tmp:329 = tmp':324 /\ mid_x:327 = x':322
                  /\ mid___cost:328 = __cost':323)
                 \/ (1 <= K:330 /\ 0 <= (-1 + -mid_x:327 + param0:53)
                       /\ 0 <= mid___cost:328 /\ 0 <= mid_x:327
                       /\ 0 <= (-x':322 + param0:53) /\ 0 <= __cost':323
                       /\ 0 <= (-1 + x':322)))
           /\ (0 = K:330 \/ -mid___cost:328 <= 0) /\ (K:326 + K:330) = K:325
           /\ 0 <= K:325 /\ 0 <= x':322 /\ param0:53 <= x':322)})


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':394
 return := 0
 param0 := havoc:13
 return@pos := type_err:408
 param0@pos := type_err:404
 return@width := type_err:409
 param0@width := type_err:406
 when ((!(0 <= K:387) \/ (-mid___cost:388 + mid_x:389) <= K:387)
         /\ (!(0 <= K:387) \/ mid___cost:388 <= (-K:387 + (havoc:13 * K:387)))
         /\ (!(0 <= K:387) \/ -mid___cost:388 <= -K:387)
         /\ (!(0 <= K:387) \/ (mid___cost:388 + -mid_x:389) <= 0)
         /\ ((K:387 = 0 /\ tmp:390 = mid_tmp:391 /\ 0 = mid_x:389
                /\ 0 = mid___cost:388)
               \/ (1 <= K:387 /\ 0 <= (-2 + havoc:13)
                     /\ 0 <= (-mid_x:389 + havoc:13) /\ 0 <= (-2 + havoc:13)
                     /\ 0 <= (-1 + mid___cost:388) /\ 0 <= (-1 + mid_x:389)))
         /\ (0 = K:387 \/ (2 + -havoc:13) <= 0)
         /\ (!((0 <= K:392 /\ K:392 <= 0)) \/ x':393 = mid_x:389)
         /\ (!(1 <= K:392) \/ x':393 = havoc:13)
         /\ (!(0 <= K:392) \/ __cost':394 = mid___cost:388)
         /\ (!(0 <= K:392) \/ tmp':395 = mid_tmp:391)
         /\ ((K:392 = 0 /\ mid_tmp:391 = tmp':395 /\ mid_x:389 = x':393
                /\ mid___cost:388 = __cost':394)
               \/ (1 <= K:392 /\ (-1 + -mid_x:389 + havoc:13) = 0
                     /\ 0 <= mid_x:389 /\ (-havoc:13 + x':393) = 0
                     /\ 0 <= (-1 + havoc:13)))
         /\ (0 = K:392 \/ !((2 + mid_x:389 + -havoc:13) <= 0))
         /\ (K:387 + K:392) = K:396
         /\ (!((0 <= K:397 /\ K:397 <= 0)) \/ mid_x:398 = 0)
         /\ (!(1 <= K:397) \/ mid_x:398 = havoc:13)
         /\ (!(0 <= K:397) \/ mid___cost:399 = 0)
         /\ (!(0 <= K:397) \/ mid_tmp:400 = tmp:390) /\ K:397 = 0
         /\ tmp:390 = mid_tmp:400 /\ 0 = mid_x:398 /\ 0 = mid___cost:399
         /\ 0 = K:397
         /\ (!(0 <= K:401)
               \/ (-__cost':394 + x':393) <= ((-mid___cost:399 + mid_x:398)
                                                + K:401))
         /\ (!(0 <= K:401)
               \/ __cost':394 <= (mid___cost:399 + -K:401
                                    + (havoc:13 * K:401)))
         /\ (!(0 <= K:401)
               \/ (__cost':394 + -x':393) <= (mid___cost:399 + -mid_x:398))
         /\ (!(0 <= K:401) \/ -x':393 <= (-mid_x:398 + -K:401))
         /\ ((K:401 = 0 /\ mid_tmp:400 = tmp':395 /\ mid_x:398 = x':393
                /\ mid___cost:399 = __cost':394)
               \/ (1 <= K:401 /\ 0 <= (-1 + -mid_x:398 + havoc:13)
                     /\ 0 <= mid___cost:399 /\ 0 <= mid_x:398
                     /\ 0 <= (-x':393 + havoc:13) /\ 0 <= __cost':394
                     /\ 0 <= (-1 + x':393)))
         /\ (0 = K:401 \/ -mid___cost:399 <= 0) /\ (K:397 + K:401) = K:396
         /\ 0 <= K:396 /\ 0 <= x':393 /\ havoc:13 <= x':393
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:407)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:407)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':417
 return := havoc:428
 param0 := param0:53
 return@pos := type_err:429
 param0@pos := type_err:54
 return@width := type_err:430
 param0@width := type_err:55
 when ((!(0 <= K:410)
          \/ (-mid___cost:411 + mid_x:412) <= (-__cost:64 + K:410))
         /\ (!(0 <= K:410)
               \/ mid___cost:411 <= (__cost:64 + -K:410 + (param0:53 * K:410)))
         /\ (!(0 <= K:410) \/ -mid___cost:411 <= (-__cost:64 + -K:410))
         /\ (!(0 <= K:410) \/ (mid___cost:411 + -mid_x:412) <= __cost:64)
         /\ ((K:410 = 0 /\ tmp:413 = mid_tmp:414 /\ 0 = mid_x:412
                /\ __cost:64 = mid___cost:411)
               \/ (1 <= K:410 /\ 0 <= (-2 + param0:53) /\ 0 <= __cost:64
                     /\ 0 <= (-mid_x:412 + param0:53)
                     /\ 0 <= (-2 + param0:53) /\ 0 <= (-1 + mid___cost:411)
                     /\ 0 <= (-1 + mid_x:412)))
         /\ (0 = K:410 \/ (2 + -param0:53) <= 0)
         /\ (!((0 <= K:415 /\ K:415 <= 0)) \/ x':416 = mid_x:412)
         /\ (!(1 <= K:415) \/ x':416 = param0:53)
         /\ (!(0 <= K:415) \/ __cost':417 = mid___cost:411)
         /\ (!(0 <= K:415) \/ tmp':418 = mid_tmp:414)
         /\ ((K:415 = 0 /\ mid_tmp:414 = tmp':418 /\ mid_x:412 = x':416
                /\ mid___cost:411 = __cost':417)
               \/ (1 <= K:415 /\ (-1 + -mid_x:412 + param0:53) = 0
                     /\ 0 <= mid_x:412 /\ (-param0:53 + x':416) = 0
                     /\ 0 <= (-1 + param0:53)))
         /\ (0 = K:415 \/ !((2 + mid_x:412 + -param0:53) <= 0))
         /\ (K:410 + K:415) = K:419
         /\ (!((0 <= K:420 /\ K:420 <= 0)) \/ mid_x:421 = 0)
         /\ (!(1 <= K:420) \/ mid_x:421 = param0:53)
         /\ (!(0 <= K:420) \/ mid___cost:422 = __cost:64)
         /\ (!(0 <= K:420) \/ mid_tmp:423 = tmp:413)
         /\ ((K:420 = 0 /\ tmp:413 = mid_tmp:423 /\ 0 = mid_x:421
                /\ __cost:64 = mid___cost:422)
               \/ (1 <= K:420 /\ (-1 + param0:53) = 0
                     /\ 0 <= (-1 + -__cost:64)
                     /\ (-param0:53 + mid_x:421) = 0
                     /\ 0 <= (-1 + -mid___cost:422) /\ 0 <= (-1 + param0:53)))
         /\ (0 = K:420 \/ !(-__cost:64 <= 0))
         /\ (!(0 <= K:424)
               \/ (-__cost':417 + x':416) <= ((-mid___cost:422 + mid_x:421)
                                                + K:424))
         /\ (!(0 <= K:424)
               \/ __cost':417 <= (mid___cost:422 + -K:424
                                    + (param0:53 * K:424)))
         /\ (!(0 <= K:424)
               \/ (__cost':417 + -x':416) <= (mid___cost:422 + -mid_x:421))
         /\ (!(0 <= K:424) \/ -x':416 <= (-mid_x:421 + -K:424))
         /\ ((K:424 = 0 /\ mid_tmp:423 = tmp':418 /\ mid_x:421 = x':416
                /\ mid___cost:422 = __cost':417)
               \/ (1 <= K:424 /\ 0 <= (-1 + -mid_x:421 + param0:53)
                     /\ 0 <= mid___cost:422 /\ 0 <= mid_x:421
                     /\ 0 <= (-x':416 + param0:53) /\ 0 <= __cost':417
                     /\ 0 <= (-1 + x':416)))
         /\ (0 = K:424 \/ -mid___cost:422 <= 0) /\ (K:420 + K:424) = K:419
         /\ 0 <= K:419 /\ 0 <= x':416 /\ param0:53 <= x':416)}

Evaluating variable number 20 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':323
 return := havoc:362
 return@pos := type_err:363
 return@width := type_err:364
 when ((!(0 <= K:317)
          \/ (-mid___cost:318 + mid_x:319) <= (-__cost:64 + K:317))
         /\ (!(0 <= K:317)
               \/ mid___cost:318 <= (__cost:64 + -K:317 + (param0:53 * K:317)))
         /\ (!(0 <= K:317) \/ -mid___cost:318 <= (-__cost:64 + -K:317))
         /\ (!(0 <= K:317) \/ (mid___cost:318 + -mid_x:319) <= __cost:64)
         /\ ((K:317 = 0 /\ tmp:365 = mid_tmp:320 /\ 0 = mid_x:319
                /\ __cost:64 = mid___cost:318)
               \/ (1 <= K:317 /\ 0 <= (-2 + param0:53) /\ 0 <= __cost:64
                     /\ 0 <= (-mid_x:319 + param0:53)
                     /\ 0 <= (-2 + param0:53) /\ 0 <= (-1 + mid___cost:318)
                     /\ 0 <= (-1 + mid_x:319)))
         /\ (0 = K:317 \/ (2 + -param0:53) <= 0)
         /\ (!((0 <= K:321 /\ K:321 <= 0)) \/ x':322 = mid_x:319)
         /\ (!(1 <= K:321) \/ x':322 = param0:53)
         /\ (!(0 <= K:321) \/ __cost':323 = mid___cost:318)
         /\ (!(0 <= K:321) \/ tmp':324 = mid_tmp:320)
         /\ ((K:321 = 0 /\ mid_tmp:320 = tmp':324 /\ mid_x:319 = x':322
                /\ mid___cost:318 = __cost':323)
               \/ (1 <= K:321 /\ (-1 + -mid_x:319 + param0:53) = 0
                     /\ 0 <= mid_x:319 /\ (-param0:53 + x':322) = 0
                     /\ 0 <= (-1 + param0:53)))
         /\ (0 = K:321 \/ !((2 + mid_x:319 + -param0:53) <= 0))
         /\ (K:317 + K:321) = K:325
         /\ (!((0 <= K:326 /\ K:326 <= 0)) \/ mid_x:327 = 0)
         /\ (!(1 <= K:326) \/ mid_x:327 = param0:53)
         /\ (!(0 <= K:326) \/ mid___cost:328 = __cost:64)
         /\ (!(0 <= K:326) \/ mid_tmp:329 = tmp:365)
         /\ ((K:326 = 0 /\ tmp:365 = mid_tmp:329 /\ 0 = mid_x:327
                /\ __cost:64 = mid___cost:328)
               \/ (1 <= K:326 /\ (-1 + param0:53) = 0
                     /\ 0 <= (-1 + -__cost:64)
                     /\ (-param0:53 + mid_x:327) = 0
                     /\ 0 <= (-1 + -mid___cost:328) /\ 0 <= (-1 + param0:53)))
         /\ (0 = K:326 \/ !(-__cost:64 <= 0))
         /\ (!(0 <= K:330)
               \/ (-__cost':323 + x':322) <= ((-mid___cost:328 + mid_x:327)
                                                + K:330))
         /\ (!(0 <= K:330)
               \/ __cost':323 <= (mid___cost:328 + -K:330
                                    + (param0:53 * K:330)))
         /\ (!(0 <= K:330)
               \/ (__cost':323 + -x':322) <= (mid___cost:328 + -mid_x:327))
         /\ (!(0 <= K:330) \/ -x':322 <= (-mid_x:327 + -K:330))
         /\ ((K:330 = 0 /\ mid_tmp:329 = tmp':324 /\ mid_x:327 = x':322
                /\ mid___cost:328 = __cost':323)
               \/ (1 <= K:330 /\ 0 <= (-1 + -mid_x:327 + param0:53)
                     /\ 0 <= mid___cost:328 /\ 0 <= mid_x:327
                     /\ 0 <= (-x':322 + param0:53) /\ 0 <= __cost':323
                     /\ 0 <= (-1 + x':322)))
         /\ (0 = K:330 \/ -mid___cost:328 <= 0) /\ (K:326 + K:330) = K:325
         /\ 0 <= K:325 /\ 0 <= x':322 /\ param0:53 <= x':322)}

    (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
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
<__pstate, (Unique State Name,64)_g1> -> <__pstate, (Unique State Name,60)_g1>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0xa734cd0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0xa4c1030: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
##### ANS
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}
    ( __pstate , (Unique State Name,64)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}
    ( __pstate , (Unique State Name,60)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:475
 param0@width := type_err:476}

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

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

Base relation: 
{__cost := __cost':438
 n := havoc:13
 return := 0
 param0 := havoc:13
 return@pos := type_err:452
 param0@pos := type_err:448
 return@width := type_err:453
 param0@width := type_err:450
 when ((!(0 <= K:431) \/ (-mid___cost:432 + mid_x:433) <= K:431)
         /\ (!(0 <= K:431) \/ mid___cost:432 <= (-K:431 + (havoc:13 * K:431)))
         /\ (!(0 <= K:431) \/ -mid___cost:432 <= -K:431)
         /\ (!(0 <= K:431) \/ (mid___cost:432 + -mid_x:433) <= 0)
         /\ ((K:431 = 0 /\ tmp:434 = mid_tmp:435 /\ 0 = mid_x:433
                /\ 0 = mid___cost:432)
               \/ (1 <= K:431 /\ 0 <= (-2 + havoc:13)
                     /\ 0 <= (-mid_x:433 + havoc:13) /\ 0 <= (-2 + havoc:13)
                     /\ 0 <= (-1 + mid___cost:432) /\ 0 <= (-1 + mid_x:433)))
         /\ (0 = K:431 \/ (2 + -havoc:13) <= 0)
         /\ (!((0 <= K:436 /\ K:436 <= 0)) \/ x':437 = mid_x:433)
         /\ (!(1 <= K:436) \/ x':437 = havoc:13)
         /\ (!(0 <= K:436) \/ __cost':438 = mid___cost:432)
         /\ (!(0 <= K:436) \/ tmp':439 = mid_tmp:435)
         /\ ((K:436 = 0 /\ mid_tmp:435 = tmp':439 /\ mid_x:433 = x':437
                /\ mid___cost:432 = __cost':438)
               \/ (1 <= K:436 /\ (-1 + -mid_x:433 + havoc:13) = 0
                     /\ 0 <= mid_x:433 /\ (-havoc:13 + x':437) = 0
                     /\ 0 <= (-1 + havoc:13)))
         /\ (0 = K:436 \/ !((2 + mid_x:433 + -havoc:13) <= 0))
         /\ (K:431 + K:436) = K:440
         /\ (!((0 <= K:441 /\ K:441 <= 0)) \/ mid_x:442 = 0)
         /\ (!(1 <= K:441) \/ mid_x:442 = havoc:13)
         /\ (!(0 <= K:441) \/ mid___cost:443 = 0)
         /\ (!(0 <= K:441) \/ mid_tmp:444 = tmp:434) /\ K:441 = 0
         /\ tmp:434 = mid_tmp:444 /\ 0 = mid_x:442 /\ 0 = mid___cost:443
         /\ 0 = K:441
         /\ (!(0 <= K:445)
               \/ (-__cost':438 + x':437) <= ((-mid___cost:443 + mid_x:442)
                                                + K:445))
         /\ (!(0 <= K:445)
               \/ __cost':438 <= (mid___cost:443 + -K:445
                                    + (havoc:13 * K:445)))
         /\ (!(0 <= K:445)
               \/ (__cost':438 + -x':437) <= (mid___cost:443 + -mid_x:442))
         /\ (!(0 <= K:445) \/ -x':437 <= (-mid_x:442 + -K:445))
         /\ ((K:445 = 0 /\ mid_tmp:444 = tmp':439 /\ mid_x:442 = x':437
                /\ mid___cost:443 = __cost':438)
               \/ (1 <= K:445 /\ 0 <= (-1 + -mid_x:442 + havoc:13)
                     /\ 0 <= mid___cost:443 /\ 0 <= mid_x:442
                     /\ 0 <= (-x':437 + havoc:13) /\ 0 <= __cost':438
                     /\ 0 <= (-1 + x':437)))
         /\ (0 = K:445 \/ -mid___cost:443 <= 0) /\ (K:441 + K:445) = K:440
         /\ 0 <= K:440 /\ 0 <= x':437 /\ havoc:13 <= x':437
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:451)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:451)))}

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

Base relation: 
{__cost := __cost':461
 return := havoc:472
 param0 := param0:53
 return@pos := type_err:473
 param0@pos := type_err:54
 return@width := type_err:474
 param0@width := type_err:55
 when ((!(0 <= K:454)
          \/ (-mid___cost:455 + mid_x:456) <= (-__cost:64 + K:454))
         /\ (!(0 <= K:454)
               \/ mid___cost:455 <= (__cost:64 + -K:454 + (param0:53 * K:454)))
         /\ (!(0 <= K:454) \/ -mid___cost:455 <= (-__cost:64 + -K:454))
         /\ (!(0 <= K:454) \/ (mid___cost:455 + -mid_x:456) <= __cost:64)
         /\ ((K:454 = 0 /\ tmp:457 = mid_tmp:458 /\ 0 = mid_x:456
                /\ __cost:64 = mid___cost:455)
               \/ (1 <= K:454 /\ 0 <= (-2 + param0:53) /\ 0 <= __cost:64
                     /\ 0 <= (-mid_x:456 + param0:53)
                     /\ 0 <= (-2 + param0:53) /\ 0 <= (-1 + mid___cost:455)
                     /\ 0 <= (-1 + mid_x:456)))
         /\ (0 = K:454 \/ (2 + -param0:53) <= 0)
         /\ (!((0 <= K:459 /\ K:459 <= 0)) \/ x':460 = mid_x:456)
         /\ (!(1 <= K:459) \/ x':460 = param0:53)
         /\ (!(0 <= K:459) \/ __cost':461 = mid___cost:455)
         /\ (!(0 <= K:459) \/ tmp':462 = mid_tmp:458)
         /\ ((K:459 = 0 /\ mid_tmp:458 = tmp':462 /\ mid_x:456 = x':460
                /\ mid___cost:455 = __cost':461)
               \/ (1 <= K:459 /\ (-1 + -mid_x:456 + param0:53) = 0
                     /\ 0 <= mid_x:456 /\ (-param0:53 + x':460) = 0
                     /\ 0 <= (-1 + param0:53)))
         /\ (0 = K:459 \/ !((2 + mid_x:456 + -param0:53) <= 0))
         /\ (K:454 + K:459) = K:463
         /\ (!((0 <= K:464 /\ K:464 <= 0)) \/ mid_x:465 = 0)
         /\ (!(1 <= K:464) \/ mid_x:465 = param0:53)
         /\ (!(0 <= K:464) \/ mid___cost:466 = __cost:64)
         /\ (!(0 <= K:464) \/ mid_tmp:467 = tmp:457)
         /\ ((K:464 = 0 /\ tmp:457 = mid_tmp:467 /\ 0 = mid_x:465
                /\ __cost:64 = mid___cost:466)
               \/ (1 <= K:464 /\ (-1 + param0:53) = 0
                     /\ 0 <= (-1 + -__cost:64)
                     /\ (-param0:53 + mid_x:465) = 0
                     /\ 0 <= (-1 + -mid___cost:466) /\ 0 <= (-1 + param0:53)))
         /\ (0 = K:464 \/ !(-__cost:64 <= 0))
         /\ (!(0 <= K:468)
               \/ (-__cost':461 + x':460) <= ((-mid___cost:466 + mid_x:465)
                                                + K:468))
         /\ (!(0 <= K:468)
               \/ __cost':461 <= (mid___cost:466 + -K:468
                                    + (param0:53 * K:468)))
         /\ (!(0 <= K:468)
               \/ (__cost':461 + -x':460) <= (mid___cost:466 + -mid_x:465))
         /\ (!(0 <= K:468) \/ -x':460 <= (-mid_x:465 + -K:468))
         /\ ((K:468 = 0 /\ mid_tmp:467 = tmp':462 /\ mid_x:465 = x':460
                /\ mid___cost:466 = __cost':461)
               \/ (1 <= K:468 /\ 0 <= (-1 + -mid_x:465 + param0:53)
                     /\ 0 <= mid___cost:466 /\ 0 <= mid_x:465
                     /\ 0 <= (-x':460 + param0:53) /\ 0 <= __cost':461
                     /\ 0 <= (-1 + x':460)))
         /\ (0 = K:468 \/ -mid___cost:466 <= 0) /\ (K:464 + K:468) = K:463
         /\ 0 <= K:463 /\ 0 <= x':460 /\ param0:53 <= x':460)}

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

Base relation: 
{__cost := __cost':323
 x := x':322
 tmp := tmp':324
 n := param0:53
 return := havoc:362
 return@pos := type_err:363
 return@width := type_err:364
 when ((!(0 <= K:317)
          \/ (-mid___cost:318 + mid_x:319) <= (-__cost:64 + K:317))
         /\ (!(0 <= K:317)
               \/ mid___cost:318 <= (__cost:64 + -K:317 + (param0:53 * K:317)))
         /\ (!(0 <= K:317) \/ -mid___cost:318 <= (-__cost:64 + -K:317))
         /\ (!(0 <= K:317) \/ (mid___cost:318 + -mid_x:319) <= __cost:64)
         /\ ((K:317 = 0 /\ tmp:66 = mid_tmp:320 /\ 0 = mid_x:319
                /\ __cost:64 = mid___cost:318)
               \/ (1 <= K:317 /\ 0 <= (-2 + param0:53) /\ 0 <= __cost:64
                     /\ 0 <= (-mid_x:319 + param0:53)
                     /\ 0 <= (-2 + param0:53) /\ 0 <= (-1 + mid___cost:318)
                     /\ 0 <= (-1 + mid_x:319)))
         /\ (0 = K:317 \/ (2 + -param0:53) <= 0)
         /\ (!((0 <= K:321 /\ K:321 <= 0)) \/ x':322 = mid_x:319)
         /\ (!(1 <= K:321) \/ x':322 = param0:53)
         /\ (!(0 <= K:321) \/ __cost':323 = mid___cost:318)
         /\ (!(0 <= K:321) \/ tmp':324 = mid_tmp:320)
         /\ ((K:321 = 0 /\ mid_tmp:320 = tmp':324 /\ mid_x:319 = x':322
                /\ mid___cost:318 = __cost':323)
               \/ (1 <= K:321 /\ (-1 + -mid_x:319 + param0:53) = 0
                     /\ 0 <= mid_x:319 /\ (-param0:53 + x':322) = 0
                     /\ 0 <= (-1 + param0:53)))
         /\ (0 = K:321 \/ !((2 + mid_x:319 + -param0:53) <= 0))
         /\ (K:317 + K:321) = K:325
         /\ (!((0 <= K:326 /\ K:326 <= 0)) \/ mid_x:327 = 0)
         /\ (!(1 <= K:326) \/ mid_x:327 = param0:53)
         /\ (!(0 <= K:326) \/ mid___cost:328 = __cost:64)
         /\ (!(0 <= K:326) \/ mid_tmp:329 = tmp:66)
         /\ ((K:326 = 0 /\ tmp:66 = mid_tmp:329 /\ 0 = mid_x:327
                /\ __cost:64 = mid___cost:328)
               \/ (1 <= K:326 /\ (-1 + param0:53) = 0
                     /\ 0 <= (-1 + -__cost:64)
                     /\ (-param0:53 + mid_x:327) = 0
                     /\ 0 <= (-1 + -mid___cost:328) /\ 0 <= (-1 + param0:53)))
         /\ (0 = K:326 \/ !(-__cost:64 <= 0))
         /\ (!(0 <= K:330)
               \/ (-__cost':323 + x':322) <= ((-mid___cost:328 + mid_x:327)
                                                + K:330))
         /\ (!(0 <= K:330)
               \/ __cost':323 <= (mid___cost:328 + -K:330
                                    + (param0:53 * K:330)))
         /\ (!(0 <= K:330)
               \/ (__cost':323 + -x':322) <= (mid___cost:328 + -mid_x:327))
         /\ (!(0 <= K:330) \/ -x':322 <= (-mid_x:327 + -K:330))
         /\ ((K:330 = 0 /\ mid_tmp:329 = tmp':324 /\ mid_x:327 = x':322
                /\ mid___cost:328 = __cost':323)
               \/ (1 <= K:330 /\ 0 <= (-1 + -mid_x:327 + param0:53)
                     /\ 0 <= mid___cost:328 /\ 0 <= mid_x:327
                     /\ 0 <= (-x':322 + param0:53) /\ 0 <= __cost':323
                     /\ 0 <= (-1 + x':322)))
         /\ (0 = K:330 \/ -mid___cost:328 <= 0) /\ (K:326 + K:330) = K:325
         /\ 0 <= K:325 /\ 0 <= x':322 /\ param0:53 <= x':322)}

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

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

Variable bounds at line 23 in run

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

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