/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, 54> -> <Unique State Name, 51 53>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 15> -> <Unique State Name, 54>	Base relation: 
{__cost := 0
 x := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
<Unique State Name, 57> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 47> -> <Unique State Name, 23>	Base relation: 
{i := 1
 j := 0
 x := param0:53}	
<Unique State Name, 23> -> <Unique State Name, 58>	Base relation: 
{when (0 <= j:62 /\ i:65 <= 4 /\ 1 <= i:65)}	
<Unique State Name, 49> -> <Unique State Name, 17>	Base relation: 
{}	
<Unique State Name, 55> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 50> -> <Unique State Name, 47 49>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 58> -> <Unique State Name, 27>	Base relation: 
{}	
<Unique State Name, 17> -> <Unique State Name, 56>	Base relation: 
{return := havoc:41
 return@pos := type_err:44
 return@width := type_err:45}	
<Unique State Name, 51> -> <Unique State Name, 50>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
<Unique State Name, 53> -> <Unique State Name, 57>	Base relation: 
{return := 0
 return@pos := type_err:19
 return@width := type_err:20
 when ((0 < x:2 /\ x:2 = phi_tmp___0:14) \/ (x:2 <= 0 /\ 0 = phi_tmp___0:14))}	
<Unique State Name, 27> -> <Unique State Name, 23>	Base relation: 
{__cost := (__cost:64 + 1)
 i := phi_i:75
 j := (j:62 + 1)
 when (j:62 < x:63 /\ 0 <= __cost:64 /\ 0 <= (__cost:64 + 1)
         /\ ((4 <= i:65 /\ 1 = phi_i:75)
               \/ (i:65 < 4 /\ (i:65 + 1) = phi_i:75)))}	
<Unique State Name, 27> -> <Unique State Name, 55>	Base relation: 
{return := havoc:72
 return@pos := type_err:73
 return@width := type_err:74
 when x:63 <= j:62}	
<Unique State Name, 56> -> <Unique State Name, >	Base relation: 
{}	
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:64 + 1)
 i := phi_i:182
 j := (j:62 + 1)
 when (0 <= j:62 /\ i:65 <= 4 /\ 1 <= i:65 /\ j:62 < x:63 /\ 0 <= __cost:64
         /\ 0 <= (__cost:64 + 1)
         /\ ((4 <= i:65 /\ 1 = phi_i:182)
               \/ (i:65 < 4 /\ (i:65 + 1) = phi_i:182)))}
