/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, 61> -> <Unique State Name, 56 60>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 23> -> <Unique State Name, 61>	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}	
<Unique State Name, 64> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 50> -> <Unique State Name, 29>	Base relation: 
{x := param0:80
 y := param1:83}	
<Unique State Name, 29> -> <Unique State Name, 65>	Base relation: 
{}	
<Unique State Name, 54> -> <Unique State Name, 25>	Base relation: 
{}	
<Unique State Name, 62> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 55> -> <Unique State Name, 50 54>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 65> -> <Unique State Name, 33>	Base relation: 
{}	
<Unique State Name, 25> -> <Unique State Name, 63>	Base relation: 
{return := havoc:63
 return@pos := type_err:66
 return@width := type_err:67}	
<Unique State Name, 56> -> <Unique State Name, 55>	Base relation: 
{param0 := param0:80
 param1 := param1:83
 param0@pos := type_err:88
 param1@pos := type_err:89
 param0@width := type_err:90
 param1@width := type_err:91}	
<Unique State Name, 60> -> <Unique State Name, 64>	Base relation: 
{return := 0
 return@pos := type_err:32
 return@width := type_err:33
 when (((0 < x:4 /\ x:4 = phi_tmp___1:23) \/ (x:4 <= 0 /\ 0 = phi_tmp___1:23))
         /\ ((0 < y:5 /\ y:5 = phi_tmp___2:31)
               \/ (y:5 <= 0 /\ 0 = phi_tmp___2:31)))}	
