/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, 69> -> <Unique State Name, 62 68>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 25> -> <Unique State Name, 69>	Base relation: 
{__cost := 0
 x := havoc:28
 z := havoc:29
 n := havoc:30
 param0 := havoc:28
 param1 := havoc:29
 param2 := havoc:30
 param0@pos := type_err:35
 param1@pos := type_err:37
 param2@pos := type_err:39
 param0@width := type_err:36
 param1@width := type_err:38
 param2@width := type_err:40}	
<Unique State Name, 72> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 54> -> <Unique State Name, 31>	Base relation: 
{x := param0:100
 z := param1:103
 n := param2:106}	
<Unique State Name, 31> -> <Unique State Name, 73>	Base relation: 
{}	
<Unique State Name, 60> -> <Unique State Name, 27>	Base relation: 
{}	
<Unique State Name, 70> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 61> -> <Unique State Name, 54 60>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 73> -> <Unique State Name, 35>	Base relation: 
{}	
<Unique State Name, 27> -> <Unique State Name, 71>	Base relation: 
{return := havoc:78
 return@pos := type_err:81
 return@width := type_err:82}	
<Unique State Name, 62> -> <Unique State Name, 61>	Base relation: 
{param0 := param0:100
 param1 := param1:103
 param2 := param2:106
 param0@pos := type_err:113
 param1@pos := type_err:114
 param2@pos := type_err:115
 param0@width := type_err:116
 param1@width := type_err:117
 param2@width := type_err:118}	
<Unique State Name, 68> -> <Unique State Name, 72>	Base relation: 
{return := 0
 return@pos := type_err:42
 return@width := type_err:43
 when (((x:6 < n:7 /\ (n:7 + -x:6) = phi_tmp___2:31)
          \/ (n:7 <= x:6 /\ 0 = phi_tmp___2:31))
         /\ ((z:8 < n:7 /\ (n:7 + -z:8) = phi_tmp___3:41)
               \/ (n:7 <= z:8 /\ 0 = phi_tmp___3:41)))}	
<Unique State Name, 35> -> <Unique State Name, 31>	Base relation: 
{__cost := (__cost:133 + 1)
 x := phi_x:145
 z := phi_z:146
 when (x:131 < n:132 /\ 0 <= __cost:133 /\ 0 <= (__cost:133 + 1)
         /\ ((x:131 < z:134 /\ (x:131 + 1) = phi_x:145 /\ z:134 = phi_z:146)
               \/ (z:134 <= x:131 /\ x:131 = phi_x:145
                     /\ (z:134 + 1) = phi_z:146)))}	
<Unique State Name, 35> -> <Unique State Name, 70>	Base relation: 
{return := havoc:142
 return@pos := type_err:143
 return@width := type_err:144
 when n:132 <= x:131}	
<Unique State Name, 71> -> <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:133 + 1)
 x := phi_x:145
 z := phi_z:146
 when (x:131 < n:132 /\ 0 <= __cost:133 /\ 0 <= (__cost:133 + 1)
         /\ ((x:131 < z:134 /\ (x:131 + 1) = phi_x:145 /\ z:134 = phi_z:146)
               \/ (z:134 <= x:131 /\ x:131 = phi_x:145
                     /\ (z:134 + 1) = phi_z:146)))}