**** alpha hat: 
  {<Split [true
            (j':185) = (1)*(j:62) + 1
           (__cost':183) = (1)*(__cost:64) + 1
           (i':184) <= (1)*(i:65) + 1
           (-i':184) <= (1)*(-i:65) + 3*1
           }
          pre:
            [|-j:62+x:63-1>=0; -i:65+4>=0; __cost:64>=0; i:65-1>=0; j:62>=0|]
          post:
            [|-j':185+x:63>=0; -i':184+4>=0; __cost':183-1>=0; i':184-1>=0;
              j':185-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':183
   i := i':184
   j := j':185
   when ((!(0 <= K:196) \/ mid_j:198 = (j:62 + K:196))
           /\ (!(0 <= K:196) \/ mid___cost:200 = (__cost:64 + K:196))
           /\ (!(0 <= K:196) \/ mid_i:199 <= (i:65 + K:196))
           /\ (!(0 <= K:196) \/ -mid_i:199 <= (-i:65 + (3 * K:196)))
           /\ ((K:196 = 0 /\ j:62 = mid_j:198 /\ i:65 = mid_i:199
                  /\ __cost:64 = mid___cost:200)
                 \/ (1 <= K:196 /\ 0 <= (-1 + -j:62 + x:63)
                       /\ 0 <= (4 + -i:65) /\ 0 <= __cost:64
                       /\ 0 <= (-1 + i:65) /\ 0 <= j:62
                       /\ 0 <= (-mid_j:198 + x:63) /\ 0 <= (4 + -mid_i:199)
                       /\ 0 <= (-1 + mid___cost:200) /\ 0 <= (-1 + mid_i:199)
                       /\ 0 <= (-1 + mid_j:198))) /\ K:197 = 0
           /\ mid_j:198 = j':185 /\ mid_i:199 = i':184
           /\ mid___cost:200 = __cost':183 /\ 0 = K:197
           /\ (K:196 + K:197) = K:195 /\ 0 <= K:195)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  19  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       x := 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 < x:2 /\ x:2 = phi_tmp___0:14)
             \/ (x: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(19)
  )
  ,
  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=19: 
Weight(Base relation: 
  {__cost := __cost':208
   i := i':207
   j := j':206
   x := param0:53
   return := havoc:210
   return@pos := type_err:211
   return@width := type_err:212
   when ((!(0 <= K:201) \/ mid_j:202 = K:201)
           /\ (!(0 <= K:201) \/ mid___cost:203 = (__cost:64 + K:201))
           /\ (!(0 <= K:201) \/ mid_i:204 <= (1 + K:201))
           /\ (!(0 <= K:201) \/ -mid_i:204 <= (-1 + (3 * K:201)))
           /\ ((K:201 = 0 /\ 0 = mid_j:202 /\ 1 = mid_i:204
                  /\ __cost:64 = mid___cost:203)
                 \/ (1 <= K:201 /\ 0 <= (-1 + param0:53) /\ 0 <= (4 + -1)
                       /\ 0 <= __cost:64 /\ 0 <= (-1 + 1)
                       /\ 0 <= (-mid_j:202 + param0:53)
                       /\ 0 <= (4 + -mid_i:204) /\ 0 <= (-1 + mid___cost:203)
                       /\ 0 <= (-1 + mid_i:204) /\ 0 <= (-1 + mid_j:202)))
           /\ K:205 = 0 /\ mid_j:202 = j':206 /\ mid_i:204 = i':207
           /\ mid___cost:203 = __cost':208 /\ 0 = K:205
           /\ (K:201 + K:205) = K:209 /\ 0 <= K:209 /\ 0 <= j':206
           /\ i':207 <= 4 /\ 1 <= i':207 /\ param0:53 <= j':206)})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := 0
         x := havoc: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 < x:2 /\ x:2 = phi_tmp___0:14)
               \/ (x: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(19)
    )
    ,
    Weight(Base relation: 
      {return := havoc:41
       return@pos := type_err:44
       return@width := type_err:45}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':208
   return := havoc:210
   return@pos := type_err:211
   return@width := type_err:212
   when ((!(0 <= K:201) \/ mid_j:202 = K:201)
           /\ (!(0 <= K:201) \/ mid___cost:203 = (__cost:64 + K:201))
           /\ (!(0 <= K:201) \/ mid_i:204 <= (1 + K:201))
           /\ (!(0 <= K:201) \/ -mid_i:204 <= (-1 + (3 * K:201)))
           /\ ((K:201 = 0 /\ 0 = mid_j:202 /\ 1 = mid_i:204
                  /\ __cost:64 = mid___cost:203)
                 \/ (1 <= K:201 /\ 0 <= (-1 + param0:53) /\ 0 <= (4 + -1)
                       /\ 0 <= __cost:64 /\ 0 <= (-1 + 1)
                       /\ 0 <= (-mid_j:202 + param0:53)
                       /\ 0 <= (4 + -mid_i:204) /\ 0 <= (-1 + mid___cost:203)
                       /\ 0 <= (-1 + mid_i:204) /\ 0 <= (-1 + mid_j:202)))
           /\ K:205 = 0 /\ mid_j:202 = j':206 /\ mid_i:204 = i':207
           /\ mid___cost:203 = __cost':208 /\ 0 = K:205
           /\ (K:201 + K:205) = K:209 /\ 0 <= K:209 /\ 0 <= j':206
           /\ i':207 <= 4 /\ 1 <= i':207 /\ param0:53 <= j':206)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':235
   return := 0
   param0 := havoc:13
   return@pos := type_err:243
   param0@pos := type_err:239
   return@width := type_err:244
   param0@width := type_err:241
   when ((!(0 <= K:228) \/ mid_j:229 = K:228)
           /\ (!(0 <= K:228) \/ mid___cost:230 = K:228)
           /\ (!(0 <= K:228) \/ mid_i:231 <= (1 + K:228))
           /\ (!(0 <= K:228) \/ -mid_i:231 <= (-1 + (3 * K:228)))
           /\ ((K:228 = 0 /\ 0 = mid_j:229 /\ 1 = mid_i:231
                  /\ 0 = mid___cost:230)
                 \/ (1 <= K:228 /\ 0 <= (-1 + havoc:13) /\ 0 <= (4 + -1)
                       /\ 0 <= (-1 + 1) /\ 0 <= (-mid_j:229 + havoc:13)
                       /\ 0 <= (4 + -mid_i:231) /\ 0 <= (-1 + mid___cost:230)
                       /\ 0 <= (-1 + mid_i:231) /\ 0 <= (-1 + mid_j:229)))
           /\ K:232 = 0 /\ mid_j:229 = j':233 /\ mid_i:231 = i':234
           /\ mid___cost:230 = __cost':235 /\ 0 = K:232
           /\ (K:228 + K:232) = K:236 /\ 0 <= K:236 /\ 0 <= j':233
           /\ i':234 <= 4 /\ 1 <= i':234 /\ havoc:13 <= j':233
           /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:242)
                 \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:242)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':252
   return := havoc:257
   param0 := param0:53
   return@pos := type_err:258
   param0@pos := type_err:54
   return@width := type_err:259
   param0@width := type_err:55
   when ((!(0 <= K:245) \/ mid_j:246 = K:245)
           /\ (!(0 <= K:245) \/ mid___cost:247 = (__cost:64 + K:245))
           /\ (!(0 <= K:245) \/ mid_i:248 <= (1 + K:245))
           /\ (!(0 <= K:245) \/ -mid_i:248 <= (-1 + (3 * K:245)))
           /\ ((K:245 = 0 /\ 0 = mid_j:246 /\ 1 = mid_i:248
                  /\ __cost:64 = mid___cost:247)
                 \/ (1 <= K:245 /\ 0 <= (-1 + param0:53) /\ 0 <= (4 + -1)
                       /\ 0 <= __cost:64 /\ 0 <= (-1 + 1)
                       /\ 0 <= (-mid_j:246 + param0:53)
                       /\ 0 <= (4 + -mid_i:248) /\ 0 <= (-1 + mid___cost:247)
                       /\ 0 <= (-1 + mid_i:248) /\ 0 <= (-1 + mid_j:246)))
           /\ K:249 = 0 /\ mid_j:246 = j':250 /\ mid_i:248 = i':251
           /\ mid___cost:247 = __cost':252 /\ 0 = K:249
           /\ (K:245 + K:249) = K:253 /\ 0 <= K:253 /\ 0 <= j':250
           /\ i':251 <= 4 /\ 1 <= i':251 /\ param0:53 <= j':250)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=19: 
Weight(Base relation: 
  {__cost := __cost':208
   return := havoc:210
   return@pos := type_err:211
   return@width := type_err:212
   when ((!(0 <= K:201) \/ mid_j:202 = K:201)
           /\ (!(0 <= K:201) \/ mid___cost:203 = (__cost:64 + K:201))
           /\ (!(0 <= K:201) \/ mid_i:204 <= (1 + K:201))
           /\ (!(0 <= K:201) \/ -mid_i:204 <= (-1 + (3 * K:201)))
           /\ ((K:201 = 0 /\ 0 = mid_j:202 /\ 1 = mid_i:204
                  /\ __cost:64 = mid___cost:203)
                 \/ (1 <= K:201 /\ 0 <= (-1 + param0:53) /\ 0 <= (4 + -1)
                       /\ 0 <= __cost:64 /\ 0 <= (-1 + 1)
                       /\ 0 <= (-mid_j:202 + param0:53)
                       /\ 0 <= (4 + -mid_i:204) /\ 0 <= (-1 + mid___cost:203)
                       /\ 0 <= (-1 + mid_i:204) /\ 0 <= (-1 + mid_j:202)))
           /\ K:205 = 0 /\ mid_j:202 = j':206 /\ mid_i:204 = i':207
           /\ mid___cost:203 = __cost':208 /\ 0 = K:205
           /\ (K:201 + K:205) = K:209 /\ 0 <= K:209 /\ 0 <= j':206
           /\ i':207 <= 4 /\ 1 <= i':207 /\ param0:53 <= j':206)})


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':235
 return := 0
 param0 := havoc:13
 return@pos := type_err:243
 param0@pos := type_err:239
 return@width := type_err:244
 param0@width := type_err:241
 when ((!(0 <= K:228) \/ mid_j:229 = K:228)
         /\ (!(0 <= K:228) \/ mid___cost:230 = K:228)
         /\ (!(0 <= K:228) \/ mid_i:231 <= (1 + K:228))
         /\ (!(0 <= K:228) \/ -mid_i:231 <= (-1 + (3 * K:228)))
         /\ ((K:228 = 0 /\ 0 = mid_j:229 /\ 1 = mid_i:231
                /\ 0 = mid___cost:230)
               \/ (1 <= K:228 /\ 0 <= (-1 + havoc:13) /\ 0 <= (4 + -1)
                     /\ 0 <= (-1 + 1) /\ 0 <= (-mid_j:229 + havoc:13)
                     /\ 0 <= (4 + -mid_i:231) /\ 0 <= (-1 + mid___cost:230)
                     /\ 0 <= (-1 + mid_i:231) /\ 0 <= (-1 + mid_j:229)))
         /\ K:232 = 0 /\ mid_j:229 = j':233 /\ mid_i:231 = i':234
         /\ mid___cost:230 = __cost':235 /\ 0 = K:232
         /\ (K:228 + K:232) = K:236 /\ 0 <= K:236 /\ 0 <= j':233
         /\ i':234 <= 4 /\ 1 <= i':234 /\ havoc:13 <= j':233
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:242)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:242)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':252
 return := havoc:257
 param0 := param0:53
 return@pos := type_err:258
 param0@pos := type_err:54
 return@width := type_err:259
 param0@width := type_err:55
 when ((!(0 <= K:245) \/ mid_j:246 = K:245)
         /\ (!(0 <= K:245) \/ mid___cost:247 = (__cost:64 + K:245))
         /\ (!(0 <= K:245) \/ mid_i:248 <= (1 + K:245))
         /\ (!(0 <= K:245) \/ -mid_i:248 <= (-1 + (3 * K:245)))
         /\ ((K:245 = 0 /\ 0 = mid_j:246 /\ 1 = mid_i:248
                /\ __cost:64 = mid___cost:247)
               \/ (1 <= K:245 /\ 0 <= (-1 + param0:53) /\ 0 <= (4 + -1)
                     /\ 0 <= __cost:64 /\ 0 <= (-1 + 1)
                     /\ 0 <= (-mid_j:246 + param0:53)
                     /\ 0 <= (4 + -mid_i:248) /\ 0 <= (-1 + mid___cost:247)
                     /\ 0 <= (-1 + mid_i:248) /\ 0 <= (-1 + mid_j:246)))
         /\ K:249 = 0 /\ mid_j:246 = j':250 /\ mid_i:248 = i':251
         /\ mid___cost:247 = __cost':252 /\ 0 = K:249
         /\ (K:245 + K:249) = K:253 /\ 0 <= K:253 /\ 0 <= j':250
         /\ i':251 <= 4 /\ 1 <= i':251 /\ param0:53 <= j':250)}

Evaluating variable number 19 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':208
 return := havoc:210
 return@pos := type_err:211
 return@width := type_err:212
 when ((!(0 <= K:201) \/ mid_j:202 = K:201)
         /\ (!(0 <= K:201) \/ mid___cost:203 = (__cost:64 + K:201))
         /\ (!(0 <= K:201) \/ mid_i:204 <= (1 + K:201))
         /\ (!(0 <= K:201) \/ -mid_i:204 <= (-1 + (3 * K:201)))
         /\ ((K:201 = 0 /\ 0 = mid_j:202 /\ 1 = mid_i:204
                /\ __cost:64 = mid___cost:203)
               \/ (1 <= K:201 /\ 0 <= (-1 + param0:53) /\ 0 <= (4 + -1)
                     /\ 0 <= __cost:64 /\ 0 <= (-1 + 1)
                     /\ 0 <= (-mid_j:202 + param0:53)
                     /\ 0 <= (4 + -mid_i:204) /\ 0 <= (-1 + mid___cost:203)
                     /\ 0 <= (-1 + mid_i:204) /\ 0 <= (-1 + mid_j:202)))
         /\ K:205 = 0 /\ mid_j:202 = j':206 /\ mid_i:204 = i':207
         /\ mid___cost:203 = __cost':208 /\ 0 = K:205
         /\ (K:201 + K:205) = K:209 /\ 0 <= K:209 /\ 0 <= j':206
         /\ i':207 <= 4 /\ 1 <= i':207 /\ param0:53 <= j':206)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,51)_g1> -> <__pstate, (Unique State Name,47)_g1>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
<__pstate, accept> -> <__pstate, (Unique State Name,51)_g1>	Base relation: 
{__cost := 0
 x := 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: 
__done 0x5ea40c0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x5e6f640: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
##### ANS
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}
    ( __pstate , (Unique State Name,47)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:13
 param0 := havoc:13
 param0@pos := type_err:292
 param0@width := type_err:293}
    ( __pstate , (Unique State Name,51)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}

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

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

Base relation: 
{__cost := __cost':267
 x := havoc:13
 return := 0
 param0 := havoc:13
 return@pos := type_err:275
 param0@pos := type_err:271
 return@width := type_err:276
 param0@width := type_err:273
 when ((!(0 <= K:260) \/ mid_j:261 = K:260)
         /\ (!(0 <= K:260) \/ mid___cost:262 = K:260)
         /\ (!(0 <= K:260) \/ mid_i:263 <= (1 + K:260))
         /\ (!(0 <= K:260) \/ -mid_i:263 <= (-1 + (3 * K:260)))
         /\ ((K:260 = 0 /\ 0 = mid_j:261 /\ 1 = mid_i:263
                /\ 0 = mid___cost:262)
               \/ (1 <= K:260 /\ 0 <= (-1 + havoc:13) /\ 0 <= (4 + -1)
                     /\ 0 <= (-1 + 1) /\ 0 <= (-mid_j:261 + havoc:13)
                     /\ 0 <= (4 + -mid_i:263) /\ 0 <= (-1 + mid___cost:262)
                     /\ 0 <= (-1 + mid_i:263) /\ 0 <= (-1 + mid_j:261)))
         /\ K:264 = 0 /\ mid_j:261 = j':265 /\ mid_i:263 = i':266
         /\ mid___cost:262 = __cost':267 /\ 0 = K:264
         /\ (K:260 + K:264) = K:268 /\ 0 <= K:268 /\ 0 <= j':265
         /\ i':266 <= 4 /\ 1 <= i':266 /\ havoc:13 <= j':265
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:274)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:274)))}

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

Base relation: 
{__cost := __cost':284
 return := havoc:289
 param0 := param0:53
 return@pos := type_err:290
 param0@pos := type_err:54
 return@width := type_err:291
 param0@width := type_err:55
 when ((!(0 <= K:277) \/ mid_j:278 = K:277)
         /\ (!(0 <= K:277) \/ mid___cost:279 = (__cost:64 + K:277))
         /\ (!(0 <= K:277) \/ mid_i:280 <= (1 + K:277))
         /\ (!(0 <= K:277) \/ -mid_i:280 <= (-1 + (3 * K:277)))
         /\ ((K:277 = 0 /\ 0 = mid_j:278 /\ 1 = mid_i:280
                /\ __cost:64 = mid___cost:279)
               \/ (1 <= K:277 /\ 0 <= (-1 + param0:53) /\ 0 <= (4 + -1)
                     /\ 0 <= __cost:64 /\ 0 <= (-1 + 1)
                     /\ 0 <= (-mid_j:278 + param0:53)
                     /\ 0 <= (4 + -mid_i:280) /\ 0 <= (-1 + mid___cost:279)
                     /\ 0 <= (-1 + mid_i:280) /\ 0 <= (-1 + mid_j:278)))
         /\ K:281 = 0 /\ mid_j:278 = j':282 /\ mid_i:280 = i':283
         /\ mid___cost:279 = __cost':284 /\ 0 = K:281
         /\ (K:277 + K:281) = K:285 /\ 0 <= K:285 /\ 0 <= j':282
         /\ i':283 <= 4 /\ 1 <= i':283 /\ param0:53 <= j':282)}

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

Base relation: 
{__cost := __cost':208
 i := i':207
 j := j':206
 x := param0:53
 return := havoc:210
 return@pos := type_err:211
 return@width := type_err:212
 when ((!(0 <= K:201) \/ mid_j:202 = K:201)
         /\ (!(0 <= K:201) \/ mid___cost:203 = (__cost:64 + K:201))
         /\ (!(0 <= K:201) \/ mid_i:204 <= (1 + K:201))
         /\ (!(0 <= K:201) \/ -mid_i:204 <= (-1 + (3 * K:201)))
         /\ ((K:201 = 0 /\ 0 = mid_j:202 /\ 1 = mid_i:204
                /\ __cost:64 = mid___cost:203)
               \/ (1 <= K:201 /\ 0 <= (-1 + param0:53) /\ 0 <= (4 + -1)
                     /\ 0 <= __cost:64 /\ 0 <= (-1 + 1)
                     /\ 0 <= (-mid_j:202 + param0:53)
                     /\ 0 <= (4 + -mid_i:204) /\ 0 <= (-1 + mid___cost:203)
                     /\ 0 <= (-1 + mid_i:204) /\ 0 <= (-1 + mid_j:202)))
         /\ K:205 = 0 /\ mid_j:202 = j':206 /\ mid_i:204 = i':207
         /\ mid___cost:203 = __cost':208 /\ 0 = K:205
         /\ (K:201 + K:205) = K:209 /\ 0 <= K:209 /\ 0 <= j':206
         /\ i':207 <= 4 /\ 1 <= i':207 /\ param0:53 <= j':206)}

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

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

Variable bounds at line 22 in run

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

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