<Unique State Name, 33> -> <Unique State Name, 29>	Base relation: 
{__cost := (__cost:102 + 1)
 x := y:103
 y := (x:101 + -1)
 when (0 < x:101 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}	
<Unique State Name, 33> -> <Unique State Name, 62>	Base relation: 
{return := havoc:110
 return@pos := type_err:111
 return@width := type_err:112
 when x:101 <= 0}	
<Unique State Name, 63> -> <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:102 + 1)
 x := y:103
 y := (x:101 + -1)
 when (0 < x:101 /\ 0 <= __cost:102 /\ 0 <= (__cost:102 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':134) = (1)*(__cost:102) + 1
           (x':135) = (1)*(y:103) + 0
           (y':136) = (1)*(x:101) + (-1)*1
           }
          pre:
            [|__cost:102>=0; x:101-1>=0|]
          post:
            [|y':136>=0; __cost':134-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':134
   x := x':135
   y := y':136
   when ((!(0 <= K:147) \/ mid___cost:151 = (__cost:102 + K:147))
           /\ (!(0 <= K:147)
                 \/ mid_x:150 = (1/4 + (1/2 * x:101) + (1/2 * y:103)
                                   + (-1/4 * ite((K:147 mod 2) = 0, 1, -1))
                                   + (1/2 * x:101
                                        * ite((K:147 mod 2) = 0, 1, -1))
                                   + (-1/2 * y:103
                                        * ite((K:147 mod 2) = 0, 1, -1))
                                   + (-1/2 * K:147)))
           /\ (!(0 <= K:147)
                 \/ mid_y:149 = (-1/4 + y:103 + (1/2 * x:101)
                                   + (-1/2 * y:103)
                                   + (1/4 * ite((K:147 mod 2) = 0, 1, -1))
                                   + (-1/2 * x:101
                                        * ite((K:147 mod 2) = 0, 1, -1))
                                   + (1/2 * y:103
                                        * ite((K:147 mod 2) = 0, 1, -1))
                                   + (-1/2 * K:147)))
           /\ ((K:147 = 0 /\ y:103 = mid_y:149 /\ x:101 = mid_x:150
                  /\ __cost:102 = mid___cost:151)
                 \/ (1 <= K:147 /\ 0 <= __cost:102 /\ 0 <= (-1 + x:101)
                       /\ 0 <= mid_y:149 /\ 0 <= (-1 + mid___cost:151)))
           /\ K:148 = 0 /\ mid_y:149 = y':136 /\ mid_x:150 = x':135
           /\ mid___cost:151 = __cost':134 /\ 0 = K:148
           /\ (K:147 + K:148) = K:146 /\ 0 <= K:146)}
}
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:21
       y := havoc:22
       param0 := havoc:21
       param1 := havoc:22
       param0@pos := type_err:27
       param1@pos := type_err:29
       param0@width := type_err:28
       param1@width := type_err:30}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:32
     return@width := type_err:33
     when (((0 < x:4 /\ x:4 = phi_tmp___1:23)
              \/ (x:4 <= 0 /\ 0 = phi_tmp___1:23))
             /\ ((0 < y:5 /\ y:5 = phi_tmp___2:31)
                   \/ (y:5 <= 0 /\ 0 = phi_tmp___2:31)))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:80
       param1 := param1:83
       param0@pos := type_err:88
       param1@pos := type_err:89
       param0@width := type_err:90
       param1@width := type_err:91}    )
    ,
    Var(19)
  )
  ,
  Weight(Base relation: 
    {return := havoc:63
     return@pos := type_err:66
     return@width := type_err:67}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=19: 
Weight(Base relation: 
  {__cost := __cost':159
   x := x':158
   y := y':157
   return := havoc:161
   return@pos := type_err:162
   return@width := type_err:163
   when ((!(0 <= K:152) \/ mid___cost:153 = (__cost:102 + K:152))
           /\ (!(0 <= K:152)
                 \/ mid_x:154 = (1/4 + (1/2 * param0:80) + (1/2 * param1:83)
                                   + (-1/4 * ite((K:152 mod 2) = 0, 1, -1))
                                   + (1/2 * param0:80
                                        * ite((K:152 mod 2) = 0, 1, -1))
                                   + (-1/2 * param1:83
                                        * ite((K:152 mod 2) = 0, 1, -1))
                                   + (-1/2 * K:152)))
           /\ (!(0 <= K:152)
                 \/ mid_y:155 = (-1/4 + param1:83 + (1/2 * param0:80)
                                   + (-1/2 * param1:83)
                                   + (1/4 * ite((K:152 mod 2) = 0, 1, -1))
                                   + (-1/2 * param0:80
                                        * ite((K:152 mod 2) = 0, 1, -1))
                                   + (1/2 * param1:83
                                        * ite((K:152 mod 2) = 0, 1, -1))
                                   + (-1/2 * K:152)))
           /\ ((K:152 = 0 /\ param1:83 = mid_y:155 /\ param0:80 = mid_x:154
                  /\ __cost:102 = mid___cost:153)
                 \/ (1 <= K:152 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                       /\ 0 <= mid_y:155 /\ 0 <= (-1 + mid___cost:153)))
           /\ K:156 = 0 /\ mid_y:155 = y':157 /\ mid_x:154 = x':158
           /\ mid___cost:153 = __cost':159 /\ 0 = K:156
           /\ (K:152 + K:156) = K:160 /\ 0 <= K:160 /\ x':158 <= 0)})



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



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:80
         param1 := param1:83
         param0@pos := type_err:88
         param1@pos := type_err:89
         param0@width := type_err:90
         param1@width := type_err:91}      )
      ,
      Var(19)
    )
    ,
    Weight(Base relation: 
      {return := havoc:63
       return@pos := type_err:66
       return@width := type_err:67}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':159
   return := havoc:161
   return@pos := type_err:162
   return@width := type_err:163
   when ((!(0 <= K:152) \/ mid___cost:153 = (__cost:102 + K:152))
           /\ (!(0 <= K:152)
                 \/ mid_x:154 = (1/4 + (1/2 * param0:80) + (1/2 * param1:83)
                                   + (-1/4 * ite((K:152 mod 2) = 0, 1, -1))
                                   + (1/2 * param0:80
                                        * ite((K:152 mod 2) = 0, 1, -1))
                                   + (-1/2 * param1:83
                                        * ite((K:152 mod 2) = 0, 1, -1))
                                   + (-1/2 * K:152)))
           /\ (!(0 <= K:152)
                 \/ mid_y:155 = (-1/4 + param1:83 + (1/2 * param0:80)
                                   + (-1/2 * param1:83)
                                   + (1/4 * ite((K:152 mod 2) = 0, 1, -1))
                                   + (-1/2 * param0:80
                                        * ite((K:152 mod 2) = 0, 1, -1))
                                   + (1/2 * param1:83
                                        * ite((K:152 mod 2) = 0, 1, -1))
                                   + (-1/2 * K:152)))
           /\ ((K:152 = 0 /\ param1:83 = mid_y:155 /\ param0:80 = mid_x:154
                  /\ __cost:102 = mid___cost:153)
                 \/ (1 <= K:152 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                       /\ 0 <= mid_y:155 /\ 0 <= (-1 + mid___cost:153)))
           /\ K:156 = 0 /\ mid_y:155 = y':157 /\ mid_x:154 = x':158
           /\ mid___cost:153 = __cost':159 /\ 0 = K:156
           /\ (K:152 + K:156) = K:160 /\ 0 <= K:160 /\ x':158 <= 0)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':186
   return := 0
   param0 := havoc:21
   param1 := havoc:22
   return@pos := type_err:197
   param0@pos := type_err:190
   param1@pos := type_err:191
   return@width := type_err:198
   param0@width := type_err:193
   param1@width := type_err:194
   when ((!(0 <= K:179) \/ mid___cost:180 = K:179)
           /\ (!(0 <= K:179)
                 \/ mid_x:181 = (1/4 + (1/2 * havoc:21) + (1/2 * havoc:22)
                                   + (-1/4 * ite((K:179 mod 2) = 0, 1, -1))
                                   + (1/2 * havoc:21
                                        * ite((K:179 mod 2) = 0, 1, -1))
                                   + (-1/2 * havoc:22
                                        * ite((K:179 mod 2) = 0, 1, -1))
                                   + (-1/2 * K:179)))
           /\ (!(0 <= K:179)
                 \/ mid_y:182 = (-1/4 + havoc:22 + (1/2 * havoc:21)
                                   + (-1/2 * havoc:22)
                                   + (1/4 * ite((K:179 mod 2) = 0, 1, -1))
                                   + (-1/2 * havoc:21
                                        * ite((K:179 mod 2) = 0, 1, -1))
                                   + (1/2 * havoc:22
                                        * ite((K:179 mod 2) = 0, 1, -1))
                                   + (-1/2 * K:179)))
           /\ ((K:179 = 0 /\ havoc:22 = mid_y:182 /\ havoc:21 = mid_x:181
                  /\ 0 = mid___cost:180)
                 \/ (1 <= K:179 /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_y:182
                       /\ 0 <= (-1 + mid___cost:180))) /\ K:183 = 0
           /\ mid_y:182 = y':184 /\ mid_x:181 = x':185
           /\ mid___cost:180 = __cost':186 /\ 0 = K:183
           /\ (K:179 + K:183) = K:187 /\ 0 <= K:187 /\ x':185 <= 0
           /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:195)
                 \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:195))
           /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:196)
                 \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:196)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':206
   return := havoc:211
   param0 := param0:80
   param1 := param1:83
   return@pos := type_err:212
   param0@pos := type_err:88
   param1@pos := type_err:89
   return@width := type_err:213
   param0@width := type_err:90
   param1@width := type_err:91
   when ((!(0 <= K:199) \/ mid___cost:200 = (__cost:102 + K:199))
           /\ (!(0 <= K:199)
                 \/ mid_x:201 = (1/4 + (1/2 * param0:80) + (1/2 * param1:83)
                                   + (-1/4 * ite((K:199 mod 2) = 0, 1, -1))
                                   + (1/2 * param0:80
                                        * ite((K:199 mod 2) = 0, 1, -1))
                                   + (-1/2 * param1:83
                                        * ite((K:199 mod 2) = 0, 1, -1))
                                   + (-1/2 * K:199)))
           /\ (!(0 <= K:199)
                 \/ mid_y:202 = (-1/4 + param1:83 + (1/2 * param0:80)
                                   + (-1/2 * param1:83)
                                   + (1/4 * ite((K:199 mod 2) = 0, 1, -1))
                                   + (-1/2 * param0:80
                                        * ite((K:199 mod 2) = 0, 1, -1))
                                   + (1/2 * param1:83
                                        * ite((K:199 mod 2) = 0, 1, -1))
                                   + (-1/2 * K:199)))
           /\ ((K:199 = 0 /\ param1:83 = mid_y:202 /\ param0:80 = mid_x:201
                  /\ __cost:102 = mid___cost:200)
                 \/ (1 <= K:199 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                       /\ 0 <= mid_y:202 /\ 0 <= (-1 + mid___cost:200)))
           /\ K:203 = 0 /\ mid_y:202 = y':204 /\ mid_x:201 = x':205
           /\ mid___cost:200 = __cost':206 /\ 0 = K:203
           /\ (K:199 + K:203) = K:207 /\ 0 <= K:207 /\ x':205 <= 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=19: 
Weight(Base relation: 
  {__cost := __cost':159
   return := havoc:161
   return@pos := type_err:162
   return@width := type_err:163
   when ((!(0 <= K:152) \/ mid___cost:153 = (__cost:102 + K:152))
           /\ (!(0 <= K:152)
                 \/ mid_x:154 = (1/4 + (1/2 * param0:80) + (1/2 * param1:83)
                                   + (-1/4 * ite((K:152 mod 2) = 0, 1, -1))
                                   + (1/2 * param0:80
                                        * ite((K:152 mod 2) = 0, 1, -1))
                                   + (-1/2 * param1:83
                                        * ite((K:152 mod 2) = 0, 1, -1))
                                   + (-1/2 * K:152)))
           /\ (!(0 <= K:152)
                 \/ mid_y:155 = (-1/4 + param1:83 + (1/2 * param0:80)
                                   + (-1/2 * param1:83)
                                   + (1/4 * ite((K:152 mod 2) = 0, 1, -1))
                                   + (-1/2 * param0:80
                                        * ite((K:152 mod 2) = 0, 1, -1))
                                   + (1/2 * param1:83
                                        * ite((K:152 mod 2) = 0, 1, -1))
                                   + (-1/2 * K:152)))
           /\ ((K:152 = 0 /\ param1:83 = mid_y:155 /\ param0:80 = mid_x:154
                  /\ __cost:102 = mid___cost:153)
                 \/ (1 <= K:152 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                       /\ 0 <= mid_y:155 /\ 0 <= (-1 + mid___cost:153)))
           /\ K:156 = 0 /\ mid_y:155 = y':157 /\ mid_x:154 = x':158
           /\ mid___cost:153 = __cost':159 /\ 0 = K:156
           /\ (K:152 + K:156) = K:160 /\ 0 <= K:160 /\ x':158 <= 0)})


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':186
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:197
 param0@pos := type_err:190
 param1@pos := type_err:191
 return@width := type_err:198
 param0@width := type_err:193
 param1@width := type_err:194
 when ((!(0 <= K:179) \/ mid___cost:180 = K:179)
         /\ (!(0 <= K:179)
               \/ mid_x:181 = (1/4 + (1/2 * havoc:21) + (1/2 * havoc:22)
                                 + (-1/4 * ite((K:179 mod 2) = 0, 1, -1))
                                 + (1/2 * havoc:21
                                      * ite((K:179 mod 2) = 0, 1, -1))
                                 + (-1/2 * havoc:22
                                      * ite((K:179 mod 2) = 0, 1, -1))
                                 + (-1/2 * K:179)))
         /\ (!(0 <= K:179)
               \/ mid_y:182 = (-1/4 + havoc:22 + (1/2 * havoc:21)
                                 + (-1/2 * havoc:22)
                                 + (1/4 * ite((K:179 mod 2) = 0, 1, -1))
                                 + (-1/2 * havoc:21
                                      * ite((K:179 mod 2) = 0, 1, -1))
                                 + (1/2 * havoc:22
                                      * ite((K:179 mod 2) = 0, 1, -1))
                                 + (-1/2 * K:179)))
         /\ ((K:179 = 0 /\ havoc:22 = mid_y:182 /\ havoc:21 = mid_x:181
                /\ 0 = mid___cost:180)
               \/ (1 <= K:179 /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_y:182
                     /\ 0 <= (-1 + mid___cost:180))) /\ K:183 = 0
         /\ mid_y:182 = y':184 /\ mid_x:181 = x':185
         /\ mid___cost:180 = __cost':186 /\ 0 = K:183
         /\ (K:179 + K:183) = K:187 /\ 0 <= K:187 /\ x':185 <= 0
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:195)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:195))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:196)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:196)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':206
 return := havoc:211
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:212
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:213
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:199) \/ mid___cost:200 = (__cost:102 + K:199))
         /\ (!(0 <= K:199)
               \/ mid_x:201 = (1/4 + (1/2 * param0:80) + (1/2 * param1:83)
                                 + (-1/4 * ite((K:199 mod 2) = 0, 1, -1))
                                 + (1/2 * param0:80
                                      * ite((K:199 mod 2) = 0, 1, -1))
                                 + (-1/2 * param1:83
                                      * ite((K:199 mod 2) = 0, 1, -1))
                                 + (-1/2 * K:199)))
         /\ (!(0 <= K:199)
               \/ mid_y:202 = (-1/4 + param1:83 + (1/2 * param0:80)
                                 + (-1/2 * param1:83)
                                 + (1/4 * ite((K:199 mod 2) = 0, 1, -1))
                                 + (-1/2 * param0:80
                                      * ite((K:199 mod 2) = 0, 1, -1))
                                 + (1/2 * param1:83
                                      * ite((K:199 mod 2) = 0, 1, -1))
                                 + (-1/2 * K:199)))
         /\ ((K:199 = 0 /\ param1:83 = mid_y:202 /\ param0:80 = mid_x:201
                /\ __cost:102 = mid___cost:200)
               \/ (1 <= K:199 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= mid_y:202 /\ 0 <= (-1 + mid___cost:200)))
         /\ K:203 = 0 /\ mid_y:202 = y':204 /\ mid_x:201 = x':205
         /\ mid___cost:200 = __cost':206 /\ 0 = K:203
         /\ (K:199 + K:203) = K:207 /\ 0 <= K:207 /\ x':205 <= 0)}

