/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, 58> -> <Unique State Name, 53 57>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 17> -> <Unique State Name, 58>	Base relation: 
{__cost := 0
 x := havoc:20
 y := havoc:21
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:25
 param1@pos := type_err:27
 param0@width := type_err:26
 param1@width := type_err:28}	
<Unique State Name, 61> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 47> -> <Unique State Name, 23>	Base relation: 
{x := param0:73
 y := param1:76}	
<Unique State Name, 23> -> <Unique State Name, 62>	Base relation: 
{}	
<Unique State Name, 51> -> <Unique State Name, 19>	Base relation: 
{}	
<Unique State Name, 59> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 52> -> <Unique State Name, 47 51>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 62> -> <Unique State Name, 27>	Base relation: 
{}	
<Unique State Name, 19> -> <Unique State Name, 60>	Base relation: 
{return := havoc:56
 return@pos := type_err:59
 return@width := type_err:60}	
<Unique State Name, 53> -> <Unique State Name, 52>	Base relation: 
{param0 := param0:73
 param1 := param1:76
 param0@pos := type_err:81
 param1@pos := type_err:82
 param0@width := type_err:83
 param1@width := type_err:84}	
<Unique State Name, 57> -> <Unique State Name, 61>	Base relation: 
{return := 0
 return@pos := type_err:29
 return@width := type_err:30
 when ((y:4 < x:5 /\ (x:5 + -y:4) = phi_tmp___1:22)
         \/ (x:5 <= y:4 /\ 0 = phi_tmp___1:22))}	
<Unique State Name, 27> -> <Unique State Name, 23>	Base relation: 
{__cost := (__cost:96 + 1)
 x := phi_x:110
 y := phi_y:111
 when (y:94 < x:95 /\ 0 <= __cost:96 /\ 0 <= (__cost:96 + 1)
         /\ ((!(havoc:104 = 0) /\ x:95 = phi_x:110 /\ (y:94 + 1) = phi_y:111)
               \/ (havoc:104 = 0 /\ (x:95 + -1) = phi_x:110
                     /\ y:94 = phi_y:111)))}	
<Unique State Name, 27> -> <Unique State Name, 59>	Base relation: 
{return := havoc:107
 return@pos := type_err:108
 return@width := type_err:109
 when x:95 <= y:94}	
<Unique State Name, 60> -> <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:96 + 1)
 x := phi_x:110
 y := phi_y:111
 when (y:94 < x:95 /\ 0 <= __cost:96 /\ 0 <= (__cost:96 + 1)
         /\ ((!(havoc:104 = 0) /\ x:95 = phi_x:110 /\ (y:94 + 1) = phi_y:111)
               \/ (havoc:104 = 0 /\ (x:95 + -1) = phi_x:110
                     /\ y:94 = phi_y:111)))}
