/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, 26> -> <Unique State Name, 31>	Base relation: 
{j := (i:62 + 1)
 when i:62 < n:63}	
<Unique State Name, 26> -> <Unique State Name, 69>	Base relation: 
{return := havoc:77
 return@pos := type_err:78
 return@width := type_err:79
 when n:63 <= i:62}	
<Unique State Name, 70> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 63> -> <Unique State Name, 17>	Base relation: 
{}	
<Unique State Name, 68> -> <Unique State Name, 65 67>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 72> -> <Unique State Name, 35>	Base relation: 
{}	
<Unique State Name, 15> -> <Unique State Name, 68>	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
<Unique State Name, 35> -> <Unique State Name, 22>	Base relation: 
{i := (i:62 + 1)
 when n:63 <= j:64}	
<Unique State Name, 35> -> <Unique State Name, 31>	Base relation: 
{__cost := phi___cost:80
 j := (phi_j:81 + 1)
 n := phi_n:82
 when (j:64 < n:63
         /\ ((!(havoc:73 = 0) /\ 0 <= __cost:66 /\ 0 <= (__cost:66 + 1)
                /\ (__cost:66 + 1) = phi___cost:80 /\ (j:64 + -1) = phi_j:81
                /\ (n:63 + -1) = phi_n:82)
               \/ (havoc:73 = 0 /\ __cost:66 = phi___cost:80
                     /\ j:64 = phi_j:81 /\ n:63 = phi_n:82)))}	
<Unique State Name, 73> -> <Unique State Name, 26>	Base relation: 
{}	
<Unique State Name, 17> -> <Unique State Name, 70>	Base relation: 
{return := havoc:41
 return@pos := type_err:44
 return@width := type_err:45}	
<Unique State Name, 69> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 67> -> <Unique State Name, 71>	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, 22> -> <Unique State Name, 73>	Base relation: 
{when 0 <= i:62}	
<Unique State Name, 31> -> <Unique State Name, 72>	Base relation: 
{when (1 <= n:63 /\ 1 <= j:64)}	
<Unique State Name, 65> -> <Unique State Name, 64>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
<Unique State Name, 61> -> <Unique State Name, 22>	Base relation: 
{i := 0
 n := param0:53}	
<Unique State Name, 71> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 64> -> <Unique State Name, 61 63>	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 := phi___cost:374
 j := (phi_j:375 + 1)
 n := phi_n:376
 when (1 <= n:63 /\ 1 <= j:64 /\ j:64 < n:63
         /\ ((!(havoc:373 = 0) /\ 0 <= __cost:66 /\ 0 <= (__cost:66 + 1)
                /\ (__cost:66 + 1) = phi___cost:374
                /\ (j:64 + -1) = phi_j:375 /\ (n:63 + -1) = phi_n:376)
               \/ (havoc:373 = 0 /\ __cost:66 = phi___cost:374
                     /\ j:64 = phi_j:375 /\ n:63 = phi_n:376)))}