Evaluating variable number 19 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':159
 return := havoc:161
 return@pos := type_err:162
 return@width := type_err:163
 when ((!(0 <= K:152) \/ mid___cost:153 = (__cost:102 + K:152))
         /\ (!(0 <= K:152)
               \/ mid_x:154 = (1/4 + (1/2 * param0:80) + (1/2 * param1:83)
                                 + (-1/4 * ite((K:152 mod 2) = 0, 1, -1))
                                 + (1/2 * param0:80
                                      * ite((K:152 mod 2) = 0, 1, -1))
                                 + (-1/2 * param1:83
                                      * ite((K:152 mod 2) = 0, 1, -1))
                                 + (-1/2 * K:152)))
         /\ (!(0 <= K:152)
               \/ mid_y:155 = (-1/4 + param1:83 + (1/2 * param0:80)
                                 + (-1/2 * param1:83)
                                 + (1/4 * ite((K:152 mod 2) = 0, 1, -1))
                                 + (-1/2 * param0:80
                                      * ite((K:152 mod 2) = 0, 1, -1))
                                 + (1/2 * param1:83
                                      * ite((K:152 mod 2) = 0, 1, -1))
                                 + (-1/2 * K:152)))
         /\ ((K:152 = 0 /\ param1:83 = mid_y:155 /\ param0:80 = mid_x:154
                /\ __cost:102 = mid___cost:153)
               \/ (1 <= K:152 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= mid_y:155 /\ 0 <= (-1 + mid___cost:153)))
         /\ K:156 = 0 /\ mid_y:155 = y':157 /\ mid_x:154 = x':158
         /\ mid___cost:153 = __cost':159 /\ 0 = K:156
         /\ (K:152 + K:156) = K:160 /\ 0 <= K:160 /\ x':158 <= 0)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,56)_g1> -> <__pstate, (Unique State Name,50)_g1>	Base relation: 
{param0 := param0:80
 param1 := param1:83
 param0@pos := type_err:88
 param1@pos := type_err:89
 param0@width := type_err:90
 param1@width := type_err:91}	
<__pstate, accept> -> <__pstate, (Unique State Name,56)_g1>	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x2aa5c40: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x325a3b0: 
	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,50)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:249
 param1@pos := type_err:250
 param0@width := type_err:251
 param1@width := type_err:252}
    ( __pstate , (Unique State Name,56)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}

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

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