**** alpha hat: 
  {<Split [true
            ((-y':136 + x':135)) = (1)*((-y:94 + x:95)) + (-1)*1
           (__cost':134) = (1)*(__cost:96) + 1
           (y':136) <= (1)*(y:94) + 1
           (-y':136) <= (1)*(-y:94) + 0
           }
          pre:
            [|-y:94+x:95-1>=0; __cost:96>=0|]
          post:
            [|-y':136+x':135>=0; __cost':134-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':134
   x := x':135
   y := y':136
   when ((!(0 <= K:146)
            \/ (-mid_y:148 + mid_x:149) = ((-y:94 + x:95) + -K:146))
           /\ (!(0 <= K:146) \/ mid___cost:150 = (__cost:96 + K:146))
           /\ (!(0 <= K:146) \/ mid_y:148 <= (y:94 + K:146))
           /\ (!(0 <= K:146) \/ -mid_y:148 <= -y:94)
           /\ ((K:146 = 0 /\ y:94 = mid_y:148 /\ x:95 = mid_x:149
                  /\ __cost:96 = mid___cost:150)
                 \/ (1 <= K:146 /\ 0 <= (-1 + -y:94 + x:95) /\ 0 <= __cost:96
                       /\ 0 <= (-mid_y:148 + mid_x:149)
                       /\ 0 <= (-1 + mid___cost:150))) /\ K:147 = 0
           /\ mid_y:148 = y':136 /\ mid_x:149 = x':135
           /\ mid___cost:150 = __cost':134 /\ 0 = K:147
           /\ (K:146 + K:147) = K:145 /\ 0 <= K:145)}
}
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:20
       y := havoc:21
       param0 := havoc:20
       param1 := havoc:21
       param0@pos := type_err:25
       param1@pos := type_err:27
       param0@width := type_err:26
       param1@width := type_err:28}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:29
     return@width := type_err:30
     when ((y:4 < x:5 /\ (x:5 + -y:4) = phi_tmp___1:22)
             \/ (x:5 <= y:4 /\ 0 = phi_tmp___1:22))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:73
       param1 := param1:76
       param0@pos := type_err:81
       param1@pos := type_err:82
       param0@width := type_err:83
       param1@width := type_err:84}    )
    ,
    Var(19)
  )
  ,
  Weight(Base relation: 
    {return := havoc:56
     return@pos := type_err:59
     return@width := type_err:60}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=19: 
Weight(Base relation: 
  {__cost := __cost':158
   x := x':157
   y := y':156
   return := havoc:160
   return@pos := type_err:161
   return@width := type_err:162
   when ((!(0 <= K:151)
            \/ (-mid_y:152 + mid_x:153) = ((-param1:76 + param0:73) + -K:151))
           /\ (!(0 <= K:151) \/ mid___cost:154 = (__cost:96 + K:151))
           /\ (!(0 <= K:151) \/ mid_y:152 <= (param1:76 + K:151))
           /\ (!(0 <= K:151) \/ -mid_y:152 <= -param1:76)
           /\ ((K:151 = 0 /\ param1:76 = mid_y:152 /\ param0:73 = mid_x:153
                  /\ __cost:96 = mid___cost:154)
                 \/ (1 <= K:151 /\ 0 <= (-1 + -param1:76 + param0:73)
                       /\ 0 <= __cost:96 /\ 0 <= (-mid_y:152 + mid_x:153)
                       /\ 0 <= (-1 + mid___cost:154))) /\ K:155 = 0
           /\ mid_y:152 = y':156 /\ mid_x:153 = x':157
           /\ mid___cost:154 = __cost':158 /\ 0 = K:155
           /\ (K:151 + K:155) = K:159 /\ 0 <= K:159 /\ x':157 <= y':156)})



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:20
         y := havoc:21
         param0 := havoc:20
         param1 := havoc:21
         param0@pos := type_err:25
         param1@pos := type_err:27
         param0@width := type_err:26
         param1@width := type_err:28}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:29
       return@width := type_err:30
       when ((y:4 < x:5 /\ (x:5 + -y:4) = phi_tmp___1:22)
               \/ (x:5 <= y:4 /\ 0 = phi_tmp___1:22))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:73
         param1 := param1:76
         param0@pos := type_err:81
         param1@pos := type_err:82
         param0@width := type_err:83
         param1@width := type_err:84}      )
      ,
      Var(19)
    )
    ,
    Weight(Base relation: 
      {return := havoc:56
       return@pos := type_err:59
       return@width := type_err:60}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':158
   return := havoc:160
   return@pos := type_err:161
   return@width := type_err:162
   when ((!(0 <= K:151)
            \/ (-mid_y:152 + mid_x:153) = ((-param1:76 + param0:73) + -K:151))
           /\ (!(0 <= K:151) \/ mid___cost:154 = (__cost:96 + K:151))
           /\ (!(0 <= K:151) \/ mid_y:152 <= (param1:76 + K:151))
           /\ (!(0 <= K:151) \/ -mid_y:152 <= -param1:76)
           /\ ((K:151 = 0 /\ param1:76 = mid_y:152 /\ param0:73 = mid_x:153
                  /\ __cost:96 = mid___cost:154)
                 \/ (1 <= K:151 /\ 0 <= (-1 + -param1:76 + param0:73)
                       /\ 0 <= __cost:96 /\ 0 <= (-mid_y:152 + mid_x:153)
                       /\ 0 <= (-1 + mid___cost:154))) /\ K:155 = 0
           /\ mid_y:152 = y':156 /\ mid_x:153 = x':157
           /\ mid___cost:154 = __cost':158 /\ 0 = K:155
           /\ (K:151 + K:155) = K:159 /\ 0 <= K:159 /\ x':157 <= y':156)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':185
   return := 0
   param0 := havoc:20
   param1 := havoc:21
   return@pos := type_err:195
   param0@pos := type_err:189
   param1@pos := type_err:190
   return@width := type_err:196
   param0@width := type_err:192
   param1@width := type_err:193
   when ((!(0 <= K:178)
            \/ (-mid_y:179 + mid_x:180) = ((-havoc:21 + havoc:20) + -K:178))
           /\ (!(0 <= K:178) \/ mid___cost:181 = K:178)
           /\ (!(0 <= K:178) \/ mid_y:179 <= (havoc:21 + K:178))
           /\ (!(0 <= K:178) \/ -mid_y:179 <= -havoc:21)
           /\ ((K:178 = 0 /\ havoc:21 = mid_y:179 /\ havoc:20 = mid_x:180
                  /\ 0 = mid___cost:181)
                 \/ (1 <= K:178 /\ 0 <= (-1 + -havoc:21 + havoc:20)
                       /\ 0 <= (-mid_y:179 + mid_x:180)
                       /\ 0 <= (-1 + mid___cost:181))) /\ K:182 = 0
           /\ mid_y:179 = y':183 /\ mid_x:180 = x':184
           /\ mid___cost:181 = __cost':185 /\ 0 = K:182
           /\ (K:178 + K:182) = K:186 /\ 0 <= K:186 /\ x':184 <= y':183
           /\ ((havoc:21 < havoc:20
                  /\ (havoc:20 + -havoc:21) = phi_tmp___1:194)
                 \/ (havoc:20 <= havoc:21 /\ 0 = phi_tmp___1:194)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':204
   return := havoc:209
   param0 := param0:73
   param1 := param1:76
   return@pos := type_err:210
   param0@pos := type_err:81
   param1@pos := type_err:82
   return@width := type_err:211
   param0@width := type_err:83
   param1@width := type_err:84
   when ((!(0 <= K:197)
            \/ (-mid_y:198 + mid_x:199) = ((-param1:76 + param0:73) + -K:197))
           /\ (!(0 <= K:197) \/ mid___cost:200 = (__cost:96 + K:197))
           /\ (!(0 <= K:197) \/ mid_y:198 <= (param1:76 + K:197))
           /\ (!(0 <= K:197) \/ -mid_y:198 <= -param1:76)
           /\ ((K:197 = 0 /\ param1:76 = mid_y:198 /\ param0:73 = mid_x:199
                  /\ __cost:96 = mid___cost:200)
                 \/ (1 <= K:197 /\ 0 <= (-1 + -param1:76 + param0:73)
                       /\ 0 <= __cost:96 /\ 0 <= (-mid_y:198 + mid_x:199)
                       /\ 0 <= (-1 + mid___cost:200))) /\ K:201 = 0
           /\ mid_y:198 = y':202 /\ mid_x:199 = x':203
           /\ mid___cost:200 = __cost':204 /\ 0 = K:201
           /\ (K:197 + K:201) = K:205 /\ 0 <= K:205 /\ x':203 <= y':202)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=19: 
Weight(Base relation: 
  {__cost := __cost':158
   return := havoc:160
   return@pos := type_err:161
   return@width := type_err:162
   when ((!(0 <= K:151)
            \/ (-mid_y:152 + mid_x:153) = ((-param1:76 + param0:73) + -K:151))
           /\ (!(0 <= K:151) \/ mid___cost:154 = (__cost:96 + K:151))
           /\ (!(0 <= K:151) \/ mid_y:152 <= (param1:76 + K:151))
           /\ (!(0 <= K:151) \/ -mid_y:152 <= -param1:76)
           /\ ((K:151 = 0 /\ param1:76 = mid_y:152 /\ param0:73 = mid_x:153
                  /\ __cost:96 = mid___cost:154)
                 \/ (1 <= K:151 /\ 0 <= (-1 + -param1:76 + param0:73)
                       /\ 0 <= __cost:96 /\ 0 <= (-mid_y:152 + mid_x:153)
                       /\ 0 <= (-1 + mid___cost:154))) /\ K:155 = 0
           /\ mid_y:152 = y':156 /\ mid_x:153 = x':157
           /\ mid___cost:154 = __cost':158 /\ 0 = K:155
           /\ (K:151 + K:155) = K:159 /\ 0 <= K:159 /\ x':157 <= y':156)})


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':185
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:195
 param0@pos := type_err:189
 param1@pos := type_err:190
 return@width := type_err:196
 param0@width := type_err:192
 param1@width := type_err:193
 when ((!(0 <= K:178)
          \/ (-mid_y:179 + mid_x:180) = ((-havoc:21 + havoc:20) + -K:178))
         /\ (!(0 <= K:178) \/ mid___cost:181 = K:178)
         /\ (!(0 <= K:178) \/ mid_y:179 <= (havoc:21 + K:178))
         /\ (!(0 <= K:178) \/ -mid_y:179 <= -havoc:21)
         /\ ((K:178 = 0 /\ havoc:21 = mid_y:179 /\ havoc:20 = mid_x:180
                /\ 0 = mid___cost:181)
               \/ (1 <= K:178 /\ 0 <= (-1 + -havoc:21 + havoc:20)
                     /\ 0 <= (-mid_y:179 + mid_x:180)
                     /\ 0 <= (-1 + mid___cost:181))) /\ K:182 = 0
         /\ mid_y:179 = y':183 /\ mid_x:180 = x':184
         /\ mid___cost:181 = __cost':185 /\ 0 = K:182
         /\ (K:178 + K:182) = K:186 /\ 0 <= K:186 /\ x':184 <= y':183
         /\ ((havoc:21 < havoc:20 /\ (havoc:20 + -havoc:21) = phi_tmp___1:194)
               \/ (havoc:20 <= havoc:21 /\ 0 = phi_tmp___1:194)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':204
 return := havoc:209
 param0 := param0:73
 param1 := param1:76
 return@pos := type_err:210
 param0@pos := type_err:81
 param1@pos := type_err:82
 return@width := type_err:211
 param0@width := type_err:83
 param1@width := type_err:84
 when ((!(0 <= K:197)
          \/ (-mid_y:198 + mid_x:199) = ((-param1:76 + param0:73) + -K:197))
         /\ (!(0 <= K:197) \/ mid___cost:200 = (__cost:96 + K:197))
         /\ (!(0 <= K:197) \/ mid_y:198 <= (param1:76 + K:197))
         /\ (!(0 <= K:197) \/ -mid_y:198 <= -param1:76)
         /\ ((K:197 = 0 /\ param1:76 = mid_y:198 /\ param0:73 = mid_x:199
                /\ __cost:96 = mid___cost:200)
               \/ (1 <= K:197 /\ 0 <= (-1 + -param1:76 + param0:73)
                     /\ 0 <= __cost:96 /\ 0 <= (-mid_y:198 + mid_x:199)
                     /\ 0 <= (-1 + mid___cost:200))) /\ K:201 = 0
         /\ mid_y:198 = y':202 /\ mid_x:199 = x':203
         /\ mid___cost:200 = __cost':204 /\ 0 = K:201
         /\ (K:197 + K:201) = K:205 /\ 0 <= K:205 /\ x':203 <= y':202)}

Evaluating variable number 19 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':158
 return := havoc:160
 return@pos := type_err:161
 return@width := type_err:162
 when ((!(0 <= K:151)
          \/ (-mid_y:152 + mid_x:153) = ((-param1:76 + param0:73) + -K:151))
         /\ (!(0 <= K:151) \/ mid___cost:154 = (__cost:96 + K:151))
         /\ (!(0 <= K:151) \/ mid_y:152 <= (param1:76 + K:151))
         /\ (!(0 <= K:151) \/ -mid_y:152 <= -param1:76)
         /\ ((K:151 = 0 /\ param1:76 = mid_y:152 /\ param0:73 = mid_x:153
                /\ __cost:96 = mid___cost:154)
               \/ (1 <= K:151 /\ 0 <= (-1 + -param1:76 + param0:73)
                     /\ 0 <= __cost:96 /\ 0 <= (-mid_y:152 + mid_x:153)
                     /\ 0 <= (-1 + mid___cost:154))) /\ K:155 = 0
         /\ mid_y:152 = y':156 /\ mid_x:153 = x':157
         /\ mid___cost:154 = __cost':158 /\ 0 = K:155
         /\ (K:151 + K:155) = K:159 /\ 0 <= K:159 /\ x':157 <= y':156)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,53)_g1> -> <__pstate, (Unique State Name,47)_g1>	Base relation: 
{param0 := param0:73
 param1 := param1:76
 param0@pos := type_err:81
 param1@pos := type_err:82
 param0@width := type_err:83
 param1@width := type_err:84}	
<__pstate, accept> -> <__pstate, (Unique State Name,53)_g1>	Base relation: 
{__cost := 0
 x := havoc:20
 y := havoc:21
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:25
 param1@pos := type_err:27
 param0@width := type_err:26
 param1@width := type_err:28}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x3cb1d30: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x4cde350: 
	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:20
 y := havoc:21
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:246
 param1@pos := type_err:247
 param0@width := type_err:248
 param1@width := type_err:249}
    ( __pstate , (Unique State Name,53)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:20
 y := havoc:21
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:25
 param1@pos := type_err:27
 param0@width := type_err:26
 param1@width := type_err:28}

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

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

Base relation: 
{__cost := __cost':219
 x := havoc:20
 y := havoc:21
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:229
 param0@pos := type_err:223
 param1@pos := type_err:224
 return@width := type_err:230
 param0@width := type_err:226
 param1@width := type_err:227
 when ((!(0 <= K:212)
          \/ (-mid_y:213 + mid_x:214) = ((-havoc:21 + havoc:20) + -K:212))
         /\ (!(0 <= K:212) \/ mid___cost:215 = K:212)
         /\ (!(0 <= K:212) \/ mid_y:213 <= (havoc:21 + K:212))
         /\ (!(0 <= K:212) \/ -mid_y:213 <= -havoc:21)
         /\ ((K:212 = 0 /\ havoc:21 = mid_y:213 /\ havoc:20 = mid_x:214
                /\ 0 = mid___cost:215)
               \/ (1 <= K:212 /\ 0 <= (-1 + -havoc:21 + havoc:20)
                     /\ 0 <= (-mid_y:213 + mid_x:214)
                     /\ 0 <= (-1 + mid___cost:215))) /\ K:216 = 0
         /\ mid_y:213 = y':217 /\ mid_x:214 = x':218
         /\ mid___cost:215 = __cost':219 /\ 0 = K:216
         /\ (K:212 + K:216) = K:220 /\ 0 <= K:220 /\ x':218 <= y':217
         /\ ((havoc:21 < havoc:20 /\ (havoc:20 + -havoc:21) = phi_tmp___1:228)
               \/ (havoc:20 <= havoc:21 /\ 0 = phi_tmp___1:228)))}

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

Base relation: 
{__cost := __cost':238
 return := havoc:243
 param0 := param0:73
 param1 := param1:76
 return@pos := type_err:244
 param0@pos := type_err:81
 param1@pos := type_err:82
 return@width := type_err:245
 param0@width := type_err:83
 param1@width := type_err:84
 when ((!(0 <= K:231)
          \/ (-mid_y:232 + mid_x:233) = ((-param1:76 + param0:73) + -K:231))
         /\ (!(0 <= K:231) \/ mid___cost:234 = (__cost:96 + K:231))
         /\ (!(0 <= K:231) \/ mid_y:232 <= (param1:76 + K:231))
         /\ (!(0 <= K:231) \/ -mid_y:232 <= -param1:76)
         /\ ((K:231 = 0 /\ param1:76 = mid_y:232 /\ param0:73 = mid_x:233
                /\ __cost:96 = mid___cost:234)
               \/ (1 <= K:231 /\ 0 <= (-1 + -param1:76 + param0:73)
                     /\ 0 <= __cost:96 /\ 0 <= (-mid_y:232 + mid_x:233)
                     /\ 0 <= (-1 + mid___cost:234))) /\ K:235 = 0
         /\ mid_y:232 = y':236 /\ mid_x:233 = x':237
         /\ mid___cost:234 = __cost':238 /\ 0 = K:235
         /\ (K:231 + K:235) = K:239 /\ 0 <= K:239 /\ x':237 <= y':236)}

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

Base relation: 
{__cost := __cost':158
 x := x':157
 y := y':156
 return := havoc:160
 return@pos := type_err:161
 return@width := type_err:162
 when ((!(0 <= K:151)
          \/ (-mid_y:152 + mid_x:153) = ((-param1:76 + param0:73) + -K:151))
         /\ (!(0 <= K:151) \/ mid___cost:154 = (__cost:96 + K:151))
         /\ (!(0 <= K:151) \/ mid_y:152 <= (param1:76 + K:151))
         /\ (!(0 <= K:151) \/ -mid_y:152 <= -param1:76)
         /\ ((K:151 = 0 /\ param1:76 = mid_y:152 /\ param0:73 = mid_x:153
                /\ __cost:96 = mid___cost:154)
               \/ (1 <= K:151 /\ 0 <= (-1 + -param1:76 + param0:73)
                     /\ 0 <= __cost:96 /\ 0 <= (-mid_y:152 + mid_x:153)
                     /\ 0 <= (-1 + mid___cost:154))) /\ K:155 = 0
         /\ mid_y:152 = y':156 /\ mid_x:153 = x':157
         /\ mid___cost:154 = __cost':158 /\ 0 = K:155
         /\ (K:151 + K:155) = K:159 /\ 0 <= K:159 /\ x':157 <= y':156)}

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

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

Variable bounds at line 19 in run

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

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