**** alpha hat: 
  {<Split [!(-__cost:66 <= 0)
            (__cost':377) = (1)*(__cost:66) + 0
           (n':379) = (1)*(n:63) + 0
           (j':378) = (1)*(j:64) + 1
           }
          pre:
            [|-__cost:66-1>=0; j:64-1>=0; n:63-j:64-1>=0|]
          post:
            [|-__cost':377-1>=0; j':378-2>=0; n':379-j':378>=0|]
           ((-n':379 + j':378)) = (1)*((-n:63 + j:64)) + 1
          ((n':379 + __cost':377)) = (1)*((n:63 + __cost:66)) + 0
          (n':379) <= (1)*(n:63) + 0
          (-n':379) <= (1)*(-n:63) + 1
          }
  pre:
    [|__cost:66>=0; j:64-1>=0; n:63-j:64-1>=0|]
  post:
    [|__cost':377>=0; j':378-1>=0; j':378+__cost':377-2>=0; n':379-j':378>=0|]],
[!((-1 + -__cost:66) <= 0)
  (n':379) = (1)*(n:63) + 0
 (__cost':377) = (1)*(__cost:66) + 0
 (j':378) = (1)*(j:64) + 1
 } pre:   [|-__cost:66-2>=0; j:64-1>=0; n:63-j:64-1>=0|] post:
  [|-__cost':377-2>=0; j':378-2>=0; n':379-j':378>=0|]
 ((-n':379 + j':378)) = (1)*((-n:63 + j:64)) + 1
((n':379 + __cost':377)) = (1)*((n:63 + __cost:66)) + 0
(n':379) <= (1)*(n:63) + 0 (-n':379) <= (1)*(-n:63) + 1
(-n':379) <= (1)*(-n:63) + (-n:63 + j:64) + (n:63 + __cost:66) } pre:
  [|__cost:66+1>=0; j:64-1>=0; n:63-j:64-1>=0|] post:
  [|__cost':377+1>=0; j':378-1>=0; 2j':378+__cost':377-3>=0; n':379-j':378>=0|]]>}
**** star transition: 
  {__cost := __cost':377
   j := j':378
   n := n':379
   when ((!(0 <= K:403) \/ mid___cost:407 = __cost:66)
           /\ (!(0 <= K:403) \/ mid_n:405 = n:63)
           /\ (!(0 <= K:403) \/ mid_j:406 = (j:64 + K:403))
           /\ ((K:403 = 0 /\ n:63 = mid_n:405 /\ j:64 = mid_j:406
                  /\ __cost:66 = mid___cost:407)
                 \/ (1 <= K:403 /\ 0 <= (-1 + -__cost:66) /\ 0 <= (-1 + j:64)
                       /\ 0 <= (-1 + n:63 + -j:64)
                       /\ 0 <= (-1 + -mid___cost:407)
                       /\ 0 <= (-2 + mid_j:406)
                       /\ 0 <= (mid_n:405 + -mid_j:406)))
           /\ (0 = K:403 \/ !(-__cost:66 <= 0))
           /\ (!(0 <= K:404)
                 \/ (-n':379 + j':378) = ((-mid_n:405 + mid_j:406) + K:404))
           /\ (!(0 <= K:404)
                 \/ (n':379 + __cost':377) = (mid_n:405 + mid___cost:407))
           /\ (!(0 <= K:404) \/ n':379 <= mid_n:405)
           /\ (!(0 <= K:404) \/ -n':379 <= (-mid_n:405 + K:404))
           /\ ((K:404 = 0 /\ mid_n:405 = n':379 /\ mid_j:406 = j':378
                  /\ mid___cost:407 = __cost':377)
                 \/ (1 <= K:404 /\ 0 <= mid___cost:407
                       /\ 0 <= (-1 + mid_j:406)
                       /\ 0 <= (-1 + mid_n:405 + -mid_j:406)
                       /\ 0 <= __cost':377 /\ 0 <= (-1 + j':378)
                       /\ 0 <= (-2 + j':378 + __cost':377)
                       /\ 0 <= (n':379 + -j':378)))
           /\ (0 = K:404 \/ -mid___cost:407 <= 0) /\ (K:403 + K:404) = K:402
           /\ (!(0 <= K:408) \/ mid_n:410 = n:63)
           /\ (!(0 <= K:408) \/ mid___cost:412 = __cost:66)
           /\ (!(0 <= K:408) \/ mid_j:411 = (j:64 + K:408))
           /\ ((K:408 = 0 /\ n:63 = mid_n:410 /\ j:64 = mid_j:411
                  /\ __cost:66 = mid___cost:412)
                 \/ (1 <= K:408 /\ 0 <= (-2 + -__cost:66) /\ 0 <= (-1 + j:64)
                       /\ 0 <= (-1 + n:63 + -j:64)
                       /\ 0 <= (-2 + -mid___cost:412)
                       /\ 0 <= (-2 + mid_j:411)
                       /\ 0 <= (mid_n:410 + -mid_j:411)))
           /\ (0 = K:408 \/ !((-1 + -__cost:66) <= 0))
           /\ (!(0 <= K:409)
                 \/ (-n':379 + j':378) = ((-mid_n:410 + mid_j:411) + K:409))
           /\ (!(0 <= K:409)
                 \/ (n':379 + __cost':377) = (mid_n:410 + mid___cost:412))
           /\ (!(0 <= K:409) \/ n':379 <= mid_n:410)
           /\ (!(0 <= K:409) \/ -n':379 <= (-mid_n:410 + K:409))
           /\ (!(0 <= K:409)
                 \/ -n':379 <= (-mid_n:410 + (-1/2 * K:409)
                                  + ((-mid_n:410 + mid_j:411) * K:409)
                                  + ((mid_n:410 + mid___cost:412) * K:409)
                                  + (1/2 * (K:409 * K:409))))
           /\ ((K:409 = 0 /\ mid_n:410 = n':379 /\ mid_j:411 = j':378
                  /\ mid___cost:412 = __cost':377)
                 \/ (1 <= K:409 /\ 0 <= (1 + mid___cost:412)
                       /\ 0 <= (-1 + mid_j:411)
                       /\ 0 <= (-1 + mid_n:410 + -mid_j:411)
                       /\ 0 <= (1 + __cost':377) /\ 0 <= (-1 + j':378)
                       /\ 0 <= (-3 + (2 * j':378) + __cost':377)
                       /\ 0 <= (n':379 + -j':378)))
           /\ (0 = K:409 \/ (-1 + -mid___cost:412) <= 0)
           /\ (K:408 + K:409) = K:402 /\ 0 <= K:402)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':434
 i := (i:62 + 1)
 j := j':433
 n := n':432
 when (0 <= i:62 /\ i:62 < n:63
         /\ (!(0 <= K:427) \/ mid___cost:428 = __cost:66)
         /\ (!(0 <= K:427) \/ mid_n:429 = n:63)
         /\ (!(0 <= K:427) \/ mid_j:430 = ((i:62 + 1) + K:427))
         /\ ((K:427 = 0 /\ n:63 = mid_n:429 /\ (i:62 + 1) = mid_j:430
                /\ __cost:66 = mid___cost:428)
               \/ (1 <= K:427 /\ 0 <= (-1 + -__cost:66)
                     /\ 0 <= (-1 + (i:62 + 1))
                     /\ 0 <= (-1 + n:63 + -((i:62 + 1)))
                     /\ 0 <= (-1 + -mid___cost:428) /\ 0 <= (-2 + mid_j:430)
                     /\ 0 <= (mid_n:429 + -mid_j:430)))
         /\ (0 = K:427 \/ !(-__cost:66 <= 0))
         /\ (!(0 <= K:431)
               \/ (-n':432 + j':433) = ((-mid_n:429 + mid_j:430) + K:431))
         /\ (!(0 <= K:431)
               \/ (n':432 + __cost':434) = (mid_n:429 + mid___cost:428))
         /\ (!(0 <= K:431) \/ n':432 <= mid_n:429)
         /\ (!(0 <= K:431) \/ -n':432 <= (-mid_n:429 + K:431))
         /\ ((K:431 = 0 /\ mid_n:429 = n':432 /\ mid_j:430 = j':433
                /\ mid___cost:428 = __cost':434)
               \/ (1 <= K:431 /\ 0 <= mid___cost:428 /\ 0 <= (-1 + mid_j:430)
                     /\ 0 <= (-1 + mid_n:429 + -mid_j:430)
                     /\ 0 <= __cost':434 /\ 0 <= (-1 + j':433)
                     /\ 0 <= (-2 + j':433 + __cost':434)
                     /\ 0 <= (n':432 + -j':433)))
         /\ (0 = K:431 \/ -mid___cost:428 <= 0) /\ (K:427 + K:431) = K:435
         /\ (!(0 <= K:436) \/ mid_n:437 = n:63)
         /\ (!(0 <= K:436) \/ mid___cost:438 = __cost:66)
         /\ (!(0 <= K:436) \/ mid_j:439 = ((i:62 + 1) + K:436))
         /\ ((K:436 = 0 /\ n:63 = mid_n:437 /\ (i:62 + 1) = mid_j:439
                /\ __cost:66 = mid___cost:438)
               \/ (1 <= K:436 /\ 0 <= (-2 + -__cost:66)
                     /\ 0 <= (-1 + (i:62 + 1))
                     /\ 0 <= (-1 + n:63 + -((i:62 + 1)))
                     /\ 0 <= (-2 + -mid___cost:438) /\ 0 <= (-2 + mid_j:439)
                     /\ 0 <= (mid_n:437 + -mid_j:439)))
         /\ (0 = K:436 \/ !((-1 + -__cost:66) <= 0))
         /\ (!(0 <= K:440)
               \/ (-n':432 + j':433) = ((-mid_n:437 + mid_j:439) + K:440))
         /\ (!(0 <= K:440)
               \/ (n':432 + __cost':434) = (mid_n:437 + mid___cost:438))
         /\ (!(0 <= K:440) \/ n':432 <= mid_n:437)
         /\ (!(0 <= K:440) \/ -n':432 <= (-mid_n:437 + K:440))
         /\ (!(0 <= K:440)
               \/ -n':432 <= (-mid_n:437 + (-1/2 * K:440)
                                + ((-mid_n:437 + mid_j:439) * K:440)
                                + ((mid_n:437 + mid___cost:438) * K:440)
                                + (1/2 * (K:440 * K:440))))
         /\ ((K:440 = 0 /\ mid_n:437 = n':432 /\ mid_j:439 = j':433
                /\ mid___cost:438 = __cost':434)
               \/ (1 <= K:440 /\ 0 <= (1 + mid___cost:438)
                     /\ 0 <= (-1 + mid_j:439)
                     /\ 0 <= (-1 + mid_n:437 + -mid_j:439)
                     /\ 0 <= (1 + __cost':434) /\ 0 <= (-1 + j':433)
                     /\ 0 <= (-3 + (2 * j':433) + __cost':434)
                     /\ 0 <= (n':432 + -j':433)))
         /\ (0 = K:440 \/ (-1 + -mid___cost:438) <= 0)
         /\ (K:436 + K:440) = K:435 /\ 0 <= K:435 /\ 1 <= n':432
         /\ 1 <= j':433 /\ n':432 <= j':433)}
**** alpha hat: 
  {<Split [!(-__cost:66 <= 0)
            (__cost':377) = (1)*(__cost:66) + 0
           (j':378) = (1)*(n:63) + 0
           (i':441) = (1)*(i:62) + 1
           (n':379) = (1)*(n:63) + 0
           (-j':378) <= (1)*(-j:64) + (-1)*1 + j:64 + (-1)*i:62
           }
          pre:
            [|-i:62+n:63-1>=0; -__cost:66-1>=0;
              i:62-n:63+((-1 + -i:62 + n:63) * (-1 + -i:62 + n:63))+1>=0;
              i:62-n:63+((-1 + -i:62 + n:63) * (1 + i:62))+1>=0; i:62>=0|]
          post:
            [|-j':378+n':379=0; -i':441+j':378>=0; -__cost':377-1>=0;
              i':441-j':378+((-i':441 + j':378) * (-i':441 + j':378))>=0;
              i':441-j':378+((-i':441 + j':378) * i':441)>=0; i':441-1>=0|]
           ((-n':379 + j':378)) = 0
          (i':441) = (1)*(i:62) + 1
          ((n':379 + __cost':377)) = (1)*((n:63 + __cost:66)) + 0
          (n':379) <= (1)*(n:63) + 0
          (-n':379) <= (1)*(-n:63) + (-1)*1 + (-1)*i:62 + (n:63 + __cost:66)
          }
  pre:
    [|-i:62+n:63-1>=0; ((-1 + -i:62 + n:63) * __cost:66)>=0; __cost:66>=0;
      i:62-n:63+((-1 + -i:62 + n:63) * (-1 + -i:62 + n:63))+1>=0;
      i:62-n:63+((-1 + -i:62 + n:63) * (1 + i:62))+1>=0; i:62>=0|]
  post:
    [|-n':379+j':378=0; -i':441+n':379>=0; __cost':377>=0; i':441-1>=0|]],
[!((-1 + -__cost:66) <= 0)
  (i':441) = (1)*(i:62) + 1
 (__cost':377) = (1)*(__cost:66) + 0
 ((-n':379 + j':378)) = 0
 (n':379) = (1)*(n:63) + 0
 } pre:   [|-i:62+n:63-1>=0; -__cost:66-2>=0; i:62>=0|] post:
  [|-n':379+j':378=0; -__cost':377-2>=0; i':441-1>=0; n':379-i':441>=0|]
 ((-n':379 + j':378)) = 0 (i':441) = (1)*(i:62) + 1
((n':379 + __cost':377)) = (1)*((n:63 + __cost:66)) + 0
(n':379) <= (1)*(n:63) + 0
(-n':379) <= (1)*(-n:63) + (-1)*i:62 + (n:63 + __cost:66) } pre:
  [|-i:62+n:63-1>=0; -i:62+n:63+((-1 + -i:62 + n:63) * __cost:66)-1>=0;
    __cost:66+1>=0; i:62-n:63+((-1 + -i:62 + n:63) * (1 + i:62))+1>=0;
    i:62-n:63+((-1 + -i:62 + n:63) * (-1 + -i:62 + n:63))+1>=0; i:62>=0|]
post:
  [|-n':379+j':378=0; -i':441+n':379>=0; __cost':377+1>=0; i':441-1>=0|]],
[(2 + i:62 + -n:63) <= 0
  ((-n':379 + j':378)) = 0
 (i':441) = (1)*(i:62) + 1
 ((n':379 + __cost':377)) = (1)*((n:63 + __cost:66)) + 0
 (n':379) <= (1)*(n:63) + 0
 } pre:
  [|-i:62+n:63-2>=0; -n:63+((-1 + -i:62 + n:63) * (1 + i:62))+1>=0;
    i:62-n:63+((-1 + -i:62 + n:63) * (-1 + -i:62 + n:63))+1>=0; i:62>=0|]
post:   [|-n':379+j':378=0; -i':441+n':379>=0; i':441-1>=0|]
 (j':378) = (1)*(i:62) + 1 (n':379) = (1)*(i:62) + 1
(__cost':377) = (1)*(__cost:66) + 0 (i':441) = (1)*(i:62) + 1
(-j':378) <= (1)*(-j:64) + (-1)*1 + j:64 } pre:   [|-i:62+n:63-1=0; i:62>=0|]
post:   [|-j':378+n':379=0; -j':378+i':441=0; j':378-1>=0|]],
[!((1 + __cost:66) <= 0)
  (i':441) = (1)*(i:62) + 1
 ((n':379 + __cost':377)) = (1)*((n:63 + __cost:66)) + 0
 ((-n':379 + j':378)) = 0
 (n':379) <= (1)*(n:63) + 0
 (-n':379) <= (1)*(-n:63) + (-1)*1 + (-1)*i:62 + (n:63 + __cost:66)
 } pre:
  [|-i:62+n:63-1>=0; ((-1 + -i:62 + n:63) * __cost:66)>=0; __cost:66>=0;
    i:62-n:63+((-1 + -i:62 + n:63) * (-1 + -i:62 + n:63))+1>=0;
    i:62-n:63+((-1 + -i:62 + n:63) * (1 + i:62))+1>=0; i:62>=0|] post:
  [|-n':379+j':378=0; __cost':377>=0; i':441-1>=0; n':379-i':441>=0|]
 (__cost':377) = (1)*(__cost:66) + 0 (n':379) = (1)*(n:63) + 0
(i':441) = (1)*(i:62) + 1 (j':378) = (1)*(n:63) + 0 } pre:
  [|-i:62+n:63-1>=0; -__cost:66-1>=0;
    i:62-n:63+((-1 + -i:62 + n:63) * (-1 + -i:62 + n:63))+1>=0;
    i:62-n:63+((-1 + -i:62 + n:63) * (1 + i:62))+1>=0; i:62>=0|] post:
  [|-n':379+j':378=0; -i':441+n':379>=0; -__cost':377-1>=0;
    i':441-n':379+((-i':441 + n':379) * (-i':441 + n':379))>=0;
    i':441-n':379+((-i':441 + n':379) * i':441)>=0; i':441-1>=0|]],
[!((2 + __cost:66) <= 0)
  ((n':379 + __cost':377)) = (1)*((n:63 + __cost:66)) + 0
 ((-n':379 + j':378)) = 0
 (i':441) = (1)*(i:62) + 1
 (n':379) <= (1)*(n:63) + 0
 (-n':379) <= (1)*(-n:63) + (n:63 + __cost:66) + (-1)*i:62
 } pre:
  [|-i:62+n:63-1>=0; -i:62+n:63+((-1 + -i:62 + n:63) * __cost:66)-1>=0;
    __cost:66+1>=0; i:62-n:63+((-1 + -i:62 + n:63) * (1 + i:62))+1>=0;
    i:62-n:63+((-1 + -i:62 + n:63) * (-1 + -i:62 + n:63))+1>=0; i:62>=0|]
post:
  [|-n':379+j':378=0; -i':441+n':379>=0; __cost':377+1>=0; i':441-1>=0|]
 (i':441) = (1)*(i:62) + 1 (__cost':377) = (1)*(__cost:66) + 0
((-n':379 + j':378)) = 0 (n':379) = (1)*(n:63) + 0 } pre:
  [|-i:62+n:63-1>=0; -__cost:66-2>=0; i:62>=0|] post:
  [|-n':379+j':378=0; -__cost':377-2>=0; i':441-1>=0; n':379-i':441>=0|]]>}
**** star transition: 
  {__cost := __cost':377
   i := i':441
   j := j':378
   n := n':379
   when ((!(0 <= K:548) \/ mid___cost:553 = __cost:66)
           /\ (!((0 <= K:548 /\ K:548 <= 0)) \/ mid_j:551 = j:64)
           /\ (!(1 <= K:548) \/ mid_j:551 = (j:64 + n:63 + -j:64))
           /\ (!(0 <= K:548) \/ mid_i:552 = (i:62 + K:548))
           /\ (!(0 <= K:548) \/ mid_n:550 = n:63)
           /\ (!((0 <= K:548 /\ K:548 <= 0))
                 \/ -mid_j:551 <= (-j:64 + (-1/2 * K:548) + -((i:62 * K:548))
                                     + (n:63 * K:548)
                                     + (-1/2 * (K:548 * K:548))))
           /\ (!(1 <= K:548)
                 \/ -mid_j:551 <= (j:64 + -j:64 + -n:63 + (-1/2 * K:548)
                                     + -((i:62 * K:548)) + (n:63 * K:548)
                                     + (-1/2 * (K:548 * K:548))))
           /\ ((K:548 = 0 /\ n:63 = mid_n:550 /\ j:64 = mid_j:551
                  /\ i:62 = mid_i:552 /\ __cost:66 = mid___cost:553)
                 \/ (1 <= K:548 /\ 0 <= (-1 + -i:62 + n:63)
                       /\ 0 <= (-1 + -__cost:66)
                       /\ 0 <= (1 + i:62 + -n:63
                                  + ((-1 + -i:62 + n:63)
                                       * (-1 + -i:62 + n:63)))
                       /\ 0 <= (1 + i:62 + -n:63
                                  + ((-1 + -i:62 + n:63) * (1 + i:62)))
                       /\ 0 <= i:62 /\ (-mid_j:551 + mid_n:550) = 0
                       /\ 0 <= (-mid_i:552 + mid_j:551)
                       /\ 0 <= (-1 + -mid___cost:553)
                       /\ 0 <= (mid_i:552 + -mid_j:551
                                  + ((-mid_i:552 + mid_j:551)
                                       * (-mid_i:552 + mid_j:551)))
                       /\ 0 <= (mid_i:552 + -mid_j:551
                                  + ((-mid_i:552 + mid_j:551) * mid_i:552))
                       /\ 0 <= (-1 + mid_i:552)))
           /\ (0 = K:548 \/ !(-__cost:66 <= 0))
           /\ (!((0 <= K:549 /\ K:549 <= 0))
                 \/ (-n':379 + j':378) = (-mid_n:550 + mid_j:551))
           /\ (!(1 <= K:549) \/ (-n':379 + j':378) = 0)
           /\ (!(0 <= K:549) \/ i':441 = (mid_i:552 + K:549))
           /\ (!(0 <= K:549)
                 \/ (n':379 + __cost':377) = (mid_n:550 + mid___cost:553))
           /\ (!(0 <= K:549) \/ n':379 <= mid_n:550)
           /\ (!(0 <= K:549)
                 \/ -n':379 <= (-mid_n:550 + (-1/2 * K:549)
                                  + -((mid_i:552 * K:549))
                                  + ((mid_n:550 + mid___cost:553) * K:549)
                                  + (-1/2 * (K:549 * K:549))))
           /\ ((K:549 = 0 /\ mid_n:550 = n':379 /\ mid_j:551 = j':378
                  /\ mid_i:552 = i':441 /\ mid___cost:553 = __cost':377)
                 \/ (1 <= K:549 /\ 0 <= (-1 + -mid_i:552 + mid_n:550)
                       /\ 0 <= ((-1 + -mid_i:552 + mid_n:550)
                                  * mid___cost:553) /\ 0 <= mid___cost:553
                       /\ 0 <= (1 + mid_i:552 + -mid_n:550
                                  + ((-1 + -mid_i:552 + mid_n:550)
                                       * (-1 + -mid_i:552 + mid_n:550)))
                       /\ 0 <= (1 + mid_i:552 + -mid_n:550
                                  + ((-1 + -mid_i:552 + mid_n:550)
                                       * (1 + mid_i:552))) /\ 0 <= mid_i:552
                       /\ (-n':379 + j':378) = 0 /\ 0 <= (-i':441 + n':379)
                       /\ 0 <= __cost':377 /\ 0 <= (-1 + i':441)))
           /\ (0 = K:549 \/ -mid___cost:553 <= 0) /\ (K:548 + K:549) = K:547
           /\ (!(0 <= K:554) \/ mid_i:558 = (i:62 + K:554))
           /\ (!(0 <= K:554) \/ mid___cost:559 = __cost:66)
           /\ (!((0 <= K:554 /\ K:554 <= 0))
                 \/ (-mid_n:556 + mid_j:557) = (-n:63 + j:64))
           /\ (!(1 <= K:554) \/ (-mid_n:556 + mid_j:557) = 0)
           /\ (!(0 <= K:554) \/ mid_n:556 = n:63)
           /\ ((K:554 = 0 /\ n:63 = mid_n:556 /\ j:64 = mid_j:557
                  /\ i:62 = mid_i:558 /\ __cost:66 = mid___cost:559)
                 \/ (1 <= K:554 /\ 0 <= (-1 + -i:62 + n:63)
                       /\ 0 <= (-2 + -__cost:66) /\ 0 <= i:62
                       /\ (-mid_n:556 + mid_j:557) = 0
                       /\ 0 <= (-2 + -mid___cost:559)
                       /\ 0 <= (-1 + mid_i:558)
                       /\ 0 <= (mid_n:556 + -mid_i:558)))
           /\ (0 = K:554 \/ !((-1 + -__cost:66) <= 0))
           /\ (!((0 <= K:555 /\ K:555 <= 0))
                 \/ (-n':379 + j':378) = (-mid_n:556 + mid_j:557))
           /\ (!(1 <= K:555) \/ (-n':379 + j':378) = 0)
           /\ (!(0 <= K:555) \/ i':441 = (mid_i:558 + K:555))
           /\ (!(0 <= K:555)
                 \/ (n':379 + __cost':377) = (mid_n:556 + mid___cost:559))
           /\ (!(0 <= K:555) \/ n':379 <= mid_n:556)
           /\ (!(0 <= K:555)
                 \/ -n':379 <= (-mid_n:556 + (1/2 * K:555)
                                  + -((mid_i:558 * K:555))
                                  + ((mid_n:556 + mid___cost:559) * K:555)
                                  + (-1/2 * (K:555 * K:555))))
           /\ ((K:555 = 0 /\ mid_n:556 = n':379 /\ mid_j:557 = j':378
                  /\ mid_i:558 = i':441 /\ mid___cost:559 = __cost':377)
                 \/ (1 <= K:555 /\ 0 <= (-1 + -mid_i:558 + mid_n:556)
                       /\ 0 <= (-1 + -mid_i:558 + mid_n:556
                                  + ((-1 + -mid_i:558 + mid_n:556)
                                       * mid___cost:559))
                       /\ 0 <= (1 + mid___cost:559)
                       /\ 0 <= (1 + mid_i:558 + -mid_n:556
                                  + ((-1 + -mid_i:558 + mid_n:556)
                                       * (1 + mid_i:558)))
                       /\ 0 <= (1 + mid_i:558 + -mid_n:556
                                  + ((-1 + -mid_i:558 + mid_n:556)
                                       * (-1 + -mid_i:558 + mid_n:556)))
                       /\ 0 <= mid_i:558 /\ (-n':379 + j':378) = 0
                       /\ 0 <= (-i':441 + n':379) /\ 0 <= (1 + __cost':377)
                       /\ 0 <= (-1 + i':441)))
           /\ (0 = K:555 \/ (-1 + -mid___cost:559) <= 0)
           /\ (K:554 + K:555) = K:547
           /\ (!((0 <= K:560 /\ K:560 <= 0))
                 \/ (-mid_n:562 + mid_j:563) = (-n:63 + j:64))
           /\ (!(1 <= K:560) \/ (-mid_n:562 + mid_j:563) = 0)
           /\ (!(0 <= K:560) \/ mid_i:564 = (i:62 + K:560))
           /\ (!(0 <= K:560)
                 \/ (mid_n:562 + mid___cost:565) = (n:63 + __cost:66))
           /\ (!(0 <= K:560) \/ mid_n:562 <= n:63)
           /\ ((K:560 = 0 /\ n:63 = mid_n:562 /\ j:64 = mid_j:563
                  /\ i:62 = mid_i:564 /\ __cost:66 = mid___cost:565)
                 \/ (1 <= K:560 /\ 0 <= (-2 + -i:62 + n:63)
                       /\ 0 <= (1 + -n:63
                                  + ((-1 + -i:62 + n:63) * (1 + i:62)))
                       /\ 0 <= (1 + i:62 + -n:63
                                  + ((-1 + -i:62 + n:63)
                                       * (-1 + -i:62 + n:63))) /\ 0 <= i:62
                       /\ (-mid_n:562 + mid_j:563) = 0
                       /\ 0 <= (-mid_i:564 + mid_n:562)
                       /\ 0 <= (-1 + mid_i:564)))
           /\ (0 = K:560 \/ (2 + i:62 + -n:63) <= 0)
           /\ (!((0 <= K:561 /\ K:561 <= 0)) \/ j':378 = (mid_j:563 + K:561))
           /\ (!(1 <= K:561)
                 \/ j':378 = (mid_j:563 + mid_i:564 + -mid_j:563 + K:561))
           /\ (!((0 <= K:561 /\ K:561 <= 0)) \/ n':379 = (mid_n:562 + K:561))
           /\ (!(1 <= K:561)
                 \/ n':379 = (mid_n:562 + mid_i:564 + -mid_n:562 + K:561))
           /\ (!(0 <= K:561) \/ __cost':377 = mid___cost:565)
           /\ (!(0 <= K:561) \/ i':441 = (mid_i:564 + K:561))
           /\ (!((0 <= K:561 /\ K:561 <= 0))
                 \/ -j':378 <= (-mid_j:563 + (-3/2 * K:561)
                                  + (mid_i:564 * K:561)
                                  + (1/2 * (K:561 * K:561))))
           /\ (!(1 <= K:561)
                 \/ -j':378 <= (mid_j:563 + -mid_j:563 + -mid_i:564
                                  + (-3/2 * K:561) + (mid_i:564 * K:561)
                                  + (1/2 * (K:561 * K:561))))
           /\ ((K:561 = 0 /\ mid_n:562 = n':379 /\ mid_j:563 = j':378
                  /\ mid_i:564 = i':441 /\ mid___cost:565 = __cost':377)
                 \/ (1 <= K:561 /\ (-1 + -mid_i:564 + mid_n:562) = 0
                       /\ 0 <= mid_i:564 /\ (-j':378 + n':379) = 0
                       /\ (-j':378 + i':441) = 0 /\ 0 <= (-1 + j':378)))
           /\ (0 = K:561 \/ !((2 + mid_i:564 + -mid_n:562) <= 0))
           /\ (K:560 + K:561) = K:547
           /\ (!(0 <= K:566) \/ mid_i:570 = (i:62 + K:566))
           /\ (!(0 <= K:566)
                 \/ (mid_n:568 + mid___cost:571) = (n:63 + __cost:66))
           /\ (!((0 <= K:566 /\ K:566 <= 0))
                 \/ (-mid_n:568 + mid_j:569) = (-n:63 + j:64))
           /\ (!(1 <= K:566) \/ (-mid_n:568 + mid_j:569) = 0)
           /\ (!(0 <= K:566) \/ mid_n:568 <= n:63)
           /\ (!(0 <= K:566)
                 \/ -mid_n:568 <= (-n:63 + (-1/2 * K:566) + -((i:62 * K:566))
                                     + ((n:63 + __cost:66) * K:566)
                                     + (-1/2 * (K:566 * K:566))))
           /\ ((K:566 = 0 /\ n:63 = mid_n:568 /\ j:64 = mid_j:569
                  /\ i:62 = mid_i:570 /\ __cost:66 = mid___cost:571)
                 \/ (1 <= K:566 /\ 0 <= (-1 + -i:62 + n:63)
                       /\ 0 <= ((-1 + -i:62 + n:63) * __cost:66)
                       /\ 0 <= __cost:66
                       /\ 0 <= (1 + i:62 + -n:63
                                  + ((-1 + -i:62 + n:63)
                                       * (-1 + -i:62 + n:63)))
                       /\ 0 <= (1 + i:62 + -n:63
                                  + ((-1 + -i:62 + n:63) * (1 + i:62)))
                       /\ 0 <= i:62 /\ (-mid_n:568 + mid_j:569) = 0
                       /\ 0 <= mid___cost:571 /\ 0 <= (-1 + mid_i:570)
                       /\ 0 <= (mid_n:568 + -mid_i:570)))
           /\ (0 = K:566 \/ !((1 + __cost:66) <= 0))
           /\ (!(0 <= K:567) \/ __cost':377 = mid___cost:571)
           /\ (!(0 <= K:567) \/ n':379 = mid_n:568)
           /\ (!(0 <= K:567) \/ i':441 = (mid_i:570 + K:567))
           /\ (!((0 <= K:567 /\ K:567 <= 0)) \/ j':378 = mid_j:569)
           /\ (!(1 <= K:567) \/ j':378 = mid_n:568)
           /\ ((K:567 = 0 /\ mid_n:568 = n':379 /\ mid_j:569 = j':378
                  /\ mid_i:570 = i':441 /\ mid___cost:571 = __cost':377)
                 \/ (1 <= K:567 /\ 0 <= (-1 + -mid_i:570 + mid_n:568)
                       /\ 0 <= (-1 + -mid___cost:571)
                       /\ 0 <= (1 + mid_i:570 + -mid_n:568
                                  + ((-1 + -mid_i:570 + mid_n:568)
                                       * (-1 + -mid_i:570 + mid_n:568)))
                       /\ 0 <= (1 + mid_i:570 + -mid_n:568
                                  + ((-1 + -mid_i:570 + mid_n:568)
                                       * (1 + mid_i:570))) /\ 0 <= mid_i:570
                       /\ (-n':379 + j':378) = 0 /\ 0 <= (-i':441 + n':379)
                       /\ 0 <= (-1 + -__cost':377)
                       /\ 0 <= (i':441 + -n':379
                                  + ((-i':441 + n':379) * (-i':441 + n':379)))
                       /\ 0 <= (i':441 + -n':379
                                  + ((-i':441 + n':379) * i':441))
                       /\ 0 <= (-1 + i':441)))
           /\ (0 = K:567 \/ (1 + mid___cost:571) <= 0)
           /\ (K:566 + K:567) = K:547
           /\ (!(0 <= K:572)
                 \/ (mid_n:574 + mid___cost:577) = (n:63 + __cost:66))
           /\ (!((0 <= K:572 /\ K:572 <= 0))
                 \/ (-mid_n:574 + mid_j:575) = (-n:63 + j:64))
           /\ (!(1 <= K:572) \/ (-mid_n:574 + mid_j:575) = 0)
           /\ (!(0 <= K:572) \/ mid_i:576 = (i:62 + K:572))
           /\ (!(0 <= K:572) \/ mid_n:574 <= n:63)
           /\ (!(0 <= K:572)
                 \/ -mid_n:574 <= (-n:63 + (1/2 * K:572)
                                     + ((n:63 + __cost:66) * K:572)
                                     + -((i:62 * K:572))
                                     + (-1/2 * (K:572 * K:572))))
           /\ ((K:572 = 0 /\ n:63 = mid_n:574 /\ j:64 = mid_j:575
                  /\ i:62 = mid_i:576 /\ __cost:66 = mid___cost:577)
                 \/ (1 <= K:572 /\ 0 <= (-1 + -i:62 + n:63)
                       /\ 0 <= (-1 + -i:62 + n:63
                                  + ((-1 + -i:62 + n:63) * __cost:66))
                       /\ 0 <= (1 + __cost:66)
                       /\ 0 <= (1 + i:62 + -n:63
                                  + ((-1 + -i:62 + n:63) * (1 + i:62)))
                       /\ 0 <= (1 + i:62 + -n:63
                                  + ((-1 + -i:62 + n:63)
                                       * (-1 + -i:62 + n:63))) /\ 0 <= i:62
                       /\ (-mid_n:574 + mid_j:575) = 0
                       /\ 0 <= (-mid_i:576 + mid_n:574)
                       /\ 0 <= (1 + mid___cost:577) /\ 0 <= (-1 + mid_i:576)))
           /\ (0 = K:572 \/ !((2 + __cost:66) <= 0))
           /\ (!(0 <= K:573) \/ i':441 = (mid_i:576 + K:573))
           /\ (!(0 <= K:573) \/ __cost':377 = mid___cost:577)
           /\ (!((0 <= K:573 /\ K:573 <= 0))
                 \/ (-n':379 + j':378) = (-mid_n:574 + mid_j:575))
           /\ (!(1 <= K:573) \/ (-n':379 + j':378) = 0)
           /\ (!(0 <= K:573) \/ n':379 = mid_n:574)
           /\ ((K:573 = 0 /\ mid_n:574 = n':379 /\ mid_j:575 = j':378
                  /\ mid_i:576 = i':441 /\ mid___cost:577 = __cost':377)
                 \/ (1 <= K:573 /\ 0 <= (-1 + -mid_i:576 + mid_n:574)
                       /\ 0 <= (-2 + -mid___cost:577) /\ 0 <= mid_i:576
                       /\ (-n':379 + j':378) = 0 /\ 0 <= (-2 + -__cost':377)
                       /\ 0 <= (-1 + i':441) /\ 0 <= (n':379 + -i':441)))
           /\ (0 = K:573 \/ (2 + mid___cost:577) <= 0)
           /\ (K:572 + K:573) = K:547 /\ 0 <= K:547)}
}
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':587
   i := i':586
   j := j':585
   n := n':584
   return := havoc:641
   return@pos := type_err:642
   return@width := type_err:643
   when ((!(0 <= K:578) \/ mid___cost:579 = __cost:66)
           /\ (!((0 <= K:578 /\ K:578 <= 0)) \/ mid_j:580 = j:64)
           /\ (!(1 <= K:578) \/ mid_j:580 = (j:64 + param0:53 + -j:64))
           /\ (!(0 <= K:578) \/ mid_i:581 = K:578)
           /\ (!(0 <= K:578) \/ mid_n:582 = param0:53)
           /\ (!((0 <= K:578 /\ K:578 <= 0))
                 \/ -mid_j:580 <= (-j:64 + (-1/2 * K:578)
                                     + (param0:53 * K:578)
                                     + (-1/2 * (K:578 * K:578))))
           /\ (!(1 <= K:578)
                 \/ -mid_j:580 <= (j:64 + -j:64 + -param0:53 + (-1/2 * K:578)
                                     + (param0:53 * K:578)
                                     + (-1/2 * (K:578 * K:578))))
           /\ ((K:578 = 0 /\ param0:53 = mid_n:582 /\ j:64 = mid_j:580
                  /\ 0 = mid_i:581 /\ __cost:66 = mid___cost:579)
                 \/ (1 <= K:578 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= (-1 + -__cost:66)
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ (-mid_j:580 + mid_n:582) = 0
                       /\ 0 <= (-mid_i:581 + mid_j:580)
                       /\ 0 <= (-1 + -mid___cost:579)
                       /\ 0 <= (mid_i:581 + -mid_j:580
                                  + ((-mid_i:581 + mid_j:580)
                                       * (-mid_i:581 + mid_j:580)))
                       /\ 0 <= (mid_i:581 + -mid_j:580
                                  + ((-mid_i:581 + mid_j:580) * mid_i:581))
                       /\ 0 <= (-1 + mid_i:581)))
           /\ (0 = K:578 \/ !(-__cost:66 <= 0))
           /\ (!((0 <= K:583 /\ K:583 <= 0))
                 \/ (-n':584 + j':585) = (-mid_n:582 + mid_j:580))
           /\ (!(1 <= K:583) \/ (-n':584 + j':585) = 0)
           /\ (!(0 <= K:583) \/ i':586 = (mid_i:581 + K:583))
           /\ (!(0 <= K:583)
                 \/ (n':584 + __cost':587) = (mid_n:582 + mid___cost:579))
           /\ (!(0 <= K:583) \/ n':584 <= mid_n:582)
           /\ (!(0 <= K:583)
                 \/ -n':584 <= (-mid_n:582 + (-1/2 * K:583)
                                  + -((mid_i:581 * K:583))
                                  + ((mid_n:582 + mid___cost:579) * K:583)
                                  + (-1/2 * (K:583 * K:583))))
           /\ ((K:583 = 0 /\ mid_n:582 = n':584 /\ mid_j:580 = j':585
                  /\ mid_i:581 = i':586 /\ mid___cost:579 = __cost':587)
                 \/ (1 <= K:583 /\ 0 <= (-1 + -mid_i:581 + mid_n:582)
                       /\ 0 <= ((-1 + -mid_i:581 + mid_n:582)
                                  * mid___cost:579) /\ 0 <= mid___cost:579
                       /\ 0 <= (1 + mid_i:581 + -mid_n:582
                                  + ((-1 + -mid_i:581 + mid_n:582)
                                       * (-1 + -mid_i:581 + mid_n:582)))
                       /\ 0 <= (1 + mid_i:581 + -mid_n:582
                                  + ((-1 + -mid_i:581 + mid_n:582)
                                       * (1 + mid_i:581))) /\ 0 <= mid_i:581
                       /\ (-n':584 + j':585) = 0 /\ 0 <= (-i':586 + n':584)
                       /\ 0 <= __cost':587 /\ 0 <= (-1 + i':586)))
           /\ (0 = K:583 \/ -mid___cost:579 <= 0) /\ (K:578 + K:583) = K:588
           /\ (!(0 <= K:589) \/ mid_i:590 = K:589)
           /\ (!(0 <= K:589) \/ mid___cost:591 = __cost:66)
           /\ (!((0 <= K:589 /\ K:589 <= 0))
                 \/ (-mid_n:592 + mid_j:593) = (-param0:53 + j:64))
           /\ (!(1 <= K:589) \/ (-mid_n:592 + mid_j:593) = 0)
           /\ (!(0 <= K:589) \/ mid_n:592 = param0:53)
           /\ ((K:589 = 0 /\ param0:53 = mid_n:592 /\ j:64 = mid_j:593
                  /\ 0 = mid_i:590 /\ __cost:66 = mid___cost:591)
                 \/ (1 <= K:589 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= (-2 + -__cost:66)
                       /\ (-mid_n:592 + mid_j:593) = 0
                       /\ 0 <= (-2 + -mid___cost:591)
                       /\ 0 <= (-1 + mid_i:590)
                       /\ 0 <= (mid_n:592 + -mid_i:590)))
           /\ (0 = K:589 \/ !((-1 + -__cost:66) <= 0))
           /\ (!((0 <= K:594 /\ K:594 <= 0))
                 \/ (-n':584 + j':585) = (-mid_n:592 + mid_j:593))
           /\ (!(1 <= K:594) \/ (-n':584 + j':585) = 0)
           /\ (!(0 <= K:594) \/ i':586 = (mid_i:590 + K:594))
           /\ (!(0 <= K:594)
                 \/ (n':584 + __cost':587) = (mid_n:592 + mid___cost:591))
           /\ (!(0 <= K:594) \/ n':584 <= mid_n:592)
           /\ (!(0 <= K:594)
                 \/ -n':584 <= (-mid_n:592 + (1/2 * K:594)
                                  + -((mid_i:590 * K:594))
                                  + ((mid_n:592 + mid___cost:591) * K:594)
                                  + (-1/2 * (K:594 * K:594))))
           /\ ((K:594 = 0 /\ mid_n:592 = n':584 /\ mid_j:593 = j':585
                  /\ mid_i:590 = i':586 /\ mid___cost:591 = __cost':587)
                 \/ (1 <= K:594 /\ 0 <= (-1 + -mid_i:590 + mid_n:592)
                       /\ 0 <= (-1 + -mid_i:590 + mid_n:592
                                  + ((-1 + -mid_i:590 + mid_n:592)
                                       * mid___cost:591))
                       /\ 0 <= (1 + mid___cost:591)
                       /\ 0 <= (1 + mid_i:590 + -mid_n:592
                                  + ((-1 + -mid_i:590 + mid_n:592)
                                       * (1 + mid_i:590)))
                       /\ 0 <= (1 + mid_i:590 + -mid_n:592
                                  + ((-1 + -mid_i:590 + mid_n:592)
                                       * (-1 + -mid_i:590 + mid_n:592)))
                       /\ 0 <= mid_i:590 /\ (-n':584 + j':585) = 0
                       /\ 0 <= (-i':586 + n':584) /\ 0 <= (1 + __cost':587)
                       /\ 0 <= (-1 + i':586)))
           /\ (0 = K:594 \/ (-1 + -mid___cost:591) <= 0)
           /\ (K:589 + K:594) = K:588
           /\ (!((0 <= K:595 /\ K:595 <= 0))
                 \/ (-mid_n:596 + mid_j:597) = (-param0:53 + j:64))
           /\ (!(1 <= K:595) \/ (-mid_n:596 + mid_j:597) = 0)
           /\ (!(0 <= K:595) \/ mid_i:598 = K:595)
           /\ (!(0 <= K:595)
                 \/ (mid_n:596 + mid___cost:599) = (param0:53 + __cost:66))
           /\ (!(0 <= K:595) \/ mid_n:596 <= param0:53)
           /\ ((K:595 = 0 /\ param0:53 = mid_n:596 /\ j:64 = mid_j:597
                  /\ 0 = mid_i:598 /\ __cost:66 = mid___cost:599)
                 \/ (1 <= K:595 /\ 0 <= (-2 + param0:53)
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ (-mid_n:596 + mid_j:597) = 0
                       /\ 0 <= (-mid_i:598 + mid_n:596)
                       /\ 0 <= (-1 + mid_i:598)))
           /\ (0 = K:595 \/ (2 + -param0:53) <= 0)
           /\ (!((0 <= K:600 /\ K:600 <= 0)) \/ j':585 = (mid_j:597 + K:600))
           /\ (!(1 <= K:600)
                 \/ j':585 = (mid_j:597 + mid_i:598 + -mid_j:597 + K:600))
           /\ (!((0 <= K:600 /\ K:600 <= 0)) \/ n':584 = (mid_n:596 + K:600))
           /\ (!(1 <= K:600)
                 \/ n':584 = (mid_n:596 + mid_i:598 + -mid_n:596 + K:600))
           /\ (!(0 <= K:600) \/ __cost':587 = mid___cost:599)
           /\ (!(0 <= K:600) \/ i':586 = (mid_i:598 + K:600))
           /\ (!((0 <= K:600 /\ K:600 <= 0))
                 \/ -j':585 <= (-mid_j:597 + (-3/2 * K:600)
                                  + (mid_i:598 * K:600)
                                  + (1/2 * (K:600 * K:600))))
           /\ (!(1 <= K:600)
                 \/ -j':585 <= (mid_j:597 + -mid_j:597 + -mid_i:598
                                  + (-3/2 * K:600) + (mid_i:598 * K:600)
                                  + (1/2 * (K:600 * K:600))))
           /\ ((K:600 = 0 /\ mid_n:596 = n':584 /\ mid_j:597 = j':585
                  /\ mid_i:598 = i':586 /\ mid___cost:599 = __cost':587)
                 \/ (1 <= K:600 /\ (-1 + -mid_i:598 + mid_n:596) = 0
                       /\ 0 <= mid_i:598 /\ (-j':585 + n':584) = 0
                       /\ (-j':585 + i':586) = 0 /\ 0 <= (-1 + j':585)))
           /\ (0 = K:600 \/ !((2 + mid_i:598 + -mid_n:596) <= 0))
           /\ (K:595 + K:600) = K:588 /\ (!(0 <= K:601) \/ mid_i:602 = K:601)
           /\ (!(0 <= K:601)
                 \/ (mid_n:603 + mid___cost:604) = (param0:53 + __cost:66))
           /\ (!((0 <= K:601 /\ K:601 <= 0))
                 \/ (-mid_n:603 + mid_j:605) = (-param0:53 + j:64))
           /\ (!(1 <= K:601) \/ (-mid_n:603 + mid_j:605) = 0)
           /\ (!(0 <= K:601) \/ mid_n:603 <= param0:53)
           /\ (!(0 <= K:601)
                 \/ -mid_n:603 <= (-param0:53 + (-1/2 * K:601)
                                     + ((param0:53 + __cost:66) * K:601)
                                     + (-1/2 * (K:601 * K:601))))
           /\ ((K:601 = 0 /\ param0:53 = mid_n:603 /\ j:64 = mid_j:605
                  /\ 0 = mid_i:602 /\ __cost:66 = mid___cost:604)
                 \/ (1 <= K:601 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= ((-1 + param0:53) * __cost:66)
                       /\ 0 <= __cost:66
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ (-mid_n:603 + mid_j:605) = 0 /\ 0 <= mid___cost:604
                       /\ 0 <= (-1 + mid_i:602)
                       /\ 0 <= (mid_n:603 + -mid_i:602)))
           /\ (0 = K:601 \/ !((1 + __cost:66) <= 0))
           /\ (!(0 <= K:606) \/ __cost':587 = mid___cost:604)
           /\ (!(0 <= K:606) \/ n':584 = mid_n:603)
           /\ (!(0 <= K:606) \/ i':586 = (mid_i:602 + K:606))
           /\ (!((0 <= K:606 /\ K:606 <= 0)) \/ j':585 = mid_j:605)
           /\ (!(1 <= K:606) \/ j':585 = mid_n:603)
           /\ ((K:606 = 0 /\ mid_n:603 = n':584 /\ mid_j:605 = j':585
                  /\ mid_i:602 = i':586 /\ mid___cost:604 = __cost':587)
                 \/ (1 <= K:606 /\ 0 <= (-1 + -mid_i:602 + mid_n:603)
                       /\ 0 <= (-1 + -mid___cost:604)
                       /\ 0 <= (1 + mid_i:602 + -mid_n:603
                                  + ((-1 + -mid_i:602 + mid_n:603)
                                       * (-1 + -mid_i:602 + mid_n:603)))
                       /\ 0 <= (1 + mid_i:602 + -mid_n:603
                                  + ((-1 + -mid_i:602 + mid_n:603)
                                       * (1 + mid_i:602))) /\ 0 <= mid_i:602
                       /\ (-n':584 + j':585) = 0 /\ 0 <= (-i':586 + n':584)
                       /\ 0 <= (-1 + -__cost':587)
                       /\ 0 <= (i':586 + -n':584
                                  + ((-i':586 + n':584) * (-i':586 + n':584)))
                       /\ 0 <= (i':586 + -n':584
                                  + ((-i':586 + n':584) * i':586))
                       /\ 0 <= (-1 + i':586)))
           /\ (0 = K:606 \/ (1 + mid___cost:604) <= 0)
           /\ (K:601 + K:606) = K:588
           /\ (!(0 <= K:607)
                 \/ (mid_n:608 + mid___cost:609) = (param0:53 + __cost:66))
           /\ (!((0 <= K:607 /\ K:607 <= 0))
                 \/ (-mid_n:608 + mid_j:610) = (-param0:53 + j:64))
           /\ (!(1 <= K:607) \/ (-mid_n:608 + mid_j:610) = 0)
           /\ (!(0 <= K:607) \/ mid_i:611 = K:607)
           /\ (!(0 <= K:607) \/ mid_n:608 <= param0:53)
           /\ (!(0 <= K:607)
                 \/ -mid_n:608 <= (-param0:53 + (1/2 * K:607)
                                     + ((param0:53 + __cost:66) * K:607)
                                     + (-1/2 * (K:607 * K:607))))
           /\ ((K:607 = 0 /\ param0:53 = mid_n:608 /\ j:64 = mid_j:610
                  /\ 0 = mid_i:611 /\ __cost:66 = mid___cost:609)
                 \/ (1 <= K:607 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= (-1 + param0:53
                                  + ((-1 + param0:53) * __cost:66))
                       /\ 0 <= (1 + __cost:66)
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ (-mid_n:608 + mid_j:610) = 0
                       /\ 0 <= (-mid_i:611 + mid_n:608)
                       /\ 0 <= (1 + mid___cost:609) /\ 0 <= (-1 + mid_i:611)))
           /\ (0 = K:607 \/ !((2 + __cost:66) <= 0))
           /\ (!(0 <= K:612) \/ i':586 = (mid_i:611 + K:612))
           /\ (!(0 <= K:612) \/ __cost':587 = mid___cost:609)
           /\ (!((0 <= K:612 /\ K:612 <= 0))
                 \/ (-n':584 + j':585) = (-mid_n:608 + mid_j:610))
           /\ (!(1 <= K:612) \/ (-n':584 + j':585) = 0)
           /\ (!(0 <= K:612) \/ n':584 = mid_n:608)
           /\ ((K:612 = 0 /\ mid_n:608 = n':584 /\ mid_j:610 = j':585
                  /\ mid_i:611 = i':586 /\ mid___cost:609 = __cost':587)
                 \/ (1 <= K:612 /\ 0 <= (-1 + -mid_i:611 + mid_n:608)
                       /\ 0 <= (-2 + -mid___cost:609) /\ 0 <= mid_i:611
                       /\ (-n':584 + j':585) = 0 /\ 0 <= (-2 + -__cost':587)
                       /\ 0 <= (-1 + i':586) /\ 0 <= (n':584 + -i':586)))
           /\ (0 = K:612 \/ (2 + mid___cost:609) <= 0)
           /\ (K:607 + K:612) = K:588 /\ 0 <= K:588 /\ 0 <= i':586
           /\ n':584 <= i':586)})



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':587
   return := havoc:641
   return@pos := type_err:642
   return@width := type_err:643
   when ((!(0 <= K:578) \/ mid___cost:579 = __cost:66)
           /\ (!((0 <= K:578 /\ K:578 <= 0)) \/ mid_j:580 = j:644)
           /\ (!(1 <= K:578) \/ mid_j:580 = (j:644 + param0:53 + -j:644))
           /\ (!(0 <= K:578) \/ mid_i:581 = K:578)
           /\ (!(0 <= K:578) \/ mid_n:582 = param0:53)
           /\ (!((0 <= K:578 /\ K:578 <= 0))
                 \/ -mid_j:580 <= (-j:644 + (-1/2 * K:578)
                                     + (param0:53 * K:578)
                                     + (-1/2 * (K:578 * K:578))))
           /\ (!(1 <= K:578)
                 \/ -mid_j:580 <= (j:644 + -j:644 + -param0:53
                                     + (-1/2 * K:578) + (param0:53 * K:578)
                                     + (-1/2 * (K:578 * K:578))))
           /\ ((K:578 = 0 /\ param0:53 = mid_n:582 /\ j:644 = mid_j:580
                  /\ 0 = mid_i:581 /\ __cost:66 = mid___cost:579)
                 \/ (1 <= K:578 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= (-1 + -__cost:66)
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ (-mid_j:580 + mid_n:582) = 0
                       /\ 0 <= (-mid_i:581 + mid_j:580)
                       /\ 0 <= (-1 + -mid___cost:579)
                       /\ 0 <= (mid_i:581 + -mid_j:580
                                  + ((-mid_i:581 + mid_j:580)
                                       * (-mid_i:581 + mid_j:580)))
                       /\ 0 <= (mid_i:581 + -mid_j:580
                                  + ((-mid_i:581 + mid_j:580) * mid_i:581))
                       /\ 0 <= (-1 + mid_i:581)))
           /\ (0 = K:578 \/ !(-__cost:66 <= 0))
           /\ (!((0 <= K:583 /\ K:583 <= 0))
                 \/ (-n':584 + j':585) = (-mid_n:582 + mid_j:580))
           /\ (!(1 <= K:583) \/ (-n':584 + j':585) = 0)
           /\ (!(0 <= K:583) \/ i':586 = (mid_i:581 + K:583))
           /\ (!(0 <= K:583)
                 \/ (n':584 + __cost':587) = (mid_n:582 + mid___cost:579))
           /\ (!(0 <= K:583) \/ n':584 <= mid_n:582)
           /\ (!(0 <= K:583)
                 \/ -n':584 <= (-mid_n:582 + (-1/2 * K:583)
                                  + -((mid_i:581 * K:583))
                                  + ((mid_n:582 + mid___cost:579) * K:583)
                                  + (-1/2 * (K:583 * K:583))))
           /\ ((K:583 = 0 /\ mid_n:582 = n':584 /\ mid_j:580 = j':585
                  /\ mid_i:581 = i':586 /\ mid___cost:579 = __cost':587)
                 \/ (1 <= K:583 /\ 0 <= (-1 + -mid_i:581 + mid_n:582)
                       /\ 0 <= ((-1 + -mid_i:581 + mid_n:582)
                                  * mid___cost:579) /\ 0 <= mid___cost:579
                       /\ 0 <= (1 + mid_i:581 + -mid_n:582
                                  + ((-1 + -mid_i:581 + mid_n:582)
                                       * (-1 + -mid_i:581 + mid_n:582)))
                       /\ 0 <= (1 + mid_i:581 + -mid_n:582
                                  + ((-1 + -mid_i:581 + mid_n:582)
                                       * (1 + mid_i:581))) /\ 0 <= mid_i:581
                       /\ (-n':584 + j':585) = 0 /\ 0 <= (-i':586 + n':584)
                       /\ 0 <= __cost':587 /\ 0 <= (-1 + i':586)))
           /\ (0 = K:583 \/ -mid___cost:579 <= 0) /\ (K:578 + K:583) = K:588
           /\ (!(0 <= K:589) \/ mid_i:590 = K:589)
           /\ (!(0 <= K:589) \/ mid___cost:591 = __cost:66)
           /\ (!((0 <= K:589 /\ K:589 <= 0))
                 \/ (-mid_n:592 + mid_j:593) = (-param0:53 + j:644))
           /\ (!(1 <= K:589) \/ (-mid_n:592 + mid_j:593) = 0)
           /\ (!(0 <= K:589) \/ mid_n:592 = param0:53)
           /\ ((K:589 = 0 /\ param0:53 = mid_n:592 /\ j:644 = mid_j:593
                  /\ 0 = mid_i:590 /\ __cost:66 = mid___cost:591)
                 \/ (1 <= K:589 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= (-2 + -__cost:66)
                       /\ (-mid_n:592 + mid_j:593) = 0
                       /\ 0 <= (-2 + -mid___cost:591)
                       /\ 0 <= (-1 + mid_i:590)
                       /\ 0 <= (mid_n:592 + -mid_i:590)))
           /\ (0 = K:589 \/ !((-1 + -__cost:66) <= 0))
           /\ (!((0 <= K:594 /\ K:594 <= 0))
                 \/ (-n':584 + j':585) = (-mid_n:592 + mid_j:593))
           /\ (!(1 <= K:594) \/ (-n':584 + j':585) = 0)
           /\ (!(0 <= K:594) \/ i':586 = (mid_i:590 + K:594))
           /\ (!(0 <= K:594)
                 \/ (n':584 + __cost':587) = (mid_n:592 + mid___cost:591))
           /\ (!(0 <= K:594) \/ n':584 <= mid_n:592)
           /\ (!(0 <= K:594)
                 \/ -n':584 <= (-mid_n:592 + (1/2 * K:594)
                                  + -((mid_i:590 * K:594))
                                  + ((mid_n:592 + mid___cost:591) * K:594)
                                  + (-1/2 * (K:594 * K:594))))
           /\ ((K:594 = 0 /\ mid_n:592 = n':584 /\ mid_j:593 = j':585
                  /\ mid_i:590 = i':586 /\ mid___cost:591 = __cost':587)
                 \/ (1 <= K:594 /\ 0 <= (-1 + -mid_i:590 + mid_n:592)
                       /\ 0 <= (-1 + -mid_i:590 + mid_n:592
                                  + ((-1 + -mid_i:590 + mid_n:592)
                                       * mid___cost:591))
                       /\ 0 <= (1 + mid___cost:591)
                       /\ 0 <= (1 + mid_i:590 + -mid_n:592
                                  + ((-1 + -mid_i:590 + mid_n:592)
                                       * (1 + mid_i:590)))
                       /\ 0 <= (1 + mid_i:590 + -mid_n:592
                                  + ((-1 + -mid_i:590 + mid_n:592)
                                       * (-1 + -mid_i:590 + mid_n:592)))
                       /\ 0 <= mid_i:590 /\ (-n':584 + j':585) = 0
                       /\ 0 <= (-i':586 + n':584) /\ 0 <= (1 + __cost':587)
                       /\ 0 <= (-1 + i':586)))
           /\ (0 = K:594 \/ (-1 + -mid___cost:591) <= 0)
           /\ (K:589 + K:594) = K:588
           /\ (!((0 <= K:595 /\ K:595 <= 0))
                 \/ (-mid_n:596 + mid_j:597) = (-param0:53 + j:644))
           /\ (!(1 <= K:595) \/ (-mid_n:596 + mid_j:597) = 0)
           /\ (!(0 <= K:595) \/ mid_i:598 = K:595)
           /\ (!(0 <= K:595)
                 \/ (mid_n:596 + mid___cost:599) = (param0:53 + __cost:66))
           /\ (!(0 <= K:595) \/ mid_n:596 <= param0:53)
           /\ ((K:595 = 0 /\ param0:53 = mid_n:596 /\ j:644 = mid_j:597
                  /\ 0 = mid_i:598 /\ __cost:66 = mid___cost:599)
                 \/ (1 <= K:595 /\ 0 <= (-2 + param0:53)
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ (-mid_n:596 + mid_j:597) = 0
                       /\ 0 <= (-mid_i:598 + mid_n:596)
                       /\ 0 <= (-1 + mid_i:598)))
           /\ (0 = K:595 \/ (2 + -param0:53) <= 0)
           /\ (!((0 <= K:600 /\ K:600 <= 0)) \/ j':585 = (mid_j:597 + K:600))
           /\ (!(1 <= K:600)
                 \/ j':585 = (mid_j:597 + mid_i:598 + -mid_j:597 + K:600))
           /\ (!((0 <= K:600 /\ K:600 <= 0)) \/ n':584 = (mid_n:596 + K:600))
           /\ (!(1 <= K:600)
                 \/ n':584 = (mid_n:596 + mid_i:598 + -mid_n:596 + K:600))
           /\ (!(0 <= K:600) \/ __cost':587 = mid___cost:599)
           /\ (!(0 <= K:600) \/ i':586 = (mid_i:598 + K:600))
           /\ (!((0 <= K:600 /\ K:600 <= 0))
                 \/ -j':585 <= (-mid_j:597 + (-3/2 * K:600)
                                  + (mid_i:598 * K:600)
                                  + (1/2 * (K:600 * K:600))))
           /\ (!(1 <= K:600)
                 \/ -j':585 <= (mid_j:597 + -mid_j:597 + -mid_i:598
                                  + (-3/2 * K:600) + (mid_i:598 * K:600)
                                  + (1/2 * (K:600 * K:600))))
           /\ ((K:600 = 0 /\ mid_n:596 = n':584 /\ mid_j:597 = j':585
                  /\ mid_i:598 = i':586 /\ mid___cost:599 = __cost':587)
                 \/ (1 <= K:600 /\ (-1 + -mid_i:598 + mid_n:596) = 0
                       /\ 0 <= mid_i:598 /\ (-j':585 + n':584) = 0
                       /\ (-j':585 + i':586) = 0 /\ 0 <= (-1 + j':585)))
           /\ (0 = K:600 \/ !((2 + mid_i:598 + -mid_n:596) <= 0))
           /\ (K:595 + K:600) = K:588 /\ (!(0 <= K:601) \/ mid_i:602 = K:601)
           /\ (!(0 <= K:601)
                 \/ (mid_n:603 + mid___cost:604) = (param0:53 + __cost:66))
           /\ (!((0 <= K:601 /\ K:601 <= 0))
                 \/ (-mid_n:603 + mid_j:605) = (-param0:53 + j:644))
           /\ (!(1 <= K:601) \/ (-mid_n:603 + mid_j:605) = 0)
           /\ (!(0 <= K:601) \/ mid_n:603 <= param0:53)
           /\ (!(0 <= K:601)
                 \/ -mid_n:603 <= (-param0:53 + (-1/2 * K:601)
                                     + ((param0:53 + __cost:66) * K:601)
                                     + (-1/2 * (K:601 * K:601))))
           /\ ((K:601 = 0 /\ param0:53 = mid_n:603 /\ j:644 = mid_j:605
                  /\ 0 = mid_i:602 /\ __cost:66 = mid___cost:604)
                 \/ (1 <= K:601 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= ((-1 + param0:53) * __cost:66)
                       /\ 0 <= __cost:66
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ (-mid_n:603 + mid_j:605) = 0 /\ 0 <= mid___cost:604
                       /\ 0 <= (-1 + mid_i:602)
                       /\ 0 <= (mid_n:603 + -mid_i:602)))
           /\ (0 = K:601 \/ !((1 + __cost:66) <= 0))
           /\ (!(0 <= K:606) \/ __cost':587 = mid___cost:604)
           /\ (!(0 <= K:606) \/ n':584 = mid_n:603)
           /\ (!(0 <= K:606) \/ i':586 = (mid_i:602 + K:606))
           /\ (!((0 <= K:606 /\ K:606 <= 0)) \/ j':585 = mid_j:605)
           /\ (!(1 <= K:606) \/ j':585 = mid_n:603)
           /\ ((K:606 = 0 /\ mid_n:603 = n':584 /\ mid_j:605 = j':585
                  /\ mid_i:602 = i':586 /\ mid___cost:604 = __cost':587)
                 \/ (1 <= K:606 /\ 0 <= (-1 + -mid_i:602 + mid_n:603)
                       /\ 0 <= (-1 + -mid___cost:604)
                       /\ 0 <= (1 + mid_i:602 + -mid_n:603
                                  + ((-1 + -mid_i:602 + mid_n:603)
                                       * (-1 + -mid_i:602 + mid_n:603)))
                       /\ 0 <= (1 + mid_i:602 + -mid_n:603
                                  + ((-1 + -mid_i:602 + mid_n:603)
                                       * (1 + mid_i:602))) /\ 0 <= mid_i:602
                       /\ (-n':584 + j':585) = 0 /\ 0 <= (-i':586 + n':584)
                       /\ 0 <= (-1 + -__cost':587)
                       /\ 0 <= (i':586 + -n':584
                                  + ((-i':586 + n':584) * (-i':586 + n':584)))
                       /\ 0 <= (i':586 + -n':584
                                  + ((-i':586 + n':584) * i':586))
                       /\ 0 <= (-1 + i':586)))
           /\ (0 = K:606 \/ (1 + mid___cost:604) <= 0)
           /\ (K:601 + K:606) = K:588
           /\ (!(0 <= K:607)
                 \/ (mid_n:608 + mid___cost:609) = (param0:53 + __cost:66))
           /\ (!((0 <= K:607 /\ K:607 <= 0))
                 \/ (-mid_n:608 + mid_j:610) = (-param0:53 + j:644))
           /\ (!(1 <= K:607) \/ (-mid_n:608 + mid_j:610) = 0)
           /\ (!(0 <= K:607) \/ mid_i:611 = K:607)
           /\ (!(0 <= K:607) \/ mid_n:608 <= param0:53)
           /\ (!(0 <= K:607)
                 \/ -mid_n:608 <= (-param0:53 + (1/2 * K:607)
                                     + ((param0:53 + __cost:66) * K:607)
                                     + (-1/2 * (K:607 * K:607))))
           /\ ((K:607 = 0 /\ param0:53 = mid_n:608 /\ j:644 = mid_j:610
                  /\ 0 = mid_i:611 /\ __cost:66 = mid___cost:609)
                 \/ (1 <= K:607 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= (-1 + param0:53
                                  + ((-1 + param0:53) * __cost:66))
                       /\ 0 <= (1 + __cost:66)
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ (-mid_n:608 + mid_j:610) = 0
                       /\ 0 <= (-mid_i:611 + mid_n:608)
                       /\ 0 <= (1 + mid___cost:609) /\ 0 <= (-1 + mid_i:611)))
           /\ (0 = K:607 \/ !((2 + __cost:66) <= 0))
           /\ (!(0 <= K:612) \/ i':586 = (mid_i:611 + K:612))
           /\ (!(0 <= K:612) \/ __cost':587 = mid___cost:609)
           /\ (!((0 <= K:612 /\ K:612 <= 0))
                 \/ (-n':584 + j':585) = (-mid_n:608 + mid_j:610))
           /\ (!(1 <= K:612) \/ (-n':584 + j':585) = 0)
           /\ (!(0 <= K:612) \/ n':584 = mid_n:608)
           /\ ((K:612 = 0 /\ mid_n:608 = n':584 /\ mid_j:610 = j':585
                  /\ mid_i:611 = i':586 /\ mid___cost:609 = __cost':587)
                 \/ (1 <= K:612 /\ 0 <= (-1 + -mid_i:611 + mid_n:608)
                       /\ 0 <= (-2 + -mid___cost:609) /\ 0 <= mid_i:611
                       /\ (-n':584 + j':585) = 0 /\ 0 <= (-2 + -__cost':587)
                       /\ 0 <= (-1 + i':586) /\ 0 <= (n':584 + -i':586)))
           /\ (0 = K:612 \/ (2 + mid___cost:609) <= 0)
           /\ (K:607 + K:612) = K:588 /\ 0 <= K:588 /\ 0 <= i':586
           /\ n':584 <= i':586)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':697
   return := 0
   param0 := havoc:13
   return@pos := type_err:729
   param0@pos := type_err:725
   return@width := type_err:730
   param0@width := type_err:727
   when ((!(0 <= K:687) \/ mid___cost:688 = 0)
           /\ (!((0 <= K:687 /\ K:687 <= 0)) \/ mid_j:689 = j:690)
           /\ (!(1 <= K:687) \/ mid_j:689 = (j:690 + havoc:13 + -j:690))
           /\ (!(0 <= K:687) \/ mid_i:691 = K:687)
           /\ (!(0 <= K:687) \/ mid_n:692 = havoc:13)
           /\ (!((0 <= K:687 /\ K:687 <= 0))
                 \/ -mid_j:689 <= (-j:690 + (-1/2 * K:687)
                                     + (havoc:13 * K:687)
                                     + (-1/2 * (K:687 * K:687))))
           /\ (!(1 <= K:687)
                 \/ -mid_j:689 <= (j:690 + -j:690 + -havoc:13
                                     + (-1/2 * K:687) + (havoc:13 * K:687)
                                     + (-1/2 * (K:687 * K:687))))
           /\ K:687 = 0 /\ havoc:13 = mid_n:692 /\ j:690 = mid_j:689
           /\ 0 = mid_i:691 /\ 0 = mid___cost:688 /\ 0 = K:687
           /\ (!((0 <= K:693 /\ K:693 <= 0))
                 \/ (-n':694 + j':695) = (-mid_n:692 + mid_j:689))
           /\ (!(1 <= K:693) \/ (-n':694 + j':695) = 0)
           /\ (!(0 <= K:693) \/ i':696 = (mid_i:691 + K:693))
           /\ (!(0 <= K:693)
                 \/ (n':694 + __cost':697) = (mid_n:692 + mid___cost:688))
           /\ (!(0 <= K:693) \/ n':694 <= mid_n:692)
           /\ (!(0 <= K:693)
                 \/ -n':694 <= (-mid_n:692 + (-1/2 * K:693)
                                  + -((mid_i:691 * K:693))
                                  + ((mid_n:692 + mid___cost:688) * K:693)
                                  + (-1/2 * (K:693 * K:693))))
           /\ ((K:693 = 0 /\ mid_n:692 = n':694 /\ mid_j:689 = j':695
                  /\ mid_i:691 = i':696 /\ mid___cost:688 = __cost':697)
                 \/ (1 <= K:693 /\ 0 <= (-1 + -mid_i:691 + mid_n:692)
                       /\ 0 <= ((-1 + -mid_i:691 + mid_n:692)
                                  * mid___cost:688) /\ 0 <= mid___cost:688
                       /\ 0 <= (1 + mid_i:691 + -mid_n:692
                                  + ((-1 + -mid_i:691 + mid_n:692)
                                       * (-1 + -mid_i:691 + mid_n:692)))
                       /\ 0 <= (1 + mid_i:691 + -mid_n:692
                                  + ((-1 + -mid_i:691 + mid_n:692)
                                       * (1 + mid_i:691))) /\ 0 <= mid_i:691
                       /\ (-n':694 + j':695) = 0 /\ 0 <= (-i':696 + n':694)
                       /\ 0 <= __cost':697 /\ 0 <= (-1 + i':696)))
           /\ (0 = K:693 \/ -mid___cost:688 <= 0) /\ (K:687 + K:693) = K:698
           /\ (!(0 <= K:699) \/ mid_i:700 = K:699)
           /\ (!(0 <= K:699) \/ mid___cost:701 = 0)
           /\ (!((0 <= K:699 /\ K:699 <= 0))
                 \/ (-mid_n:702 + mid_j:703) = (-havoc:13 + j:690))
           /\ (!(1 <= K:699) \/ (-mid_n:702 + mid_j:703) = 0)
           /\ (!(0 <= K:699) \/ mid_n:702 = havoc:13) /\ K:699 = 0
           /\ havoc:13 = mid_n:702 /\ j:690 = mid_j:703 /\ 0 = mid_i:700
           /\ 0 = mid___cost:701 /\ 0 = K:699
           /\ (!((0 <= K:704 /\ K:704 <= 0))
                 \/ (-n':694 + j':695) = (-mid_n:702 + mid_j:703))
           /\ (!(1 <= K:704) \/ (-n':694 + j':695) = 0)
           /\ (!(0 <= K:704) \/ i':696 = (mid_i:700 + K:704))
           /\ (!(0 <= K:704)
                 \/ (n':694 + __cost':697) = (mid_n:702 + mid___cost:701))
           /\ (!(0 <= K:704) \/ n':694 <= mid_n:702)
           /\ (!(0 <= K:704)
                 \/ -n':694 <= (-mid_n:702 + (1/2 * K:704)
                                  + -((mid_i:700 * K:704))
                                  + ((mid_n:702 + mid___cost:701) * K:704)
                                  + (-1/2 * (K:704 * K:704))))
           /\ ((K:704 = 0 /\ mid_n:702 = n':694 /\ mid_j:703 = j':695
                  /\ mid_i:700 = i':696 /\ mid___cost:701 = __cost':697)
                 \/ (1 <= K:704 /\ 0 <= (-1 + -mid_i:700 + mid_n:702)
                       /\ 0 <= (-1 + -mid_i:700 + mid_n:702
                                  + ((-1 + -mid_i:700 + mid_n:702)
                                       * mid___cost:701))
                       /\ 0 <= (1 + mid___cost:701)
                       /\ 0 <= (1 + mid_i:700 + -mid_n:702
                                  + ((-1 + -mid_i:700 + mid_n:702)
                                       * (1 + mid_i:700)))
                       /\ 0 <= (1 + mid_i:700 + -mid_n:702
                                  + ((-1 + -mid_i:700 + mid_n:702)
                                       * (-1 + -mid_i:700 + mid_n:702)))
                       /\ 0 <= mid_i:700 /\ (-n':694 + j':695) = 0
                       /\ 0 <= (-i':696 + n':694) /\ 0 <= (1 + __cost':697)
                       /\ 0 <= (-1 + i':696)))
           /\ (0 = K:704 \/ (-1 + -mid___cost:701) <= 0)
           /\ (K:699 + K:704) = K:698
           /\ (!((0 <= K:705 /\ K:705 <= 0))
                 \/ (-mid_n:706 + mid_j:707) = (-havoc:13 + j:690))
           /\ (!(1 <= K:705) \/ (-mid_n:706 + mid_j:707) = 0)
           /\ (!(0 <= K:705) \/ mid_i:708 = K:705)
           /\ (!(0 <= K:705) \/ (mid_n:706 + mid___cost:709) = havoc:13)
           /\ (!(0 <= K:705) \/ mid_n:706 <= havoc:13)
           /\ ((K:705 = 0 /\ havoc:13 = mid_n:706 /\ j:690 = mid_j:707
                  /\ 0 = mid_i:708 /\ 0 = mid___cost:709)
                 \/ (1 <= K:705 /\ 0 <= (-2 + havoc:13)
                       /\ 0 <= (1 + -havoc:13 + (-1 + havoc:13))
                       /\ 0 <= (1 + -havoc:13
                                  + ((-1 + havoc:13) * (-1 + havoc:13)))
                       /\ (-mid_n:706 + mid_j:707) = 0
                       /\ 0 <= (-mid_i:708 + mid_n:706)
                       /\ 0 <= (-1 + mid_i:708)))
           /\ (0 = K:705 \/ (2 + -havoc:13) <= 0)
           /\ (!((0 <= K:710 /\ K:710 <= 0)) \/ j':695 = (mid_j:707 + K:710))
           /\ (!(1 <= K:710)
                 \/ j':695 = (mid_j:707 + mid_i:708 + -mid_j:707 + K:710))
           /\ (!((0 <= K:710 /\ K:710 <= 0)) \/ n':694 = (mid_n:706 + K:710))
           /\ (!(1 <= K:710)
                 \/ n':694 = (mid_n:706 + mid_i:708 + -mid_n:706 + K:710))
           /\ (!(0 <= K:710) \/ __cost':697 = mid___cost:709)
           /\ (!(0 <= K:710) \/ i':696 = (mid_i:708 + K:710))
           /\ (!((0 <= K:710 /\ K:710 <= 0))
                 \/ -j':695 <= (-mid_j:707 + (-3/2 * K:710)
                                  + (mid_i:708 * K:710)
                                  + (1/2 * (K:710 * K:710))))
           /\ (!(1 <= K:710)
                 \/ -j':695 <= (mid_j:707 + -mid_j:707 + -mid_i:708
                                  + (-3/2 * K:710) + (mid_i:708 * K:710)
                                  + (1/2 * (K:710 * K:710))))
           /\ ((K:710 = 0 /\ mid_n:706 = n':694 /\ mid_j:707 = j':695
                  /\ mid_i:708 = i':696 /\ mid___cost:709 = __cost':697)
                 \/ (1 <= K:710 /\ (-1 + -mid_i:708 + mid_n:706) = 0
                       /\ 0 <= mid_i:708 /\ (-j':695 + n':694) = 0
                       /\ (-j':695 + i':696) = 0 /\ 0 <= (-1 + j':695)))
           /\ (0 = K:710 \/ !((2 + mid_i:708 + -mid_n:706) <= 0))
           /\ (K:705 + K:710) = K:698 /\ (!(0 <= K:711) \/ mid_i:712 = K:711)
           /\ (!(0 <= K:711) \/ (mid_n:713 + mid___cost:714) = havoc:13)
           /\ (!((0 <= K:711 /\ K:711 <= 0))
                 \/ (-mid_n:713 + mid_j:715) = (-havoc:13 + j:690))
           /\ (!(1 <= K:711) \/ (-mid_n:713 + mid_j:715) = 0)
           /\ (!(0 <= K:711) \/ mid_n:713 <= havoc:13)
           /\ (!(0 <= K:711)
                 \/ -mid_n:713 <= (-havoc:13 + (-1/2 * K:711)
                                     + (havoc:13 * K:711)
                                     + (-1/2 * (K:711 * K:711))))
           /\ ((K:711 = 0 /\ havoc:13 = mid_n:713 /\ j:690 = mid_j:715
                  /\ 0 = mid_i:712 /\ 0 = mid___cost:714)
                 \/ (1 <= K:711 /\ 0 <= (-1 + havoc:13)
                       /\ 0 <= (1 + -havoc:13
                                  + ((-1 + havoc:13) * (-1 + havoc:13)))
                       /\ 0 <= (1 + -havoc:13 + (-1 + havoc:13))
                       /\ (-mid_n:713 + mid_j:715) = 0 /\ 0 <= mid___cost:714
                       /\ 0 <= (-1 + mid_i:712)
                       /\ 0 <= (mid_n:713 + -mid_i:712)))
           /\ (!(0 <= K:716) \/ __cost':697 = mid___cost:714)
           /\ (!(0 <= K:716) \/ n':694 = mid_n:713)
           /\ (!(0 <= K:716) \/ i':696 = (mid_i:712 + K:716))
           /\ (!((0 <= K:716 /\ K:716 <= 0)) \/ j':695 = mid_j:715)
           /\ (!(1 <= K:716) \/ j':695 = mid_n:713)
           /\ ((K:716 = 0 /\ mid_n:713 = n':694 /\ mid_j:715 = j':695
                  /\ mid_i:712 = i':696 /\ mid___cost:714 = __cost':697)
                 \/ (1 <= K:716 /\ 0 <= (-1 + -mid_i:712 + mid_n:713)
                       /\ 0 <= (-1 + -mid___cost:714)
                       /\ 0 <= (1 + mid_i:712 + -mid_n:713
                                  + ((-1 + -mid_i:712 + mid_n:713)
                                       * (-1 + -mid_i:712 + mid_n:713)))
                       /\ 0 <= (1 + mid_i:712 + -mid_n:713
                                  + ((-1 + -mid_i:712 + mid_n:713)
                                       * (1 + mid_i:712))) /\ 0 <= mid_i:712
                       /\ (-n':694 + j':695) = 0 /\ 0 <= (-i':696 + n':694)
                       /\ 0 <= (-1 + -__cost':697)
                       /\ 0 <= (i':696 + -n':694
                                  + ((-i':696 + n':694) * (-i':696 + n':694)))
                       /\ 0 <= (i':696 + -n':694
                                  + ((-i':696 + n':694) * i':696))
                       /\ 0 <= (-1 + i':696)))
           /\ (0 = K:716 \/ (1 + mid___cost:714) <= 0)
           /\ (K:711 + K:716) = K:698
           /\ (!(0 <= K:717) \/ (mid_n:718 + mid___cost:719) = havoc:13)
           /\ (!((0 <= K:717 /\ K:717 <= 0))
                 \/ (-mid_n:718 + mid_j:720) = (-havoc:13 + j:690))
           /\ (!(1 <= K:717) \/ (-mid_n:718 + mid_j:720) = 0)
           /\ (!(0 <= K:717) \/ mid_i:721 = K:717)
           /\ (!(0 <= K:717) \/ mid_n:718 <= havoc:13)
           /\ (!(0 <= K:717)
                 \/ -mid_n:718 <= (-havoc:13 + (1/2 * K:717)
                                     + (havoc:13 * K:717)
                                     + (-1/2 * (K:717 * K:717))))
           /\ ((K:717 = 0 /\ havoc:13 = mid_n:718 /\ j:690 = mid_j:720
                  /\ 0 = mid_i:721 /\ 0 = mid___cost:719)
                 \/ (1 <= K:717 /\ 0 <= (-1 + havoc:13)
                       /\ 0 <= (-1 + havoc:13)
                       /\ 0 <= (1 + -havoc:13 + (-1 + havoc:13))
                       /\ 0 <= (1 + -havoc:13
                                  + ((-1 + havoc:13) * (-1 + havoc:13)))
                       /\ (-mid_n:718 + mid_j:720) = 0
                       /\ 0 <= (-mid_i:721 + mid_n:718)
                       /\ 0 <= (1 + mid___cost:719) /\ 0 <= (-1 + mid_i:721)))
           /\ (!(0 <= K:722) \/ i':696 = (mid_i:721 + K:722))
           /\ (!(0 <= K:722) \/ __cost':697 = mid___cost:719)
           /\ (!((0 <= K:722 /\ K:722 <= 0))
                 \/ (-n':694 + j':695) = (-mid_n:718 + mid_j:720))
           /\ (!(1 <= K:722) \/ (-n':694 + j':695) = 0)
           /\ (!(0 <= K:722) \/ n':694 = mid_n:718)
           /\ ((K:722 = 0 /\ mid_n:718 = n':694 /\ mid_j:720 = j':695
                  /\ mid_i:721 = i':696 /\ mid___cost:719 = __cost':697)
                 \/ (1 <= K:722 /\ 0 <= (-1 + -mid_i:721 + mid_n:718)
                       /\ 0 <= (-2 + -mid___cost:719) /\ 0 <= mid_i:721
                       /\ (-n':694 + j':695) = 0 /\ 0 <= (-2 + -__cost':697)
                       /\ 0 <= (-1 + i':696) /\ 0 <= (n':694 + -i':696)))
           /\ (0 = K:722 \/ (2 + mid___cost:719) <= 0)
           /\ (K:717 + K:722) = K:698 /\ 0 <= K:698 /\ 0 <= i':696
           /\ n':694 <= i':696
           /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:728)
                 \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:728)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':741
   return := havoc:770
   param0 := param0:53
   return@pos := type_err:771
   param0@pos := type_err:54
   return@width := type_err:772
   param0@width := type_err:55
   when ((!(0 <= K:731) \/ mid___cost:732 = __cost:66)
           /\ (!((0 <= K:731 /\ K:731 <= 0)) \/ mid_j:733 = j:734)
           /\ (!(1 <= K:731) \/ mid_j:733 = (j:734 + param0:53 + -j:734))
           /\ (!(0 <= K:731) \/ mid_i:735 = K:731)
           /\ (!(0 <= K:731) \/ mid_n:736 = param0:53)
           /\ (!((0 <= K:731 /\ K:731 <= 0))
                 \/ -mid_j:733 <= (-j:734 + (-1/2 * K:731)
                                     + (param0:53 * K:731)
                                     + (-1/2 * (K:731 * K:731))))
           /\ (!(1 <= K:731)
                 \/ -mid_j:733 <= (j:734 + -j:734 + -param0:53
                                     + (-1/2 * K:731) + (param0:53 * K:731)
                                     + (-1/2 * (K:731 * K:731))))
           /\ ((K:731 = 0 /\ param0:53 = mid_n:736 /\ j:734 = mid_j:733
                  /\ 0 = mid_i:735 /\ __cost:66 = mid___cost:732)
                 \/ (1 <= K:731 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= (-1 + -__cost:66)
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ (-mid_j:733 + mid_n:736) = 0
                       /\ 0 <= (-mid_i:735 + mid_j:733)
                       /\ 0 <= (-1 + -mid___cost:732)
                       /\ 0 <= (mid_i:735 + -mid_j:733
                                  + ((-mid_i:735 + mid_j:733)
                                       * (-mid_i:735 + mid_j:733)))
                       /\ 0 <= (mid_i:735 + -mid_j:733
                                  + ((-mid_i:735 + mid_j:733) * mid_i:735))
                       /\ 0 <= (-1 + mid_i:735)))
           /\ (0 = K:731 \/ !(-__cost:66 <= 0))
           /\ (!((0 <= K:737 /\ K:737 <= 0))
                 \/ (-n':738 + j':739) = (-mid_n:736 + mid_j:733))
           /\ (!(1 <= K:737) \/ (-n':738 + j':739) = 0)
           /\ (!(0 <= K:737) \/ i':740 = (mid_i:735 + K:737))
           /\ (!(0 <= K:737)
                 \/ (n':738 + __cost':741) = (mid_n:736 + mid___cost:732))
           /\ (!(0 <= K:737) \/ n':738 <= mid_n:736)
           /\ (!(0 <= K:737)
                 \/ -n':738 <= (-mid_n:736 + (-1/2 * K:737)
                                  + -((mid_i:735 * K:737))
                                  + ((mid_n:736 + mid___cost:732) * K:737)
                                  + (-1/2 * (K:737 * K:737))))
           /\ ((K:737 = 0 /\ mid_n:736 = n':738 /\ mid_j:733 = j':739
                  /\ mid_i:735 = i':740 /\ mid___cost:732 = __cost':741)
                 \/ (1 <= K:737 /\ 0 <= (-1 + -mid_i:735 + mid_n:736)
                       /\ 0 <= ((-1 + -mid_i:735 + mid_n:736)
                                  * mid___cost:732) /\ 0 <= mid___cost:732
                       /\ 0 <= (1 + mid_i:735 + -mid_n:736
                                  + ((-1 + -mid_i:735 + mid_n:736)
                                       * (-1 + -mid_i:735 + mid_n:736)))
                       /\ 0 <= (1 + mid_i:735 + -mid_n:736
                                  + ((-1 + -mid_i:735 + mid_n:736)
                                       * (1 + mid_i:735))) /\ 0 <= mid_i:735
                       /\ (-n':738 + j':739) = 0 /\ 0 <= (-i':740 + n':738)
                       /\ 0 <= __cost':741 /\ 0 <= (-1 + i':740)))
           /\ (0 = K:737 \/ -mid___cost:732 <= 0) /\ (K:731 + K:737) = K:742
           /\ (!(0 <= K:743) \/ mid_i:744 = K:743)
           /\ (!(0 <= K:743) \/ mid___cost:745 = __cost:66)
           /\ (!((0 <= K:743 /\ K:743 <= 0))
                 \/ (-mid_n:746 + mid_j:747) = (-param0:53 + j:734))
           /\ (!(1 <= K:743) \/ (-mid_n:746 + mid_j:747) = 0)
           /\ (!(0 <= K:743) \/ mid_n:746 = param0:53)
           /\ ((K:743 = 0 /\ param0:53 = mid_n:746 /\ j:734 = mid_j:747
                  /\ 0 = mid_i:744 /\ __cost:66 = mid___cost:745)
                 \/ (1 <= K:743 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= (-2 + -__cost:66)
                       /\ (-mid_n:746 + mid_j:747) = 0
                       /\ 0 <= (-2 + -mid___cost:745)
                       /\ 0 <= (-1 + mid_i:744)
                       /\ 0 <= (mid_n:746 + -mid_i:744)))
           /\ (0 = K:743 \/ !((-1 + -__cost:66) <= 0))
           /\ (!((0 <= K:748 /\ K:748 <= 0))
                 \/ (-n':738 + j':739) = (-mid_n:746 + mid_j:747))
           /\ (!(1 <= K:748) \/ (-n':738 + j':739) = 0)
           /\ (!(0 <= K:748) \/ i':740 = (mid_i:744 + K:748))
           /\ (!(0 <= K:748)
                 \/ (n':738 + __cost':741) = (mid_n:746 + mid___cost:745))
           /\ (!(0 <= K:748) \/ n':738 <= mid_n:746)
           /\ (!(0 <= K:748)
                 \/ -n':738 <= (-mid_n:746 + (1/2 * K:748)
                                  + -((mid_i:744 * K:748))
                                  + ((mid_n:746 + mid___cost:745) * K:748)
                                  + (-1/2 * (K:748 * K:748))))
           /\ ((K:748 = 0 /\ mid_n:746 = n':738 /\ mid_j:747 = j':739
                  /\ mid_i:744 = i':740 /\ mid___cost:745 = __cost':741)
                 \/ (1 <= K:748 /\ 0 <= (-1 + -mid_i:744 + mid_n:746)
                       /\ 0 <= (-1 + -mid_i:744 + mid_n:746
                                  + ((-1 + -mid_i:744 + mid_n:746)
                                       * mid___cost:745))
                       /\ 0 <= (1 + mid___cost:745)
                       /\ 0 <= (1 + mid_i:744 + -mid_n:746
                                  + ((-1 + -mid_i:744 + mid_n:746)
                                       * (1 + mid_i:744)))
                       /\ 0 <= (1 + mid_i:744 + -mid_n:746
                                  + ((-1 + -mid_i:744 + mid_n:746)
                                       * (-1 + -mid_i:744 + mid_n:746)))
                       /\ 0 <= mid_i:744 /\ (-n':738 + j':739) = 0
                       /\ 0 <= (-i':740 + n':738) /\ 0 <= (1 + __cost':741)
                       /\ 0 <= (-1 + i':740)))
           /\ (0 = K:748 \/ (-1 + -mid___cost:745) <= 0)
           /\ (K:743 + K:748) = K:742
           /\ (!((0 <= K:749 /\ K:749 <= 0))
                 \/ (-mid_n:750 + mid_j:751) = (-param0:53 + j:734))
           /\ (!(1 <= K:749) \/ (-mid_n:750 + mid_j:751) = 0)
           /\ (!(0 <= K:749) \/ mid_i:752 = K:749)
           /\ (!(0 <= K:749)
                 \/ (mid_n:750 + mid___cost:753) = (param0:53 + __cost:66))
           /\ (!(0 <= K:749) \/ mid_n:750 <= param0:53)
           /\ ((K:749 = 0 /\ param0:53 = mid_n:750 /\ j:734 = mid_j:751
                  /\ 0 = mid_i:752 /\ __cost:66 = mid___cost:753)
                 \/ (1 <= K:749 /\ 0 <= (-2 + param0:53)
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ (-mid_n:750 + mid_j:751) = 0
                       /\ 0 <= (-mid_i:752 + mid_n:750)
                       /\ 0 <= (-1 + mid_i:752)))
           /\ (0 = K:749 \/ (2 + -param0:53) <= 0)
           /\ (!((0 <= K:754 /\ K:754 <= 0)) \/ j':739 = (mid_j:751 + K:754))
           /\ (!(1 <= K:754)
                 \/ j':739 = (mid_j:751 + mid_i:752 + -mid_j:751 + K:754))
           /\ (!((0 <= K:754 /\ K:754 <= 0)) \/ n':738 = (mid_n:750 + K:754))
           /\ (!(1 <= K:754)
                 \/ n':738 = (mid_n:750 + mid_i:752 + -mid_n:750 + K:754))
           /\ (!(0 <= K:754) \/ __cost':741 = mid___cost:753)
           /\ (!(0 <= K:754) \/ i':740 = (mid_i:752 + K:754))
           /\ (!((0 <= K:754 /\ K:754 <= 0))
                 \/ -j':739 <= (-mid_j:751 + (-3/2 * K:754)
                                  + (mid_i:752 * K:754)
                                  + (1/2 * (K:754 * K:754))))
           /\ (!(1 <= K:754)
                 \/ -j':739 <= (mid_j:751 + -mid_j:751 + -mid_i:752
                                  + (-3/2 * K:754) + (mid_i:752 * K:754)
                                  + (1/2 * (K:754 * K:754))))
           /\ ((K:754 = 0 /\ mid_n:750 = n':738 /\ mid_j:751 = j':739
                  /\ mid_i:752 = i':740 /\ mid___cost:753 = __cost':741)
                 \/ (1 <= K:754 /\ (-1 + -mid_i:752 + mid_n:750) = 0
                       /\ 0 <= mid_i:752 /\ (-j':739 + n':738) = 0
                       /\ (-j':739 + i':740) = 0 /\ 0 <= (-1 + j':739)))
           /\ (0 = K:754 \/ !((2 + mid_i:752 + -mid_n:750) <= 0))
           /\ (K:749 + K:754) = K:742 /\ (!(0 <= K:755) \/ mid_i:756 = K:755)
           /\ (!(0 <= K:755)
                 \/ (mid_n:757 + mid___cost:758) = (param0:53 + __cost:66))
           /\ (!((0 <= K:755 /\ K:755 <= 0))
                 \/ (-mid_n:757 + mid_j:759) = (-param0:53 + j:734))
           /\ (!(1 <= K:755) \/ (-mid_n:757 + mid_j:759) = 0)
           /\ (!(0 <= K:755) \/ mid_n:757 <= param0:53)
           /\ (!(0 <= K:755)
                 \/ -mid_n:757 <= (-param0:53 + (-1/2 * K:755)
                                     + ((param0:53 + __cost:66) * K:755)
                                     + (-1/2 * (K:755 * K:755))))
           /\ ((K:755 = 0 /\ param0:53 = mid_n:757 /\ j:734 = mid_j:759
                  /\ 0 = mid_i:756 /\ __cost:66 = mid___cost:758)
                 \/ (1 <= K:755 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= ((-1 + param0:53) * __cost:66)
                       /\ 0 <= __cost:66
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ (-mid_n:757 + mid_j:759) = 0 /\ 0 <= mid___cost:758
                       /\ 0 <= (-1 + mid_i:756)
                       /\ 0 <= (mid_n:757 + -mid_i:756)))
           /\ (0 = K:755 \/ !((1 + __cost:66) <= 0))
           /\ (!(0 <= K:760) \/ __cost':741 = mid___cost:758)
           /\ (!(0 <= K:760) \/ n':738 = mid_n:757)
           /\ (!(0 <= K:760) \/ i':740 = (mid_i:756 + K:760))
           /\ (!((0 <= K:760 /\ K:760 <= 0)) \/ j':739 = mid_j:759)
           /\ (!(1 <= K:760) \/ j':739 = mid_n:757)
           /\ ((K:760 = 0 /\ mid_n:757 = n':738 /\ mid_j:759 = j':739
                  /\ mid_i:756 = i':740 /\ mid___cost:758 = __cost':741)
                 \/ (1 <= K:760 /\ 0 <= (-1 + -mid_i:756 + mid_n:757)
                       /\ 0 <= (-1 + -mid___cost:758)
                       /\ 0 <= (1 + mid_i:756 + -mid_n:757
                                  + ((-1 + -mid_i:756 + mid_n:757)
                                       * (-1 + -mid_i:756 + mid_n:757)))
                       /\ 0 <= (1 + mid_i:756 + -mid_n:757
                                  + ((-1 + -mid_i:756 + mid_n:757)
                                       * (1 + mid_i:756))) /\ 0 <= mid_i:756
                       /\ (-n':738 + j':739) = 0 /\ 0 <= (-i':740 + n':738)
                       /\ 0 <= (-1 + -__cost':741)
                       /\ 0 <= (i':740 + -n':738
                                  + ((-i':740 + n':738) * (-i':740 + n':738)))
                       /\ 0 <= (i':740 + -n':738
                                  + ((-i':740 + n':738) * i':740))
                       /\ 0 <= (-1 + i':740)))
           /\ (0 = K:760 \/ (1 + mid___cost:758) <= 0)
           /\ (K:755 + K:760) = K:742
           /\ (!(0 <= K:761)
                 \/ (mid_n:762 + mid___cost:763) = (param0:53 + __cost:66))
           /\ (!((0 <= K:761 /\ K:761 <= 0))
                 \/ (-mid_n:762 + mid_j:764) = (-param0:53 + j:734))
           /\ (!(1 <= K:761) \/ (-mid_n:762 + mid_j:764) = 0)
           /\ (!(0 <= K:761) \/ mid_i:765 = K:761)
           /\ (!(0 <= K:761) \/ mid_n:762 <= param0:53)
           /\ (!(0 <= K:761)
                 \/ -mid_n:762 <= (-param0:53 + (1/2 * K:761)
                                     + ((param0:53 + __cost:66) * K:761)
                                     + (-1/2 * (K:761 * K:761))))
           /\ ((K:761 = 0 /\ param0:53 = mid_n:762 /\ j:734 = mid_j:764
                  /\ 0 = mid_i:765 /\ __cost:66 = mid___cost:763)
                 \/ (1 <= K:761 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= (-1 + param0:53
                                  + ((-1 + param0:53) * __cost:66))
                       /\ 0 <= (1 + __cost:66)
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ (-mid_n:762 + mid_j:764) = 0
                       /\ 0 <= (-mid_i:765 + mid_n:762)
                       /\ 0 <= (1 + mid___cost:763) /\ 0 <= (-1 + mid_i:765)))
           /\ (0 = K:761 \/ !((2 + __cost:66) <= 0))
           /\ (!(0 <= K:766) \/ i':740 = (mid_i:765 + K:766))
           /\ (!(0 <= K:766) \/ __cost':741 = mid___cost:763)
           /\ (!((0 <= K:766 /\ K:766 <= 0))
                 \/ (-n':738 + j':739) = (-mid_n:762 + mid_j:764))
           /\ (!(1 <= K:766) \/ (-n':738 + j':739) = 0)
           /\ (!(0 <= K:766) \/ n':738 = mid_n:762)
           /\ ((K:766 = 0 /\ mid_n:762 = n':738 /\ mid_j:764 = j':739
                  /\ mid_i:765 = i':740 /\ mid___cost:763 = __cost':741)
                 \/ (1 <= K:766 /\ 0 <= (-1 + -mid_i:765 + mid_n:762)
                       /\ 0 <= (-2 + -mid___cost:763) /\ 0 <= mid_i:765
                       /\ (-n':738 + j':739) = 0 /\ 0 <= (-2 + -__cost':741)
                       /\ 0 <= (-1 + i':740) /\ 0 <= (n':738 + -i':740)))
           /\ (0 = K:766 \/ (2 + mid___cost:763) <= 0)
           /\ (K:761 + K:766) = K:742 /\ 0 <= K:742 /\ 0 <= i':740
           /\ n':738 <= i':740)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=20: 
Weight(Base relation: 
  {__cost := __cost':587
   return := havoc:641
   return@pos := type_err:642
   return@width := type_err:643
   when ((!(0 <= K:578) \/ mid___cost:579 = __cost:66)
           /\ (!((0 <= K:578 /\ K:578 <= 0)) \/ mid_j:580 = j:644)
           /\ (!(1 <= K:578) \/ mid_j:580 = (j:644 + param0:53 + -j:644))
           /\ (!(0 <= K:578) \/ mid_i:581 = K:578)
           /\ (!(0 <= K:578) \/ mid_n:582 = param0:53)
           /\ (!((0 <= K:578 /\ K:578 <= 0))
                 \/ -mid_j:580 <= (-j:644 + (-1/2 * K:578)
                                     + (param0:53 * K:578)
                                     + (-1/2 * (K:578 * K:578))))
           /\ (!(1 <= K:578)
                 \/ -mid_j:580 <= (j:644 + -j:644 + -param0:53
                                     + (-1/2 * K:578) + (param0:53 * K:578)
                                     + (-1/2 * (K:578 * K:578))))
           /\ ((K:578 = 0 /\ param0:53 = mid_n:582 /\ j:644 = mid_j:580
                  /\ 0 = mid_i:581 /\ __cost:66 = mid___cost:579)
                 \/ (1 <= K:578 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= (-1 + -__cost:66)
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ (-mid_j:580 + mid_n:582) = 0
                       /\ 0 <= (-mid_i:581 + mid_j:580)
                       /\ 0 <= (-1 + -mid___cost:579)
                       /\ 0 <= (mid_i:581 + -mid_j:580
                                  + ((-mid_i:581 + mid_j:580)
                                       * (-mid_i:581 + mid_j:580)))
                       /\ 0 <= (mid_i:581 + -mid_j:580
                                  + ((-mid_i:581 + mid_j:580) * mid_i:581))
                       /\ 0 <= (-1 + mid_i:581)))
           /\ (0 = K:578 \/ !(-__cost:66 <= 0))
           /\ (!((0 <= K:583 /\ K:583 <= 0))
                 \/ (-n':584 + j':585) = (-mid_n:582 + mid_j:580))
           /\ (!(1 <= K:583) \/ (-n':584 + j':585) = 0)
           /\ (!(0 <= K:583) \/ i':586 = (mid_i:581 + K:583))
           /\ (!(0 <= K:583)
                 \/ (n':584 + __cost':587) = (mid_n:582 + mid___cost:579))
           /\ (!(0 <= K:583) \/ n':584 <= mid_n:582)
           /\ (!(0 <= K:583)
                 \/ -n':584 <= (-mid_n:582 + (-1/2 * K:583)
                                  + -((mid_i:581 * K:583))
                                  + ((mid_n:582 + mid___cost:579) * K:583)
                                  + (-1/2 * (K:583 * K:583))))
           /\ ((K:583 = 0 /\ mid_n:582 = n':584 /\ mid_j:580 = j':585
                  /\ mid_i:581 = i':586 /\ mid___cost:579 = __cost':587)
                 \/ (1 <= K:583 /\ 0 <= (-1 + -mid_i:581 + mid_n:582)
                       /\ 0 <= ((-1 + -mid_i:581 + mid_n:582)
                                  * mid___cost:579) /\ 0 <= mid___cost:579
                       /\ 0 <= (1 + mid_i:581 + -mid_n:582
                                  + ((-1 + -mid_i:581 + mid_n:582)
                                       * (-1 + -mid_i:581 + mid_n:582)))
                       /\ 0 <= (1 + mid_i:581 + -mid_n:582
                                  + ((-1 + -mid_i:581 + mid_n:582)
                                       * (1 + mid_i:581))) /\ 0 <= mid_i:581
                       /\ (-n':584 + j':585) = 0 /\ 0 <= (-i':586 + n':584)
                       /\ 0 <= __cost':587 /\ 0 <= (-1 + i':586)))
           /\ (0 = K:583 \/ -mid___cost:579 <= 0) /\ (K:578 + K:583) = K:588
           /\ (!(0 <= K:589) \/ mid_i:590 = K:589)
           /\ (!(0 <= K:589) \/ mid___cost:591 = __cost:66)
           /\ (!((0 <= K:589 /\ K:589 <= 0))
                 \/ (-mid_n:592 + mid_j:593) = (-param0:53 + j:644))
           /\ (!(1 <= K:589) \/ (-mid_n:592 + mid_j:593) = 0)
           /\ (!(0 <= K:589) \/ mid_n:592 = param0:53)
           /\ ((K:589 = 0 /\ param0:53 = mid_n:592 /\ j:644 = mid_j:593
                  /\ 0 = mid_i:590 /\ __cost:66 = mid___cost:591)
                 \/ (1 <= K:589 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= (-2 + -__cost:66)
                       /\ (-mid_n:592 + mid_j:593) = 0
                       /\ 0 <= (-2 + -mid___cost:591)
                       /\ 0 <= (-1 + mid_i:590)
                       /\ 0 <= (mid_n:592 + -mid_i:590)))
           /\ (0 = K:589 \/ !((-1 + -__cost:66) <= 0))
           /\ (!((0 <= K:594 /\ K:594 <= 0))
                 \/ (-n':584 + j':585) = (-mid_n:592 + mid_j:593))
           /\ (!(1 <= K:594) \/ (-n':584 + j':585) = 0)
           /\ (!(0 <= K:594) \/ i':586 = (mid_i:590 + K:594))
           /\ (!(0 <= K:594)
                 \/ (n':584 + __cost':587) = (mid_n:592 + mid___cost:591))
           /\ (!(0 <= K:594) \/ n':584 <= mid_n:592)
           /\ (!(0 <= K:594)
                 \/ -n':584 <= (-mid_n:592 + (1/2 * K:594)
                                  + -((mid_i:590 * K:594))
                                  + ((mid_n:592 + mid___cost:591) * K:594)
                                  + (-1/2 * (K:594 * K:594))))
           /\ ((K:594 = 0 /\ mid_n:592 = n':584 /\ mid_j:593 = j':585
                  /\ mid_i:590 = i':586 /\ mid___cost:591 = __cost':587)
                 \/ (1 <= K:594 /\ 0 <= (-1 + -mid_i:590 + mid_n:592)
                       /\ 0 <= (-1 + -mid_i:590 + mid_n:592
                                  + ((-1 + -mid_i:590 + mid_n:592)
                                       * mid___cost:591))
                       /\ 0 <= (1 + mid___cost:591)
                       /\ 0 <= (1 + mid_i:590 + -mid_n:592
                                  + ((-1 + -mid_i:590 + mid_n:592)
                                       * (1 + mid_i:590)))
                       /\ 0 <= (1 + mid_i:590 + -mid_n:592
                                  + ((-1 + -mid_i:590 + mid_n:592)
                                       * (-1 + -mid_i:590 + mid_n:592)))
                       /\ 0 <= mid_i:590 /\ (-n':584 + j':585) = 0
                       /\ 0 <= (-i':586 + n':584) /\ 0 <= (1 + __cost':587)
                       /\ 0 <= (-1 + i':586)))
           /\ (0 = K:594 \/ (-1 + -mid___cost:591) <= 0)
           /\ (K:589 + K:594) = K:588
           /\ (!((0 <= K:595 /\ K:595 <= 0))
                 \/ (-mid_n:596 + mid_j:597) = (-param0:53 + j:644))
           /\ (!(1 <= K:595) \/ (-mid_n:596 + mid_j:597) = 0)
           /\ (!(0 <= K:595) \/ mid_i:598 = K:595)
           /\ (!(0 <= K:595)
                 \/ (mid_n:596 + mid___cost:599) = (param0:53 + __cost:66))
           /\ (!(0 <= K:595) \/ mid_n:596 <= param0:53)
           /\ ((K:595 = 0 /\ param0:53 = mid_n:596 /\ j:644 = mid_j:597
                  /\ 0 = mid_i:598 /\ __cost:66 = mid___cost:599)
                 \/ (1 <= K:595 /\ 0 <= (-2 + param0:53)
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ (-mid_n:596 + mid_j:597) = 0
                       /\ 0 <= (-mid_i:598 + mid_n:596)
                       /\ 0 <= (-1 + mid_i:598)))
           /\ (0 = K:595 \/ (2 + -param0:53) <= 0)
           /\ (!((0 <= K:600 /\ K:600 <= 0)) \/ j':585 = (mid_j:597 + K:600))
           /\ (!(1 <= K:600)
                 \/ j':585 = (mid_j:597 + mid_i:598 + -mid_j:597 + K:600))
           /\ (!((0 <= K:600 /\ K:600 <= 0)) \/ n':584 = (mid_n:596 + K:600))
           /\ (!(1 <= K:600)
                 \/ n':584 = (mid_n:596 + mid_i:598 + -mid_n:596 + K:600))
           /\ (!(0 <= K:600) \/ __cost':587 = mid___cost:599)
           /\ (!(0 <= K:600) \/ i':586 = (mid_i:598 + K:600))
           /\ (!((0 <= K:600 /\ K:600 <= 0))
                 \/ -j':585 <= (-mid_j:597 + (-3/2 * K:600)
                                  + (mid_i:598 * K:600)
                                  + (1/2 * (K:600 * K:600))))
           /\ (!(1 <= K:600)
                 \/ -j':585 <= (mid_j:597 + -mid_j:597 + -mid_i:598
                                  + (-3/2 * K:600) + (mid_i:598 * K:600)
                                  + (1/2 * (K:600 * K:600))))
           /\ ((K:600 = 0 /\ mid_n:596 = n':584 /\ mid_j:597 = j':585
                  /\ mid_i:598 = i':586 /\ mid___cost:599 = __cost':587)
                 \/ (1 <= K:600 /\ (-1 + -mid_i:598 + mid_n:596) = 0
                       /\ 0 <= mid_i:598 /\ (-j':585 + n':584) = 0
                       /\ (-j':585 + i':586) = 0 /\ 0 <= (-1 + j':585)))
           /\ (0 = K:600 \/ !((2 + mid_i:598 + -mid_n:596) <= 0))
           /\ (K:595 + K:600) = K:588 /\ (!(0 <= K:601) \/ mid_i:602 = K:601)
           /\ (!(0 <= K:601)
                 \/ (mid_n:603 + mid___cost:604) = (param0:53 + __cost:66))
           /\ (!((0 <= K:601 /\ K:601 <= 0))
                 \/ (-mid_n:603 + mid_j:605) = (-param0:53 + j:644))
           /\ (!(1 <= K:601) \/ (-mid_n:603 + mid_j:605) = 0)
           /\ (!(0 <= K:601) \/ mid_n:603 <= param0:53)
           /\ (!(0 <= K:601)
                 \/ -mid_n:603 <= (-param0:53 + (-1/2 * K:601)
                                     + ((param0:53 + __cost:66) * K:601)
                                     + (-1/2 * (K:601 * K:601))))
           /\ ((K:601 = 0 /\ param0:53 = mid_n:603 /\ j:644 = mid_j:605
                  /\ 0 = mid_i:602 /\ __cost:66 = mid___cost:604)
                 \/ (1 <= K:601 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= ((-1 + param0:53) * __cost:66)
                       /\ 0 <= __cost:66
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ (-mid_n:603 + mid_j:605) = 0 /\ 0 <= mid___cost:604
                       /\ 0 <= (-1 + mid_i:602)
                       /\ 0 <= (mid_n:603 + -mid_i:602)))
           /\ (0 = K:601 \/ !((1 + __cost:66) <= 0))
           /\ (!(0 <= K:606) \/ __cost':587 = mid___cost:604)
           /\ (!(0 <= K:606) \/ n':584 = mid_n:603)
           /\ (!(0 <= K:606) \/ i':586 = (mid_i:602 + K:606))
           /\ (!((0 <= K:606 /\ K:606 <= 0)) \/ j':585 = mid_j:605)
           /\ (!(1 <= K:606) \/ j':585 = mid_n:603)
           /\ ((K:606 = 0 /\ mid_n:603 = n':584 /\ mid_j:605 = j':585
                  /\ mid_i:602 = i':586 /\ mid___cost:604 = __cost':587)
                 \/ (1 <= K:606 /\ 0 <= (-1 + -mid_i:602 + mid_n:603)
                       /\ 0 <= (-1 + -mid___cost:604)
                       /\ 0 <= (1 + mid_i:602 + -mid_n:603
                                  + ((-1 + -mid_i:602 + mid_n:603)
                                       * (-1 + -mid_i:602 + mid_n:603)))
                       /\ 0 <= (1 + mid_i:602 + -mid_n:603
                                  + ((-1 + -mid_i:602 + mid_n:603)
                                       * (1 + mid_i:602))) /\ 0 <= mid_i:602
                       /\ (-n':584 + j':585) = 0 /\ 0 <= (-i':586 + n':584)
                       /\ 0 <= (-1 + -__cost':587)
                       /\ 0 <= (i':586 + -n':584
                                  + ((-i':586 + n':584) * (-i':586 + n':584)))
                       /\ 0 <= (i':586 + -n':584
                                  + ((-i':586 + n':584) * i':586))
                       /\ 0 <= (-1 + i':586)))
           /\ (0 = K:606 \/ (1 + mid___cost:604) <= 0)
           /\ (K:601 + K:606) = K:588
           /\ (!(0 <= K:607)
                 \/ (mid_n:608 + mid___cost:609) = (param0:53 + __cost:66))
           /\ (!((0 <= K:607 /\ K:607 <= 0))
                 \/ (-mid_n:608 + mid_j:610) = (-param0:53 + j:644))
           /\ (!(1 <= K:607) \/ (-mid_n:608 + mid_j:610) = 0)
           /\ (!(0 <= K:607) \/ mid_i:611 = K:607)
           /\ (!(0 <= K:607) \/ mid_n:608 <= param0:53)
           /\ (!(0 <= K:607)
                 \/ -mid_n:608 <= (-param0:53 + (1/2 * K:607)
                                     + ((param0:53 + __cost:66) * K:607)
                                     + (-1/2 * (K:607 * K:607))))
           /\ ((K:607 = 0 /\ param0:53 = mid_n:608 /\ j:644 = mid_j:610
                  /\ 0 = mid_i:611 /\ __cost:66 = mid___cost:609)
                 \/ (1 <= K:607 /\ 0 <= (-1 + param0:53)
                       /\ 0 <= (-1 + param0:53
                                  + ((-1 + param0:53) * __cost:66))
                       /\ 0 <= (1 + __cost:66)
                       /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                       /\ 0 <= (1 + -param0:53
                                  + ((-1 + param0:53) * (-1 + param0:53)))
                       /\ (-mid_n:608 + mid_j:610) = 0
                       /\ 0 <= (-mid_i:611 + mid_n:608)
                       /\ 0 <= (1 + mid___cost:609) /\ 0 <= (-1 + mid_i:611)))
           /\ (0 = K:607 \/ !((2 + __cost:66) <= 0))
           /\ (!(0 <= K:612) \/ i':586 = (mid_i:611 + K:612))
           /\ (!(0 <= K:612) \/ __cost':587 = mid___cost:609)
           /\ (!((0 <= K:612 /\ K:612 <= 0))
                 \/ (-n':584 + j':585) = (-mid_n:608 + mid_j:610))
           /\ (!(1 <= K:612) \/ (-n':584 + j':585) = 0)
           /\ (!(0 <= K:612) \/ n':584 = mid_n:608)
           /\ ((K:612 = 0 /\ mid_n:608 = n':584 /\ mid_j:610 = j':585
                  /\ mid_i:611 = i':586 /\ mid___cost:609 = __cost':587)
                 \/ (1 <= K:612 /\ 0 <= (-1 + -mid_i:611 + mid_n:608)
                       /\ 0 <= (-2 + -mid___cost:609) /\ 0 <= mid_i:611
                       /\ (-n':584 + j':585) = 0 /\ 0 <= (-2 + -__cost':587)
                       /\ 0 <= (-1 + i':586) /\ 0 <= (n':584 + -i':586)))
           /\ (0 = K:612 \/ (2 + mid___cost:609) <= 0)
           /\ (K:607 + K:612) = K:588 /\ 0 <= K:588 /\ 0 <= i':586
           /\ n':584 <= i':586)})


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':697
 return := 0
 param0 := havoc:13
 return@pos := type_err:729
 param0@pos := type_err:725
 return@width := type_err:730
 param0@width := type_err:727
 when ((!(0 <= K:687) \/ mid___cost:688 = 0)
         /\ (!((0 <= K:687 /\ K:687 <= 0)) \/ mid_j:689 = j:690)
         /\ (!(1 <= K:687) \/ mid_j:689 = (j:690 + havoc:13 + -j:690))
         /\ (!(0 <= K:687) \/ mid_i:691 = K:687)
         /\ (!(0 <= K:687) \/ mid_n:692 = havoc:13)
         /\ (!((0 <= K:687 /\ K:687 <= 0))
               \/ -mid_j:689 <= (-j:690 + (-1/2 * K:687) + (havoc:13 * K:687)
                                   + (-1/2 * (K:687 * K:687))))
         /\ (!(1 <= K:687)
               \/ -mid_j:689 <= (j:690 + -j:690 + -havoc:13 + (-1/2 * K:687)
                                   + (havoc:13 * K:687)
                                   + (-1/2 * (K:687 * K:687)))) /\ K:687 = 0
         /\ havoc:13 = mid_n:692 /\ j:690 = mid_j:689 /\ 0 = mid_i:691
         /\ 0 = mid___cost:688 /\ 0 = K:687
         /\ (!((0 <= K:693 /\ K:693 <= 0))
               \/ (-n':694 + j':695) = (-mid_n:692 + mid_j:689))
         /\ (!(1 <= K:693) \/ (-n':694 + j':695) = 0)
         /\ (!(0 <= K:693) \/ i':696 = (mid_i:691 + K:693))
         /\ (!(0 <= K:693)
               \/ (n':694 + __cost':697) = (mid_n:692 + mid___cost:688))
         /\ (!(0 <= K:693) \/ n':694 <= mid_n:692)
         /\ (!(0 <= K:693)
               \/ -n':694 <= (-mid_n:692 + (-1/2 * K:693)
                                + -((mid_i:691 * K:693))
                                + ((mid_n:692 + mid___cost:688) * K:693)
                                + (-1/2 * (K:693 * K:693))))
         /\ ((K:693 = 0 /\ mid_n:692 = n':694 /\ mid_j:689 = j':695
                /\ mid_i:691 = i':696 /\ mid___cost:688 = __cost':697)
               \/ (1 <= K:693 /\ 0 <= (-1 + -mid_i:691 + mid_n:692)
                     /\ 0 <= ((-1 + -mid_i:691 + mid_n:692) * mid___cost:688)
                     /\ 0 <= mid___cost:688
                     /\ 0 <= (1 + mid_i:691 + -mid_n:692
                                + ((-1 + -mid_i:691 + mid_n:692)
                                     * (-1 + -mid_i:691 + mid_n:692)))
                     /\ 0 <= (1 + mid_i:691 + -mid_n:692
                                + ((-1 + -mid_i:691 + mid_n:692)
                                     * (1 + mid_i:691))) /\ 0 <= mid_i:691
                     /\ (-n':694 + j':695) = 0 /\ 0 <= (-i':696 + n':694)
                     /\ 0 <= __cost':697 /\ 0 <= (-1 + i':696)))
         /\ (0 = K:693 \/ -mid___cost:688 <= 0) /\ (K:687 + K:693) = K:698
         /\ (!(0 <= K:699) \/ mid_i:700 = K:699)
         /\ (!(0 <= K:699) \/ mid___cost:701 = 0)
         /\ (!((0 <= K:699 /\ K:699 <= 0))
               \/ (-mid_n:702 + mid_j:703) = (-havoc:13 + j:690))
         /\ (!(1 <= K:699) \/ (-mid_n:702 + mid_j:703) = 0)
         /\ (!(0 <= K:699) \/ mid_n:702 = havoc:13) /\ K:699 = 0
         /\ havoc:13 = mid_n:702 /\ j:690 = mid_j:703 /\ 0 = mid_i:700
         /\ 0 = mid___cost:701 /\ 0 = K:699
         /\ (!((0 <= K:704 /\ K:704 <= 0))
               \/ (-n':694 + j':695) = (-mid_n:702 + mid_j:703))
         /\ (!(1 <= K:704) \/ (-n':694 + j':695) = 0)
         /\ (!(0 <= K:704) \/ i':696 = (mid_i:700 + K:704))
         /\ (!(0 <= K:704)
               \/ (n':694 + __cost':697) = (mid_n:702 + mid___cost:701))
         /\ (!(0 <= K:704) \/ n':694 <= mid_n:702)
         /\ (!(0 <= K:704)
               \/ -n':694 <= (-mid_n:702 + (1/2 * K:704)
                                + -((mid_i:700 * K:704))
                                + ((mid_n:702 + mid___cost:701) * K:704)
                                + (-1/2 * (K:704 * K:704))))
         /\ ((K:704 = 0 /\ mid_n:702 = n':694 /\ mid_j:703 = j':695
                /\ mid_i:700 = i':696 /\ mid___cost:701 = __cost':697)
               \/ (1 <= K:704 /\ 0 <= (-1 + -mid_i:700 + mid_n:702)
                     /\ 0 <= (-1 + -mid_i:700 + mid_n:702
                                + ((-1 + -mid_i:700 + mid_n:702)
                                     * mid___cost:701))
                     /\ 0 <= (1 + mid___cost:701)
                     /\ 0 <= (1 + mid_i:700 + -mid_n:702
                                + ((-1 + -mid_i:700 + mid_n:702)
                                     * (1 + mid_i:700)))
                     /\ 0 <= (1 + mid_i:700 + -mid_n:702
                                + ((-1 + -mid_i:700 + mid_n:702)
                                     * (-1 + -mid_i:700 + mid_n:702)))
                     /\ 0 <= mid_i:700 /\ (-n':694 + j':695) = 0
                     /\ 0 <= (-i':696 + n':694) /\ 0 <= (1 + __cost':697)
                     /\ 0 <= (-1 + i':696)))
         /\ (0 = K:704 \/ (-1 + -mid___cost:701) <= 0)
         /\ (K:699 + K:704) = K:698
         /\ (!((0 <= K:705 /\ K:705 <= 0))
               \/ (-mid_n:706 + mid_j:707) = (-havoc:13 + j:690))
         /\ (!(1 <= K:705) \/ (-mid_n:706 + mid_j:707) = 0)
         /\ (!(0 <= K:705) \/ mid_i:708 = K:705)
         /\ (!(0 <= K:705) \/ (mid_n:706 + mid___cost:709) = havoc:13)
         /\ (!(0 <= K:705) \/ mid_n:706 <= havoc:13)
         /\ ((K:705 = 0 /\ havoc:13 = mid_n:706 /\ j:690 = mid_j:707
                /\ 0 = mid_i:708 /\ 0 = mid___cost:709)
               \/ (1 <= K:705 /\ 0 <= (-2 + havoc:13)
                     /\ 0 <= (1 + -havoc:13 + (-1 + havoc:13))
                     /\ 0 <= (1 + -havoc:13
                                + ((-1 + havoc:13) * (-1 + havoc:13)))
                     /\ (-mid_n:706 + mid_j:707) = 0
                     /\ 0 <= (-mid_i:708 + mid_n:706)
                     /\ 0 <= (-1 + mid_i:708)))
         /\ (0 = K:705 \/ (2 + -havoc:13) <= 0)
         /\ (!((0 <= K:710 /\ K:710 <= 0)) \/ j':695 = (mid_j:707 + K:710))
         /\ (!(1 <= K:710)
               \/ j':695 = (mid_j:707 + mid_i:708 + -mid_j:707 + K:710))
         /\ (!((0 <= K:710 /\ K:710 <= 0)) \/ n':694 = (mid_n:706 + K:710))
         /\ (!(1 <= K:710)
               \/ n':694 = (mid_n:706 + mid_i:708 + -mid_n:706 + K:710))
         /\ (!(0 <= K:710) \/ __cost':697 = mid___cost:709)
         /\ (!(0 <= K:710) \/ i':696 = (mid_i:708 + K:710))
         /\ (!((0 <= K:710 /\ K:710 <= 0))
               \/ -j':695 <= (-mid_j:707 + (-3/2 * K:710)
                                + (mid_i:708 * K:710)
                                + (1/2 * (K:710 * K:710))))
         /\ (!(1 <= K:710)
               \/ -j':695 <= (mid_j:707 + -mid_j:707 + -mid_i:708
                                + (-3/2 * K:710) + (mid_i:708 * K:710)
                                + (1/2 * (K:710 * K:710))))
         /\ ((K:710 = 0 /\ mid_n:706 = n':694 /\ mid_j:707 = j':695
                /\ mid_i:708 = i':696 /\ mid___cost:709 = __cost':697)
               \/ (1 <= K:710 /\ (-1 + -mid_i:708 + mid_n:706) = 0
                     /\ 0 <= mid_i:708 /\ (-j':695 + n':694) = 0
                     /\ (-j':695 + i':696) = 0 /\ 0 <= (-1 + j':695)))
         /\ (0 = K:710 \/ !((2 + mid_i:708 + -mid_n:706) <= 0))
         /\ (K:705 + K:710) = K:698 /\ (!(0 <= K:711) \/ mid_i:712 = K:711)
         /\ (!(0 <= K:711) \/ (mid_n:713 + mid___cost:714) = havoc:13)
         /\ (!((0 <= K:711 /\ K:711 <= 0))
               \/ (-mid_n:713 + mid_j:715) = (-havoc:13 + j:690))
         /\ (!(1 <= K:711) \/ (-mid_n:713 + mid_j:715) = 0)
         /\ (!(0 <= K:711) \/ mid_n:713 <= havoc:13)
         /\ (!(0 <= K:711)
               \/ -mid_n:713 <= (-havoc:13 + (-1/2 * K:711)
                                   + (havoc:13 * K:711)
                                   + (-1/2 * (K:711 * K:711))))
         /\ ((K:711 = 0 /\ havoc:13 = mid_n:713 /\ j:690 = mid_j:715
                /\ 0 = mid_i:712 /\ 0 = mid___cost:714)
               \/ (1 <= K:711 /\ 0 <= (-1 + havoc:13)
                     /\ 0 <= (1 + -havoc:13
                                + ((-1 + havoc:13) * (-1 + havoc:13)))
                     /\ 0 <= (1 + -havoc:13 + (-1 + havoc:13))
                     /\ (-mid_n:713 + mid_j:715) = 0 /\ 0 <= mid___cost:714
                     /\ 0 <= (-1 + mid_i:712)
                     /\ 0 <= (mid_n:713 + -mid_i:712)))
         /\ (!(0 <= K:716) \/ __cost':697 = mid___cost:714)
         /\ (!(0 <= K:716) \/ n':694 = mid_n:713)
         /\ (!(0 <= K:716) \/ i':696 = (mid_i:712 + K:716))
         /\ (!((0 <= K:716 /\ K:716 <= 0)) \/ j':695 = mid_j:715)
         /\ (!(1 <= K:716) \/ j':695 = mid_n:713)
         /\ ((K:716 = 0 /\ mid_n:713 = n':694 /\ mid_j:715 = j':695
                /\ mid_i:712 = i':696 /\ mid___cost:714 = __cost':697)
               \/ (1 <= K:716 /\ 0 <= (-1 + -mid_i:712 + mid_n:713)
                     /\ 0 <= (-1 + -mid___cost:714)
                     /\ 0 <= (1 + mid_i:712 + -mid_n:713
                                + ((-1 + -mid_i:712 + mid_n:713)
                                     * (-1 + -mid_i:712 + mid_n:713)))
                     /\ 0 <= (1 + mid_i:712 + -mid_n:713
                                + ((-1 + -mid_i:712 + mid_n:713)
                                     * (1 + mid_i:712))) /\ 0 <= mid_i:712
                     /\ (-n':694 + j':695) = 0 /\ 0 <= (-i':696 + n':694)
                     /\ 0 <= (-1 + -__cost':697)
                     /\ 0 <= (i':696 + -n':694
                                + ((-i':696 + n':694) * (-i':696 + n':694)))
                     /\ 0 <= (i':696 + -n':694
                                + ((-i':696 + n':694) * i':696))
                     /\ 0 <= (-1 + i':696)))
         /\ (0 = K:716 \/ (1 + mid___cost:714) <= 0)
         /\ (K:711 + K:716) = K:698
         /\ (!(0 <= K:717) \/ (mid_n:718 + mid___cost:719) = havoc:13)
         /\ (!((0 <= K:717 /\ K:717 <= 0))
               \/ (-mid_n:718 + mid_j:720) = (-havoc:13 + j:690))
         /\ (!(1 <= K:717) \/ (-mid_n:718 + mid_j:720) = 0)
         /\ (!(0 <= K:717) \/ mid_i:721 = K:717)
         /\ (!(0 <= K:717) \/ mid_n:718 <= havoc:13)
         /\ (!(0 <= K:717)
               \/ -mid_n:718 <= (-havoc:13 + (1/2 * K:717)
                                   + (havoc:13 * K:717)
                                   + (-1/2 * (K:717 * K:717))))
         /\ ((K:717 = 0 /\ havoc:13 = mid_n:718 /\ j:690 = mid_j:720
                /\ 0 = mid_i:721 /\ 0 = mid___cost:719)
               \/ (1 <= K:717 /\ 0 <= (-1 + havoc:13) /\ 0 <= (-1 + havoc:13)
                     /\ 0 <= (1 + -havoc:13 + (-1 + havoc:13))
                     /\ 0 <= (1 + -havoc:13
                                + ((-1 + havoc:13) * (-1 + havoc:13)))
                     /\ (-mid_n:718 + mid_j:720) = 0
                     /\ 0 <= (-mid_i:721 + mid_n:718)
                     /\ 0 <= (1 + mid___cost:719) /\ 0 <= (-1 + mid_i:721)))
         /\ (!(0 <= K:722) \/ i':696 = (mid_i:721 + K:722))
         /\ (!(0 <= K:722) \/ __cost':697 = mid___cost:719)
         /\ (!((0 <= K:722 /\ K:722 <= 0))
               \/ (-n':694 + j':695) = (-mid_n:718 + mid_j:720))
         /\ (!(1 <= K:722) \/ (-n':694 + j':695) = 0)
         /\ (!(0 <= K:722) \/ n':694 = mid_n:718)
         /\ ((K:722 = 0 /\ mid_n:718 = n':694 /\ mid_j:720 = j':695
                /\ mid_i:721 = i':696 /\ mid___cost:719 = __cost':697)
               \/ (1 <= K:722 /\ 0 <= (-1 + -mid_i:721 + mid_n:718)
                     /\ 0 <= (-2 + -mid___cost:719) /\ 0 <= mid_i:721
                     /\ (-n':694 + j':695) = 0 /\ 0 <= (-2 + -__cost':697)
                     /\ 0 <= (-1 + i':696) /\ 0 <= (n':694 + -i':696)))
         /\ (0 = K:722 \/ (2 + mid___cost:719) <= 0)
         /\ (K:717 + K:722) = K:698 /\ 0 <= K:698 /\ 0 <= i':696
         /\ n':694 <= i':696
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:728)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:728)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':741
 return := havoc:770
 param0 := param0:53
 return@pos := type_err:771
 param0@pos := type_err:54
 return@width := type_err:772
 param0@width := type_err:55
 when ((!(0 <= K:731) \/ mid___cost:732 = __cost:66)
         /\ (!((0 <= K:731 /\ K:731 <= 0)) \/ mid_j:733 = j:734)
         /\ (!(1 <= K:731) \/ mid_j:733 = (j:734 + param0:53 + -j:734))
         /\ (!(0 <= K:731) \/ mid_i:735 = K:731)
         /\ (!(0 <= K:731) \/ mid_n:736 = param0:53)
         /\ (!((0 <= K:731 /\ K:731 <= 0))
               \/ -mid_j:733 <= (-j:734 + (-1/2 * K:731)
                                   + (param0:53 * K:731)
                                   + (-1/2 * (K:731 * K:731))))
         /\ (!(1 <= K:731)
               \/ -mid_j:733 <= (j:734 + -j:734 + -param0:53 + (-1/2 * K:731)
                                   + (param0:53 * K:731)
                                   + (-1/2 * (K:731 * K:731))))
         /\ ((K:731 = 0 /\ param0:53 = mid_n:736 /\ j:734 = mid_j:733
                /\ 0 = mid_i:735 /\ __cost:66 = mid___cost:732)
               \/ (1 <= K:731 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= (-1 + -__cost:66)
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ (-mid_j:733 + mid_n:736) = 0
                     /\ 0 <= (-mid_i:735 + mid_j:733)
                     /\ 0 <= (-1 + -mid___cost:732)
                     /\ 0 <= (mid_i:735 + -mid_j:733
                                + ((-mid_i:735 + mid_j:733)
                                     * (-mid_i:735 + mid_j:733)))
                     /\ 0 <= (mid_i:735 + -mid_j:733
                                + ((-mid_i:735 + mid_j:733) * mid_i:735))
                     /\ 0 <= (-1 + mid_i:735)))
         /\ (0 = K:731 \/ !(-__cost:66 <= 0))
         /\ (!((0 <= K:737 /\ K:737 <= 0))
               \/ (-n':738 + j':739) = (-mid_n:736 + mid_j:733))
         /\ (!(1 <= K:737) \/ (-n':738 + j':739) = 0)
         /\ (!(0 <= K:737) \/ i':740 = (mid_i:735 + K:737))
         /\ (!(0 <= K:737)
               \/ (n':738 + __cost':741) = (mid_n:736 + mid___cost:732))
         /\ (!(0 <= K:737) \/ n':738 <= mid_n:736)
         /\ (!(0 <= K:737)
               \/ -n':738 <= (-mid_n:736 + (-1/2 * K:737)
                                + -((mid_i:735 * K:737))
                                + ((mid_n:736 + mid___cost:732) * K:737)
                                + (-1/2 * (K:737 * K:737))))
         /\ ((K:737 = 0 /\ mid_n:736 = n':738 /\ mid_j:733 = j':739
                /\ mid_i:735 = i':740 /\ mid___cost:732 = __cost':741)
               \/ (1 <= K:737 /\ 0 <= (-1 + -mid_i:735 + mid_n:736)
                     /\ 0 <= ((-1 + -mid_i:735 + mid_n:736) * mid___cost:732)
                     /\ 0 <= mid___cost:732
                     /\ 0 <= (1 + mid_i:735 + -mid_n:736
                                + ((-1 + -mid_i:735 + mid_n:736)
                                     * (-1 + -mid_i:735 + mid_n:736)))
                     /\ 0 <= (1 + mid_i:735 + -mid_n:736
                                + ((-1 + -mid_i:735 + mid_n:736)
                                     * (1 + mid_i:735))) /\ 0 <= mid_i:735
                     /\ (-n':738 + j':739) = 0 /\ 0 <= (-i':740 + n':738)
                     /\ 0 <= __cost':741 /\ 0 <= (-1 + i':740)))
         /\ (0 = K:737 \/ -mid___cost:732 <= 0) /\ (K:731 + K:737) = K:742
         /\ (!(0 <= K:743) \/ mid_i:744 = K:743)
         /\ (!(0 <= K:743) \/ mid___cost:745 = __cost:66)
         /\ (!((0 <= K:743 /\ K:743 <= 0))
               \/ (-mid_n:746 + mid_j:747) = (-param0:53 + j:734))
         /\ (!(1 <= K:743) \/ (-mid_n:746 + mid_j:747) = 0)
         /\ (!(0 <= K:743) \/ mid_n:746 = param0:53)
         /\ ((K:743 = 0 /\ param0:53 = mid_n:746 /\ j:734 = mid_j:747
                /\ 0 = mid_i:744 /\ __cost:66 = mid___cost:745)
               \/ (1 <= K:743 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= (-2 + -__cost:66)
                     /\ (-mid_n:746 + mid_j:747) = 0
                     /\ 0 <= (-2 + -mid___cost:745) /\ 0 <= (-1 + mid_i:744)
                     /\ 0 <= (mid_n:746 + -mid_i:744)))
         /\ (0 = K:743 \/ !((-1 + -__cost:66) <= 0))
         /\ (!((0 <= K:748 /\ K:748 <= 0))
               \/ (-n':738 + j':739) = (-mid_n:746 + mid_j:747))
         /\ (!(1 <= K:748) \/ (-n':738 + j':739) = 0)
         /\ (!(0 <= K:748) \/ i':740 = (mid_i:744 + K:748))
         /\ (!(0 <= K:748)
               \/ (n':738 + __cost':741) = (mid_n:746 + mid___cost:745))
         /\ (!(0 <= K:748) \/ n':738 <= mid_n:746)
         /\ (!(0 <= K:748)
               \/ -n':738 <= (-mid_n:746 + (1/2 * K:748)
                                + -((mid_i:744 * K:748))
                                + ((mid_n:746 + mid___cost:745) * K:748)
                                + (-1/2 * (K:748 * K:748))))
         /\ ((K:748 = 0 /\ mid_n:746 = n':738 /\ mid_j:747 = j':739
                /\ mid_i:744 = i':740 /\ mid___cost:745 = __cost':741)
               \/ (1 <= K:748 /\ 0 <= (-1 + -mid_i:744 + mid_n:746)
                     /\ 0 <= (-1 + -mid_i:744 + mid_n:746
                                + ((-1 + -mid_i:744 + mid_n:746)
                                     * mid___cost:745))
                     /\ 0 <= (1 + mid___cost:745)
                     /\ 0 <= (1 + mid_i:744 + -mid_n:746
                                + ((-1 + -mid_i:744 + mid_n:746)
                                     * (1 + mid_i:744)))
                     /\ 0 <= (1 + mid_i:744 + -mid_n:746
                                + ((-1 + -mid_i:744 + mid_n:746)
                                     * (-1 + -mid_i:744 + mid_n:746)))
                     /\ 0 <= mid_i:744 /\ (-n':738 + j':739) = 0
                     /\ 0 <= (-i':740 + n':738) /\ 0 <= (1 + __cost':741)
                     /\ 0 <= (-1 + i':740)))
         /\ (0 = K:748 \/ (-1 + -mid___cost:745) <= 0)
         /\ (K:743 + K:748) = K:742
         /\ (!((0 <= K:749 /\ K:749 <= 0))
               \/ (-mid_n:750 + mid_j:751) = (-param0:53 + j:734))
         /\ (!(1 <= K:749) \/ (-mid_n:750 + mid_j:751) = 0)
         /\ (!(0 <= K:749) \/ mid_i:752 = K:749)
         /\ (!(0 <= K:749)
               \/ (mid_n:750 + mid___cost:753) = (param0:53 + __cost:66))
         /\ (!(0 <= K:749) \/ mid_n:750 <= param0:53)
         /\ ((K:749 = 0 /\ param0:53 = mid_n:750 /\ j:734 = mid_j:751
                /\ 0 = mid_i:752 /\ __cost:66 = mid___cost:753)
               \/ (1 <= K:749 /\ 0 <= (-2 + param0:53)
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ (-mid_n:750 + mid_j:751) = 0
                     /\ 0 <= (-mid_i:752 + mid_n:750)
                     /\ 0 <= (-1 + mid_i:752)))
         /\ (0 = K:749 \/ (2 + -param0:53) <= 0)
         /\ (!((0 <= K:754 /\ K:754 <= 0)) \/ j':739 = (mid_j:751 + K:754))
         /\ (!(1 <= K:754)
               \/ j':739 = (mid_j:751 + mid_i:752 + -mid_j:751 + K:754))
         /\ (!((0 <= K:754 /\ K:754 <= 0)) \/ n':738 = (mid_n:750 + K:754))
         /\ (!(1 <= K:754)
               \/ n':738 = (mid_n:750 + mid_i:752 + -mid_n:750 + K:754))
         /\ (!(0 <= K:754) \/ __cost':741 = mid___cost:753)
         /\ (!(0 <= K:754) \/ i':740 = (mid_i:752 + K:754))
         /\ (!((0 <= K:754 /\ K:754 <= 0))
               \/ -j':739 <= (-mid_j:751 + (-3/2 * K:754)
                                + (mid_i:752 * K:754)
                                + (1/2 * (K:754 * K:754))))
         /\ (!(1 <= K:754)
               \/ -j':739 <= (mid_j:751 + -mid_j:751 + -mid_i:752
                                + (-3/2 * K:754) + (mid_i:752 * K:754)
                                + (1/2 * (K:754 * K:754))))
         /\ ((K:754 = 0 /\ mid_n:750 = n':738 /\ mid_j:751 = j':739
                /\ mid_i:752 = i':740 /\ mid___cost:753 = __cost':741)
               \/ (1 <= K:754 /\ (-1 + -mid_i:752 + mid_n:750) = 0
                     /\ 0 <= mid_i:752 /\ (-j':739 + n':738) = 0
                     /\ (-j':739 + i':740) = 0 /\ 0 <= (-1 + j':739)))
         /\ (0 = K:754 \/ !((2 + mid_i:752 + -mid_n:750) <= 0))
         /\ (K:749 + K:754) = K:742 /\ (!(0 <= K:755) \/ mid_i:756 = K:755)
         /\ (!(0 <= K:755)
               \/ (mid_n:757 + mid___cost:758) = (param0:53 + __cost:66))
         /\ (!((0 <= K:755 /\ K:755 <= 0))
               \/ (-mid_n:757 + mid_j:759) = (-param0:53 + j:734))
         /\ (!(1 <= K:755) \/ (-mid_n:757 + mid_j:759) = 0)
         /\ (!(0 <= K:755) \/ mid_n:757 <= param0:53)
         /\ (!(0 <= K:755)
               \/ -mid_n:757 <= (-param0:53 + (-1/2 * K:755)
                                   + ((param0:53 + __cost:66) * K:755)
                                   + (-1/2 * (K:755 * K:755))))
         /\ ((K:755 = 0 /\ param0:53 = mid_n:757 /\ j:734 = mid_j:759
                /\ 0 = mid_i:756 /\ __cost:66 = mid___cost:758)
               \/ (1 <= K:755 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= ((-1 + param0:53) * __cost:66) /\ 0 <= __cost:66
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ (-mid_n:757 + mid_j:759) = 0 /\ 0 <= mid___cost:758
                     /\ 0 <= (-1 + mid_i:756)
                     /\ 0 <= (mid_n:757 + -mid_i:756)))
         /\ (0 = K:755 \/ !((1 + __cost:66) <= 0))
         /\ (!(0 <= K:760) \/ __cost':741 = mid___cost:758)
         /\ (!(0 <= K:760) \/ n':738 = mid_n:757)
         /\ (!(0 <= K:760) \/ i':740 = (mid_i:756 + K:760))
         /\ (!((0 <= K:760 /\ K:760 <= 0)) \/ j':739 = mid_j:759)
         /\ (!(1 <= K:760) \/ j':739 = mid_n:757)
         /\ ((K:760 = 0 /\ mid_n:757 = n':738 /\ mid_j:759 = j':739
                /\ mid_i:756 = i':740 /\ mid___cost:758 = __cost':741)
               \/ (1 <= K:760 /\ 0 <= (-1 + -mid_i:756 + mid_n:757)
                     /\ 0 <= (-1 + -mid___cost:758)
                     /\ 0 <= (1 + mid_i:756 + -mid_n:757
                                + ((-1 + -mid_i:756 + mid_n:757)
                                     * (-1 + -mid_i:756 + mid_n:757)))
                     /\ 0 <= (1 + mid_i:756 + -mid_n:757
                                + ((-1 + -mid_i:756 + mid_n:757)
                                     * (1 + mid_i:756))) /\ 0 <= mid_i:756
                     /\ (-n':738 + j':739) = 0 /\ 0 <= (-i':740 + n':738)
                     /\ 0 <= (-1 + -__cost':741)
                     /\ 0 <= (i':740 + -n':738
                                + ((-i':740 + n':738) * (-i':740 + n':738)))
                     /\ 0 <= (i':740 + -n':738
                                + ((-i':740 + n':738) * i':740))
                     /\ 0 <= (-1 + i':740)))
         /\ (0 = K:760 \/ (1 + mid___cost:758) <= 0)
         /\ (K:755 + K:760) = K:742
         /\ (!(0 <= K:761)
               \/ (mid_n:762 + mid___cost:763) = (param0:53 + __cost:66))
         /\ (!((0 <= K:761 /\ K:761 <= 0))
               \/ (-mid_n:762 + mid_j:764) = (-param0:53 + j:734))
         /\ (!(1 <= K:761) \/ (-mid_n:762 + mid_j:764) = 0)
         /\ (!(0 <= K:761) \/ mid_i:765 = K:761)
         /\ (!(0 <= K:761) \/ mid_n:762 <= param0:53)
         /\ (!(0 <= K:761)
               \/ -mid_n:762 <= (-param0:53 + (1/2 * K:761)
                                   + ((param0:53 + __cost:66) * K:761)
                                   + (-1/2 * (K:761 * K:761))))
         /\ ((K:761 = 0 /\ param0:53 = mid_n:762 /\ j:734 = mid_j:764
                /\ 0 = mid_i:765 /\ __cost:66 = mid___cost:763)
               \/ (1 <= K:761 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= (-1 + param0:53 + ((-1 + param0:53) * __cost:66))
                     /\ 0 <= (1 + __cost:66)
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ (-mid_n:762 + mid_j:764) = 0
                     /\ 0 <= (-mid_i:765 + mid_n:762)
                     /\ 0 <= (1 + mid___cost:763) /\ 0 <= (-1 + mid_i:765)))
         /\ (0 = K:761 \/ !((2 + __cost:66) <= 0))
         /\ (!(0 <= K:766) \/ i':740 = (mid_i:765 + K:766))
         /\ (!(0 <= K:766) \/ __cost':741 = mid___cost:763)
         /\ (!((0 <= K:766 /\ K:766 <= 0))
               \/ (-n':738 + j':739) = (-mid_n:762 + mid_j:764))
         /\ (!(1 <= K:766) \/ (-n':738 + j':739) = 0)
         /\ (!(0 <= K:766) \/ n':738 = mid_n:762)
         /\ ((K:766 = 0 /\ mid_n:762 = n':738 /\ mid_j:764 = j':739
                /\ mid_i:765 = i':740 /\ mid___cost:763 = __cost':741)
               \/ (1 <= K:766 /\ 0 <= (-1 + -mid_i:765 + mid_n:762)
                     /\ 0 <= (-2 + -mid___cost:763) /\ 0 <= mid_i:765
                     /\ (-n':738 + j':739) = 0 /\ 0 <= (-2 + -__cost':741)
                     /\ 0 <= (-1 + i':740) /\ 0 <= (n':738 + -i':740)))
         /\ (0 = K:766 \/ (2 + mid___cost:763) <= 0)
         /\ (K:761 + K:766) = K:742 /\ 0 <= K:742 /\ 0 <= i':740
         /\ n':738 <= i':740)}

Evaluating variable number 20 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':587
 return := havoc:641
 return@pos := type_err:642
 return@width := type_err:643
 when ((!(0 <= K:578) \/ mid___cost:579 = __cost:66)
         /\ (!((0 <= K:578 /\ K:578 <= 0)) \/ mid_j:580 = j:644)
         /\ (!(1 <= K:578) \/ mid_j:580 = (j:644 + param0:53 + -j:644))
         /\ (!(0 <= K:578) \/ mid_i:581 = K:578)
         /\ (!(0 <= K:578) \/ mid_n:582 = param0:53)
         /\ (!((0 <= K:578 /\ K:578 <= 0))
               \/ -mid_j:580 <= (-j:644 + (-1/2 * K:578)
                                   + (param0:53 * K:578)
                                   + (-1/2 * (K:578 * K:578))))
         /\ (!(1 <= K:578)
               \/ -mid_j:580 <= (j:644 + -j:644 + -param0:53 + (-1/2 * K:578)
                                   + (param0:53 * K:578)
                                   + (-1/2 * (K:578 * K:578))))
         /\ ((K:578 = 0 /\ param0:53 = mid_n:582 /\ j:644 = mid_j:580
                /\ 0 = mid_i:581 /\ __cost:66 = mid___cost:579)
               \/ (1 <= K:578 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= (-1 + -__cost:66)
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ (-mid_j:580 + mid_n:582) = 0
                     /\ 0 <= (-mid_i:581 + mid_j:580)
                     /\ 0 <= (-1 + -mid___cost:579)
                     /\ 0 <= (mid_i:581 + -mid_j:580
                                + ((-mid_i:581 + mid_j:580)
                                     * (-mid_i:581 + mid_j:580)))
                     /\ 0 <= (mid_i:581 + -mid_j:580
                                + ((-mid_i:581 + mid_j:580) * mid_i:581))
                     /\ 0 <= (-1 + mid_i:581)))
         /\ (0 = K:578 \/ !(-__cost:66 <= 0))
         /\ (!((0 <= K:583 /\ K:583 <= 0))
               \/ (-n':584 + j':585) = (-mid_n:582 + mid_j:580))
         /\ (!(1 <= K:583) \/ (-n':584 + j':585) = 0)
         /\ (!(0 <= K:583) \/ i':586 = (mid_i:581 + K:583))
         /\ (!(0 <= K:583)
               \/ (n':584 + __cost':587) = (mid_n:582 + mid___cost:579))
         /\ (!(0 <= K:583) \/ n':584 <= mid_n:582)
         /\ (!(0 <= K:583)
               \/ -n':584 <= (-mid_n:582 + (-1/2 * K:583)
                                + -((mid_i:581 * K:583))
                                + ((mid_n:582 + mid___cost:579) * K:583)
                                + (-1/2 * (K:583 * K:583))))
         /\ ((K:583 = 0 /\ mid_n:582 = n':584 /\ mid_j:580 = j':585
                /\ mid_i:581 = i':586 /\ mid___cost:579 = __cost':587)
               \/ (1 <= K:583 /\ 0 <= (-1 + -mid_i:581 + mid_n:582)
                     /\ 0 <= ((-1 + -mid_i:581 + mid_n:582) * mid___cost:579)
                     /\ 0 <= mid___cost:579
                     /\ 0 <= (1 + mid_i:581 + -mid_n:582
                                + ((-1 + -mid_i:581 + mid_n:582)
                                     * (-1 + -mid_i:581 + mid_n:582)))
                     /\ 0 <= (1 + mid_i:581 + -mid_n:582
                                + ((-1 + -mid_i:581 + mid_n:582)
                                     * (1 + mid_i:581))) /\ 0 <= mid_i:581
                     /\ (-n':584 + j':585) = 0 /\ 0 <= (-i':586 + n':584)
                     /\ 0 <= __cost':587 /\ 0 <= (-1 + i':586)))
         /\ (0 = K:583 \/ -mid___cost:579 <= 0) /\ (K:578 + K:583) = K:588
         /\ (!(0 <= K:589) \/ mid_i:590 = K:589)
         /\ (!(0 <= K:589) \/ mid___cost:591 = __cost:66)
         /\ (!((0 <= K:589 /\ K:589 <= 0))
               \/ (-mid_n:592 + mid_j:593) = (-param0:53 + j:644))
         /\ (!(1 <= K:589) \/ (-mid_n:592 + mid_j:593) = 0)
         /\ (!(0 <= K:589) \/ mid_n:592 = param0:53)
         /\ ((K:589 = 0 /\ param0:53 = mid_n:592 /\ j:644 = mid_j:593
                /\ 0 = mid_i:590 /\ __cost:66 = mid___cost:591)
               \/ (1 <= K:589 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= (-2 + -__cost:66)
                     /\ (-mid_n:592 + mid_j:593) = 0
                     /\ 0 <= (-2 + -mid___cost:591) /\ 0 <= (-1 + mid_i:590)
                     /\ 0 <= (mid_n:592 + -mid_i:590)))
         /\ (0 = K:589 \/ !((-1 + -__cost:66) <= 0))
         /\ (!((0 <= K:594 /\ K:594 <= 0))
               \/ (-n':584 + j':585) = (-mid_n:592 + mid_j:593))
         /\ (!(1 <= K:594) \/ (-n':584 + j':585) = 0)
         /\ (!(0 <= K:594) \/ i':586 = (mid_i:590 + K:594))
         /\ (!(0 <= K:594)
               \/ (n':584 + __cost':587) = (mid_n:592 + mid___cost:591))
         /\ (!(0 <= K:594) \/ n':584 <= mid_n:592)
         /\ (!(0 <= K:594)
               \/ -n':584 <= (-mid_n:592 + (1/2 * K:594)
                                + -((mid_i:590 * K:594))
                                + ((mid_n:592 + mid___cost:591) * K:594)
                                + (-1/2 * (K:594 * K:594))))
         /\ ((K:594 = 0 /\ mid_n:592 = n':584 /\ mid_j:593 = j':585
                /\ mid_i:590 = i':586 /\ mid___cost:591 = __cost':587)
               \/ (1 <= K:594 /\ 0 <= (-1 + -mid_i:590 + mid_n:592)
                     /\ 0 <= (-1 + -mid_i:590 + mid_n:592
                                + ((-1 + -mid_i:590 + mid_n:592)
                                     * mid___cost:591))
                     /\ 0 <= (1 + mid___cost:591)
                     /\ 0 <= (1 + mid_i:590 + -mid_n:592
                                + ((-1 + -mid_i:590 + mid_n:592)
                                     * (1 + mid_i:590)))
                     /\ 0 <= (1 + mid_i:590 + -mid_n:592
                                + ((-1 + -mid_i:590 + mid_n:592)
                                     * (-1 + -mid_i:590 + mid_n:592)))
                     /\ 0 <= mid_i:590 /\ (-n':584 + j':585) = 0
                     /\ 0 <= (-i':586 + n':584) /\ 0 <= (1 + __cost':587)
                     /\ 0 <= (-1 + i':586)))
         /\ (0 = K:594 \/ (-1 + -mid___cost:591) <= 0)
         /\ (K:589 + K:594) = K:588
         /\ (!((0 <= K:595 /\ K:595 <= 0))
               \/ (-mid_n:596 + mid_j:597) = (-param0:53 + j:644))
         /\ (!(1 <= K:595) \/ (-mid_n:596 + mid_j:597) = 0)
         /\ (!(0 <= K:595) \/ mid_i:598 = K:595)
         /\ (!(0 <= K:595)
               \/ (mid_n:596 + mid___cost:599) = (param0:53 + __cost:66))
         /\ (!(0 <= K:595) \/ mid_n:596 <= param0:53)
         /\ ((K:595 = 0 /\ param0:53 = mid_n:596 /\ j:644 = mid_j:597
                /\ 0 = mid_i:598 /\ __cost:66 = mid___cost:599)
               \/ (1 <= K:595 /\ 0 <= (-2 + param0:53)
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ (-mid_n:596 + mid_j:597) = 0
                     /\ 0 <= (-mid_i:598 + mid_n:596)
                     /\ 0 <= (-1 + mid_i:598)))
         /\ (0 = K:595 \/ (2 + -param0:53) <= 0)
         /\ (!((0 <= K:600 /\ K:600 <= 0)) \/ j':585 = (mid_j:597 + K:600))
         /\ (!(1 <= K:600)
               \/ j':585 = (mid_j:597 + mid_i:598 + -mid_j:597 + K:600))
         /\ (!((0 <= K:600 /\ K:600 <= 0)) \/ n':584 = (mid_n:596 + K:600))
         /\ (!(1 <= K:600)
               \/ n':584 = (mid_n:596 + mid_i:598 + -mid_n:596 + K:600))
         /\ (!(0 <= K:600) \/ __cost':587 = mid___cost:599)
         /\ (!(0 <= K:600) \/ i':586 = (mid_i:598 + K:600))
         /\ (!((0 <= K:600 /\ K:600 <= 0))
               \/ -j':585 <= (-mid_j:597 + (-3/2 * K:600)
                                + (mid_i:598 * K:600)
                                + (1/2 * (K:600 * K:600))))
         /\ (!(1 <= K:600)
               \/ -j':585 <= (mid_j:597 + -mid_j:597 + -mid_i:598
                                + (-3/2 * K:600) + (mid_i:598 * K:600)
                                + (1/2 * (K:600 * K:600))))
         /\ ((K:600 = 0 /\ mid_n:596 = n':584 /\ mid_j:597 = j':585
                /\ mid_i:598 = i':586 /\ mid___cost:599 = __cost':587)
               \/ (1 <= K:600 /\ (-1 + -mid_i:598 + mid_n:596) = 0
                     /\ 0 <= mid_i:598 /\ (-j':585 + n':584) = 0
                     /\ (-j':585 + i':586) = 0 /\ 0 <= (-1 + j':585)))
         /\ (0 = K:600 \/ !((2 + mid_i:598 + -mid_n:596) <= 0))
         /\ (K:595 + K:600) = K:588 /\ (!(0 <= K:601) \/ mid_i:602 = K:601)
         /\ (!(0 <= K:601)
               \/ (mid_n:603 + mid___cost:604) = (param0:53 + __cost:66))
         /\ (!((0 <= K:601 /\ K:601 <= 0))
               \/ (-mid_n:603 + mid_j:605) = (-param0:53 + j:644))
         /\ (!(1 <= K:601) \/ (-mid_n:603 + mid_j:605) = 0)
         /\ (!(0 <= K:601) \/ mid_n:603 <= param0:53)
         /\ (!(0 <= K:601)
               \/ -mid_n:603 <= (-param0:53 + (-1/2 * K:601)
                                   + ((param0:53 + __cost:66) * K:601)
                                   + (-1/2 * (K:601 * K:601))))
         /\ ((K:601 = 0 /\ param0:53 = mid_n:603 /\ j:644 = mid_j:605
                /\ 0 = mid_i:602 /\ __cost:66 = mid___cost:604)
               \/ (1 <= K:601 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= ((-1 + param0:53) * __cost:66) /\ 0 <= __cost:66
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ (-mid_n:603 + mid_j:605) = 0 /\ 0 <= mid___cost:604
                     /\ 0 <= (-1 + mid_i:602)
                     /\ 0 <= (mid_n:603 + -mid_i:602)))
         /\ (0 = K:601 \/ !((1 + __cost:66) <= 0))
         /\ (!(0 <= K:606) \/ __cost':587 = mid___cost:604)
         /\ (!(0 <= K:606) \/ n':584 = mid_n:603)
         /\ (!(0 <= K:606) \/ i':586 = (mid_i:602 + K:606))
         /\ (!((0 <= K:606 /\ K:606 <= 0)) \/ j':585 = mid_j:605)
         /\ (!(1 <= K:606) \/ j':585 = mid_n:603)
         /\ ((K:606 = 0 /\ mid_n:603 = n':584 /\ mid_j:605 = j':585
                /\ mid_i:602 = i':586 /\ mid___cost:604 = __cost':587)
               \/ (1 <= K:606 /\ 0 <= (-1 + -mid_i:602 + mid_n:603)
                     /\ 0 <= (-1 + -mid___cost:604)
                     /\ 0 <= (1 + mid_i:602 + -mid_n:603
                                + ((-1 + -mid_i:602 + mid_n:603)
                                     * (-1 + -mid_i:602 + mid_n:603)))
                     /\ 0 <= (1 + mid_i:602 + -mid_n:603
                                + ((-1 + -mid_i:602 + mid_n:603)
                                     * (1 + mid_i:602))) /\ 0 <= mid_i:602
                     /\ (-n':584 + j':585) = 0 /\ 0 <= (-i':586 + n':584)
                     /\ 0 <= (-1 + -__cost':587)
                     /\ 0 <= (i':586 + -n':584
                                + ((-i':586 + n':584) * (-i':586 + n':584)))
                     /\ 0 <= (i':586 + -n':584
                                + ((-i':586 + n':584) * i':586))
                     /\ 0 <= (-1 + i':586)))
         /\ (0 = K:606 \/ (1 + mid___cost:604) <= 0)
         /\ (K:601 + K:606) = K:588
         /\ (!(0 <= K:607)
               \/ (mid_n:608 + mid___cost:609) = (param0:53 + __cost:66))
         /\ (!((0 <= K:607 /\ K:607 <= 0))
               \/ (-mid_n:608 + mid_j:610) = (-param0:53 + j:644))
         /\ (!(1 <= K:607) \/ (-mid_n:608 + mid_j:610) = 0)
         /\ (!(0 <= K:607) \/ mid_i:611 = K:607)
         /\ (!(0 <= K:607) \/ mid_n:608 <= param0:53)
         /\ (!(0 <= K:607)
               \/ -mid_n:608 <= (-param0:53 + (1/2 * K:607)
                                   + ((param0:53 + __cost:66) * K:607)
                                   + (-1/2 * (K:607 * K:607))))
         /\ ((K:607 = 0 /\ param0:53 = mid_n:608 /\ j:644 = mid_j:610
                /\ 0 = mid_i:611 /\ __cost:66 = mid___cost:609)
               \/ (1 <= K:607 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= (-1 + param0:53 + ((-1 + param0:53) * __cost:66))
                     /\ 0 <= (1 + __cost:66)
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ (-mid_n:608 + mid_j:610) = 0
                     /\ 0 <= (-mid_i:611 + mid_n:608)
                     /\ 0 <= (1 + mid___cost:609) /\ 0 <= (-1 + mid_i:611)))
         /\ (0 = K:607 \/ !((2 + __cost:66) <= 0))
         /\ (!(0 <= K:612) \/ i':586 = (mid_i:611 + K:612))
         /\ (!(0 <= K:612) \/ __cost':587 = mid___cost:609)
         /\ (!((0 <= K:612 /\ K:612 <= 0))
               \/ (-n':584 + j':585) = (-mid_n:608 + mid_j:610))
         /\ (!(1 <= K:612) \/ (-n':584 + j':585) = 0)
         /\ (!(0 <= K:612) \/ n':584 = mid_n:608)
         /\ ((K:612 = 0 /\ mid_n:608 = n':584 /\ mid_j:610 = j':585
                /\ mid_i:611 = i':586 /\ mid___cost:609 = __cost':587)
               \/ (1 <= K:612 /\ 0 <= (-1 + -mid_i:611 + mid_n:608)
                     /\ 0 <= (-2 + -mid___cost:609) /\ 0 <= mid_i:611
                     /\ (-n':584 + j':585) = 0 /\ 0 <= (-2 + -__cost':587)
                     /\ 0 <= (-1 + i':586) /\ 0 <= (n':584 + -i':586)))
         /\ (0 = K:612 \/ (2 + mid___cost:609) <= 0)
         /\ (K:607 + K:612) = K:588 /\ 0 <= K:588 /\ 0 <= i':586
         /\ n':584 <= i':586)}

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

NumRnds: 1

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

Weights on states: 
__pstate 0xc853b90: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0xb9b9770: 
	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,61)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:859
 param0@width := type_err:860}
    ( __pstate , (Unique State Name,65)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}

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

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

Base relation: 
{__cost := __cost':783
 n := havoc:13
 return := 0
 param0 := havoc:13
 return@pos := type_err:815
 param0@pos := type_err:811
 return@width := type_err:816
 param0@width := type_err:813
 when ((!(0 <= K:773) \/ mid___cost:774 = 0)
         /\ (!((0 <= K:773 /\ K:773 <= 0)) \/ mid_j:775 = j:776)
         /\ (!(1 <= K:773) \/ mid_j:775 = (j:776 + havoc:13 + -j:776))
         /\ (!(0 <= K:773) \/ mid_i:777 = K:773)
         /\ (!(0 <= K:773) \/ mid_n:778 = havoc:13)
         /\ (!((0 <= K:773 /\ K:773 <= 0))
               \/ -mid_j:775 <= (-j:776 + (-1/2 * K:773) + (havoc:13 * K:773)
                                   + (-1/2 * (K:773 * K:773))))
         /\ (!(1 <= K:773)
               \/ -mid_j:775 <= (j:776 + -j:776 + -havoc:13 + (-1/2 * K:773)
                                   + (havoc:13 * K:773)
                                   + (-1/2 * (K:773 * K:773)))) /\ K:773 = 0
         /\ havoc:13 = mid_n:778 /\ j:776 = mid_j:775 /\ 0 = mid_i:777
         /\ 0 = mid___cost:774 /\ 0 = K:773
         /\ (!((0 <= K:779 /\ K:779 <= 0))
               \/ (-n':780 + j':781) = (-mid_n:778 + mid_j:775))
         /\ (!(1 <= K:779) \/ (-n':780 + j':781) = 0)
         /\ (!(0 <= K:779) \/ i':782 = (mid_i:777 + K:779))
         /\ (!(0 <= K:779)
               \/ (n':780 + __cost':783) = (mid_n:778 + mid___cost:774))
         /\ (!(0 <= K:779) \/ n':780 <= mid_n:778)
         /\ (!(0 <= K:779)
               \/ -n':780 <= (-mid_n:778 + (-1/2 * K:779)
                                + -((mid_i:777 * K:779))
                                + ((mid_n:778 + mid___cost:774) * K:779)
                                + (-1/2 * (K:779 * K:779))))
         /\ ((K:779 = 0 /\ mid_n:778 = n':780 /\ mid_j:775 = j':781
                /\ mid_i:777 = i':782 /\ mid___cost:774 = __cost':783)
               \/ (1 <= K:779 /\ 0 <= (-1 + -mid_i:777 + mid_n:778)
                     /\ 0 <= ((-1 + -mid_i:777 + mid_n:778) * mid___cost:774)
                     /\ 0 <= mid___cost:774
                     /\ 0 <= (1 + mid_i:777 + -mid_n:778
                                + ((-1 + -mid_i:777 + mid_n:778)
                                     * (-1 + -mid_i:777 + mid_n:778)))
                     /\ 0 <= (1 + mid_i:777 + -mid_n:778
                                + ((-1 + -mid_i:777 + mid_n:778)
                                     * (1 + mid_i:777))) /\ 0 <= mid_i:777
                     /\ (-n':780 + j':781) = 0 /\ 0 <= (-i':782 + n':780)
                     /\ 0 <= __cost':783 /\ 0 <= (-1 + i':782)))
         /\ (0 = K:779 \/ -mid___cost:774 <= 0) /\ (K:773 + K:779) = K:784
         /\ (!(0 <= K:785) \/ mid_i:786 = K:785)
         /\ (!(0 <= K:785) \/ mid___cost:787 = 0)
         /\ (!((0 <= K:785 /\ K:785 <= 0))
               \/ (-mid_n:788 + mid_j:789) = (-havoc:13 + j:776))
         /\ (!(1 <= K:785) \/ (-mid_n:788 + mid_j:789) = 0)
         /\ (!(0 <= K:785) \/ mid_n:788 = havoc:13) /\ K:785 = 0
         /\ havoc:13 = mid_n:788 /\ j:776 = mid_j:789 /\ 0 = mid_i:786
         /\ 0 = mid___cost:787 /\ 0 = K:785
         /\ (!((0 <= K:790 /\ K:790 <= 0))
               \/ (-n':780 + j':781) = (-mid_n:788 + mid_j:789))
         /\ (!(1 <= K:790) \/ (-n':780 + j':781) = 0)
         /\ (!(0 <= K:790) \/ i':782 = (mid_i:786 + K:790))
         /\ (!(0 <= K:790)
               \/ (n':780 + __cost':783) = (mid_n:788 + mid___cost:787))
         /\ (!(0 <= K:790) \/ n':780 <= mid_n:788)
         /\ (!(0 <= K:790)
               \/ -n':780 <= (-mid_n:788 + (1/2 * K:790)
                                + -((mid_i:786 * K:790))
                                + ((mid_n:788 + mid___cost:787) * K:790)
                                + (-1/2 * (K:790 * K:790))))
         /\ ((K:790 = 0 /\ mid_n:788 = n':780 /\ mid_j:789 = j':781
                /\ mid_i:786 = i':782 /\ mid___cost:787 = __cost':783)
               \/ (1 <= K:790 /\ 0 <= (-1 + -mid_i:786 + mid_n:788)
                     /\ 0 <= (-1 + -mid_i:786 + mid_n:788
                                + ((-1 + -mid_i:786 + mid_n:788)
                                     * mid___cost:787))
                     /\ 0 <= (1 + mid___cost:787)
                     /\ 0 <= (1 + mid_i:786 + -mid_n:788
                                + ((-1 + -mid_i:786 + mid_n:788)
                                     * (1 + mid_i:786)))
                     /\ 0 <= (1 + mid_i:786 + -mid_n:788
                                + ((-1 + -mid_i:786 + mid_n:788)
                                     * (-1 + -mid_i:786 + mid_n:788)))
                     /\ 0 <= mid_i:786 /\ (-n':780 + j':781) = 0
                     /\ 0 <= (-i':782 + n':780) /\ 0 <= (1 + __cost':783)
                     /\ 0 <= (-1 + i':782)))
         /\ (0 = K:790 \/ (-1 + -mid___cost:787) <= 0)
         /\ (K:785 + K:790) = K:784
         /\ (!((0 <= K:791 /\ K:791 <= 0))
               \/ (-mid_n:792 + mid_j:793) = (-havoc:13 + j:776))
         /\ (!(1 <= K:791) \/ (-mid_n:792 + mid_j:793) = 0)
         /\ (!(0 <= K:791) \/ mid_i:794 = K:791)
         /\ (!(0 <= K:791) \/ (mid_n:792 + mid___cost:795) = havoc:13)
         /\ (!(0 <= K:791) \/ mid_n:792 <= havoc:13)
         /\ ((K:791 = 0 /\ havoc:13 = mid_n:792 /\ j:776 = mid_j:793
                /\ 0 = mid_i:794 /\ 0 = mid___cost:795)
               \/ (1 <= K:791 /\ 0 <= (-2 + havoc:13)
                     /\ 0 <= (1 + -havoc:13 + (-1 + havoc:13))
                     /\ 0 <= (1 + -havoc:13
                                + ((-1 + havoc:13) * (-1 + havoc:13)))
                     /\ (-mid_n:792 + mid_j:793) = 0
                     /\ 0 <= (-mid_i:794 + mid_n:792)
                     /\ 0 <= (-1 + mid_i:794)))
         /\ (0 = K:791 \/ (2 + -havoc:13) <= 0)
         /\ (!((0 <= K:796 /\ K:796 <= 0)) \/ j':781 = (mid_j:793 + K:796))
         /\ (!(1 <= K:796)
               \/ j':781 = (mid_j:793 + mid_i:794 + -mid_j:793 + K:796))
         /\ (!((0 <= K:796 /\ K:796 <= 0)) \/ n':780 = (mid_n:792 + K:796))
         /\ (!(1 <= K:796)
               \/ n':780 = (mid_n:792 + mid_i:794 + -mid_n:792 + K:796))
         /\ (!(0 <= K:796) \/ __cost':783 = mid___cost:795)
         /\ (!(0 <= K:796) \/ i':782 = (mid_i:794 + K:796))
         /\ (!((0 <= K:796 /\ K:796 <= 0))
               \/ -j':781 <= (-mid_j:793 + (-3/2 * K:796)
                                + (mid_i:794 * K:796)
                                + (1/2 * (K:796 * K:796))))
         /\ (!(1 <= K:796)
               \/ -j':781 <= (mid_j:793 + -mid_j:793 + -mid_i:794
                                + (-3/2 * K:796) + (mid_i:794 * K:796)
                                + (1/2 * (K:796 * K:796))))
         /\ ((K:796 = 0 /\ mid_n:792 = n':780 /\ mid_j:793 = j':781
                /\ mid_i:794 = i':782 /\ mid___cost:795 = __cost':783)
               \/ (1 <= K:796 /\ (-1 + -mid_i:794 + mid_n:792) = 0
                     /\ 0 <= mid_i:794 /\ (-j':781 + n':780) = 0
                     /\ (-j':781 + i':782) = 0 /\ 0 <= (-1 + j':781)))
         /\ (0 = K:796 \/ !((2 + mid_i:794 + -mid_n:792) <= 0))
         /\ (K:791 + K:796) = K:784 /\ (!(0 <= K:797) \/ mid_i:798 = K:797)
         /\ (!(0 <= K:797) \/ (mid_n:799 + mid___cost:800) = havoc:13)
         /\ (!((0 <= K:797 /\ K:797 <= 0))
               \/ (-mid_n:799 + mid_j:801) = (-havoc:13 + j:776))
         /\ (!(1 <= K:797) \/ (-mid_n:799 + mid_j:801) = 0)
         /\ (!(0 <= K:797) \/ mid_n:799 <= havoc:13)
         /\ (!(0 <= K:797)
               \/ -mid_n:799 <= (-havoc:13 + (-1/2 * K:797)
                                   + (havoc:13 * K:797)
                                   + (-1/2 * (K:797 * K:797))))
         /\ ((K:797 = 0 /\ havoc:13 = mid_n:799 /\ j:776 = mid_j:801
                /\ 0 = mid_i:798 /\ 0 = mid___cost:800)
               \/ (1 <= K:797 /\ 0 <= (-1 + havoc:13)
                     /\ 0 <= (1 + -havoc:13
                                + ((-1 + havoc:13) * (-1 + havoc:13)))
                     /\ 0 <= (1 + -havoc:13 + (-1 + havoc:13))
                     /\ (-mid_n:799 + mid_j:801) = 0 /\ 0 <= mid___cost:800
                     /\ 0 <= (-1 + mid_i:798)
                     /\ 0 <= (mid_n:799 + -mid_i:798)))
         /\ (!(0 <= K:802) \/ __cost':783 = mid___cost:800)
         /\ (!(0 <= K:802) \/ n':780 = mid_n:799)
         /\ (!(0 <= K:802) \/ i':782 = (mid_i:798 + K:802))
         /\ (!((0 <= K:802 /\ K:802 <= 0)) \/ j':781 = mid_j:801)
         /\ (!(1 <= K:802) \/ j':781 = mid_n:799)
         /\ ((K:802 = 0 /\ mid_n:799 = n':780 /\ mid_j:801 = j':781
                /\ mid_i:798 = i':782 /\ mid___cost:800 = __cost':783)
               \/ (1 <= K:802 /\ 0 <= (-1 + -mid_i:798 + mid_n:799)
                     /\ 0 <= (-1 + -mid___cost:800)
                     /\ 0 <= (1 + mid_i:798 + -mid_n:799
                                + ((-1 + -mid_i:798 + mid_n:799)
                                     * (-1 + -mid_i:798 + mid_n:799)))
                     /\ 0 <= (1 + mid_i:798 + -mid_n:799
                                + ((-1 + -mid_i:798 + mid_n:799)
                                     * (1 + mid_i:798))) /\ 0 <= mid_i:798
                     /\ (-n':780 + j':781) = 0 /\ 0 <= (-i':782 + n':780)
                     /\ 0 <= (-1 + -__cost':783)
                     /\ 0 <= (i':782 + -n':780
                                + ((-i':782 + n':780) * (-i':782 + n':780)))
                     /\ 0 <= (i':782 + -n':780
                                + ((-i':782 + n':780) * i':782))
                     /\ 0 <= (-1 + i':782)))
         /\ (0 = K:802 \/ (1 + mid___cost:800) <= 0)
         /\ (K:797 + K:802) = K:784
         /\ (!(0 <= K:803) \/ (mid_n:804 + mid___cost:805) = havoc:13)
         /\ (!((0 <= K:803 /\ K:803 <= 0))
               \/ (-mid_n:804 + mid_j:806) = (-havoc:13 + j:776))
         /\ (!(1 <= K:803) \/ (-mid_n:804 + mid_j:806) = 0)
         /\ (!(0 <= K:803) \/ mid_i:807 = K:803)
         /\ (!(0 <= K:803) \/ mid_n:804 <= havoc:13)
         /\ (!(0 <= K:803)
               \/ -mid_n:804 <= (-havoc:13 + (1/2 * K:803)
                                   + (havoc:13 * K:803)
                                   + (-1/2 * (K:803 * K:803))))
         /\ ((K:803 = 0 /\ havoc:13 = mid_n:804 /\ j:776 = mid_j:806
                /\ 0 = mid_i:807 /\ 0 = mid___cost:805)
               \/ (1 <= K:803 /\ 0 <= (-1 + havoc:13) /\ 0 <= (-1 + havoc:13)
                     /\ 0 <= (1 + -havoc:13 + (-1 + havoc:13))
                     /\ 0 <= (1 + -havoc:13
                                + ((-1 + havoc:13) * (-1 + havoc:13)))
                     /\ (-mid_n:804 + mid_j:806) = 0
                     /\ 0 <= (-mid_i:807 + mid_n:804)
                     /\ 0 <= (1 + mid___cost:805) /\ 0 <= (-1 + mid_i:807)))
         /\ (!(0 <= K:808) \/ i':782 = (mid_i:807 + K:808))
         /\ (!(0 <= K:808) \/ __cost':783 = mid___cost:805)
         /\ (!((0 <= K:808 /\ K:808 <= 0))
               \/ (-n':780 + j':781) = (-mid_n:804 + mid_j:806))
         /\ (!(1 <= K:808) \/ (-n':780 + j':781) = 0)
         /\ (!(0 <= K:808) \/ n':780 = mid_n:804)
         /\ ((K:808 = 0 /\ mid_n:804 = n':780 /\ mid_j:806 = j':781
                /\ mid_i:807 = i':782 /\ mid___cost:805 = __cost':783)
               \/ (1 <= K:808 /\ 0 <= (-1 + -mid_i:807 + mid_n:804)
                     /\ 0 <= (-2 + -mid___cost:805) /\ 0 <= mid_i:807
                     /\ (-n':780 + j':781) = 0 /\ 0 <= (-2 + -__cost':783)
                     /\ 0 <= (-1 + i':782) /\ 0 <= (n':780 + -i':782)))
         /\ (0 = K:808 \/ (2 + mid___cost:805) <= 0)
         /\ (K:803 + K:808) = K:784 /\ 0 <= K:784 /\ 0 <= i':782
         /\ n':780 <= i':782
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:814)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:814)))}

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

Base relation: 
{__cost := __cost':827
 return := havoc:856
 param0 := param0:53
 return@pos := type_err:857
 param0@pos := type_err:54
 return@width := type_err:858
 param0@width := type_err:55
 when ((!(0 <= K:817) \/ mid___cost:818 = __cost:66)
         /\ (!((0 <= K:817 /\ K:817 <= 0)) \/ mid_j:819 = j:820)
         /\ (!(1 <= K:817) \/ mid_j:819 = (j:820 + param0:53 + -j:820))
         /\ (!(0 <= K:817) \/ mid_i:821 = K:817)
         /\ (!(0 <= K:817) \/ mid_n:822 = param0:53)
         /\ (!((0 <= K:817 /\ K:817 <= 0))
               \/ -mid_j:819 <= (-j:820 + (-1/2 * K:817)
                                   + (param0:53 * K:817)
                                   + (-1/2 * (K:817 * K:817))))
         /\ (!(1 <= K:817)
               \/ -mid_j:819 <= (j:820 + -j:820 + -param0:53 + (-1/2 * K:817)
                                   + (param0:53 * K:817)
                                   + (-1/2 * (K:817 * K:817))))
         /\ ((K:817 = 0 /\ param0:53 = mid_n:822 /\ j:820 = mid_j:819
                /\ 0 = mid_i:821 /\ __cost:66 = mid___cost:818)
               \/ (1 <= K:817 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= (-1 + -__cost:66)
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ (-mid_j:819 + mid_n:822) = 0
                     /\ 0 <= (-mid_i:821 + mid_j:819)
                     /\ 0 <= (-1 + -mid___cost:818)
                     /\ 0 <= (mid_i:821 + -mid_j:819
                                + ((-mid_i:821 + mid_j:819)
                                     * (-mid_i:821 + mid_j:819)))
                     /\ 0 <= (mid_i:821 + -mid_j:819
                                + ((-mid_i:821 + mid_j:819) * mid_i:821))
                     /\ 0 <= (-1 + mid_i:821)))
         /\ (0 = K:817 \/ !(-__cost:66 <= 0))
         /\ (!((0 <= K:823 /\ K:823 <= 0))
               \/ (-n':824 + j':825) = (-mid_n:822 + mid_j:819))
         /\ (!(1 <= K:823) \/ (-n':824 + j':825) = 0)
         /\ (!(0 <= K:823) \/ i':826 = (mid_i:821 + K:823))
         /\ (!(0 <= K:823)
               \/ (n':824 + __cost':827) = (mid_n:822 + mid___cost:818))
         /\ (!(0 <= K:823) \/ n':824 <= mid_n:822)
         /\ (!(0 <= K:823)
               \/ -n':824 <= (-mid_n:822 + (-1/2 * K:823)
                                + -((mid_i:821 * K:823))
                                + ((mid_n:822 + mid___cost:818) * K:823)
                                + (-1/2 * (K:823 * K:823))))
         /\ ((K:823 = 0 /\ mid_n:822 = n':824 /\ mid_j:819 = j':825
                /\ mid_i:821 = i':826 /\ mid___cost:818 = __cost':827)
               \/ (1 <= K:823 /\ 0 <= (-1 + -mid_i:821 + mid_n:822)
                     /\ 0 <= ((-1 + -mid_i:821 + mid_n:822) * mid___cost:818)
                     /\ 0 <= mid___cost:818
                     /\ 0 <= (1 + mid_i:821 + -mid_n:822
                                + ((-1 + -mid_i:821 + mid_n:822)
                                     * (-1 + -mid_i:821 + mid_n:822)))
                     /\ 0 <= (1 + mid_i:821 + -mid_n:822
                                + ((-1 + -mid_i:821 + mid_n:822)
                                     * (1 + mid_i:821))) /\ 0 <= mid_i:821
                     /\ (-n':824 + j':825) = 0 /\ 0 <= (-i':826 + n':824)
                     /\ 0 <= __cost':827 /\ 0 <= (-1 + i':826)))
         /\ (0 = K:823 \/ -mid___cost:818 <= 0) /\ (K:817 + K:823) = K:828
         /\ (!(0 <= K:829) \/ mid_i:830 = K:829)
         /\ (!(0 <= K:829) \/ mid___cost:831 = __cost:66)
         /\ (!((0 <= K:829 /\ K:829 <= 0))
               \/ (-mid_n:832 + mid_j:833) = (-param0:53 + j:820))
         /\ (!(1 <= K:829) \/ (-mid_n:832 + mid_j:833) = 0)
         /\ (!(0 <= K:829) \/ mid_n:832 = param0:53)
         /\ ((K:829 = 0 /\ param0:53 = mid_n:832 /\ j:820 = mid_j:833
                /\ 0 = mid_i:830 /\ __cost:66 = mid___cost:831)
               \/ (1 <= K:829 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= (-2 + -__cost:66)
                     /\ (-mid_n:832 + mid_j:833) = 0
                     /\ 0 <= (-2 + -mid___cost:831) /\ 0 <= (-1 + mid_i:830)
                     /\ 0 <= (mid_n:832 + -mid_i:830)))
         /\ (0 = K:829 \/ !((-1 + -__cost:66) <= 0))
         /\ (!((0 <= K:834 /\ K:834 <= 0))
               \/ (-n':824 + j':825) = (-mid_n:832 + mid_j:833))
         /\ (!(1 <= K:834) \/ (-n':824 + j':825) = 0)
         /\ (!(0 <= K:834) \/ i':826 = (mid_i:830 + K:834))
         /\ (!(0 <= K:834)
               \/ (n':824 + __cost':827) = (mid_n:832 + mid___cost:831))
         /\ (!(0 <= K:834) \/ n':824 <= mid_n:832)
         /\ (!(0 <= K:834)
               \/ -n':824 <= (-mid_n:832 + (1/2 * K:834)
                                + -((mid_i:830 * K:834))
                                + ((mid_n:832 + mid___cost:831) * K:834)
                                + (-1/2 * (K:834 * K:834))))
         /\ ((K:834 = 0 /\ mid_n:832 = n':824 /\ mid_j:833 = j':825
                /\ mid_i:830 = i':826 /\ mid___cost:831 = __cost':827)
               \/ (1 <= K:834 /\ 0 <= (-1 + -mid_i:830 + mid_n:832)
                     /\ 0 <= (-1 + -mid_i:830 + mid_n:832
                                + ((-1 + -mid_i:830 + mid_n:832)
                                     * mid___cost:831))
                     /\ 0 <= (1 + mid___cost:831)
                     /\ 0 <= (1 + mid_i:830 + -mid_n:832
                                + ((-1 + -mid_i:830 + mid_n:832)
                                     * (1 + mid_i:830)))
                     /\ 0 <= (1 + mid_i:830 + -mid_n:832
                                + ((-1 + -mid_i:830 + mid_n:832)
                                     * (-1 + -mid_i:830 + mid_n:832)))
                     /\ 0 <= mid_i:830 /\ (-n':824 + j':825) = 0
                     /\ 0 <= (-i':826 + n':824) /\ 0 <= (1 + __cost':827)
                     /\ 0 <= (-1 + i':826)))
         /\ (0 = K:834 \/ (-1 + -mid___cost:831) <= 0)
         /\ (K:829 + K:834) = K:828
         /\ (!((0 <= K:835 /\ K:835 <= 0))
               \/ (-mid_n:836 + mid_j:837) = (-param0:53 + j:820))
         /\ (!(1 <= K:835) \/ (-mid_n:836 + mid_j:837) = 0)
         /\ (!(0 <= K:835) \/ mid_i:838 = K:835)
         /\ (!(0 <= K:835)
               \/ (mid_n:836 + mid___cost:839) = (param0:53 + __cost:66))
         /\ (!(0 <= K:835) \/ mid_n:836 <= param0:53)
         /\ ((K:835 = 0 /\ param0:53 = mid_n:836 /\ j:820 = mid_j:837
                /\ 0 = mid_i:838 /\ __cost:66 = mid___cost:839)
               \/ (1 <= K:835 /\ 0 <= (-2 + param0:53)
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ (-mid_n:836 + mid_j:837) = 0
                     /\ 0 <= (-mid_i:838 + mid_n:836)
                     /\ 0 <= (-1 + mid_i:838)))
         /\ (0 = K:835 \/ (2 + -param0:53) <= 0)
         /\ (!((0 <= K:840 /\ K:840 <= 0)) \/ j':825 = (mid_j:837 + K:840))
         /\ (!(1 <= K:840)
               \/ j':825 = (mid_j:837 + mid_i:838 + -mid_j:837 + K:840))
         /\ (!((0 <= K:840 /\ K:840 <= 0)) \/ n':824 = (mid_n:836 + K:840))
         /\ (!(1 <= K:840)
               \/ n':824 = (mid_n:836 + mid_i:838 + -mid_n:836 + K:840))
         /\ (!(0 <= K:840) \/ __cost':827 = mid___cost:839)
         /\ (!(0 <= K:840) \/ i':826 = (mid_i:838 + K:840))
         /\ (!((0 <= K:840 /\ K:840 <= 0))
               \/ -j':825 <= (-mid_j:837 + (-3/2 * K:840)
                                + (mid_i:838 * K:840)
                                + (1/2 * (K:840 * K:840))))
         /\ (!(1 <= K:840)
               \/ -j':825 <= (mid_j:837 + -mid_j:837 + -mid_i:838
                                + (-3/2 * K:840) + (mid_i:838 * K:840)
                                + (1/2 * (K:840 * K:840))))
         /\ ((K:840 = 0 /\ mid_n:836 = n':824 /\ mid_j:837 = j':825
                /\ mid_i:838 = i':826 /\ mid___cost:839 = __cost':827)
               \/ (1 <= K:840 /\ (-1 + -mid_i:838 + mid_n:836) = 0
                     /\ 0 <= mid_i:838 /\ (-j':825 + n':824) = 0
                     /\ (-j':825 + i':826) = 0 /\ 0 <= (-1 + j':825)))
         /\ (0 = K:840 \/ !((2 + mid_i:838 + -mid_n:836) <= 0))
         /\ (K:835 + K:840) = K:828 /\ (!(0 <= K:841) \/ mid_i:842 = K:841)
         /\ (!(0 <= K:841)
               \/ (mid_n:843 + mid___cost:844) = (param0:53 + __cost:66))
         /\ (!((0 <= K:841 /\ K:841 <= 0))
               \/ (-mid_n:843 + mid_j:845) = (-param0:53 + j:820))
         /\ (!(1 <= K:841) \/ (-mid_n:843 + mid_j:845) = 0)
         /\ (!(0 <= K:841) \/ mid_n:843 <= param0:53)
         /\ (!(0 <= K:841)
               \/ -mid_n:843 <= (-param0:53 + (-1/2 * K:841)
                                   + ((param0:53 + __cost:66) * K:841)
                                   + (-1/2 * (K:841 * K:841))))
         /\ ((K:841 = 0 /\ param0:53 = mid_n:843 /\ j:820 = mid_j:845
                /\ 0 = mid_i:842 /\ __cost:66 = mid___cost:844)
               \/ (1 <= K:841 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= ((-1 + param0:53) * __cost:66) /\ 0 <= __cost:66
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ (-mid_n:843 + mid_j:845) = 0 /\ 0 <= mid___cost:844
                     /\ 0 <= (-1 + mid_i:842)
                     /\ 0 <= (mid_n:843 + -mid_i:842)))
         /\ (0 = K:841 \/ !((1 + __cost:66) <= 0))
         /\ (!(0 <= K:846) \/ __cost':827 = mid___cost:844)
         /\ (!(0 <= K:846) \/ n':824 = mid_n:843)
         /\ (!(0 <= K:846) \/ i':826 = (mid_i:842 + K:846))
         /\ (!((0 <= K:846 /\ K:846 <= 0)) \/ j':825 = mid_j:845)
         /\ (!(1 <= K:846) \/ j':825 = mid_n:843)
         /\ ((K:846 = 0 /\ mid_n:843 = n':824 /\ mid_j:845 = j':825
                /\ mid_i:842 = i':826 /\ mid___cost:844 = __cost':827)
               \/ (1 <= K:846 /\ 0 <= (-1 + -mid_i:842 + mid_n:843)
                     /\ 0 <= (-1 + -mid___cost:844)
                     /\ 0 <= (1 + mid_i:842 + -mid_n:843
                                + ((-1 + -mid_i:842 + mid_n:843)
                                     * (-1 + -mid_i:842 + mid_n:843)))
                     /\ 0 <= (1 + mid_i:842 + -mid_n:843
                                + ((-1 + -mid_i:842 + mid_n:843)
                                     * (1 + mid_i:842))) /\ 0 <= mid_i:842
                     /\ (-n':824 + j':825) = 0 /\ 0 <= (-i':826 + n':824)
                     /\ 0 <= (-1 + -__cost':827)
                     /\ 0 <= (i':826 + -n':824
                                + ((-i':826 + n':824) * (-i':826 + n':824)))
                     /\ 0 <= (i':826 + -n':824
                                + ((-i':826 + n':824) * i':826))
                     /\ 0 <= (-1 + i':826)))
         /\ (0 = K:846 \/ (1 + mid___cost:844) <= 0)
         /\ (K:841 + K:846) = K:828
         /\ (!(0 <= K:847)
               \/ (mid_n:848 + mid___cost:849) = (param0:53 + __cost:66))
         /\ (!((0 <= K:847 /\ K:847 <= 0))
               \/ (-mid_n:848 + mid_j:850) = (-param0:53 + j:820))
         /\ (!(1 <= K:847) \/ (-mid_n:848 + mid_j:850) = 0)
         /\ (!(0 <= K:847) \/ mid_i:851 = K:847)
         /\ (!(0 <= K:847) \/ mid_n:848 <= param0:53)
         /\ (!(0 <= K:847)
               \/ -mid_n:848 <= (-param0:53 + (1/2 * K:847)
                                   + ((param0:53 + __cost:66) * K:847)
                                   + (-1/2 * (K:847 * K:847))))
         /\ ((K:847 = 0 /\ param0:53 = mid_n:848 /\ j:820 = mid_j:850
                /\ 0 = mid_i:851 /\ __cost:66 = mid___cost:849)
               \/ (1 <= K:847 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= (-1 + param0:53 + ((-1 + param0:53) * __cost:66))
                     /\ 0 <= (1 + __cost:66)
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ (-mid_n:848 + mid_j:850) = 0
                     /\ 0 <= (-mid_i:851 + mid_n:848)
                     /\ 0 <= (1 + mid___cost:849) /\ 0 <= (-1 + mid_i:851)))
         /\ (0 = K:847 \/ !((2 + __cost:66) <= 0))
         /\ (!(0 <= K:852) \/ i':826 = (mid_i:851 + K:852))
         /\ (!(0 <= K:852) \/ __cost':827 = mid___cost:849)
         /\ (!((0 <= K:852 /\ K:852 <= 0))
               \/ (-n':824 + j':825) = (-mid_n:848 + mid_j:850))
         /\ (!(1 <= K:852) \/ (-n':824 + j':825) = 0)
         /\ (!(0 <= K:852) \/ n':824 = mid_n:848)
         /\ ((K:852 = 0 /\ mid_n:848 = n':824 /\ mid_j:850 = j':825
                /\ mid_i:851 = i':826 /\ mid___cost:849 = __cost':827)
               \/ (1 <= K:852 /\ 0 <= (-1 + -mid_i:851 + mid_n:848)
                     /\ 0 <= (-2 + -mid___cost:849) /\ 0 <= mid_i:851
                     /\ (-n':824 + j':825) = 0 /\ 0 <= (-2 + -__cost':827)
                     /\ 0 <= (-1 + i':826) /\ 0 <= (n':824 + -i':826)))
         /\ (0 = K:852 \/ (2 + mid___cost:849) <= 0)
         /\ (K:847 + K:852) = K:828 /\ 0 <= K:828 /\ 0 <= i':826
         /\ n':824 <= i':826)}

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

Base relation: 
{__cost := __cost':587
 i := i':586
 j := j':585
 n := n':584
 return := havoc:641
 return@pos := type_err:642
 return@width := type_err:643
 when ((!(0 <= K:578) \/ mid___cost:579 = __cost:66)
         /\ (!((0 <= K:578 /\ K:578 <= 0)) \/ mid_j:580 = j:64)
         /\ (!(1 <= K:578) \/ mid_j:580 = (j:64 + param0:53 + -j:64))
         /\ (!(0 <= K:578) \/ mid_i:581 = K:578)
         /\ (!(0 <= K:578) \/ mid_n:582 = param0:53)
         /\ (!((0 <= K:578 /\ K:578 <= 0))
               \/ -mid_j:580 <= (-j:64 + (-1/2 * K:578) + (param0:53 * K:578)
                                   + (-1/2 * (K:578 * K:578))))
         /\ (!(1 <= K:578)
               \/ -mid_j:580 <= (j:64 + -j:64 + -param0:53 + (-1/2 * K:578)
                                   + (param0:53 * K:578)
                                   + (-1/2 * (K:578 * K:578))))
         /\ ((K:578 = 0 /\ param0:53 = mid_n:582 /\ j:64 = mid_j:580
                /\ 0 = mid_i:581 /\ __cost:66 = mid___cost:579)
               \/ (1 <= K:578 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= (-1 + -__cost:66)
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ (-mid_j:580 + mid_n:582) = 0
                     /\ 0 <= (-mid_i:581 + mid_j:580)
                     /\ 0 <= (-1 + -mid___cost:579)
                     /\ 0 <= (mid_i:581 + -mid_j:580
                                + ((-mid_i:581 + mid_j:580)
                                     * (-mid_i:581 + mid_j:580)))
                     /\ 0 <= (mid_i:581 + -mid_j:580
                                + ((-mid_i:581 + mid_j:580) * mid_i:581))
                     /\ 0 <= (-1 + mid_i:581)))
         /\ (0 = K:578 \/ !(-__cost:66 <= 0))
         /\ (!((0 <= K:583 /\ K:583 <= 0))
               \/ (-n':584 + j':585) = (-mid_n:582 + mid_j:580))
         /\ (!(1 <= K:583) \/ (-n':584 + j':585) = 0)
         /\ (!(0 <= K:583) \/ i':586 = (mid_i:581 + K:583))
         /\ (!(0 <= K:583)
               \/ (n':584 + __cost':587) = (mid_n:582 + mid___cost:579))
         /\ (!(0 <= K:583) \/ n':584 <= mid_n:582)
         /\ (!(0 <= K:583)
               \/ -n':584 <= (-mid_n:582 + (-1/2 * K:583)
                                + -((mid_i:581 * K:583))
                                + ((mid_n:582 + mid___cost:579) * K:583)
                                + (-1/2 * (K:583 * K:583))))
         /\ ((K:583 = 0 /\ mid_n:582 = n':584 /\ mid_j:580 = j':585
                /\ mid_i:581 = i':586 /\ mid___cost:579 = __cost':587)
               \/ (1 <= K:583 /\ 0 <= (-1 + -mid_i:581 + mid_n:582)
                     /\ 0 <= ((-1 + -mid_i:581 + mid_n:582) * mid___cost:579)
                     /\ 0 <= mid___cost:579
                     /\ 0 <= (1 + mid_i:581 + -mid_n:582
                                + ((-1 + -mid_i:581 + mid_n:582)
                                     * (-1 + -mid_i:581 + mid_n:582)))
                     /\ 0 <= (1 + mid_i:581 + -mid_n:582
                                + ((-1 + -mid_i:581 + mid_n:582)
                                     * (1 + mid_i:581))) /\ 0 <= mid_i:581
                     /\ (-n':584 + j':585) = 0 /\ 0 <= (-i':586 + n':584)
                     /\ 0 <= __cost':587 /\ 0 <= (-1 + i':586)))
         /\ (0 = K:583 \/ -mid___cost:579 <= 0) /\ (K:578 + K:583) = K:588
         /\ (!(0 <= K:589) \/ mid_i:590 = K:589)
         /\ (!(0 <= K:589) \/ mid___cost:591 = __cost:66)
         /\ (!((0 <= K:589 /\ K:589 <= 0))
               \/ (-mid_n:592 + mid_j:593) = (-param0:53 + j:64))
         /\ (!(1 <= K:589) \/ (-mid_n:592 + mid_j:593) = 0)
         /\ (!(0 <= K:589) \/ mid_n:592 = param0:53)
         /\ ((K:589 = 0 /\ param0:53 = mid_n:592 /\ j:64 = mid_j:593
                /\ 0 = mid_i:590 /\ __cost:66 = mid___cost:591)
               \/ (1 <= K:589 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= (-2 + -__cost:66)
                     /\ (-mid_n:592 + mid_j:593) = 0
                     /\ 0 <= (-2 + -mid___cost:591) /\ 0 <= (-1 + mid_i:590)
                     /\ 0 <= (mid_n:592 + -mid_i:590)))
         /\ (0 = K:589 \/ !((-1 + -__cost:66) <= 0))
         /\ (!((0 <= K:594 /\ K:594 <= 0))
               \/ (-n':584 + j':585) = (-mid_n:592 + mid_j:593))
         /\ (!(1 <= K:594) \/ (-n':584 + j':585) = 0)
         /\ (!(0 <= K:594) \/ i':586 = (mid_i:590 + K:594))
         /\ (!(0 <= K:594)
               \/ (n':584 + __cost':587) = (mid_n:592 + mid___cost:591))
         /\ (!(0 <= K:594) \/ n':584 <= mid_n:592)
         /\ (!(0 <= K:594)
               \/ -n':584 <= (-mid_n:592 + (1/2 * K:594)
                                + -((mid_i:590 * K:594))
                                + ((mid_n:592 + mid___cost:591) * K:594)
                                + (-1/2 * (K:594 * K:594))))
         /\ ((K:594 = 0 /\ mid_n:592 = n':584 /\ mid_j:593 = j':585
                /\ mid_i:590 = i':586 /\ mid___cost:591 = __cost':587)
               \/ (1 <= K:594 /\ 0 <= (-1 + -mid_i:590 + mid_n:592)
                     /\ 0 <= (-1 + -mid_i:590 + mid_n:592
                                + ((-1 + -mid_i:590 + mid_n:592)
                                     * mid___cost:591))
                     /\ 0 <= (1 + mid___cost:591)
                     /\ 0 <= (1 + mid_i:590 + -mid_n:592
                                + ((-1 + -mid_i:590 + mid_n:592)
                                     * (1 + mid_i:590)))
                     /\ 0 <= (1 + mid_i:590 + -mid_n:592
                                + ((-1 + -mid_i:590 + mid_n:592)
                                     * (-1 + -mid_i:590 + mid_n:592)))
                     /\ 0 <= mid_i:590 /\ (-n':584 + j':585) = 0
                     /\ 0 <= (-i':586 + n':584) /\ 0 <= (1 + __cost':587)
                     /\ 0 <= (-1 + i':586)))
         /\ (0 = K:594 \/ (-1 + -mid___cost:591) <= 0)
         /\ (K:589 + K:594) = K:588
         /\ (!((0 <= K:595 /\ K:595 <= 0))
               \/ (-mid_n:596 + mid_j:597) = (-param0:53 + j:64))
         /\ (!(1 <= K:595) \/ (-mid_n:596 + mid_j:597) = 0)
         /\ (!(0 <= K:595) \/ mid_i:598 = K:595)
         /\ (!(0 <= K:595)
               \/ (mid_n:596 + mid___cost:599) = (param0:53 + __cost:66))
         /\ (!(0 <= K:595) \/ mid_n:596 <= param0:53)
         /\ ((K:595 = 0 /\ param0:53 = mid_n:596 /\ j:64 = mid_j:597
                /\ 0 = mid_i:598 /\ __cost:66 = mid___cost:599)
               \/ (1 <= K:595 /\ 0 <= (-2 + param0:53)
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ (-mid_n:596 + mid_j:597) = 0
                     /\ 0 <= (-mid_i:598 + mid_n:596)
                     /\ 0 <= (-1 + mid_i:598)))
         /\ (0 = K:595 \/ (2 + -param0:53) <= 0)
         /\ (!((0 <= K:600 /\ K:600 <= 0)) \/ j':585 = (mid_j:597 + K:600))
         /\ (!(1 <= K:600)
               \/ j':585 = (mid_j:597 + mid_i:598 + -mid_j:597 + K:600))
         /\ (!((0 <= K:600 /\ K:600 <= 0)) \/ n':584 = (mid_n:596 + K:600))
         /\ (!(1 <= K:600)
               \/ n':584 = (mid_n:596 + mid_i:598 + -mid_n:596 + K:600))
         /\ (!(0 <= K:600) \/ __cost':587 = mid___cost:599)
         /\ (!(0 <= K:600) \/ i':586 = (mid_i:598 + K:600))
         /\ (!((0 <= K:600 /\ K:600 <= 0))
               \/ -j':585 <= (-mid_j:597 + (-3/2 * K:600)
                                + (mid_i:598 * K:600)
                                + (1/2 * (K:600 * K:600))))
         /\ (!(1 <= K:600)
               \/ -j':585 <= (mid_j:597 + -mid_j:597 + -mid_i:598
                                + (-3/2 * K:600) + (mid_i:598 * K:600)
                                + (1/2 * (K:600 * K:600))))
         /\ ((K:600 = 0 /\ mid_n:596 = n':584 /\ mid_j:597 = j':585
                /\ mid_i:598 = i':586 /\ mid___cost:599 = __cost':587)
               \/ (1 <= K:600 /\ (-1 + -mid_i:598 + mid_n:596) = 0
                     /\ 0 <= mid_i:598 /\ (-j':585 + n':584) = 0
                     /\ (-j':585 + i':586) = 0 /\ 0 <= (-1 + j':585)))
         /\ (0 = K:600 \/ !((2 + mid_i:598 + -mid_n:596) <= 0))
         /\ (K:595 + K:600) = K:588 /\ (!(0 <= K:601) \/ mid_i:602 = K:601)
         /\ (!(0 <= K:601)
               \/ (mid_n:603 + mid___cost:604) = (param0:53 + __cost:66))
         /\ (!((0 <= K:601 /\ K:601 <= 0))
               \/ (-mid_n:603 + mid_j:605) = (-param0:53 + j:64))
         /\ (!(1 <= K:601) \/ (-mid_n:603 + mid_j:605) = 0)
         /\ (!(0 <= K:601) \/ mid_n:603 <= param0:53)
         /\ (!(0 <= K:601)
               \/ -mid_n:603 <= (-param0:53 + (-1/2 * K:601)
                                   + ((param0:53 + __cost:66) * K:601)
                                   + (-1/2 * (K:601 * K:601))))
         /\ ((K:601 = 0 /\ param0:53 = mid_n:603 /\ j:64 = mid_j:605
                /\ 0 = mid_i:602 /\ __cost:66 = mid___cost:604)
               \/ (1 <= K:601 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= ((-1 + param0:53) * __cost:66) /\ 0 <= __cost:66
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ (-mid_n:603 + mid_j:605) = 0 /\ 0 <= mid___cost:604
                     /\ 0 <= (-1 + mid_i:602)
                     /\ 0 <= (mid_n:603 + -mid_i:602)))
         /\ (0 = K:601 \/ !((1 + __cost:66) <= 0))
         /\ (!(0 <= K:606) \/ __cost':587 = mid___cost:604)
         /\ (!(0 <= K:606) \/ n':584 = mid_n:603)
         /\ (!(0 <= K:606) \/ i':586 = (mid_i:602 + K:606))
         /\ (!((0 <= K:606 /\ K:606 <= 0)) \/ j':585 = mid_j:605)
         /\ (!(1 <= K:606) \/ j':585 = mid_n:603)
         /\ ((K:606 = 0 /\ mid_n:603 = n':584 /\ mid_j:605 = j':585
                /\ mid_i:602 = i':586 /\ mid___cost:604 = __cost':587)
               \/ (1 <= K:606 /\ 0 <= (-1 + -mid_i:602 + mid_n:603)
                     /\ 0 <= (-1 + -mid___cost:604)
                     /\ 0 <= (1 + mid_i:602 + -mid_n:603
                                + ((-1 + -mid_i:602 + mid_n:603)
                                     * (-1 + -mid_i:602 + mid_n:603)))
                     /\ 0 <= (1 + mid_i:602 + -mid_n:603
                                + ((-1 + -mid_i:602 + mid_n:603)
                                     * (1 + mid_i:602))) /\ 0 <= mid_i:602
                     /\ (-n':584 + j':585) = 0 /\ 0 <= (-i':586 + n':584)
                     /\ 0 <= (-1 + -__cost':587)
                     /\ 0 <= (i':586 + -n':584
                                + ((-i':586 + n':584) * (-i':586 + n':584)))
                     /\ 0 <= (i':586 + -n':584
                                + ((-i':586 + n':584) * i':586))
                     /\ 0 <= (-1 + i':586)))
         /\ (0 = K:606 \/ (1 + mid___cost:604) <= 0)
         /\ (K:601 + K:606) = K:588
         /\ (!(0 <= K:607)
               \/ (mid_n:608 + mid___cost:609) = (param0:53 + __cost:66))
         /\ (!((0 <= K:607 /\ K:607 <= 0))
               \/ (-mid_n:608 + mid_j:610) = (-param0:53 + j:64))
         /\ (!(1 <= K:607) \/ (-mid_n:608 + mid_j:610) = 0)
         /\ (!(0 <= K:607) \/ mid_i:611 = K:607)
         /\ (!(0 <= K:607) \/ mid_n:608 <= param0:53)
         /\ (!(0 <= K:607)
               \/ -mid_n:608 <= (-param0:53 + (1/2 * K:607)
                                   + ((param0:53 + __cost:66) * K:607)
                                   + (-1/2 * (K:607 * K:607))))
         /\ ((K:607 = 0 /\ param0:53 = mid_n:608 /\ j:64 = mid_j:610
                /\ 0 = mid_i:611 /\ __cost:66 = mid___cost:609)
               \/ (1 <= K:607 /\ 0 <= (-1 + param0:53)
                     /\ 0 <= (-1 + param0:53 + ((-1 + param0:53) * __cost:66))
                     /\ 0 <= (1 + __cost:66)
                     /\ 0 <= (1 + -param0:53 + (-1 + param0:53))
                     /\ 0 <= (1 + -param0:53
                                + ((-1 + param0:53) * (-1 + param0:53)))
                     /\ (-mid_n:608 + mid_j:610) = 0
                     /\ 0 <= (-mid_i:611 + mid_n:608)
                     /\ 0 <= (1 + mid___cost:609) /\ 0 <= (-1 + mid_i:611)))
         /\ (0 = K:607 \/ !((2 + __cost:66) <= 0))
         /\ (!(0 <= K:612) \/ i':586 = (mid_i:611 + K:612))
         /\ (!(0 <= K:612) \/ __cost':587 = mid___cost:609)
         /\ (!((0 <= K:612 /\ K:612 <= 0))
               \/ (-n':584 + j':585) = (-mid_n:608 + mid_j:610))
         /\ (!(1 <= K:612) \/ (-n':584 + j':585) = 0)
         /\ (!(0 <= K:612) \/ n':584 = mid_n:608)
         /\ ((K:612 = 0 /\ mid_n:608 = n':584 /\ mid_j:610 = j':585
                /\ mid_i:611 = i':586 /\ mid___cost:609 = __cost':587)
               \/ (1 <= K:612 /\ 0 <= (-1 + -mid_i:611 + mid_n:608)
                     /\ 0 <= (-2 + -mid___cost:609) /\ 0 <= mid_i:611
                     /\ (-n':584 + j':585) = 0 /\ 0 <= (-2 + -__cost':587)
                     /\ 0 <= (-1 + i':586) /\ 0 <= (n':584 + -i':586)))
         /\ (0 = K:612 \/ (2 + mid___cost:609) <= 0)
         /\ (K:607 + K:612) = K:588 /\ 0 <= K:588 /\ 0 <= i':586
         /\ n':584 <= i':586)}

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

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

Variable bounds at line 28 in run

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

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