Base relation: 
{__cost := __cost':221
 x := havoc:21
 y := havoc:22
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:232
 param0@pos := type_err:225
 param1@pos := type_err:226
 return@width := type_err:233
 param0@width := type_err:228
 param1@width := type_err:229
 when ((!(0 <= K:214) \/ mid___cost:215 = K:214)
         /\ (!(0 <= K:214)
               \/ mid_x:216 = (1/4 + (1/2 * havoc:21) + (1/2 * havoc:22)
                                 + (-1/4 * ite((K:214 mod 2) = 0, 1, -1))
                                 + (1/2 * havoc:21
                                      * ite((K:214 mod 2) = 0, 1, -1))
                                 + (-1/2 * havoc:22
                                      * ite((K:214 mod 2) = 0, 1, -1))
                                 + (-1/2 * K:214)))
         /\ (!(0 <= K:214)
               \/ mid_y:217 = (-1/4 + havoc:22 + (1/2 * havoc:21)
                                 + (-1/2 * havoc:22)
                                 + (1/4 * ite((K:214 mod 2) = 0, 1, -1))
                                 + (-1/2 * havoc:21
                                      * ite((K:214 mod 2) = 0, 1, -1))
                                 + (1/2 * havoc:22
                                      * ite((K:214 mod 2) = 0, 1, -1))
                                 + (-1/2 * K:214)))
         /\ ((K:214 = 0 /\ havoc:22 = mid_y:217 /\ havoc:21 = mid_x:216
                /\ 0 = mid___cost:215)
               \/ (1 <= K:214 /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_y:217
                     /\ 0 <= (-1 + mid___cost:215))) /\ K:218 = 0
         /\ mid_y:217 = y':219 /\ mid_x:216 = x':220
         /\ mid___cost:215 = __cost':221 /\ 0 = K:218
         /\ (K:214 + K:218) = K:222 /\ 0 <= K:222 /\ x':220 <= 0
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:230)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:230))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:231)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:231)))}

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

