/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, 146> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 26> -> <Unique State Name, 22>	Base relation: 
{i := (i:0 + 1)
 when i:0 < p_len:11}	
<Unique State Name, 26> -> <Unique State Name, 38>	Base relation: 
{i := 0
 when p_len:11 <= i:0}	
<Unique State Name, 6> -> <Unique State Name, 150>	Base relation: 
{when (i:0 <= 10 /\ 0 <= i:0 /\ t_len:1 <= 10 /\ 10 <= t_len:1)}	
<Unique State Name, 144> -> <Unique State Name, 133 143>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 121> -> <Unique State Name, 69>	Base relation: 
{i := 0
 j := 0
 k := -1
 t := param0:512
 n := param1:515
 p := param2:518
 m := param3:521
 b := param4:524
 t@pos := param0@pos:511
 p@pos := param2@pos:517
 b@pos := param4@pos:523
 t@width := param0@width:510
 p@width := param2@width:516
 b@width := param4@width:522}	
<Unique State Name, 147> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 143> -> <Unique State Name, 147>	Base relation: 
{return := 0
 return@pos := type_err:80
 return@width := type_err:81}	
<Unique State Name, 131> -> <Unique State Name, 62>	Base relation: 
{}	
<Unique State Name, 80> -> <Unique State Name, 151>	Base relation: 
{when (-1 <= k:574 /\ -1 <= j:558 /\ 1 <= __cost:191 /\ 0 <= __cost:191
         /\ 0 <= (__cost:191 + 1))}	
<Unique State Name, 150> -> <Unique State Name, 10>	Base relation: 
{}	
<Unique State Name, 145> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 62> -> <Unique State Name, 146>	Base relation: 
{return := 0
 return@pos := type_err:525
 return@width := type_err:526}	
<Unique State Name, 132> -> <Unique State Name, 121 131>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 106> -> <Unique State Name, 112>	Base relation: 
{i := (i:553 + 1)
 j := (j:558 + 1)}	
<Unique State Name, 69> -> <Unique State Name, 152>	Base relation: 
{when (-1 <= k:574 /\ 0 <= j:558 /\ 0 <= i:553 /\ 0 <= j:558)}	
<Unique State Name, 92> -> <Unique State Name, 88>	Base relation: 
{when 0 <= j:558}	
<Unique State Name, 92> -> <Unique State Name, 106>	Base relation: 
{when j:558 < 0}	
<Unique State Name, 151> -> <Unique State Name, 92>	Base relation: 
{}	
<Unique State Name, 118> -> <Unique State Name, 145>	Base relation: 
{return := i:553
 return@pos := type_err:578
 return@width := type_err:579}	
<Unique State Name, 148> -> <Unique State Name, 42>	Base relation: 
{}	
<Unique State Name, 112> -> <Unique State Name, 69>	Base relation: 
{when !(j:558 = m:575)}	
<Unique State Name, 112> -> <Unique State Name, 118>	Base relation: 
{when j:558 = m:575}	
<Unique State Name, 22> -> <Unique State Name, 149>	Base relation: 
{when (0 <= i:0 /\ p_len:11 <= 5 /\ 5 <= p_len:11 /\ i:0 < t_len:1)}	
<Unique State Name, 149> -> <Unique State Name, 26>	Base relation: 
{}	
<Unique State Name, 73> -> <Unique State Name, 80>	Base relation: 
{__cost := (__cost:191 + 1)
 when (i:553 < n:554 /\ 0 <= __cost:191 /\ 0 <= (__cost:191 + 1))}	
<Unique State Name, 73> -> <Unique State Name, 118>	Base relation: 
{when n:554 <= i:553}	
<Unique State Name, 88> -> <Unique State Name, 80>	Base relation: 
{__cost := (__cost:191 + 1)
 j := (j:558 + -tr:588)
 k := tr:588
 when ((tr:564 < tr:565 \/ tr:562 < tr:563) /\ 0 <= __cost:191
         /\ 0 <= (__cost:191 + 1) /\ 0 < tr:588 /\ tr:588 <= (j:558 + 1))}	
<Unique State Name, 88> -> <Unique State Name, 106>	Base relation: 
{when (tr:568 <= tr:569 /\ tr:566 <= tr:567)}	
<Unique State Name, 60> -> <Unique State Name, 6>	Base relation: 
{__cost := 0
 t_len := 10
 p_len := 5
 i := 0}	
<Unique State Name, 38> -> <Unique State Name, 148>	Base relation: 
{when (i:0 <= 5 /\ 0 <= i:0 /\ p_len:11 <= 5 /\ 5 <= p_len:11
         /\ i:0 < t_len:1)}	
<Unique State Name, 10> -> <Unique State Name, 6>	Base relation: 
{i := (i:0 + 1)
 when i:0 < t_len:1}	
<Unique State Name, 10> -> <Unique State Name, 22>	Base relation: 
{i := 0
 when t_len:1 <= i:0}	
<Unique State Name, 133> -> <Unique State Name, 132>	Base relation: 
{param0 := param0:512
 param1 := param1:515
 param2 := param2:518
 param3 := param3:521
 param4 := param4:524
 param0@pos := param0@pos:511
 param1@pos := type_err:531
 param2@pos := param2@pos:517
 param3@pos := type_err:532
 param4@pos := param4@pos:523
 param0@width := param0@width:510
 param1@width := type_err:533
 param2@width := param2@width:516
 param3@width := type_err:534
 param4@width := param4@width:522}	
<Unique State Name, 42> -> <Unique State Name, 38>	Base relation: 
{i := (i:0 + 1)
 when (i:0 < p_len:11 /\ 0 < tr:77 /\ tr:79 <= (i:0 + 1))}	
<Unique State Name, 42> -> <Unique State Name, 144>	Base relation: 
{param0 := t:92
 param1 := t_len:1
 param2 := p:93
 param3 := p_len:11
 param4 := b:94
 param0@pos := type_err:82
 param1@pos := type_err:84
 param2@pos := type_err:86
 param3@pos := type_err:88
 param4@pos := type_err:90
 param0@width := type_err:83
 param1@width := type_err:85
 param2@width := type_err:87
 param3@width := type_err:89
 param4@width := type_err:91
 when p_len:11 <= i:0}	
<Unique State Name, 152> -> <Unique State Name, 73>	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: 
{i := (i:0 + 1)
 when (i:0 <= 10 /\ 0 <= i:0 /\ t_len:1 <= 10 /\ 10 <= t_len:1
         /\ i:0 < t_len:1)}