**** alpha hat: 
  {<Split [true
            ((x':181 + z':182)) = (1)*((x:131 + z:134)) + 1
           (__cost':180) = (1)*(__cost:133) + 1
           (z':182) <= (1)*(z:134) + 1
           (-z':182) <= (1)*(-z:134) + 0
           }
          pre:
            [|-x:131+n:132-1>=0; __cost:133>=0|]
          post:
            [|-x':181+n:132>=0; __cost':180-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':180
   x := x':181
   z := z':182
   when ((!(0 <= K:193)
            \/ (mid_x:196 + mid_z:195) = ((x:131 + z:134) + K:193))
           /\ (!(0 <= K:193) \/ mid___cost:197 = (__cost:133 + K:193))
           /\ (!(0 <= K:193) \/ mid_z:195 <= (z:134 + K:193))
           /\ (!(0 <= K:193) \/ -mid_z:195 <= -z:134)
           /\ ((K:193 = 0 /\ z:134 = mid_z:195 /\ x:131 = mid_x:196
                  /\ __cost:133 = mid___cost:197)
                 \/ (1 <= K:193 /\ 0 <= (-1 + -x:131 + n:132)
                       /\ 0 <= __cost:133 /\ 0 <= (-mid_x:196 + n:132)
                       /\ 0 <= (-1 + mid___cost:197))) /\ K:194 = 0
           /\ mid_z:195 = z':182 /\ mid_x:196 = x':181
           /\ mid___cost:197 = __cost':180 /\ 0 = K:194
           /\ (K:193 + K:194) = K:192 /\ 0 <= K:192)}
}
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:28
       z := havoc:29
       n := havoc:30
       param0 := havoc:28
       param1 := havoc:29
       param2 := havoc:30
       param0@pos := type_err:35
       param1@pos := type_err:37
       param2@pos := type_err:39
       param0@width := type_err:36
       param1@width := type_err:38
       param2@width := type_err:40}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:42
     return@width := type_err:43
     when (((x:6 < n:7 /\ (n:7 + -x:6) = phi_tmp___2:31)
              \/ (n:7 <= x:6 /\ 0 = phi_tmp___2:31))
             /\ ((z:8 < n:7 /\ (n:7 + -z:8) = phi_tmp___3:41)
                   \/ (n:7 <= z:8 /\ 0 = phi_tmp___3:41)))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:100
       param1 := param1:103
       param2 := param2:106
       param0@pos := type_err:113
       param1@pos := type_err:114
       param2@pos := type_err:115
       param0@width := type_err:116
       param1@width := type_err:117
       param2@width := type_err:118}    )
    ,
    Var(19)
  )
  ,
  Weight(Base relation: 
    {return := havoc:78
     return@pos := type_err:81
     return@width := type_err:82}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=19: 
Weight(Base relation: 
  {__cost := __cost':205
   x := x':204
   z := z':203
   n := param2:106
   return := havoc:207
   return@pos := type_err:208
   return@width := type_err:209
   when ((!(0 <= K:198)
            \/ (mid_x:199 + mid_z:200) = ((param0:100 + param1:103) + K:198))
           /\ (!(0 <= K:198) \/ mid___cost:201 = (__cost:133 + K:198))
           /\ (!(0 <= K:198) \/ mid_z:200 <= (param1:103 + K:198))
           /\ (!(0 <= K:198) \/ -mid_z:200 <= -param1:103)
           /\ ((K:198 = 0 /\ param1:103 = mid_z:200 /\ param0:100 = mid_x:199
                  /\ __cost:133 = mid___cost:201)
                 \/ (1 <= K:198 /\ 0 <= (-1 + -param0:100 + param2:106)
                       /\ 0 <= __cost:133 /\ 0 <= (-mid_x:199 + param2:106)
                       /\ 0 <= (-1 + mid___cost:201))) /\ K:202 = 0
           /\ mid_z:200 = z':203 /\ mid_x:199 = x':204
           /\ mid___cost:201 = __cost':205 /\ 0 = K:202
           /\ (K:198 + K:202) = K:206 /\ 0 <= K:206 /\ param2:106 <= x':204)})



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:28
         z := havoc:29
         n := havoc:30
         param0 := havoc:28
         param1 := havoc:29
         param2 := havoc:30
         param0@pos := type_err:35
         param1@pos := type_err:37
         param2@pos := type_err:39
         param0@width := type_err:36
         param1@width := type_err:38
         param2@width := type_err:40}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:42
       return@width := type_err:43
       when (((x:6 < n:7 /\ (n:7 + -x:6) = phi_tmp___2:31)
                \/ (n:7 <= x:6 /\ 0 = phi_tmp___2:31))
               /\ ((z:8 < n:7 /\ (n:7 + -z:8) = phi_tmp___3:41)
                     \/ (n:7 <= z:8 /\ 0 = phi_tmp___3:41)))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:100
         param1 := param1:103
         param2 := param2:106
         param0@pos := type_err:113
         param1@pos := type_err:114
         param2@pos := type_err:115
         param0@width := type_err:116
         param1@width := type_err:117
         param2@width := type_err:118}      )
      ,
      Var(19)
    )
    ,
    Weight(Base relation: 
      {return := havoc:78
       return@pos := type_err:81
       return@width := type_err:82}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':205
   return := havoc:207
   return@pos := type_err:208
   return@width := type_err:209
   when ((!(0 <= K:198)
            \/ (mid_x:199 + mid_z:200) = ((param0:100 + param1:103) + K:198))
           /\ (!(0 <= K:198) \/ mid___cost:201 = (__cost:133 + K:198))
           /\ (!(0 <= K:198) \/ mid_z:200 <= (param1:103 + K:198))
           /\ (!(0 <= K:198) \/ -mid_z:200 <= -param1:103)
           /\ ((K:198 = 0 /\ param1:103 = mid_z:200 /\ param0:100 = mid_x:199
                  /\ __cost:133 = mid___cost:201)
                 \/ (1 <= K:198 /\ 0 <= (-1 + -param0:100 + param2:106)
                       /\ 0 <= __cost:133 /\ 0 <= (-mid_x:199 + param2:106)
                       /\ 0 <= (-1 + mid___cost:201))) /\ K:202 = 0
           /\ mid_z:200 = z':203 /\ mid_x:199 = x':204
           /\ mid___cost:201 = __cost':205 /\ 0 = K:202
           /\ (K:198 + K:202) = K:206 /\ 0 <= K:206 /\ param2:106 <= x':204)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':232
   return := 0
   param0 := havoc:28
   param1 := havoc:29
   param2 := havoc:30
   return@pos := type_err:245
   param0@pos := type_err:236
   param1@pos := type_err:237
   param2@pos := type_err:238
   return@width := type_err:246
   param0@width := type_err:240
   param1@width := type_err:241
   param2@width := type_err:242
   when ((!(0 <= K:225)
            \/ (mid_x:226 + mid_z:227) = ((havoc:28 + havoc:29) + K:225))
           /\ (!(0 <= K:225) \/ mid___cost:228 = K:225)
           /\ (!(0 <= K:225) \/ mid_z:227 <= (havoc:29 + K:225))
           /\ (!(0 <= K:225) \/ -mid_z:227 <= -havoc:29)
           /\ ((K:225 = 0 /\ havoc:29 = mid_z:227 /\ havoc:28 = mid_x:226
                  /\ 0 = mid___cost:228)
                 \/ (1 <= K:225 /\ 0 <= (-1 + -havoc:28 + havoc:30)
                       /\ 0 <= (-mid_x:226 + havoc:30)
                       /\ 0 <= (-1 + mid___cost:228))) /\ K:229 = 0
           /\ mid_z:227 = z':230 /\ mid_x:226 = x':231
           /\ mid___cost:228 = __cost':232 /\ 0 = K:229
           /\ (K:225 + K:229) = K:233 /\ 0 <= K:233 /\ havoc:30 <= x':231
           /\ ((havoc:28 < havoc:30
                  /\ (havoc:30 + -havoc:28) = phi_tmp___2:243)
                 \/ (havoc:30 <= havoc:28 /\ 0 = phi_tmp___2:243))
           /\ ((havoc:29 < havoc:30
                  /\ (havoc:30 + -havoc:29) = phi_tmp___3:244)
                 \/ (havoc:30 <= havoc:29 /\ 0 = phi_tmp___3:244)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':254
   return := havoc:259
   param0 := param0:100
   param1 := param1:103
   param2 := param2:106
   return@pos := type_err:260
   param0@pos := type_err:113
   param1@pos := type_err:114
   param2@pos := type_err:115
   return@width := type_err:261
   param0@width := type_err:116
   param1@width := type_err:117
   param2@width := type_err:118
   when ((!(0 <= K:247)
            \/ (mid_x:248 + mid_z:249) = ((param0:100 + param1:103) + K:247))
           /\ (!(0 <= K:247) \/ mid___cost:250 = (__cost:133 + K:247))
           /\ (!(0 <= K:247) \/ mid_z:249 <= (param1:103 + K:247))
           /\ (!(0 <= K:247) \/ -mid_z:249 <= -param1:103)
           /\ ((K:247 = 0 /\ param1:103 = mid_z:249 /\ param0:100 = mid_x:248
                  /\ __cost:133 = mid___cost:250)
                 \/ (1 <= K:247 /\ 0 <= (-1 + -param0:100 + param2:106)
                       /\ 0 <= __cost:133 /\ 0 <= (-mid_x:248 + param2:106)
                       /\ 0 <= (-1 + mid___cost:250))) /\ K:251 = 0
           /\ mid_z:249 = z':252 /\ mid_x:248 = x':253
           /\ mid___cost:250 = __cost':254 /\ 0 = K:251
           /\ (K:247 + K:251) = K:255 /\ 0 <= K:255 /\ param2:106 <= x':253)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=19: 
Weight(Base relation: 
  {__cost := __cost':205
   return := havoc:207
   return@pos := type_err:208
   return@width := type_err:209
   when ((!(0 <= K:198)
            \/ (mid_x:199 + mid_z:200) = ((param0:100 + param1:103) + K:198))
           /\ (!(0 <= K:198) \/ mid___cost:201 = (__cost:133 + K:198))
           /\ (!(0 <= K:198) \/ mid_z:200 <= (param1:103 + K:198))
           /\ (!(0 <= K:198) \/ -mid_z:200 <= -param1:103)
           /\ ((K:198 = 0 /\ param1:103 = mid_z:200 /\ param0:100 = mid_x:199
                  /\ __cost:133 = mid___cost:201)
                 \/ (1 <= K:198 /\ 0 <= (-1 + -param0:100 + param2:106)
                       /\ 0 <= __cost:133 /\ 0 <= (-mid_x:199 + param2:106)
                       /\ 0 <= (-1 + mid___cost:201))) /\ K:202 = 0
           /\ mid_z:200 = z':203 /\ mid_x:199 = x':204
           /\ mid___cost:201 = __cost':205 /\ 0 = K:202
           /\ (K:198 + K:202) = K:206 /\ 0 <= K:206 /\ param2:106 <= x':204)})


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':232
 return := 0
 param0 := havoc:28
 param1 := havoc:29
 param2 := havoc:30
 return@pos := type_err:245
 param0@pos := type_err:236
 param1@pos := type_err:237
 param2@pos := type_err:238
 return@width := type_err:246
 param0@width := type_err:240
 param1@width := type_err:241
 param2@width := type_err:242
 when ((!(0 <= K:225)
          \/ (mid_x:226 + mid_z:227) = ((havoc:28 + havoc:29) + K:225))
         /\ (!(0 <= K:225) \/ mid___cost:228 = K:225)
         /\ (!(0 <= K:225) \/ mid_z:227 <= (havoc:29 + K:225))
         /\ (!(0 <= K:225) \/ -mid_z:227 <= -havoc:29)
         /\ ((K:225 = 0 /\ havoc:29 = mid_z:227 /\ havoc:28 = mid_x:226
                /\ 0 = mid___cost:228)
               \/ (1 <= K:225 /\ 0 <= (-1 + -havoc:28 + havoc:30)
                     /\ 0 <= (-mid_x:226 + havoc:30)
                     /\ 0 <= (-1 + mid___cost:228))) /\ K:229 = 0
         /\ mid_z:227 = z':230 /\ mid_x:226 = x':231
         /\ mid___cost:228 = __cost':232 /\ 0 = K:229
         /\ (K:225 + K:229) = K:233 /\ 0 <= K:233 /\ havoc:30 <= x':231
         /\ ((havoc:28 < havoc:30 /\ (havoc:30 + -havoc:28) = phi_tmp___2:243)
               \/ (havoc:30 <= havoc:28 /\ 0 = phi_tmp___2:243))
         /\ ((havoc:29 < havoc:30 /\ (havoc:30 + -havoc:29) = phi_tmp___3:244)
               \/ (havoc:30 <= havoc:29 /\ 0 = phi_tmp___3:244)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':254
 return := havoc:259
 param0 := param0:100
 param1 := param1:103
 param2 := param2:106
 return@pos := type_err:260
 param0@pos := type_err:113
 param1@pos := type_err:114
 param2@pos := type_err:115
 return@width := type_err:261
 param0@width := type_err:116
 param1@width := type_err:117
 param2@width := type_err:118
 when ((!(0 <= K:247)
          \/ (mid_x:248 + mid_z:249) = ((param0:100 + param1:103) + K:247))
         /\ (!(0 <= K:247) \/ mid___cost:250 = (__cost:133 + K:247))
         /\ (!(0 <= K:247) \/ mid_z:249 <= (param1:103 + K:247))
         /\ (!(0 <= K:247) \/ -mid_z:249 <= -param1:103)
         /\ ((K:247 = 0 /\ param1:103 = mid_z:249 /\ param0:100 = mid_x:248
                /\ __cost:133 = mid___cost:250)
               \/ (1 <= K:247 /\ 0 <= (-1 + -param0:100 + param2:106)
                     /\ 0 <= __cost:133 /\ 0 <= (-mid_x:248 + param2:106)
                     /\ 0 <= (-1 + mid___cost:250))) /\ K:251 = 0
         /\ mid_z:249 = z':252 /\ mid_x:248 = x':253
         /\ mid___cost:250 = __cost':254 /\ 0 = K:251
         /\ (K:247 + K:251) = K:255 /\ 0 <= K:255 /\ param2:106 <= x':253)}

Evaluating variable number 19 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':205
 return := havoc:207
 return@pos := type_err:208
 return@width := type_err:209
 when ((!(0 <= K:198)
          \/ (mid_x:199 + mid_z:200) = ((param0:100 + param1:103) + K:198))
         /\ (!(0 <= K:198) \/ mid___cost:201 = (__cost:133 + K:198))
         /\ (!(0 <= K:198) \/ mid_z:200 <= (param1:103 + K:198))
         /\ (!(0 <= K:198) \/ -mid_z:200 <= -param1:103)
         /\ ((K:198 = 0 /\ param1:103 = mid_z:200 /\ param0:100 = mid_x:199
                /\ __cost:133 = mid___cost:201)
               \/ (1 <= K:198 /\ 0 <= (-1 + -param0:100 + param2:106)
                     /\ 0 <= __cost:133 /\ 0 <= (-mid_x:199 + param2:106)
                     /\ 0 <= (-1 + mid___cost:201))) /\ K:202 = 0
         /\ mid_z:200 = z':203 /\ mid_x:199 = x':204
         /\ mid___cost:201 = __cost':205 /\ 0 = K:202
         /\ (K:198 + K:202) = K:206 /\ 0 <= K:206 /\ param2:106 <= x':204)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,62)_g1> -> <__pstate, (Unique State Name,54)_g1>	Base relation: 
{param0 := param0:100
 param1 := param1:103
 param2 := param2:106
 param0@pos := type_err:113
 param1@pos := type_err:114
 param2@pos := type_err:115
 param0@width := type_err:116
 param1@width := type_err:117
 param2@width := type_err:118}	
<__pstate, accept> -> <__pstate, (Unique State Name,62)_g1>	Base relation: 
{__cost := 0
 x := havoc:28
 z := havoc:29
 n := havoc:30
 param0 := havoc:28
 param1 := havoc:29
 param2 := havoc:30
 param0@pos := type_err:35
 param1@pos := type_err:37
 param2@pos := type_err:39
 param0@width := type_err:36
 param1@width := type_err:38
 param2@width := type_err:40}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x340c0b0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x19c6a00: 
	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,54)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:28
 z := havoc:29
 n := havoc:30
 param0 := havoc:28
 param1 := havoc:29
 param2 := havoc:30
 param0@pos := type_err:299
 param1@pos := type_err:300
 param2@pos := type_err:301
 param0@width := type_err:302
 param1@width := type_err:303
 param2@width := type_err:304}
    ( __pstate , (Unique State Name,62)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:28
 z := havoc:29
 n := havoc:30
 param0 := havoc:28
 param1 := havoc:29
 param2 := havoc:30
 param0@pos := type_err:35
 param1@pos := type_err:37
 param2@pos := type_err:39
 param0@width := type_err:36
 param1@width := type_err:38
 param2@width := type_err:40}

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

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

Base relation: 
{__cost := __cost':269
 x := havoc:28
 z := havoc:29
 n := havoc:30
 return := 0
 param0 := havoc:28
 param1 := havoc:29
 param2 := havoc:30
 return@pos := type_err:282
 param0@pos := type_err:273
 param1@pos := type_err:274
 param2@pos := type_err:275
 return@width := type_err:283
 param0@width := type_err:277
 param1@width := type_err:278
 param2@width := type_err:279
 when ((!(0 <= K:262)
          \/ (mid_x:263 + mid_z:264) = ((havoc:28 + havoc:29) + K:262))
         /\ (!(0 <= K:262) \/ mid___cost:265 = K:262)
         /\ (!(0 <= K:262) \/ mid_z:264 <= (havoc:29 + K:262))
         /\ (!(0 <= K:262) \/ -mid_z:264 <= -havoc:29)
         /\ ((K:262 = 0 /\ havoc:29 = mid_z:264 /\ havoc:28 = mid_x:263
                /\ 0 = mid___cost:265)
               \/ (1 <= K:262 /\ 0 <= (-1 + -havoc:28 + havoc:30)
                     /\ 0 <= (-mid_x:263 + havoc:30)
                     /\ 0 <= (-1 + mid___cost:265))) /\ K:266 = 0
         /\ mid_z:264 = z':267 /\ mid_x:263 = x':268
         /\ mid___cost:265 = __cost':269 /\ 0 = K:266
         /\ (K:262 + K:266) = K:270 /\ 0 <= K:270 /\ havoc:30 <= x':268
         /\ ((havoc:28 < havoc:30 /\ (havoc:30 + -havoc:28) = phi_tmp___2:280)
               \/ (havoc:30 <= havoc:28 /\ 0 = phi_tmp___2:280))
         /\ ((havoc:29 < havoc:30 /\ (havoc:30 + -havoc:29) = phi_tmp___3:281)
               \/ (havoc:30 <= havoc:29 /\ 0 = phi_tmp___3:281)))}

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

Base relation: 
{__cost := __cost':291
 return := havoc:296
 param0 := param0:100
 param1 := param1:103
 param2 := param2:106
 return@pos := type_err:297
 param0@pos := type_err:113
 param1@pos := type_err:114
 param2@pos := type_err:115
 return@width := type_err:298
 param0@width := type_err:116
 param1@width := type_err:117
 param2@width := type_err:118
 when ((!(0 <= K:284)
          \/ (mid_x:285 + mid_z:286) = ((param0:100 + param1:103) + K:284))
         /\ (!(0 <= K:284) \/ mid___cost:287 = (__cost:133 + K:284))
         /\ (!(0 <= K:284) \/ mid_z:286 <= (param1:103 + K:284))
         /\ (!(0 <= K:284) \/ -mid_z:286 <= -param1:103)
         /\ ((K:284 = 0 /\ param1:103 = mid_z:286 /\ param0:100 = mid_x:285
                /\ __cost:133 = mid___cost:287)
               \/ (1 <= K:284 /\ 0 <= (-1 + -param0:100 + param2:106)
                     /\ 0 <= __cost:133 /\ 0 <= (-mid_x:285 + param2:106)
                     /\ 0 <= (-1 + mid___cost:287))) /\ K:288 = 0
         /\ mid_z:286 = z':289 /\ mid_x:285 = x':290
         /\ mid___cost:287 = __cost':291 /\ 0 = K:288
         /\ (K:284 + K:288) = K:292 /\ 0 <= K:292 /\ param2:106 <= x':290)}

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

Base relation: 
{__cost := __cost':205
 x := x':204
 z := z':203
 n := param2:106
 return := havoc:207
 return@pos := type_err:208
 return@width := type_err:209
 when ((!(0 <= K:198)
          \/ (mid_x:199 + mid_z:200) = ((param0:100 + param1:103) + K:198))
         /\ (!(0 <= K:198) \/ mid___cost:201 = (__cost:133 + K:198))
         /\ (!(0 <= K:198) \/ mid_z:200 <= (param1:103 + K:198))
         /\ (!(0 <= K:198) \/ -mid_z:200 <= -param1:103)
         /\ ((K:198 = 0 /\ param1:103 = mid_z:200 /\ param0:100 = mid_x:199
                /\ __cost:133 = mid___cost:201)
               \/ (1 <= K:198 /\ 0 <= (-1 + -param0:100 + param2:106)
                     /\ 0 <= __cost:133 /\ 0 <= (-mid_x:199 + param2:106)
                     /\ 0 <= (-1 + mid___cost:201))) /\ K:202 = 0
         /\ mid_z:200 = z':203 /\ mid_x:199 = x':204
         /\ mid___cost:201 = __cost':205 /\ 0 = K:202
         /\ (K:198 + K:202) = K:206 /\ 0 <= K:206 /\ param2:106 <= x':204)}

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

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

Variable bounds at line 19 in run

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

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