Base relation: 
{__cost := __cost':241
 return := havoc:246
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:247
 param0@pos := type_err:88
 param1@pos := type_err:89
 return@width := type_err:248
 param0@width := type_err:90
 param1@width := type_err:91
 when ((!(0 <= K:234) \/ mid___cost:235 = (__cost:102 + K:234))
         /\ (!(0 <= K:234)
               \/ mid_x:236 = (1/4 + (1/2 * param0:80) + (1/2 * param1:83)
                                 + (-1/4 * ite((K:234 mod 2) = 0, 1, -1))
                                 + (1/2 * param0:80
                                      * ite((K:234 mod 2) = 0, 1, -1))
                                 + (-1/2 * param1:83
                                      * ite((K:234 mod 2) = 0, 1, -1))
                                 + (-1/2 * K:234)))
         /\ (!(0 <= K:234)
               \/ mid_y:237 = (-1/4 + param1:83 + (1/2 * param0:80)
                                 + (-1/2 * param1:83)
                                 + (1/4 * ite((K:234 mod 2) = 0, 1, -1))
                                 + (-1/2 * param0:80
                                      * ite((K:234 mod 2) = 0, 1, -1))
                                 + (1/2 * param1:83
                                      * ite((K:234 mod 2) = 0, 1, -1))
                                 + (-1/2 * K:234)))
         /\ ((K:234 = 0 /\ param1:83 = mid_y:237 /\ param0:80 = mid_x:236
                /\ __cost:102 = mid___cost:235)
               \/ (1 <= K:234 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= mid_y:237 /\ 0 <= (-1 + mid___cost:235)))
         /\ K:238 = 0 /\ mid_y:237 = y':239 /\ mid_x:236 = x':240
         /\ mid___cost:235 = __cost':241 /\ 0 = K:238
         /\ (K:234 + K:238) = K:242 /\ 0 <= K:242 /\ x':240 <= 0)}

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

Base relation: 
{__cost := __cost':159
 x := x':158
 y := y':157
 return := havoc:161
 return@pos := type_err:162
 return@width := type_err:163
 when ((!(0 <= K:152) \/ mid___cost:153 = (__cost:102 + K:152))
         /\ (!(0 <= K:152)
               \/ mid_x:154 = (1/4 + (1/2 * param0:80) + (1/2 * param1:83)
                                 + (-1/4 * ite((K:152 mod 2) = 0, 1, -1))
                                 + (1/2 * param0:80
                                      * ite((K:152 mod 2) = 0, 1, -1))
                                 + (-1/2 * param1:83
                                      * ite((K:152 mod 2) = 0, 1, -1))
                                 + (-1/2 * K:152)))
         /\ (!(0 <= K:152)
               \/ mid_y:155 = (-1/4 + param1:83 + (1/2 * param0:80)
                                 + (-1/2 * param1:83)
                                 + (1/4 * ite((K:152 mod 2) = 0, 1, -1))
                                 + (-1/2 * param0:80
                                      * ite((K:152 mod 2) = 0, 1, -1))
                                 + (1/2 * param1:83
                                      * ite((K:152 mod 2) = 0, 1, -1))
                                 + (-1/2 * K:152)))
         /\ ((K:152 = 0 /\ param1:83 = mid_y:155 /\ param0:80 = mid_x:154
                /\ __cost:102 = mid___cost:153)
               \/ (1 <= K:152 /\ 0 <= __cost:102 /\ 0 <= (-1 + param0:80)
                     /\ 0 <= mid_y:155 /\ 0 <= (-1 + mid___cost:153)))
         /\ K:156 = 0 /\ mid_y:155 = y':157 /\ mid_x:154 = x':158
         /\ mid___cost:153 = __cost':159 /\ 0 = K:156
         /\ (K:152 + K:156) = K:160 /\ 0 <= K:160 /\ x':158 <= 0)}

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

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

Variable bounds at line 19 in run

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

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