**** alpha hat: 
  {<Split [true
            (i':1218) = (1)*(i:0) + 1
           }
          pre:
            [|t_len:1-10=0; -i:0+9>=0; i:0>=0|]
          post:
            [|t_len:1-10=0; -i':1218+10>=0; i':1218-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {i := i':1218
   when ((!(0 <= K:1224) \/ mid_i:1226 = (i:0 + K:1224))
           /\ ((K:1224 = 0 /\ i:0 = mid_i:1226)
                 \/ (1 <= K:1224 /\ (-10 + t_len:1) = 0 /\ 0 <= (9 + -i:0)
                       /\ 0 <= i:0 /\ (-10 + t_len:1) = 0
                       /\ 0 <= (10 + -mid_i:1226) /\ 0 <= (-1 + mid_i:1226)))
           /\ K:1225 = 0 /\ mid_i:1226 = i':1218 /\ 0 = K:1225
           /\ (K:1224 + K:1225) = K:1223 /\ 0 <= K:1223)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{i := (i:0 + 1)
 when (0 <= i:0 /\ p_len:11 <= 5 /\ 5 <= p_len:11 /\ i:0 < t_len:1
         /\ i:0 < p_len:11)}
**** alpha hat: 
  {<Split [true
            (i':1218) = (1)*(i:0) + 1
           }
          pre:
            [|p_len:11-5=0; -i:0+4>=0; -i:0+t_len:1-1>=0; i:0>=0|]
          post:
            [|p_len:11-5=0; -i':1218+5>=0; i':1218-1>=0; t_len:1-i':1218>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {i := i':1218
   when ((!(0 <= K:1238) \/ mid_i:1240 = (i:0 + K:1238))
           /\ ((K:1238 = 0 /\ i:0 = mid_i:1240)
                 \/ (1 <= K:1238 /\ (-5 + p_len:11) = 0 /\ 0 <= (4 + -i:0)
                       /\ 0 <= (-1 + -i:0 + t_len:1) /\ 0 <= i:0
                       /\ (-5 + p_len:11) = 0 /\ 0 <= (5 + -mid_i:1240)
                       /\ 0 <= (-1 + mid_i:1240)
                       /\ 0 <= (t_len:1 + -mid_i:1240))) /\ K:1239 = 0
           /\ mid_i:1240 = i':1218 /\ 0 = K:1239
           /\ (K:1238 + K:1239) = K:1237 /\ 0 <= K:1237)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{i := (i:0 + 1)
 when (i:0 <= 5 /\ 0 <= i:0 /\ p_len:11 <= 5 /\ 5 <= p_len:11
         /\ i:0 < t_len:1 /\ i:0 < p_len:11 /\ 0 < tr:1246
         /\ tr:1247 <= (i:0 + 1))}
**** alpha hat: 
  {<Split [true
            (i':1218) = (1)*(i:0) + 1
           }
          pre:
            [|p_len:11-5=0; -i:0+4>=0; -i:0+t_len:1-1>=0; i:0>=0|]
          post:
            [|p_len:11-5=0; -i':1218+5>=0; i':1218-1>=0; t_len:1-i':1218>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {i := i':1218
   when ((!(0 <= K:1254) \/ mid_i:1256 = (i:0 + K:1254))
           /\ ((K:1254 = 0 /\ i:0 = mid_i:1256)
                 \/ (1 <= K:1254 /\ (-5 + p_len:11) = 0 /\ 0 <= (4 + -i:0)
                       /\ 0 <= (-1 + -i:0 + t_len:1) /\ 0 <= i:0
                       /\ (-5 + p_len:11) = 0 /\ 0 <= (5 + -mid_i:1256)
                       /\ 0 <= (-1 + mid_i:1256)
                       /\ 0 <= (t_len:1 + -mid_i:1256))) /\ K:1255 = 0
           /\ mid_i:1256 = i':1218 /\ 0 = K:1255
           /\ (K:1254 + K:1255) = K:1253 /\ 0 <= K:1253)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:191 + 1)
 j := (j:558 + -tr:1279)
 k := tr:1279
 when (-1 <= k:574 /\ -1 <= j:558 /\ 1 <= __cost:191 /\ 0 <= __cost:191
         /\ 0 <= (__cost:191 + 1) /\ 0 <= j:558
         /\ (tr:1275 < tr:1276 \/ tr:1277 < tr:1278) /\ 0 <= __cost:191
         /\ 0 <= (__cost:191 + 1) /\ 0 < tr:1279 /\ tr:1279 <= (j:558 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':1280) = (1)*(__cost:191) + 1
           ((j':1281 + k':1282)) <= (1)*((j:558 + k:574)) + 1
           (j':1281) <= (1)*(j:558) + (-1)*1
           }
          pre:
            [|k:574+1>=0; __cost:191-1>=0; j:558>=0|]
          post:
            [|__cost':1280-2>=0; k':1282-1>=0; j':1281+1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':1280
   j := j':1281
   k := k':1282
   when ((!(0 <= K:1291) \/ mid___cost:1295 = (__cost:191 + K:1291))
           /\ (!(0 <= K:1291)
                 \/ (mid_j:1294 + mid_k:1293) <= ((j:558 + k:574) + K:1291))
           /\ (!(0 <= K:1291) \/ mid_j:1294 <= (j:558 + -K:1291))
           /\ ((K:1291 = 0 /\ k:574 = mid_k:1293 /\ j:558 = mid_j:1294
                  /\ __cost:191 = mid___cost:1295)
                 \/ (1 <= K:1291 /\ 0 <= (1 + k:574)
                       /\ 0 <= (-1 + __cost:191) /\ 0 <= j:558
                       /\ 0 <= (-2 + mid___cost:1295)
                       /\ 0 <= (-1 + mid_k:1293) /\ 0 <= (1 + mid_j:1294)))
           /\ K:1292 = 0 /\ mid_k:1293 = k':1282 /\ mid_j:1294 = j':1281
           /\ mid___cost:1295 = __cost':1280 /\ 0 = K:1292
           /\ (K:1291 + K:1292) = K:1290 /\ 0 <= K:1290)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':1312
 i := (i:553 + 1)
 j := (j':1311 + 1)
 k := k':1310
 when (-1 <= k:574 /\ 0 <= j:558 /\ 0 <= i:553 /\ 0 <= j:558 /\ i:553 < n:554
         /\ 0 <= __cost:191 /\ 0 <= (__cost:191 + 1)
         /\ (!(0 <= K:1305) \/ mid___cost:1306 = ((__cost:191 + 1) + K:1305))
         /\ (!(0 <= K:1305)
               \/ (mid_j:1307 + mid_k:1308) <= ((j:558 + k:574) + K:1305))
         /\ (!(0 <= K:1305) \/ mid_j:1307 <= (j:558 + -K:1305))
         /\ ((K:1305 = 0 /\ k:574 = mid_k:1308 /\ j:558 = mid_j:1307
                /\ (__cost:191 + 1) = mid___cost:1306)
               \/ (1 <= K:1305 /\ 0 <= (1 + k:574)
                     /\ 0 <= (-1 + (__cost:191 + 1)) /\ 0 <= j:558
                     /\ 0 <= (-2 + mid___cost:1306) /\ 0 <= (-1 + mid_k:1308)
                     /\ 0 <= (1 + mid_j:1307))) /\ K:1309 = 0
         /\ mid_k:1308 = k':1310 /\ mid_j:1307 = j':1311
         /\ mid___cost:1306 = __cost':1312 /\ 0 = K:1309
         /\ (K:1305 + K:1309) = K:1313 /\ 0 <= K:1313 /\ -1 <= k':1310
         /\ -1 <= j':1311 /\ 1 <= __cost':1312 /\ 0 <= __cost':1312
         /\ 0 <= (__cost':1312 + 1)
         /\ (j':1311 < 0
               \/ (0 <= j':1311 /\ tr:1318 <= tr:1319 /\ tr:1320 <= tr:1321))
         /\ !((j':1311 + 1) = m:575))}
**** alpha hat: 
  {<Split [true
            (i':1322) = (1)*(i:553) + 1
           ((-__cost':1280 + j':1281 + k':1282)) <= (1)*((-__cost:191 + j:558
                                                            + k:574)) + 0
           ((__cost':1280 + j':1281)) <= (1)*((__cost:191 + j:558)) + 2*1
           (-__cost':1280) <= (1)*(-__cost:191) + (-1)*1
           }
          pre:
            [|-i:553+n:554-1>=0; k:574+1>=0; __cost:191>=0; j:558>=0;
              i:553>=0|]
          post:
            [|-i':1322+n:554>=0; k':1282+1>=0; __cost':1280-1>=0; j':1281>=0;
              j':1281+__cost':1280-2>=0; 2j':1281+k':1282-1>=0; i':1322-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':1280
   i := i':1322
   j := j':1281
   k := k':1282
   when ((!(0 <= K:1335) \/ mid_i:1339 = (i:553 + K:1335))
           /\ (!(0 <= K:1335)
                 \/ (-mid___cost:1340 + mid_j:1338 + mid_k:1337) <= (
                    -__cost:191 + j:558 + k:574))
           /\ (!(0 <= K:1335)
                 \/ (mid___cost:1340 + mid_j:1338) <= ((__cost:191 + j:558)
                                                         + (2 * K:1335)))
           /\ (!(0 <= K:1335) \/ -mid___cost:1340 <= (-__cost:191 + -K:1335))
           /\ ((K:1335 = 0 /\ k:574 = mid_k:1337 /\ j:558 = mid_j:1338
                  /\ i:553 = mid_i:1339 /\ __cost:191 = mid___cost:1340)
                 \/ (1 <= K:1335 /\ 0 <= (-1 + -i:553 + n:554)
                       /\ 0 <= (1 + k:574) /\ 0 <= __cost:191 /\ 0 <= j:558
                       /\ 0 <= i:553 /\ 0 <= (-mid_i:1339 + n:554)
                       /\ 0 <= (1 + mid_k:1337)
                       /\ 0 <= (-1 + mid___cost:1340) /\ 0 <= mid_j:1338
                       /\ 0 <= (-2 + mid_j:1338 + mid___cost:1340)
                       /\ 0 <= (-1 + (2 * mid_j:1338) + mid_k:1337)
                       /\ 0 <= (-1 + mid_i:1339))) /\ K:1336 = 0
           /\ mid_k:1337 = k':1282 /\ mid_j:1338 = j':1281
           /\ mid_i:1339 = i':1322 /\ mid___cost:1340 = __cost':1280
           /\ 0 = K:1336 /\ (K:1335 + K:1336) = K:1334 /\ 0 <= K:1334)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
15  22  30  


New-style (IRE) regular expression in IREregExpMap for reID=15: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       t_len := 10
       p_len := 5
       i := i':1260
       param0 := t:1262
       param1 := 10
       param2 := p:1263
       param3 := 5
       param4 := b:1264
       param0@pos := type_err:1265
       param1@pos := type_err:1266
       param2@pos := type_err:1267
       param3@pos := type_err:1268
       param4@pos := type_err:1269
       param0@width := type_err:1270
       param1@width := type_err:1271
       param2@width := type_err:1272
       param3@width := type_err:1273
       param4@width := type_err:1274
       when ((!(0 <= K:1227) \/ mid_i:1228 = K:1227)
               /\ ((K:1227 = 0 /\ 0 = mid_i:1228)
                     \/ (1 <= K:1227 /\ (-10 + 10) = 0 /\ (-10 + 10) = 0
                           /\ 0 <= (10 + -mid_i:1228)
                           /\ 0 <= (-1 + mid_i:1228))) /\ K:1229 = 0
               /\ mid_i:1228 = i':1230 /\ 0 = K:1229
               /\ (K:1227 + K:1229) = K:1231 /\ 0 <= K:1231 /\ i':1230 <= 10
               /\ 0 <= i':1230 /\ 10 <= i':1230
               /\ (!(0 <= K:1241) \/ mid_i:1242 = K:1241)
               /\ ((K:1241 = 0 /\ 0 = mid_i:1242)
                     \/ (1 <= K:1241 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                           /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1242)
                           /\ 0 <= (-1 + mid_i:1242)
                           /\ 0 <= (10 + -mid_i:1242))) /\ K:1243 = 0
               /\ mid_i:1242 = i':1244 /\ 0 = K:1243
               /\ (K:1241 + K:1243) = K:1245 /\ 0 <= K:1245 /\ 0 <= i':1244
               /\ i':1244 < 10 /\ 5 <= i':1244
               /\ (!(0 <= K:1257) \/ mid_i:1258 = K:1257)
               /\ ((K:1257 = 0 /\ 0 = mid_i:1258)
                     \/ (1 <= K:1257 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                           /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1258)
                           /\ 0 <= (-1 + mid_i:1258)
                           /\ 0 <= (10 + -mid_i:1258))) /\ K:1259 = 0
               /\ mid_i:1258 = i':1260 /\ 0 = K:1259
               /\ (K:1257 + K:1259) = K:1261 /\ 0 <= K:1261 /\ i':1260 <= 5
               /\ 0 <= i':1260 /\ i':1260 < 10 /\ 5 <= i':1260)}    )
    ,
    Var(22)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:80
     return@width := type_err:81}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=22: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:512
       param1 := param1:515
       param2 := param2:518
       param3 := param3:521
       param4 := param4:524
       param0@pos := param0@pos:511
       param1@pos := type_err:531
       param2@pos := param2@pos:517
       param3@pos := type_err:532
       param4@pos := param4@pos:523
       param0@width := param0@width:510
       param1@width := type_err:533
       param2@width := param2@width:516
       param3@width := type_err:534
       param4@width := param4@width:522}    )
    ,
    Var(30)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:525
     return@width := type_err:526}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=30: 
Weight(Base relation: 
  {__cost := phi___cost:1368
   i := phi_i:1367
   j := phi_j:1366
   k := phi_k:1365
   t := param0:512
   n := param1:515
   p := param2:518
   m := param3:521
   b := param4:524
   return := phi_i:1367
   t@pos := param0@pos:511
   p@pos := param2@pos:517
   b@pos := param4@pos:523
   return@pos := type_err:1369
   t@width := param0@width:510
   p@width := param2@width:516
   b@width := param4@width:522
   return@width := type_err:1370
   when (((!(0 <= K:1341) \/ mid_i:1342 = K:1341)
            /\ (!(0 <= K:1341)
                  \/ (-mid___cost:1343 + mid_j:1344 + mid_k:1345) <= (
                     -__cost:191 + -1))
            /\ (!(0 <= K:1341)
                  \/ (mid___cost:1343 + mid_j:1344) <= (__cost:191
                                                          + (2 * K:1341)))
            /\ (!(0 <= K:1341) \/ -mid___cost:1343 <= (-__cost:191 + -K:1341))
            /\ ((K:1341 = 0 /\ -1 = mid_k:1345 /\ 0 = mid_j:1344
                   /\ 0 = mid_i:1342 /\ __cost:191 = mid___cost:1343)
                  \/ (1 <= K:1341 /\ 0 <= (-1 + param1:515) /\ 0 <= (1 + -1)
                        /\ 0 <= __cost:191 /\ 0 <= (-mid_i:1342 + param1:515)
                        /\ 0 <= (1 + mid_k:1345)
                        /\ 0 <= (-1 + mid___cost:1343) /\ 0 <= mid_j:1344
                        /\ 0 <= (-2 + mid_j:1344 + mid___cost:1343)
                        /\ 0 <= (-1 + (2 * mid_j:1344) + mid_k:1345)
                        /\ 0 <= (-1 + mid_i:1342))) /\ K:1346 = 0
            /\ mid_k:1345 = k':1347 /\ mid_j:1344 = j':1348
            /\ mid_i:1342 = i':1349 /\ mid___cost:1343 = __cost':1350
            /\ 0 = K:1346 /\ (K:1341 + K:1346) = K:1351 /\ 0 <= K:1351
            /\ -1 <= k':1347 /\ 0 <= j':1348 /\ 0 <= i':1349 /\ 0 <= j':1348
            /\ param1:515 <= i':1349 /\ __cost':1350 = phi___cost:1368
            /\ i':1349 = phi_i:1367 /\ j':1348 = phi_j:1366
            /\ k':1347 = phi_k:1365)
           \/ ((!(0 <= K:1341) \/ mid_i:1342 = K:1341)
                 /\ (!(0 <= K:1341)
                       \/ (-mid___cost:1343 + mid_j:1344 + mid_k:1345) <= (
                          -__cost:191 + -1))
                 /\ (!(0 <= K:1341)
                       \/ (mid___cost:1343 + mid_j:1344) <= (__cost:191
                                                               + (2 * K:1341)))
                 /\ (!(0 <= K:1341)
                       \/ -mid___cost:1343 <= (-__cost:191 + -K:1341))
                 /\ ((K:1341 = 0 /\ -1 = mid_k:1345 /\ 0 = mid_j:1344
                        /\ 0 = mid_i:1342 /\ __cost:191 = mid___cost:1343)
                       \/ (1 <= K:1341 /\ 0 <= (-1 + param1:515)
                             /\ 0 <= (1 + -1) /\ 0 <= __cost:191
                             /\ 0 <= (-mid_i:1342 + param1:515)
                             /\ 0 <= (1 + mid_k:1345)
                             /\ 0 <= (-1 + mid___cost:1343)
                             /\ 0 <= mid_j:1344
                             /\ 0 <= (-2 + mid_j:1344 + mid___cost:1343)
                             /\ 0 <= (-1 + (2 * mid_j:1344) + mid_k:1345)
                             /\ 0 <= (-1 + mid_i:1342))) /\ K:1346 = 0
                 /\ mid_k:1345 = k':1347 /\ mid_j:1344 = j':1348
                 /\ mid_i:1342 = i':1349 /\ mid___cost:1343 = __cost':1350
                 /\ 0 = K:1346 /\ (K:1341 + K:1346) = K:1351 /\ 0 <= K:1351
                 /\ -1 <= k':1347 /\ 0 <= j':1348 /\ 0 <= i':1349
                 /\ 0 <= j':1348 /\ i':1349 < param1:515 /\ 0 <= __cost':1350
                 /\ 0 <= (__cost':1350 + 1)
                 /\ (!(0 <= K:1352)
                       \/ mid___cost:1353 = ((__cost':1350 + 1) + K:1352))
                 /\ (!(0 <= K:1352)
                       \/ (mid_j:1354 + mid_k:1355) <= ((j':1348 + k':1347)
                                                          + K:1352))
                 /\ (!(0 <= K:1352) \/ mid_j:1354 <= (j':1348 + -K:1352))
                 /\ ((K:1352 = 0 /\ k':1347 = mid_k:1355
                        /\ j':1348 = mid_j:1354
                        /\ (__cost':1350 + 1) = mid___cost:1353)
                       \/ (1 <= K:1352 /\ 0 <= (1 + k':1347)
                             /\ 0 <= (-1 + (__cost':1350 + 1))
                             /\ 0 <= j':1348 /\ 0 <= (-2 + mid___cost:1353)
                             /\ 0 <= (-1 + mid_k:1355)
                             /\ 0 <= (1 + mid_j:1354))) /\ K:1356 = 0
                 /\ mid_k:1355 = k':1357 /\ mid_j:1354 = j':1358
                 /\ mid___cost:1353 = __cost':1359 /\ 0 = K:1356
                 /\ (K:1352 + K:1356) = K:1360 /\ 0 <= K:1360
                 /\ -1 <= k':1357 /\ -1 <= j':1358 /\ 1 <= __cost':1359
                 /\ 0 <= __cost':1359 /\ 0 <= (__cost':1359 + 1)
                 /\ (j':1358 < 0
                       \/ (0 <= j':1358 /\ tr:1361 <= tr:1362
                             /\ tr:1363 <= tr:1364))
                 /\ (j':1358 + 1) = param3:521
                 /\ __cost':1359 = phi___cost:1368
                 /\ (i':1349 + 1) = phi_i:1367 /\ (j':1358 + 1) = phi_j:1366
                 /\ k':1357 = phi_k:1365))})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := 0
         t_len := 10
         p_len := 5
         i := i':1260
         param0 := t:1262
         param1 := 10
         param2 := p:1263
         param3 := 5
         param4 := b:1264
         param0@pos := type_err:1265
         param1@pos := type_err:1266
         param2@pos := type_err:1267
         param3@pos := type_err:1268
         param4@pos := type_err:1269
         param0@width := type_err:1270
         param1@width := type_err:1271
         param2@width := type_err:1272
         param3@width := type_err:1273
         param4@width := type_err:1274
         when ((!(0 <= K:1227) \/ mid_i:1228 = K:1227)
                 /\ ((K:1227 = 0 /\ 0 = mid_i:1228)
                       \/ (1 <= K:1227 /\ (-10 + 10) = 0 /\ (-10 + 10) = 0
                             /\ 0 <= (10 + -mid_i:1228)
                             /\ 0 <= (-1 + mid_i:1228))) /\ K:1229 = 0
                 /\ mid_i:1228 = i':1230 /\ 0 = K:1229
                 /\ (K:1227 + K:1229) = K:1231 /\ 0 <= K:1231
                 /\ i':1230 <= 10 /\ 0 <= i':1230 /\ 10 <= i':1230
                 /\ (!(0 <= K:1241) \/ mid_i:1242 = K:1241)
                 /\ ((K:1241 = 0 /\ 0 = mid_i:1242)
                       \/ (1 <= K:1241 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                             /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1242)
                             /\ 0 <= (-1 + mid_i:1242)
                             /\ 0 <= (10 + -mid_i:1242))) /\ K:1243 = 0
                 /\ mid_i:1242 = i':1244 /\ 0 = K:1243
                 /\ (K:1241 + K:1243) = K:1245 /\ 0 <= K:1245 /\ 0 <= i':1244
                 /\ i':1244 < 10 /\ 5 <= i':1244
                 /\ (!(0 <= K:1257) \/ mid_i:1258 = K:1257)
                 /\ ((K:1257 = 0 /\ 0 = mid_i:1258)
                       \/ (1 <= K:1257 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                             /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1258)
                             /\ 0 <= (-1 + mid_i:1258)
                             /\ 0 <= (10 + -mid_i:1258))) /\ K:1259 = 0
                 /\ mid_i:1258 = i':1260 /\ 0 = K:1259
                 /\ (K:1257 + K:1259) = K:1261 /\ 0 <= K:1261 /\ i':1260 <= 5
                 /\ 0 <= i':1260 /\ i':1260 < 10 /\ 5 <= i':1260)}      )
      ,
      Var(22)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:80
       return@width := type_err:81}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:512
         param1 := param1:515
         param2 := param2:518
         param3 := param3:521
         param4 := param4:524
         param0@pos := param0@pos:511
         param1@pos := type_err:531
         param2@pos := param2@pos:517
         param3@pos := type_err:532
         param4@pos := param4@pos:523
         param0@width := param0@width:510
         param1@width := type_err:533
         param2@width := param2@width:516
         param3@width := type_err:534
         param4@width := param4@width:522}      )
      ,
      Var(30)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:525
       return@width := type_err:526}    )
  )
)



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

Weight(Base relation: 
  {__cost := phi___cost:1368
   return := phi_i:1367
   return@pos := type_err:1369
   return@width := type_err:1370
   when (((!(0 <= K:1341) \/ mid_i:1342 = K:1341)
            /\ (!(0 <= K:1341)
                  \/ (-mid___cost:1343 + mid_j:1344 + mid_k:1345) <= (
                     -__cost:191 + -1))
            /\ (!(0 <= K:1341)
                  \/ (mid___cost:1343 + mid_j:1344) <= (__cost:191
                                                          + (2 * K:1341)))
            /\ (!(0 <= K:1341) \/ -mid___cost:1343 <= (-__cost:191 + -K:1341))
            /\ ((K:1341 = 0 /\ -1 = mid_k:1345 /\ 0 = mid_j:1344
                   /\ 0 = mid_i:1342 /\ __cost:191 = mid___cost:1343)
                  \/ (1 <= K:1341 /\ 0 <= (-1 + param1:515) /\ 0 <= (1 + -1)
                        /\ 0 <= __cost:191 /\ 0 <= (-mid_i:1342 + param1:515)
                        /\ 0 <= (1 + mid_k:1345)
                        /\ 0 <= (-1 + mid___cost:1343) /\ 0 <= mid_j:1344
                        /\ 0 <= (-2 + mid_j:1344 + mid___cost:1343)
                        /\ 0 <= (-1 + (2 * mid_j:1344) + mid_k:1345)
                        /\ 0 <= (-1 + mid_i:1342))) /\ K:1346 = 0
            /\ mid_k:1345 = k':1347 /\ mid_j:1344 = j':1348
            /\ mid_i:1342 = i':1349 /\ mid___cost:1343 = __cost':1350
            /\ 0 = K:1346 /\ (K:1341 + K:1346) = K:1351 /\ 0 <= K:1351
            /\ -1 <= k':1347 /\ 0 <= j':1348 /\ 0 <= i':1349 /\ 0 <= j':1348
            /\ param1:515 <= i':1349 /\ __cost':1350 = phi___cost:1368
            /\ i':1349 = phi_i:1367 /\ j':1348 = phi_j:1366
            /\ k':1347 = phi_k:1365)
           \/ ((!(0 <= K:1341) \/ mid_i:1342 = K:1341)
                 /\ (!(0 <= K:1341)
                       \/ (-mid___cost:1343 + mid_j:1344 + mid_k:1345) <= (
                          -__cost:191 + -1))
                 /\ (!(0 <= K:1341)
                       \/ (mid___cost:1343 + mid_j:1344) <= (__cost:191
                                                               + (2 * K:1341)))
                 /\ (!(0 <= K:1341)
                       \/ -mid___cost:1343 <= (-__cost:191 + -K:1341))
                 /\ ((K:1341 = 0 /\ -1 = mid_k:1345 /\ 0 = mid_j:1344
                        /\ 0 = mid_i:1342 /\ __cost:191 = mid___cost:1343)
                       \/ (1 <= K:1341 /\ 0 <= (-1 + param1:515)
                             /\ 0 <= (1 + -1) /\ 0 <= __cost:191
                             /\ 0 <= (-mid_i:1342 + param1:515)
                             /\ 0 <= (1 + mid_k:1345)
                             /\ 0 <= (-1 + mid___cost:1343)
                             /\ 0 <= mid_j:1344
                             /\ 0 <= (-2 + mid_j:1344 + mid___cost:1343)
                             /\ 0 <= (-1 + (2 * mid_j:1344) + mid_k:1345)
                             /\ 0 <= (-1 + mid_i:1342))) /\ K:1346 = 0
                 /\ mid_k:1345 = k':1347 /\ mid_j:1344 = j':1348
                 /\ mid_i:1342 = i':1349 /\ mid___cost:1343 = __cost':1350
                 /\ 0 = K:1346 /\ (K:1341 + K:1346) = K:1351 /\ 0 <= K:1351
                 /\ -1 <= k':1347 /\ 0 <= j':1348 /\ 0 <= i':1349
                 /\ 0 <= j':1348 /\ i':1349 < param1:515 /\ 0 <= __cost':1350
                 /\ 0 <= (__cost':1350 + 1)
                 /\ (!(0 <= K:1352)
                       \/ mid___cost:1353 = ((__cost':1350 + 1) + K:1352))
                 /\ (!(0 <= K:1352)
                       \/ (mid_j:1354 + mid_k:1355) <= ((j':1348 + k':1347)
                                                          + K:1352))
                 /\ (!(0 <= K:1352) \/ mid_j:1354 <= (j':1348 + -K:1352))
                 /\ ((K:1352 = 0 /\ k':1347 = mid_k:1355
                        /\ j':1348 = mid_j:1354
                        /\ (__cost':1350 + 1) = mid___cost:1353)
                       \/ (1 <= K:1352 /\ 0 <= (1 + k':1347)
                             /\ 0 <= (-1 + (__cost':1350 + 1))
                             /\ 0 <= j':1348 /\ 0 <= (-2 + mid___cost:1353)
                             /\ 0 <= (-1 + mid_k:1355)
                             /\ 0 <= (1 + mid_j:1354))) /\ K:1356 = 0
                 /\ mid_k:1355 = k':1357 /\ mid_j:1354 = j':1358
                 /\ mid___cost:1353 = __cost':1359 /\ 0 = K:1356
                 /\ (K:1352 + K:1356) = K:1360 /\ 0 <= K:1360
                 /\ -1 <= k':1357 /\ -1 <= j':1358 /\ 1 <= __cost':1359
                 /\ 0 <= __cost':1359 /\ 0 <= (__cost':1359 + 1)
                 /\ (j':1358 < 0
                       \/ (0 <= j':1358 /\ tr:1361 <= tr:1362
                             /\ tr:1363 <= tr:1364))
                 /\ (j':1358 + 1) = param3:521
                 /\ __cost':1359 = phi___cost:1368
                 /\ (i':1349 + 1) = phi_i:1367 /\ (j':1358 + 1) = phi_j:1366
                 /\ k':1357 = phi_k:1365))})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=15: 
Weight(Base relation: 
  {__cost := phi___cost:1445
   return := 0
   param0 := t:1262
   param1 := 10
   param2 := p:1263
   param3 := 5
   param4 := b:1264
   return@pos := type_err:1468
   param0@pos := type_err:1265
   param1@pos := type_err:1463
   param2@pos := type_err:1267
   param3@pos := type_err:1464
   param4@pos := type_err:1269
   return@width := type_err:1469
   param0@width := type_err:1270
   param1@width := type_err:1466
   param2@width := type_err:1272
   param3@width := type_err:1467
   param4@width := type_err:1274
   when ((!(0 <= K:1227) \/ mid_i:1228 = K:1227)
           /\ ((K:1227 = 0 /\ 0 = mid_i:1228)
                 \/ (1 <= K:1227 /\ (-10 + 10) = 0 /\ (-10 + 10) = 0
                       /\ 0 <= (10 + -mid_i:1228) /\ 0 <= (-1 + mid_i:1228)))
           /\ K:1229 = 0 /\ mid_i:1228 = i':1230 /\ 0 = K:1229
           /\ (K:1227 + K:1229) = K:1231 /\ 0 <= K:1231 /\ i':1230 <= 10
           /\ 0 <= i':1230 /\ 10 <= i':1230
           /\ (!(0 <= K:1241) \/ mid_i:1242 = K:1241)
           /\ ((K:1241 = 0 /\ 0 = mid_i:1242)
                 \/ (1 <= K:1241 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                       /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1242)
                       /\ 0 <= (-1 + mid_i:1242) /\ 0 <= (10 + -mid_i:1242)))
           /\ K:1243 = 0 /\ mid_i:1242 = i':1244 /\ 0 = K:1243
           /\ (K:1241 + K:1243) = K:1245 /\ 0 <= K:1245 /\ 0 <= i':1244
           /\ i':1244 < 10 /\ 5 <= i':1244
           /\ (!(0 <= K:1257) \/ mid_i:1258 = K:1257)
           /\ ((K:1257 = 0 /\ 0 = mid_i:1258)
                 \/ (1 <= K:1257 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                       /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1258)
                       /\ 0 <= (-1 + mid_i:1258) /\ 0 <= (10 + -mid_i:1258)))
           /\ K:1259 = 0 /\ mid_i:1258 = i':1260 /\ 0 = K:1259
           /\ (K:1257 + K:1259) = K:1261 /\ 0 <= K:1261 /\ i':1260 <= 5
           /\ 0 <= i':1260 /\ i':1260 < 10 /\ 5 <= i':1260
           /\ (((!(0 <= K:1434) \/ mid_i:1435 = K:1434)
                  /\ (!(0 <= K:1434)
                        \/ (-mid___cost:1436 + mid_j:1437 + mid_k:1438) <= -1)
                  /\ (!(0 <= K:1434)
                        \/ (mid___cost:1436 + mid_j:1437) <= (2 * K:1434))
                  /\ (!(0 <= K:1434) \/ -mid___cost:1436 <= -K:1434)
                  /\ ((K:1434 = 0 /\ -1 = mid_k:1438 /\ 0 = mid_j:1437
                         /\ 0 = mid_i:1435 /\ 0 = mid___cost:1436)
                        \/ (1 <= K:1434 /\ 0 <= (-1 + 10) /\ 0 <= (1 + -1)
                              /\ 0 <= (-mid_i:1435 + 10)
                              /\ 0 <= (1 + mid_k:1438)
                              /\ 0 <= (-1 + mid___cost:1436)
                              /\ 0 <= mid_j:1437
                              /\ 0 <= (-2 + mid_j:1437 + mid___cost:1436)
                              /\ 0 <= (-1 + (2 * mid_j:1437) + mid_k:1438)
                              /\ 0 <= (-1 + mid_i:1435))) /\ K:1439 = 0
                  /\ mid_k:1438 = k':1440 /\ mid_j:1437 = j':1441
                  /\ mid_i:1435 = i':1442 /\ mid___cost:1436 = __cost':1443
                  /\ 0 = K:1439 /\ (K:1434 + K:1439) = K:1444 /\ 0 <= K:1444
                  /\ -1 <= k':1440 /\ 0 <= j':1441 /\ 0 <= i':1442
                  /\ 0 <= j':1441 /\ 10 <= i':1442
                  /\ __cost':1443 = phi___cost:1445 /\ i':1442 = phi_i:1446
                  /\ j':1441 = phi_j:1447 /\ k':1440 = phi_k:1448)
                 \/ ((!(0 <= K:1434) \/ mid_i:1435 = K:1434)
                       /\ (!(0 <= K:1434)
                             \/ (-mid___cost:1436 + mid_j:1437 + mid_k:1438) <= -1)
                       /\ (!(0 <= K:1434)
                             \/ (mid___cost:1436 + mid_j:1437) <= (2 * K:1434))
                       /\ (!(0 <= K:1434) \/ -mid___cost:1436 <= -K:1434)
                       /\ ((K:1434 = 0 /\ -1 = mid_k:1438 /\ 0 = mid_j:1437
                              /\ 0 = mid_i:1435 /\ 0 = mid___cost:1436)
                             \/ (1 <= K:1434 /\ 0 <= (-1 + 10)
                                   /\ 0 <= (1 + -1)
                                   /\ 0 <= (-mid_i:1435 + 10)
                                   /\ 0 <= (1 + mid_k:1438)
                                   /\ 0 <= (-1 + mid___cost:1436)
                                   /\ 0 <= mid_j:1437
                                   /\ 0 <= (-2 + mid_j:1437 + mid___cost:1436)
                                   /\ 0 <= (-1 + (2 * mid_j:1437)
                                              + mid_k:1438)
                                   /\ 0 <= (-1 + mid_i:1435))) /\ K:1439 = 0
                       /\ mid_k:1438 = k':1440 /\ mid_j:1437 = j':1441
                       /\ mid_i:1435 = i':1442
                       /\ mid___cost:1436 = __cost':1443 /\ 0 = K:1439
                       /\ (K:1434 + K:1439) = K:1444 /\ 0 <= K:1444
                       /\ -1 <= k':1440 /\ 0 <= j':1441 /\ 0 <= i':1442
                       /\ 0 <= j':1441 /\ i':1442 < 10 /\ 0 <= __cost':1443
                       /\ 0 <= (__cost':1443 + 1)
                       /\ (!(0 <= K:1449)
                             \/ mid___cost:1450 = ((__cost':1443 + 1)
                                                     + K:1449))
                       /\ (!(0 <= K:1449)
                             \/ (mid_j:1451 + mid_k:1452) <= ((j':1441
                                                                 + k':1440)
                                                                + K:1449))
                       /\ (!(0 <= K:1449)
                             \/ mid_j:1451 <= (j':1441 + -K:1449))
                       /\ ((K:1449 = 0 /\ k':1440 = mid_k:1452
                              /\ j':1441 = mid_j:1451
                              /\ (__cost':1443 + 1) = mid___cost:1450)
                             \/ (1 <= K:1449 /\ 0 <= (1 + k':1440)
                                   /\ 0 <= (-1 + (__cost':1443 + 1))
                                   /\ 0 <= j':1441
                                   /\ 0 <= (-2 + mid___cost:1450)
                                   /\ 0 <= (-1 + mid_k:1452)
                                   /\ 0 <= (1 + mid_j:1451))) /\ K:1453 = 0
                       /\ mid_k:1452 = k':1454 /\ mid_j:1451 = j':1455
                       /\ mid___cost:1450 = __cost':1456 /\ 0 = K:1453
                       /\ (K:1449 + K:1453) = K:1457 /\ 0 <= K:1457
                       /\ -1 <= k':1454 /\ -1 <= j':1455 /\ 1 <= __cost':1456
                       /\ 0 <= __cost':1456 /\ 0 <= (__cost':1456 + 1)
                       /\ (j':1455 < 0
                             \/ (0 <= j':1455 /\ tr:1458 <= tr:1459
                                   /\ tr:1460 <= tr:1461))
                       /\ (j':1455 + 1) = 5 /\ __cost':1456 = phi___cost:1445
                       /\ (i':1442 + 1) = phi_i:1446
                       /\ (j':1455 + 1) = phi_j:1447 /\ k':1454 = phi_k:1448)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=22: 
Weight(Base relation: 
  {__cost := phi___cost:1481
   return := 0
   param0 := param0:512
   param1 := param1:515
   param2 := param2:518
   param3 := param3:521
   param4 := param4:524
   return@pos := type_err:1500
   param0@pos := param0@pos:511
   param1@pos := type_err:531
   param2@pos := param2@pos:517
   param3@pos := type_err:532
   param4@pos := param4@pos:523
   return@width := type_err:1501
   param0@width := param0@width:510
   param1@width := type_err:533
   param2@width := param2@width:516
   param3@width := type_err:534
   param4@width := param4@width:522
   when (((!(0 <= K:1470) \/ mid_i:1471 = K:1470)
            /\ (!(0 <= K:1470)
                  \/ (-mid___cost:1472 + mid_j:1473 + mid_k:1474) <= (
                     -__cost:191 + -1))
            /\ (!(0 <= K:1470)
                  \/ (mid___cost:1472 + mid_j:1473) <= (__cost:191
                                                          + (2 * K:1470)))
            /\ (!(0 <= K:1470) \/ -mid___cost:1472 <= (-__cost:191 + -K:1470))
            /\ ((K:1470 = 0 /\ -1 = mid_k:1474 /\ 0 = mid_j:1473
                   /\ 0 = mid_i:1471 /\ __cost:191 = mid___cost:1472)
                  \/ (1 <= K:1470 /\ 0 <= (-1 + param1:515) /\ 0 <= (1 + -1)
                        /\ 0 <= __cost:191 /\ 0 <= (-mid_i:1471 + param1:515)
                        /\ 0 <= (1 + mid_k:1474)
                        /\ 0 <= (-1 + mid___cost:1472) /\ 0 <= mid_j:1473
                        /\ 0 <= (-2 + mid_j:1473 + mid___cost:1472)
                        /\ 0 <= (-1 + (2 * mid_j:1473) + mid_k:1474)
                        /\ 0 <= (-1 + mid_i:1471))) /\ K:1475 = 0
            /\ mid_k:1474 = k':1476 /\ mid_j:1473 = j':1477
            /\ mid_i:1471 = i':1478 /\ mid___cost:1472 = __cost':1479
            /\ 0 = K:1475 /\ (K:1470 + K:1475) = K:1480 /\ 0 <= K:1480
            /\ -1 <= k':1476 /\ 0 <= j':1477 /\ 0 <= i':1478 /\ 0 <= j':1477
            /\ param1:515 <= i':1478 /\ __cost':1479 = phi___cost:1481
            /\ i':1478 = phi_i:1482 /\ j':1477 = phi_j:1483
            /\ k':1476 = phi_k:1484)
           \/ ((!(0 <= K:1470) \/ mid_i:1471 = K:1470)
                 /\ (!(0 <= K:1470)
                       \/ (-mid___cost:1472 + mid_j:1473 + mid_k:1474) <= (
                          -__cost:191 + -1))
                 /\ (!(0 <= K:1470)
                       \/ (mid___cost:1472 + mid_j:1473) <= (__cost:191
                                                               + (2 * K:1470)))
                 /\ (!(0 <= K:1470)
                       \/ -mid___cost:1472 <= (-__cost:191 + -K:1470))
                 /\ ((K:1470 = 0 /\ -1 = mid_k:1474 /\ 0 = mid_j:1473
                        /\ 0 = mid_i:1471 /\ __cost:191 = mid___cost:1472)
                       \/ (1 <= K:1470 /\ 0 <= (-1 + param1:515)
                             /\ 0 <= (1 + -1) /\ 0 <= __cost:191
                             /\ 0 <= (-mid_i:1471 + param1:515)
                             /\ 0 <= (1 + mid_k:1474)
                             /\ 0 <= (-1 + mid___cost:1472)
                             /\ 0 <= mid_j:1473
                             /\ 0 <= (-2 + mid_j:1473 + mid___cost:1472)
                             /\ 0 <= (-1 + (2 * mid_j:1473) + mid_k:1474)
                             /\ 0 <= (-1 + mid_i:1471))) /\ K:1475 = 0
                 /\ mid_k:1474 = k':1476 /\ mid_j:1473 = j':1477
                 /\ mid_i:1471 = i':1478 /\ mid___cost:1472 = __cost':1479
                 /\ 0 = K:1475 /\ (K:1470 + K:1475) = K:1480 /\ 0 <= K:1480
                 /\ -1 <= k':1476 /\ 0 <= j':1477 /\ 0 <= i':1478
                 /\ 0 <= j':1477 /\ i':1478 < param1:515 /\ 0 <= __cost':1479
                 /\ 0 <= (__cost':1479 + 1)
                 /\ (!(0 <= K:1485)
                       \/ mid___cost:1486 = ((__cost':1479 + 1) + K:1485))
                 /\ (!(0 <= K:1485)
                       \/ (mid_j:1487 + mid_k:1488) <= ((j':1477 + k':1476)
                                                          + K:1485))
                 /\ (!(0 <= K:1485) \/ mid_j:1487 <= (j':1477 + -K:1485))
                 /\ ((K:1485 = 0 /\ k':1476 = mid_k:1488
                        /\ j':1477 = mid_j:1487
                        /\ (__cost':1479 + 1) = mid___cost:1486)
                       \/ (1 <= K:1485 /\ 0 <= (1 + k':1476)
                             /\ 0 <= (-1 + (__cost':1479 + 1))
                             /\ 0 <= j':1477 /\ 0 <= (-2 + mid___cost:1486)
                             /\ 0 <= (-1 + mid_k:1488)
                             /\ 0 <= (1 + mid_j:1487))) /\ K:1489 = 0
                 /\ mid_k:1488 = k':1490 /\ mid_j:1487 = j':1491
                 /\ mid___cost:1486 = __cost':1492 /\ 0 = K:1489
                 /\ (K:1485 + K:1489) = K:1493 /\ 0 <= K:1493
                 /\ -1 <= k':1490 /\ -1 <= j':1491 /\ 1 <= __cost':1492
                 /\ 0 <= __cost':1492 /\ 0 <= (__cost':1492 + 1)
                 /\ (j':1491 < 0
                       \/ (0 <= j':1491 /\ tr:1494 <= tr:1495
                             /\ tr:1496 <= tr:1497))
                 /\ (j':1491 + 1) = param3:521
                 /\ __cost':1492 = phi___cost:1481
                 /\ (i':1478 + 1) = phi_i:1482 /\ (j':1491 + 1) = phi_j:1483
                 /\ k':1490 = phi_k:1484))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=30: 
Weight(Base relation: 
  {__cost := phi___cost:1368
   return := phi_i:1367
   return@pos := type_err:1369
   return@width := type_err:1370
   when (((!(0 <= K:1341) \/ mid_i:1342 = K:1341)
            /\ (!(0 <= K:1341)
                  \/ (-mid___cost:1343 + mid_j:1344 + mid_k:1345) <= (
                     -__cost:191 + -1))
            /\ (!(0 <= K:1341)
                  \/ (mid___cost:1343 + mid_j:1344) <= (__cost:191
                                                          + (2 * K:1341)))
            /\ (!(0 <= K:1341) \/ -mid___cost:1343 <= (-__cost:191 + -K:1341))
            /\ ((K:1341 = 0 /\ -1 = mid_k:1345 /\ 0 = mid_j:1344
                   /\ 0 = mid_i:1342 /\ __cost:191 = mid___cost:1343)
                  \/ (1 <= K:1341 /\ 0 <= (-1 + param1:515) /\ 0 <= (1 + -1)
                        /\ 0 <= __cost:191 /\ 0 <= (-mid_i:1342 + param1:515)
                        /\ 0 <= (1 + mid_k:1345)
                        /\ 0 <= (-1 + mid___cost:1343) /\ 0 <= mid_j:1344
                        /\ 0 <= (-2 + mid_j:1344 + mid___cost:1343)
                        /\ 0 <= (-1 + (2 * mid_j:1344) + mid_k:1345)
                        /\ 0 <= (-1 + mid_i:1342))) /\ K:1346 = 0
            /\ mid_k:1345 = k':1347 /\ mid_j:1344 = j':1348
            /\ mid_i:1342 = i':1349 /\ mid___cost:1343 = __cost':1350
            /\ 0 = K:1346 /\ (K:1341 + K:1346) = K:1351 /\ 0 <= K:1351
            /\ -1 <= k':1347 /\ 0 <= j':1348 /\ 0 <= i':1349 /\ 0 <= j':1348
            /\ param1:515 <= i':1349 /\ __cost':1350 = phi___cost:1368
            /\ i':1349 = phi_i:1367 /\ j':1348 = phi_j:1366
            /\ k':1347 = phi_k:1365)
           \/ ((!(0 <= K:1341) \/ mid_i:1342 = K:1341)
                 /\ (!(0 <= K:1341)
                       \/ (-mid___cost:1343 + mid_j:1344 + mid_k:1345) <= (
                          -__cost:191 + -1))
                 /\ (!(0 <= K:1341)
                       \/ (mid___cost:1343 + mid_j:1344) <= (__cost:191
                                                               + (2 * K:1341)))
                 /\ (!(0 <= K:1341)
                       \/ -mid___cost:1343 <= (-__cost:191 + -K:1341))
                 /\ ((K:1341 = 0 /\ -1 = mid_k:1345 /\ 0 = mid_j:1344
                        /\ 0 = mid_i:1342 /\ __cost:191 = mid___cost:1343)
                       \/ (1 <= K:1341 /\ 0 <= (-1 + param1:515)
                             /\ 0 <= (1 + -1) /\ 0 <= __cost:191
                             /\ 0 <= (-mid_i:1342 + param1:515)
                             /\ 0 <= (1 + mid_k:1345)
                             /\ 0 <= (-1 + mid___cost:1343)
                             /\ 0 <= mid_j:1344
                             /\ 0 <= (-2 + mid_j:1344 + mid___cost:1343)
                             /\ 0 <= (-1 + (2 * mid_j:1344) + mid_k:1345)
                             /\ 0 <= (-1 + mid_i:1342))) /\ K:1346 = 0
                 /\ mid_k:1345 = k':1347 /\ mid_j:1344 = j':1348
                 /\ mid_i:1342 = i':1349 /\ mid___cost:1343 = __cost':1350
                 /\ 0 = K:1346 /\ (K:1341 + K:1346) = K:1351 /\ 0 <= K:1351
                 /\ -1 <= k':1347 /\ 0 <= j':1348 /\ 0 <= i':1349
                 /\ 0 <= j':1348 /\ i':1349 < param1:515 /\ 0 <= __cost':1350
                 /\ 0 <= (__cost':1350 + 1)
                 /\ (!(0 <= K:1352)
                       \/ mid___cost:1353 = ((__cost':1350 + 1) + K:1352))
                 /\ (!(0 <= K:1352)
                       \/ (mid_j:1354 + mid_k:1355) <= ((j':1348 + k':1347)
                                                          + K:1352))
                 /\ (!(0 <= K:1352) \/ mid_j:1354 <= (j':1348 + -K:1352))
                 /\ ((K:1352 = 0 /\ k':1347 = mid_k:1355
                        /\ j':1348 = mid_j:1354
                        /\ (__cost':1350 + 1) = mid___cost:1353)
                       \/ (1 <= K:1352 /\ 0 <= (1 + k':1347)
                             /\ 0 <= (-1 + (__cost':1350 + 1))
                             /\ 0 <= j':1348 /\ 0 <= (-2 + mid___cost:1353)
                             /\ 0 <= (-1 + mid_k:1355)
                             /\ 0 <= (1 + mid_j:1354))) /\ K:1356 = 0
                 /\ mid_k:1355 = k':1357 /\ mid_j:1354 = j':1358
                 /\ mid___cost:1353 = __cost':1359 /\ 0 = K:1356
                 /\ (K:1352 + K:1356) = K:1360 /\ 0 <= K:1360
                 /\ -1 <= k':1357 /\ -1 <= j':1358 /\ 1 <= __cost':1359
                 /\ 0 <= __cost':1359 /\ 0 <= (__cost':1359 + 1)
                 /\ (j':1358 < 0
                       \/ (0 <= j':1358 /\ tr:1361 <= tr:1362
                             /\ tr:1363 <= tr:1364))
                 /\ (j':1358 + 1) = param3:521
                 /\ __cost':1359 = phi___cost:1368
                 /\ (i':1349 + 1) = phi_i:1367 /\ (j':1358 + 1) = phi_j:1366
                 /\ k':1357 = phi_k:1365))})


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

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:1445
 return := 0
 param0 := t:1262
 param1 := 10
 param2 := p:1263
 param3 := 5
 param4 := b:1264
 return@pos := type_err:1468
 param0@pos := type_err:1265
 param1@pos := type_err:1463
 param2@pos := type_err:1267
 param3@pos := type_err:1464
 param4@pos := type_err:1269
 return@width := type_err:1469
 param0@width := type_err:1270
 param1@width := type_err:1466
 param2@width := type_err:1272
 param3@width := type_err:1467
 param4@width := type_err:1274
 when ((!(0 <= K:1227) \/ mid_i:1228 = K:1227)
         /\ ((K:1227 = 0 /\ 0 = mid_i:1228)
               \/ (1 <= K:1227 /\ (-10 + 10) = 0 /\ (-10 + 10) = 0
                     /\ 0 <= (10 + -mid_i:1228) /\ 0 <= (-1 + mid_i:1228)))
         /\ K:1229 = 0 /\ mid_i:1228 = i':1230 /\ 0 = K:1229
         /\ (K:1227 + K:1229) = K:1231 /\ 0 <= K:1231 /\ i':1230 <= 10
         /\ 0 <= i':1230 /\ 10 <= i':1230
         /\ (!(0 <= K:1241) \/ mid_i:1242 = K:1241)
         /\ ((K:1241 = 0 /\ 0 = mid_i:1242)
               \/ (1 <= K:1241 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                     /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1242)
                     /\ 0 <= (-1 + mid_i:1242) /\ 0 <= (10 + -mid_i:1242)))
         /\ K:1243 = 0 /\ mid_i:1242 = i':1244 /\ 0 = K:1243
         /\ (K:1241 + K:1243) = K:1245 /\ 0 <= K:1245 /\ 0 <= i':1244
         /\ i':1244 < 10 /\ 5 <= i':1244
         /\ (!(0 <= K:1257) \/ mid_i:1258 = K:1257)
         /\ ((K:1257 = 0 /\ 0 = mid_i:1258)
               \/ (1 <= K:1257 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                     /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1258)
                     /\ 0 <= (-1 + mid_i:1258) /\ 0 <= (10 + -mid_i:1258)))
         /\ K:1259 = 0 /\ mid_i:1258 = i':1260 /\ 0 = K:1259
         /\ (K:1257 + K:1259) = K:1261 /\ 0 <= K:1261 /\ i':1260 <= 5
         /\ 0 <= i':1260 /\ i':1260 < 10 /\ 5 <= i':1260
         /\ (((!(0 <= K:1434) \/ mid_i:1435 = K:1434)
                /\ (!(0 <= K:1434)
                      \/ (-mid___cost:1436 + mid_j:1437 + mid_k:1438) <= -1)
                /\ (!(0 <= K:1434)
                      \/ (mid___cost:1436 + mid_j:1437) <= (2 * K:1434))
                /\ (!(0 <= K:1434) \/ -mid___cost:1436 <= -K:1434)
                /\ ((K:1434 = 0 /\ -1 = mid_k:1438 /\ 0 = mid_j:1437
                       /\ 0 = mid_i:1435 /\ 0 = mid___cost:1436)
                      \/ (1 <= K:1434 /\ 0 <= (-1 + 10) /\ 0 <= (1 + -1)
                            /\ 0 <= (-mid_i:1435 + 10)
                            /\ 0 <= (1 + mid_k:1438)
                            /\ 0 <= (-1 + mid___cost:1436) /\ 0 <= mid_j:1437
                            /\ 0 <= (-2 + mid_j:1437 + mid___cost:1436)
                            /\ 0 <= (-1 + (2 * mid_j:1437) + mid_k:1438)
                            /\ 0 <= (-1 + mid_i:1435))) /\ K:1439 = 0
                /\ mid_k:1438 = k':1440 /\ mid_j:1437 = j':1441
                /\ mid_i:1435 = i':1442 /\ mid___cost:1436 = __cost':1443
                /\ 0 = K:1439 /\ (K:1434 + K:1439) = K:1444 /\ 0 <= K:1444
                /\ -1 <= k':1440 /\ 0 <= j':1441 /\ 0 <= i':1442
                /\ 0 <= j':1441 /\ 10 <= i':1442
                /\ __cost':1443 = phi___cost:1445 /\ i':1442 = phi_i:1446
                /\ j':1441 = phi_j:1447 /\ k':1440 = phi_k:1448)
               \/ ((!(0 <= K:1434) \/ mid_i:1435 = K:1434)
                     /\ (!(0 <= K:1434)
                           \/ (-mid___cost:1436 + mid_j:1437 + mid_k:1438) <= -1)
                     /\ (!(0 <= K:1434)
                           \/ (mid___cost:1436 + mid_j:1437) <= (2 * K:1434))
                     /\ (!(0 <= K:1434) \/ -mid___cost:1436 <= -K:1434)
                     /\ ((K:1434 = 0 /\ -1 = mid_k:1438 /\ 0 = mid_j:1437
                            /\ 0 = mid_i:1435 /\ 0 = mid___cost:1436)
                           \/ (1 <= K:1434 /\ 0 <= (-1 + 10) /\ 0 <= (1 + -1)
                                 /\ 0 <= (-mid_i:1435 + 10)
                                 /\ 0 <= (1 + mid_k:1438)
                                 /\ 0 <= (-1 + mid___cost:1436)
                                 /\ 0 <= mid_j:1437
                                 /\ 0 <= (-2 + mid_j:1437 + mid___cost:1436)
                                 /\ 0 <= (-1 + (2 * mid_j:1437) + mid_k:1438)
                                 /\ 0 <= (-1 + mid_i:1435))) /\ K:1439 = 0
                     /\ mid_k:1438 = k':1440 /\ mid_j:1437 = j':1441
                     /\ mid_i:1435 = i':1442
                     /\ mid___cost:1436 = __cost':1443 /\ 0 = K:1439
                     /\ (K:1434 + K:1439) = K:1444 /\ 0 <= K:1444
                     /\ -1 <= k':1440 /\ 0 <= j':1441 /\ 0 <= i':1442
                     /\ 0 <= j':1441 /\ i':1442 < 10 /\ 0 <= __cost':1443
                     /\ 0 <= (__cost':1443 + 1)
                     /\ (!(0 <= K:1449)
                           \/ mid___cost:1450 = ((__cost':1443 + 1) + K:1449))
                     /\ (!(0 <= K:1449)
                           \/ (mid_j:1451 + mid_k:1452) <= ((j':1441
                                                               + k':1440)
                                                              + K:1449))
                     /\ (!(0 <= K:1449) \/ mid_j:1451 <= (j':1441 + -K:1449))
                     /\ ((K:1449 = 0 /\ k':1440 = mid_k:1452
                            /\ j':1441 = mid_j:1451
                            /\ (__cost':1443 + 1) = mid___cost:1450)
                           \/ (1 <= K:1449 /\ 0 <= (1 + k':1440)
                                 /\ 0 <= (-1 + (__cost':1443 + 1))
                                 /\ 0 <= j':1441
                                 /\ 0 <= (-2 + mid___cost:1450)
                                 /\ 0 <= (-1 + mid_k:1452)
                                 /\ 0 <= (1 + mid_j:1451))) /\ K:1453 = 0
                     /\ mid_k:1452 = k':1454 /\ mid_j:1451 = j':1455
                     /\ mid___cost:1450 = __cost':1456 /\ 0 = K:1453
                     /\ (K:1449 + K:1453) = K:1457 /\ 0 <= K:1457
                     /\ -1 <= k':1454 /\ -1 <= j':1455 /\ 1 <= __cost':1456
                     /\ 0 <= __cost':1456 /\ 0 <= (__cost':1456 + 1)
                     /\ (j':1455 < 0
                           \/ (0 <= j':1455 /\ tr:1458 <= tr:1459
                                 /\ tr:1460 <= tr:1461)) /\ (j':1455 + 1) = 5
                     /\ __cost':1456 = phi___cost:1445
                     /\ (i':1442 + 1) = phi_i:1446
                     /\ (j':1455 + 1) = phi_j:1447 /\ k':1454 = phi_k:1448)))}

Evaluating variable number 22 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:1481
 return := 0
 param0 := param0:512
 param1 := param1:515
 param2 := param2:518
 param3 := param3:521
 param4 := param4:524
 return@pos := type_err:1500
 param0@pos := param0@pos:511
 param1@pos := type_err:531
 param2@pos := param2@pos:517
 param3@pos := type_err:532
 param4@pos := param4@pos:523
 return@width := type_err:1501
 param0@width := param0@width:510
 param1@width := type_err:533
 param2@width := param2@width:516
 param3@width := type_err:534
 param4@width := param4@width:522
 when (((!(0 <= K:1470) \/ mid_i:1471 = K:1470)
          /\ (!(0 <= K:1470)
                \/ (-mid___cost:1472 + mid_j:1473 + mid_k:1474) <= (-__cost:191
                                                                    + -1))
          /\ (!(0 <= K:1470)
                \/ (mid___cost:1472 + mid_j:1473) <= (__cost:191
                                                        + (2 * K:1470)))
          /\ (!(0 <= K:1470) \/ -mid___cost:1472 <= (-__cost:191 + -K:1470))
          /\ ((K:1470 = 0 /\ -1 = mid_k:1474 /\ 0 = mid_j:1473
                 /\ 0 = mid_i:1471 /\ __cost:191 = mid___cost:1472)
                \/ (1 <= K:1470 /\ 0 <= (-1 + param1:515) /\ 0 <= (1 + -1)
                      /\ 0 <= __cost:191 /\ 0 <= (-mid_i:1471 + param1:515)
                      /\ 0 <= (1 + mid_k:1474) /\ 0 <= (-1 + mid___cost:1472)
                      /\ 0 <= mid_j:1473
                      /\ 0 <= (-2 + mid_j:1473 + mid___cost:1472)
                      /\ 0 <= (-1 + (2 * mid_j:1473) + mid_k:1474)
                      /\ 0 <= (-1 + mid_i:1471))) /\ K:1475 = 0
          /\ mid_k:1474 = k':1476 /\ mid_j:1473 = j':1477
          /\ mid_i:1471 = i':1478 /\ mid___cost:1472 = __cost':1479
          /\ 0 = K:1475 /\ (K:1470 + K:1475) = K:1480 /\ 0 <= K:1480
          /\ -1 <= k':1476 /\ 0 <= j':1477 /\ 0 <= i':1478 /\ 0 <= j':1477
          /\ param1:515 <= i':1478 /\ __cost':1479 = phi___cost:1481
          /\ i':1478 = phi_i:1482 /\ j':1477 = phi_j:1483
          /\ k':1476 = phi_k:1484)
         \/ ((!(0 <= K:1470) \/ mid_i:1471 = K:1470)
               /\ (!(0 <= K:1470)
                     \/ (-mid___cost:1472 + mid_j:1473 + mid_k:1474) <= (
                        -__cost:191 + -1))
               /\ (!(0 <= K:1470)
                     \/ (mid___cost:1472 + mid_j:1473) <= (__cost:191
                                                             + (2 * K:1470)))
               /\ (!(0 <= K:1470)
                     \/ -mid___cost:1472 <= (-__cost:191 + -K:1470))
               /\ ((K:1470 = 0 /\ -1 = mid_k:1474 /\ 0 = mid_j:1473
                      /\ 0 = mid_i:1471 /\ __cost:191 = mid___cost:1472)
                     \/ (1 <= K:1470 /\ 0 <= (-1 + param1:515)
                           /\ 0 <= (1 + -1) /\ 0 <= __cost:191
                           /\ 0 <= (-mid_i:1471 + param1:515)
                           /\ 0 <= (1 + mid_k:1474)
                           /\ 0 <= (-1 + mid___cost:1472) /\ 0 <= mid_j:1473
                           /\ 0 <= (-2 + mid_j:1473 + mid___cost:1472)
                           /\ 0 <= (-1 + (2 * mid_j:1473) + mid_k:1474)
                           /\ 0 <= (-1 + mid_i:1471))) /\ K:1475 = 0
               /\ mid_k:1474 = k':1476 /\ mid_j:1473 = j':1477
               /\ mid_i:1471 = i':1478 /\ mid___cost:1472 = __cost':1479
               /\ 0 = K:1475 /\ (K:1470 + K:1475) = K:1480 /\ 0 <= K:1480
               /\ -1 <= k':1476 /\ 0 <= j':1477 /\ 0 <= i':1478
               /\ 0 <= j':1477 /\ i':1478 < param1:515 /\ 0 <= __cost':1479
               /\ 0 <= (__cost':1479 + 1)
               /\ (!(0 <= K:1485)
                     \/ mid___cost:1486 = ((__cost':1479 + 1) + K:1485))
               /\ (!(0 <= K:1485)
                     \/ (mid_j:1487 + mid_k:1488) <= ((j':1477 + k':1476)
                                                        + K:1485))
               /\ (!(0 <= K:1485) \/ mid_j:1487 <= (j':1477 + -K:1485))
               /\ ((K:1485 = 0 /\ k':1476 = mid_k:1488
                      /\ j':1477 = mid_j:1487
                      /\ (__cost':1479 + 1) = mid___cost:1486)
                     \/ (1 <= K:1485 /\ 0 <= (1 + k':1476)
                           /\ 0 <= (-1 + (__cost':1479 + 1)) /\ 0 <= j':1477
                           /\ 0 <= (-2 + mid___cost:1486)
                           /\ 0 <= (-1 + mid_k:1488) /\ 0 <= (1 + mid_j:1487)))
               /\ K:1489 = 0 /\ mid_k:1488 = k':1490 /\ mid_j:1487 = j':1491
               /\ mid___cost:1486 = __cost':1492 /\ 0 = K:1489
               /\ (K:1485 + K:1489) = K:1493 /\ 0 <= K:1493 /\ -1 <= k':1490
               /\ -1 <= j':1491 /\ 1 <= __cost':1492 /\ 0 <= __cost':1492
               /\ 0 <= (__cost':1492 + 1)
               /\ (j':1491 < 0
                     \/ (0 <= j':1491 /\ tr:1494 <= tr:1495
                           /\ tr:1496 <= tr:1497))
               /\ (j':1491 + 1) = param3:521
               /\ __cost':1492 = phi___cost:1481
               /\ (i':1478 + 1) = phi_i:1482 /\ (j':1491 + 1) = phi_j:1483
               /\ k':1490 = phi_k:1484))}

Evaluating variable number 30 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:1368
 return := phi_i:1367
 return@pos := type_err:1369
 return@width := type_err:1370
 when (((!(0 <= K:1341) \/ mid_i:1342 = K:1341)
          /\ (!(0 <= K:1341)
                \/ (-mid___cost:1343 + mid_j:1344 + mid_k:1345) <= (-__cost:191
                                                                    + -1))
          /\ (!(0 <= K:1341)
                \/ (mid___cost:1343 + mid_j:1344) <= (__cost:191
                                                        + (2 * K:1341)))
          /\ (!(0 <= K:1341) \/ -mid___cost:1343 <= (-__cost:191 + -K:1341))
          /\ ((K:1341 = 0 /\ -1 = mid_k:1345 /\ 0 = mid_j:1344
                 /\ 0 = mid_i:1342 /\ __cost:191 = mid___cost:1343)
                \/ (1 <= K:1341 /\ 0 <= (-1 + param1:515) /\ 0 <= (1 + -1)
                      /\ 0 <= __cost:191 /\ 0 <= (-mid_i:1342 + param1:515)
                      /\ 0 <= (1 + mid_k:1345) /\ 0 <= (-1 + mid___cost:1343)
                      /\ 0 <= mid_j:1344
                      /\ 0 <= (-2 + mid_j:1344 + mid___cost:1343)
                      /\ 0 <= (-1 + (2 * mid_j:1344) + mid_k:1345)
                      /\ 0 <= (-1 + mid_i:1342))) /\ K:1346 = 0
          /\ mid_k:1345 = k':1347 /\ mid_j:1344 = j':1348
          /\ mid_i:1342 = i':1349 /\ mid___cost:1343 = __cost':1350
          /\ 0 = K:1346 /\ (K:1341 + K:1346) = K:1351 /\ 0 <= K:1351
          /\ -1 <= k':1347 /\ 0 <= j':1348 /\ 0 <= i':1349 /\ 0 <= j':1348
          /\ param1:515 <= i':1349 /\ __cost':1350 = phi___cost:1368
          /\ i':1349 = phi_i:1367 /\ j':1348 = phi_j:1366
          /\ k':1347 = phi_k:1365)
         \/ ((!(0 <= K:1341) \/ mid_i:1342 = K:1341)
               /\ (!(0 <= K:1341)
                     \/ (-mid___cost:1343 + mid_j:1344 + mid_k:1345) <= (
                        -__cost:191 + -1))
               /\ (!(0 <= K:1341)
                     \/ (mid___cost:1343 + mid_j:1344) <= (__cost:191
                                                             + (2 * K:1341)))
               /\ (!(0 <= K:1341)
                     \/ -mid___cost:1343 <= (-__cost:191 + -K:1341))
               /\ ((K:1341 = 0 /\ -1 = mid_k:1345 /\ 0 = mid_j:1344
                      /\ 0 = mid_i:1342 /\ __cost:191 = mid___cost:1343)
                     \/ (1 <= K:1341 /\ 0 <= (-1 + param1:515)
                           /\ 0 <= (1 + -1) /\ 0 <= __cost:191
                           /\ 0 <= (-mid_i:1342 + param1:515)
                           /\ 0 <= (1 + mid_k:1345)
                           /\ 0 <= (-1 + mid___cost:1343) /\ 0 <= mid_j:1344
                           /\ 0 <= (-2 + mid_j:1344 + mid___cost:1343)
                           /\ 0 <= (-1 + (2 * mid_j:1344) + mid_k:1345)
                           /\ 0 <= (-1 + mid_i:1342))) /\ K:1346 = 0
               /\ mid_k:1345 = k':1347 /\ mid_j:1344 = j':1348
               /\ mid_i:1342 = i':1349 /\ mid___cost:1343 = __cost':1350
               /\ 0 = K:1346 /\ (K:1341 + K:1346) = K:1351 /\ 0 <= K:1351
               /\ -1 <= k':1347 /\ 0 <= j':1348 /\ 0 <= i':1349
               /\ 0 <= j':1348 /\ i':1349 < param1:515 /\ 0 <= __cost':1350
               /\ 0 <= (__cost':1350 + 1)
               /\ (!(0 <= K:1352)
                     \/ mid___cost:1353 = ((__cost':1350 + 1) + K:1352))
               /\ (!(0 <= K:1352)
                     \/ (mid_j:1354 + mid_k:1355) <= ((j':1348 + k':1347)
                                                        + K:1352))
               /\ (!(0 <= K:1352) \/ mid_j:1354 <= (j':1348 + -K:1352))
               /\ ((K:1352 = 0 /\ k':1347 = mid_k:1355
                      /\ j':1348 = mid_j:1354
                      /\ (__cost':1350 + 1) = mid___cost:1353)
                     \/ (1 <= K:1352 /\ 0 <= (1 + k':1347)
                           /\ 0 <= (-1 + (__cost':1350 + 1)) /\ 0 <= j':1348
                           /\ 0 <= (-2 + mid___cost:1353)
                           /\ 0 <= (-1 + mid_k:1355) /\ 0 <= (1 + mid_j:1354)))
               /\ K:1356 = 0 /\ mid_k:1355 = k':1357 /\ mid_j:1354 = j':1358
               /\ mid___cost:1353 = __cost':1359 /\ 0 = K:1356
               /\ (K:1352 + K:1356) = K:1360 /\ 0 <= K:1360 /\ -1 <= k':1357
               /\ -1 <= j':1358 /\ 1 <= __cost':1359 /\ 0 <= __cost':1359
               /\ 0 <= (__cost':1359 + 1)
               /\ (j':1358 < 0
                     \/ (0 <= j':1358 /\ tr:1361 <= tr:1362
                           /\ tr:1363 <= tr:1364))
               /\ (j':1358 + 1) = param3:521
               /\ __cost':1359 = phi___cost:1368
               /\ (i':1349 + 1) = phi_i:1367 /\ (j':1358 + 1) = phi_j:1366
               /\ k':1357 = phi_k:1365))}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, accept> -> <__pstate, (Unique State Name,133)_g1>	Base relation: 
{__cost := 0
 t_len := 10
 p_len := 5
 i := i':1260
 param0 := t:1262
 param1 := 10
 param2 := p:1263
 param3 := 5
 param4 := b:1264
 param0@pos := type_err:1265
 param1@pos := type_err:1266
 param2@pos := type_err:1267
 param3@pos := type_err:1268
 param4@pos := type_err:1269
 param0@width := type_err:1270
 param1@width := type_err:1271
 param2@width := type_err:1272
 param3@width := type_err:1273
 param4@width := type_err:1274
 when ((!(0 <= K:1227) \/ mid_i:1228 = K:1227)
         /\ ((K:1227 = 0 /\ 0 = mid_i:1228)
               \/ (1 <= K:1227 /\ (-10 + 10) = 0 /\ (-10 + 10) = 0
                     /\ 0 <= (10 + -mid_i:1228) /\ 0 <= (-1 + mid_i:1228)))
         /\ K:1229 = 0 /\ mid_i:1228 = i':1230 /\ 0 = K:1229
         /\ (K:1227 + K:1229) = K:1231 /\ 0 <= K:1231 /\ i':1230 <= 10
         /\ 0 <= i':1230 /\ 10 <= i':1230
         /\ (!(0 <= K:1241) \/ mid_i:1242 = K:1241)
         /\ ((K:1241 = 0 /\ 0 = mid_i:1242)
               \/ (1 <= K:1241 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                     /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1242)
                     /\ 0 <= (-1 + mid_i:1242) /\ 0 <= (10 + -mid_i:1242)))
         /\ K:1243 = 0 /\ mid_i:1242 = i':1244 /\ 0 = K:1243
         /\ (K:1241 + K:1243) = K:1245 /\ 0 <= K:1245 /\ 0 <= i':1244
         /\ i':1244 < 10 /\ 5 <= i':1244
         /\ (!(0 <= K:1257) \/ mid_i:1258 = K:1257)
         /\ ((K:1257 = 0 /\ 0 = mid_i:1258)
               \/ (1 <= K:1257 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                     /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1258)
                     /\ 0 <= (-1 + mid_i:1258) /\ 0 <= (10 + -mid_i:1258)))
         /\ K:1259 = 0 /\ mid_i:1258 = i':1260 /\ 0 = K:1259
         /\ (K:1257 + K:1259) = K:1261 /\ 0 <= K:1261 /\ i':1260 <= 5
         /\ 0 <= i':1260 /\ i':1260 < 10 /\ 5 <= i':1260)}	
<__pstate, (Unique State Name,133)_g1> -> <__pstate, (Unique State Name,121)_g1>	Base relation: 
{param0 := param0:512
 param1 := param1:515
 param2 := param2:518
 param3 := param3:521
 param4 := param4:524
 param0@pos := param0@pos:511
 param1@pos := type_err:531
 param2@pos := param2@pos:517
 param3@pos := type_err:532
 param4@pos := param4@pos:523
 param0@width := param0@width:510
 param1@width := type_err:533
 param2@width := param2@width:516
 param3@width := type_err:534
 param4@width := param4@width:522}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x1bf5a7a0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x1bf08490: 
	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,121)_g1 , __done )	Base relation: 
{__cost := 0
 t_len := 10
 p_len := 5
 i := i':1260
 param0 := t:1262
 param1 := 10
 param2 := p:1263
 param3 := 5
 param4 := b:1264
 param0@pos := type_err:1265
 param1@pos := type_err:1570
 param2@pos := type_err:1267
 param3@pos := type_err:1571
 param4@pos := type_err:1269
 param0@width := type_err:1270
 param1@width := type_err:1572
 param2@width := type_err:1272
 param3@width := type_err:1573
 param4@width := type_err:1274
 when ((!(0 <= K:1227) \/ mid_i:1228 = K:1227)
         /\ ((K:1227 = 0 /\ 0 = mid_i:1228)
               \/ (1 <= K:1227 /\ (-10 + 10) = 0 /\ (-10 + 10) = 0
                     /\ 0 <= (10 + -mid_i:1228) /\ 0 <= (-1 + mid_i:1228)))
         /\ K:1229 = 0 /\ mid_i:1228 = i':1230 /\ 0 = K:1229
         /\ (K:1227 + K:1229) = K:1231 /\ 0 <= K:1231 /\ i':1230 <= 10
         /\ 0 <= i':1230 /\ 10 <= i':1230
         /\ (!(0 <= K:1241) \/ mid_i:1242 = K:1241)
         /\ ((K:1241 = 0 /\ 0 = mid_i:1242)
               \/ (1 <= K:1241 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                     /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1242)
                     /\ 0 <= (-1 + mid_i:1242) /\ 0 <= (10 + -mid_i:1242)))
         /\ K:1243 = 0 /\ mid_i:1242 = i':1244 /\ 0 = K:1243
         /\ (K:1241 + K:1243) = K:1245 /\ 0 <= K:1245 /\ 0 <= i':1244
         /\ i':1244 < 10 /\ 5 <= i':1244
         /\ (!(0 <= K:1257) \/ mid_i:1258 = K:1257)
         /\ ((K:1257 = 0 /\ 0 = mid_i:1258)
               \/ (1 <= K:1257 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                     /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1258)
                     /\ 0 <= (-1 + mid_i:1258) /\ 0 <= (10 + -mid_i:1258)))
         /\ K:1259 = 0 /\ mid_i:1258 = i':1260 /\ 0 = K:1259
         /\ (K:1257 + K:1259) = K:1261 /\ 0 <= K:1261 /\ i':1260 <= 5
         /\ 0 <= i':1260 /\ i':1260 < 10 /\ 5 <= i':1260)}
    ( __pstate , (Unique State Name,133)_g1 , __done )	Base relation: 
{__cost := 0
 t_len := 10
 p_len := 5
 i := i':1260
 param0 := t:1262
 param1 := 10
 param2 := p:1263
 param3 := 5
 param4 := b:1264
 param0@pos := type_err:1265
 param1@pos := type_err:1266
 param2@pos := type_err:1267
 param3@pos := type_err:1268
 param4@pos := type_err:1269
 param0@width := type_err:1270
 param1@width := type_err:1271
 param2@width := type_err:1272
 param3@width := type_err:1273
 param4@width := type_err:1274
 when ((!(0 <= K:1227) \/ mid_i:1228 = K:1227)
         /\ ((K:1227 = 0 /\ 0 = mid_i:1228)
               \/ (1 <= K:1227 /\ (-10 + 10) = 0 /\ (-10 + 10) = 0
                     /\ 0 <= (10 + -mid_i:1228) /\ 0 <= (-1 + mid_i:1228)))
         /\ K:1229 = 0 /\ mid_i:1228 = i':1230 /\ 0 = K:1229
         /\ (K:1227 + K:1229) = K:1231 /\ 0 <= K:1231 /\ i':1230 <= 10
         /\ 0 <= i':1230 /\ 10 <= i':1230
         /\ (!(0 <= K:1241) \/ mid_i:1242 = K:1241)
         /\ ((K:1241 = 0 /\ 0 = mid_i:1242)
               \/ (1 <= K:1241 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                     /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1242)
                     /\ 0 <= (-1 + mid_i:1242) /\ 0 <= (10 + -mid_i:1242)))
         /\ K:1243 = 0 /\ mid_i:1242 = i':1244 /\ 0 = K:1243
         /\ (K:1241 + K:1243) = K:1245 /\ 0 <= K:1245 /\ 0 <= i':1244
         /\ i':1244 < 10 /\ 5 <= i':1244
         /\ (!(0 <= K:1257) \/ mid_i:1258 = K:1257)
         /\ ((K:1257 = 0 /\ 0 = mid_i:1258)
               \/ (1 <= K:1257 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                     /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1258)
                     /\ 0 <= (-1 + mid_i:1258) /\ 0 <= (10 + -mid_i:1258)))
         /\ K:1259 = 0 /\ mid_i:1258 = i':1260 /\ 0 = K:1259
         /\ (K:1257 + K:1259) = K:1261 /\ 0 <= K:1261 /\ i':1260 <= 5
         /\ 0 <= i':1260 /\ i':1260 < 10 /\ 5 <= i':1260)}

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

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

Base relation: 
{__cost := phi___cost:1513
 t_len := 10
 p_len := 5
 i := i':1260
 return := 0
 param0 := t:1262
 param1 := 10
 param2 := p:1263
 param3 := 5
 param4 := b:1264
 return@pos := type_err:1536
 param0@pos := type_err:1265
 param1@pos := type_err:1531
 param2@pos := type_err:1267
 param3@pos := type_err:1532
 param4@pos := type_err:1269
 return@width := type_err:1537
 param0@width := type_err:1270
 param1@width := type_err:1534
 param2@width := type_err:1272
 param3@width := type_err:1535
 param4@width := type_err:1274
 when ((!(0 <= K:1227) \/ mid_i:1228 = K:1227)
         /\ ((K:1227 = 0 /\ 0 = mid_i:1228)
               \/ (1 <= K:1227 /\ (-10 + 10) = 0 /\ (-10 + 10) = 0
                     /\ 0 <= (10 + -mid_i:1228) /\ 0 <= (-1 + mid_i:1228)))
         /\ K:1229 = 0 /\ mid_i:1228 = i':1230 /\ 0 = K:1229
         /\ (K:1227 + K:1229) = K:1231 /\ 0 <= K:1231 /\ i':1230 <= 10
         /\ 0 <= i':1230 /\ 10 <= i':1230
         /\ (!(0 <= K:1241) \/ mid_i:1242 = K:1241)
         /\ ((K:1241 = 0 /\ 0 = mid_i:1242)
               \/ (1 <= K:1241 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                     /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1242)
                     /\ 0 <= (-1 + mid_i:1242) /\ 0 <= (10 + -mid_i:1242)))
         /\ K:1243 = 0 /\ mid_i:1242 = i':1244 /\ 0 = K:1243
         /\ (K:1241 + K:1243) = K:1245 /\ 0 <= K:1245 /\ 0 <= i':1244
         /\ i':1244 < 10 /\ 5 <= i':1244
         /\ (!(0 <= K:1257) \/ mid_i:1258 = K:1257)
         /\ ((K:1257 = 0 /\ 0 = mid_i:1258)
               \/ (1 <= K:1257 /\ (-5 + 5) = 0 /\ 0 <= (-1 + 10)
                     /\ (-5 + 5) = 0 /\ 0 <= (5 + -mid_i:1258)
                     /\ 0 <= (-1 + mid_i:1258) /\ 0 <= (10 + -mid_i:1258)))
         /\ K:1259 = 0 /\ mid_i:1258 = i':1260 /\ 0 = K:1259
         /\ (K:1257 + K:1259) = K:1261 /\ 0 <= K:1261 /\ i':1260 <= 5
         /\ 0 <= i':1260 /\ i':1260 < 10 /\ 5 <= i':1260
         /\ (((!(0 <= K:1502) \/ mid_i:1503 = K:1502)
                /\ (!(0 <= K:1502)
                      \/ (-mid___cost:1504 + mid_j:1505 + mid_k:1506) <= -1)
                /\ (!(0 <= K:1502)
                      \/ (mid___cost:1504 + mid_j:1505) <= (2 * K:1502))
                /\ (!(0 <= K:1502) \/ -mid___cost:1504 <= -K:1502)
                /\ ((K:1502 = 0 /\ -1 = mid_k:1506 /\ 0 = mid_j:1505
                       /\ 0 = mid_i:1503 /\ 0 = mid___cost:1504)
                      \/ (1 <= K:1502 /\ 0 <= (-1 + 10) /\ 0 <= (1 + -1)
                            /\ 0 <= (-mid_i:1503 + 10)
                            /\ 0 <= (1 + mid_k:1506)
                            /\ 0 <= (-1 + mid___cost:1504) /\ 0 <= mid_j:1505
                            /\ 0 <= (-2 + mid_j:1505 + mid___cost:1504)
                            /\ 0 <= (-1 + (2 * mid_j:1505) + mid_k:1506)
                            /\ 0 <= (-1 + mid_i:1503))) /\ K:1507 = 0
                /\ mid_k:1506 = k':1508 /\ mid_j:1505 = j':1509
                /\ mid_i:1503 = i':1510 /\ mid___cost:1504 = __cost':1511
                /\ 0 = K:1507 /\ (K:1502 + K:1507) = K:1512 /\ 0 <= K:1512
                /\ -1 <= k':1508 /\ 0 <= j':1509 /\ 0 <= i':1510
                /\ 0 <= j':1509 /\ 10 <= i':1510
                /\ __cost':1511 = phi___cost:1513 /\ i':1510 = phi_i:1514
                /\ j':1509 = phi_j:1515 /\ k':1508 = phi_k:1516)
               \/ ((!(0 <= K:1502) \/ mid_i:1503 = K:1502)
                     /\ (!(0 <= K:1502)
                           \/ (-mid___cost:1504 + mid_j:1505 + mid_k:1506) <= -1)
                     /\ (!(0 <= K:1502)
                           \/ (mid___cost:1504 + mid_j:1505) <= (2 * K:1502))
                     /\ (!(0 <= K:1502) \/ -mid___cost:1504 <= -K:1502)
                     /\ ((K:1502 = 0 /\ -1 = mid_k:1506 /\ 0 = mid_j:1505
                            /\ 0 = mid_i:1503 /\ 0 = mid___cost:1504)
                           \/ (1 <= K:1502 /\ 0 <= (-1 + 10) /\ 0 <= (1 + -1)
                                 /\ 0 <= (-mid_i:1503 + 10)
                                 /\ 0 <= (1 + mid_k:1506)
                                 /\ 0 <= (-1 + mid___cost:1504)
                                 /\ 0 <= mid_j:1505
                                 /\ 0 <= (-2 + mid_j:1505 + mid___cost:1504)
                                 /\ 0 <= (-1 + (2 * mid_j:1505) + mid_k:1506)
                                 /\ 0 <= (-1 + mid_i:1503))) /\ K:1507 = 0
                     /\ mid_k:1506 = k':1508 /\ mid_j:1505 = j':1509
                     /\ mid_i:1503 = i':1510
                     /\ mid___cost:1504 = __cost':1511 /\ 0 = K:1507
                     /\ (K:1502 + K:1507) = K:1512 /\ 0 <= K:1512
                     /\ -1 <= k':1508 /\ 0 <= j':1509 /\ 0 <= i':1510
                     /\ 0 <= j':1509 /\ i':1510 < 10 /\ 0 <= __cost':1511
                     /\ 0 <= (__cost':1511 + 1)
                     /\ (!(0 <= K:1517)
                           \/ mid___cost:1518 = ((__cost':1511 + 1) + K:1517))
                     /\ (!(0 <= K:1517)
                           \/ (mid_j:1519 + mid_k:1520) <= ((j':1509
                                                               + k':1508)
                                                              + K:1517))
                     /\ (!(0 <= K:1517) \/ mid_j:1519 <= (j':1509 + -K:1517))
                     /\ ((K:1517 = 0 /\ k':1508 = mid_k:1520
                            /\ j':1509 = mid_j:1519
                            /\ (__cost':1511 + 1) = mid___cost:1518)
                           \/ (1 <= K:1517 /\ 0 <= (1 + k':1508)
                                 /\ 0 <= (-1 + (__cost':1511 + 1))
                                 /\ 0 <= j':1509
                                 /\ 0 <= (-2 + mid___cost:1518)
                                 /\ 0 <= (-1 + mid_k:1520)
                                 /\ 0 <= (1 + mid_j:1519))) /\ K:1521 = 0
                     /\ mid_k:1520 = k':1522 /\ mid_j:1519 = j':1523
                     /\ mid___cost:1518 = __cost':1524 /\ 0 = K:1521
                     /\ (K:1517 + K:1521) = K:1525 /\ 0 <= K:1525
                     /\ -1 <= k':1522 /\ -1 <= j':1523 /\ 1 <= __cost':1524
                     /\ 0 <= __cost':1524 /\ 0 <= (__cost':1524 + 1)
                     /\ (j':1523 < 0
                           \/ (0 <= j':1523 /\ tr:1526 <= tr:1527
                                 /\ tr:1528 <= tr:1529)) /\ (j':1523 + 1) = 5
                     /\ __cost':1524 = phi___cost:1513
                     /\ (i':1510 + 1) = phi_i:1514
                     /\ (j':1523 + 1) = phi_j:1515 /\ k':1522 = phi_k:1516)))}

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

Base relation: 
{__cost := phi___cost:1549
 return := 0
 param0 := param0:512
 param1 := param1:515
 param2 := param2:518
 param3 := param3:521
 param4 := param4:524
 return@pos := type_err:1568
 param0@pos := param0@pos:511
 param1@pos := type_err:531
 param2@pos := param2@pos:517
 param3@pos := type_err:532
 param4@pos := param4@pos:523
 return@width := type_err:1569
 param0@width := param0@width:510
 param1@width := type_err:533
 param2@width := param2@width:516
 param3@width := type_err:534
 param4@width := param4@width:522
 when (((!(0 <= K:1538) \/ mid_i:1539 = K:1538)
          /\ (!(0 <= K:1538)
                \/ (-mid___cost:1540 + mid_j:1541 + mid_k:1542) <= (-__cost:191
                                                                    + -1))
          /\ (!(0 <= K:1538)
                \/ (mid___cost:1540 + mid_j:1541) <= (__cost:191
                                                        + (2 * K:1538)))
          /\ (!(0 <= K:1538) \/ -mid___cost:1540 <= (-__cost:191 + -K:1538))
          /\ ((K:1538 = 0 /\ -1 = mid_k:1542 /\ 0 = mid_j:1541
                 /\ 0 = mid_i:1539 /\ __cost:191 = mid___cost:1540)
                \/ (1 <= K:1538 /\ 0 <= (-1 + param1:515) /\ 0 <= (1 + -1)
                      /\ 0 <= __cost:191 /\ 0 <= (-mid_i:1539 + param1:515)
                      /\ 0 <= (1 + mid_k:1542) /\ 0 <= (-1 + mid___cost:1540)
                      /\ 0 <= mid_j:1541
                      /\ 0 <= (-2 + mid_j:1541 + mid___cost:1540)
                      /\ 0 <= (-1 + (2 * mid_j:1541) + mid_k:1542)
                      /\ 0 <= (-1 + mid_i:1539))) /\ K:1543 = 0
          /\ mid_k:1542 = k':1544 /\ mid_j:1541 = j':1545
          /\ mid_i:1539 = i':1546 /\ mid___cost:1540 = __cost':1547
          /\ 0 = K:1543 /\ (K:1538 + K:1543) = K:1548 /\ 0 <= K:1548
          /\ -1 <= k':1544 /\ 0 <= j':1545 /\ 0 <= i':1546 /\ 0 <= j':1545
          /\ param1:515 <= i':1546 /\ __cost':1547 = phi___cost:1549
          /\ i':1546 = phi_i:1550 /\ j':1545 = phi_j:1551
          /\ k':1544 = phi_k:1552)
         \/ ((!(0 <= K:1538) \/ mid_i:1539 = K:1538)
               /\ (!(0 <= K:1538)
                     \/ (-mid___cost:1540 + mid_j:1541 + mid_k:1542) <= (
                        -__cost:191 + -1))
               /\ (!(0 <= K:1538)
                     \/ (mid___cost:1540 + mid_j:1541) <= (__cost:191
                                                             + (2 * K:1538)))
               /\ (!(0 <= K:1538)
                     \/ -mid___cost:1540 <= (-__cost:191 + -K:1538))
               /\ ((K:1538 = 0 /\ -1 = mid_k:1542 /\ 0 = mid_j:1541
                      /\ 0 = mid_i:1539 /\ __cost:191 = mid___cost:1540)
                     \/ (1 <= K:1538 /\ 0 <= (-1 + param1:515)
                           /\ 0 <= (1 + -1) /\ 0 <= __cost:191
                           /\ 0 <= (-mid_i:1539 + param1:515)
                           /\ 0 <= (1 + mid_k:1542)
                           /\ 0 <= (-1 + mid___cost:1540) /\ 0 <= mid_j:1541
                           /\ 0 <= (-2 + mid_j:1541 + mid___cost:1540)
                           /\ 0 <= (-1 + (2 * mid_j:1541) + mid_k:1542)
                           /\ 0 <= (-1 + mid_i:1539))) /\ K:1543 = 0
               /\ mid_k:1542 = k':1544 /\ mid_j:1541 = j':1545
               /\ mid_i:1539 = i':1546 /\ mid___cost:1540 = __cost':1547
               /\ 0 = K:1543 /\ (K:1538 + K:1543) = K:1548 /\ 0 <= K:1548
               /\ -1 <= k':1544 /\ 0 <= j':1545 /\ 0 <= i':1546
               /\ 0 <= j':1545 /\ i':1546 < param1:515 /\ 0 <= __cost':1547
               /\ 0 <= (__cost':1547 + 1)
               /\ (!(0 <= K:1553)
                     \/ mid___cost:1554 = ((__cost':1547 + 1) + K:1553))
               /\ (!(0 <= K:1553)
                     \/ (mid_j:1555 + mid_k:1556) <= ((j':1545 + k':1544)
                                                        + K:1553))
               /\ (!(0 <= K:1553) \/ mid_j:1555 <= (j':1545 + -K:1553))
               /\ ((K:1553 = 0 /\ k':1544 = mid_k:1556
                      /\ j':1545 = mid_j:1555
                      /\ (__cost':1547 + 1) = mid___cost:1554)
                     \/ (1 <= K:1553 /\ 0 <= (1 + k':1544)
                           /\ 0 <= (-1 + (__cost':1547 + 1)) /\ 0 <= j':1545
                           /\ 0 <= (-2 + mid___cost:1554)
                           /\ 0 <= (-1 + mid_k:1556) /\ 0 <= (1 + mid_j:1555)))
               /\ K:1557 = 0 /\ mid_k:1556 = k':1558 /\ mid_j:1555 = j':1559
               /\ mid___cost:1554 = __cost':1560 /\ 0 = K:1557
               /\ (K:1553 + K:1557) = K:1561 /\ 0 <= K:1561 /\ -1 <= k':1558
               /\ -1 <= j':1559 /\ 1 <= __cost':1560 /\ 0 <= __cost':1560
               /\ 0 <= (__cost':1560 + 1)
               /\ (j':1559 < 0
                     \/ (0 <= j':1559 /\ tr:1562 <= tr:1563
                           /\ tr:1564 <= tr:1565))
               /\ (j':1559 + 1) = param3:521
               /\ __cost':1560 = phi___cost:1549
               /\ (i':1546 + 1) = phi_i:1550 /\ (j':1559 + 1) = phi_j:1551
               /\ k':1558 = phi_k:1552))}

------------------------------------------------
Procedure summary for srch

Base relation: 
{__cost := phi___cost:1368
 i := phi_i:1367
 j := phi_j:1366
 k := phi_k:1365
 t := param0:512
 n := param1:515
 p := param2:518
 m := param3:521
 b := param4:524
 return := phi_i:1367
 t@pos := param0@pos:511
 p@pos := param2@pos:517
 b@pos := param4@pos:523
 return@pos := type_err:1369
 t@width := param0@width:510
 p@width := param2@width:516
 b@width := param4@width:522
 return@width := type_err:1370
 when (((!(0 <= K:1341) \/ mid_i:1342 = K:1341)
          /\ (!(0 <= K:1341)
                \/ (-mid___cost:1343 + mid_j:1344 + mid_k:1345) <= (-__cost:191
                                                                    + -1))
          /\ (!(0 <= K:1341)
                \/ (mid___cost:1343 + mid_j:1344) <= (__cost:191
                                                        + (2 * K:1341)))
          /\ (!(0 <= K:1341) \/ -mid___cost:1343 <= (-__cost:191 + -K:1341))
          /\ ((K:1341 = 0 /\ -1 = mid_k:1345 /\ 0 = mid_j:1344
                 /\ 0 = mid_i:1342 /\ __cost:191 = mid___cost:1343)
                \/ (1 <= K:1341 /\ 0 <= (-1 + param1:515) /\ 0 <= (1 + -1)
                      /\ 0 <= __cost:191 /\ 0 <= (-mid_i:1342 + param1:515)
                      /\ 0 <= (1 + mid_k:1345) /\ 0 <= (-1 + mid___cost:1343)
                      /\ 0 <= mid_j:1344
                      /\ 0 <= (-2 + mid_j:1344 + mid___cost:1343)
                      /\ 0 <= (-1 + (2 * mid_j:1344) + mid_k:1345)
                      /\ 0 <= (-1 + mid_i:1342))) /\ K:1346 = 0
          /\ mid_k:1345 = k':1347 /\ mid_j:1344 = j':1348
          /\ mid_i:1342 = i':1349 /\ mid___cost:1343 = __cost':1350
          /\ 0 = K:1346 /\ (K:1341 + K:1346) = K:1351 /\ 0 <= K:1351
          /\ -1 <= k':1347 /\ 0 <= j':1348 /\ 0 <= i':1349 /\ 0 <= j':1348
          /\ param1:515 <= i':1349 /\ __cost':1350 = phi___cost:1368
          /\ i':1349 = phi_i:1367 /\ j':1348 = phi_j:1366
          /\ k':1347 = phi_k:1365)
         \/ ((!(0 <= K:1341) \/ mid_i:1342 = K:1341)
               /\ (!(0 <= K:1341)
                     \/ (-mid___cost:1343 + mid_j:1344 + mid_k:1345) <= (
                        -__cost:191 + -1))
               /\ (!(0 <= K:1341)
                     \/ (mid___cost:1343 + mid_j:1344) <= (__cost:191
                                                             + (2 * K:1341)))
               /\ (!(0 <= K:1341)
                     \/ -mid___cost:1343 <= (-__cost:191 + -K:1341))
               /\ ((K:1341 = 0 /\ -1 = mid_k:1345 /\ 0 = mid_j:1344
                      /\ 0 = mid_i:1342 /\ __cost:191 = mid___cost:1343)
                     \/ (1 <= K:1341 /\ 0 <= (-1 + param1:515)
                           /\ 0 <= (1 + -1) /\ 0 <= __cost:191
                           /\ 0 <= (-mid_i:1342 + param1:515)
                           /\ 0 <= (1 + mid_k:1345)
                           /\ 0 <= (-1 + mid___cost:1343) /\ 0 <= mid_j:1344
                           /\ 0 <= (-2 + mid_j:1344 + mid___cost:1343)
                           /\ 0 <= (-1 + (2 * mid_j:1344) + mid_k:1345)
                           /\ 0 <= (-1 + mid_i:1342))) /\ K:1346 = 0
               /\ mid_k:1345 = k':1347 /\ mid_j:1344 = j':1348
               /\ mid_i:1342 = i':1349 /\ mid___cost:1343 = __cost':1350
               /\ 0 = K:1346 /\ (K:1341 + K:1346) = K:1351 /\ 0 <= K:1351
               /\ -1 <= k':1347 /\ 0 <= j':1348 /\ 0 <= i':1349
               /\ 0 <= j':1348 /\ i':1349 < param1:515 /\ 0 <= __cost':1350
               /\ 0 <= (__cost':1350 + 1)
               /\ (!(0 <= K:1352)
                     \/ mid___cost:1353 = ((__cost':1350 + 1) + K:1352))
               /\ (!(0 <= K:1352)
                     \/ (mid_j:1354 + mid_k:1355) <= ((j':1348 + k':1347)
                                                        + K:1352))
               /\ (!(0 <= K:1352) \/ mid_j:1354 <= (j':1348 + -K:1352))
               /\ ((K:1352 = 0 /\ k':1347 = mid_k:1355
                      /\ j':1348 = mid_j:1354
                      /\ (__cost':1350 + 1) = mid___cost:1353)
                     \/ (1 <= K:1352 /\ 0 <= (1 + k':1347)
                           /\ 0 <= (-1 + (__cost':1350 + 1)) /\ 0 <= j':1348
                           /\ 0 <= (-2 + mid___cost:1353)
                           /\ 0 <= (-1 + mid_k:1355) /\ 0 <= (1 + mid_j:1354)))
               /\ K:1356 = 0 /\ mid_k:1355 = k':1357 /\ mid_j:1354 = j':1358
               /\ mid___cost:1353 = __cost':1359 /\ 0 = K:1356
               /\ (K:1352 + K:1356) = K:1360 /\ 0 <= K:1360 /\ -1 <= k':1357
               /\ -1 <= j':1358 /\ 1 <= __cost':1359 /\ 0 <= __cost':1359
               /\ 0 <= (__cost':1359 + 1)
               /\ (j':1358 < 0
                     \/ (0 <= j':1358 /\ tr:1361 <= tr:1362
                           /\ tr:1363 <= tr:1364))
               /\ (j':1358 + 1) = param3:521
               /\ __cost':1359 = phi___cost:1368
               /\ (i':1349 + 1) = phi_i:1367 /\ (j':1358 + 1) = phi_j:1366
               /\ k':1357 = phi_k:1365))}

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

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

Variable bounds at line 42 in run

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

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