/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, 27> -> <Unique State Name, 23>	Base relation: 
{__cost := (__cost:96 + 1)
 x := (x:94 + 1)
 when (x:94 < y:95 /\ 0 <= __cost:96 /\ 0 <= (__cost:96 + 1))}	
<Unique State Name, 27> -> <Unique State Name, 38>	Base relation: 
{when y:95 <= x:94}	
<Unique State Name, 69> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 60> -> <Unique State Name, 19>	Base relation: 
{}	
<Unique State Name, 67> -> <Unique State Name, 62 66>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 42> -> <Unique State Name, 38>	Base relation: 
{__cost := (__cost:96 + 1)
 y := (y:95 + 1)
 when (y:95 < x:94 /\ 0 <= __cost:96 /\ 0 <= (__cost:96 + 1))}	
<Unique State Name, 42> -> <Unique State Name, 68>	Base relation: 
{return := havoc:102
 return@pos := type_err:103
 return@width := type_err:104
 when x:94 <= y:95}	
<Unique State Name, 17> -> <Unique State Name, 67>	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, 68> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 72> -> <Unique State Name, 27>	Base relation: 
{}	
<Unique State Name, 19> -> <Unique State Name, 69>	Base relation: 
{return := havoc:56
 return@pos := type_err:59
 return@width := type_err:60}	
<Unique State Name, 71> -> <Unique State Name, 42>	Base relation: 
{}	
<Unique State Name, 66> -> <Unique State Name, 70>	Base relation: 
{return := 0
 return@pos := type_err:29
 return@width := type_err:30
 when ((y:5 < x:4 /\ (x:4 + -y:5) = phi_tmp___1:22)
         \/ (x:4 <= y:5 /\ (y:5 + -x:4) = phi_tmp___1:22))}	
<Unique State Name, 23> -> <Unique State Name, 72>	Base relation: 
{}	
<Unique State Name, 38> -> <Unique State Name, 71>	Base relation: 
{when y:95 <= x:94}	
<Unique State Name, 62> -> <Unique State Name, 61>	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, 56> -> <Unique State Name, 23>	Base relation: 
{x := param0:73
 y := param1:76}	
<Unique State Name, 70> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 61> -> <Unique State Name, 56 60>	Base relation: 
{}	MergeFn[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 := (x:94 + 1)
 when (x:94 < y:95 /\ 0 <= __cost:96 /\ 0 <= (__cost:96 + 1))}
**** alpha hat: 
  {<Split [true
            (x':161) = (1)*(x:94) + 1
           (__cost':160) = (1)*(__cost:96) + 1
           }
          pre:
            [|-x:94+y:95-1>=0; __cost:96>=0|]
          post:
            [|__cost':160-1>=0; y:95-x':161>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':160
   x := x':161
   when ((!(0 <= K:170) \/ mid_x:172 = (x:94 + K:170))
           /\ (!(0 <= K:170) \/ mid___cost:173 = (__cost:96 + K:170))
           /\ ((K:170 = 0 /\ x:94 = mid_x:172 /\ __cost:96 = mid___cost:173)
                 \/ (1 <= K:170 /\ 0 <= (-1 + -x:94 + y:95) /\ 0 <= __cost:96
                       /\ 0 <= (-1 + mid___cost:173)
                       /\ 0 <= (y:95 + -mid_x:172))) /\ K:171 = 0
           /\ mid_x:172 = x':161 /\ mid___cost:173 = __cost':160 /\ 0 = K:171
           /\ (K:170 + K:171) = K:169 /\ 0 <= K:169)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:96 + 1)
 y := (y:95 + 1)
 when (y:95 <= x:94 /\ y:95 < x:94 /\ 0 <= __cost:96 /\ 0 <= (__cost:96 + 1))}
**** alpha hat: 
  {<Split [true
            (y':181) = (1)*(y:95) + 1
           (__cost':160) = (1)*(__cost:96) + 1
           }
          pre:
            [|-y:95+x:94-1>=0; __cost:96>=0|]
          post:
            [|__cost':160-1>=0; x:94-y':181>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':160
   y := y':181
   when ((!(0 <= K:190) \/ mid_y:192 = (y:95 + K:190))
           /\ (!(0 <= K:190) \/ mid___cost:193 = (__cost:96 + K:190))
           /\ ((K:190 = 0 /\ y:95 = mid_y:192 /\ __cost:96 = mid___cost:193)
                 \/ (1 <= K:190 /\ 0 <= (-1 + -y:95 + x:94) /\ 0 <= __cost:96
                       /\ 0 <= (-1 + mid___cost:193)
                       /\ 0 <= (x:94 + -mid_y:192))) /\ K:191 = 0
           /\ mid_y:192 = y':181 /\ mid___cost:193 = __cost':160 /\ 0 = K:191
           /\ (K:190 + K:191) = K:189 /\ 0 <= K:189)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  22  


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:5 < x:4 /\ (x:4 + -y:5) = phi_tmp___1:22)
             \/ (x:4 <= y:5 /\ (y:5 + -x:4) = 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(22)
  )
  ,
  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=22: 
Weight(Base relation: 
  {__cost := __cost':199
   x := x':178
   y := y':198
   return := havoc:201
   return@pos := type_err:202
   return@width := type_err:203
   when ((!(0 <= K:174) \/ mid_x:175 = (param0:73 + K:174))
           /\ (!(0 <= K:174) \/ mid___cost:176 = (__cost:96 + K:174))
           /\ ((K:174 = 0 /\ param0:73 = mid_x:175
                  /\ __cost:96 = mid___cost:176)
                 \/ (1 <= K:174 /\ 0 <= (-1 + -param0:73 + param1:76)
                       /\ 0 <= __cost:96 /\ 0 <= (-1 + mid___cost:176)
                       /\ 0 <= (param1:76 + -mid_x:175))) /\ K:177 = 0
           /\ mid_x:175 = x':178 /\ mid___cost:176 = __cost':179 /\ 0 = K:177
           /\ (K:174 + K:177) = K:180 /\ 0 <= K:180 /\ param1:76 <= x':178
           /\ (!(0 <= K:194) \/ mid_y:195 = (param1:76 + K:194))
           /\ (!(0 <= K:194) \/ mid___cost:196 = (__cost':179 + K:194))
           /\ ((K:194 = 0 /\ param1:76 = mid_y:195
                  /\ __cost':179 = mid___cost:196)
                 \/ (1 <= K:194 /\ 0 <= (-1 + -param1:76 + x':178)
                       /\ 0 <= __cost':179 /\ 0 <= (-1 + mid___cost:196)
                       /\ 0 <= (x':178 + -mid_y:195))) /\ K:197 = 0
           /\ mid_y:195 = y':198 /\ mid___cost:196 = __cost':199 /\ 0 = K:197
           /\ (K:194 + K:197) = K:200 /\ 0 <= K:200 /\ y':198 <= x':178
           /\ x':178 <= y':198)})



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:5 < x:4 /\ (x:4 + -y:5) = phi_tmp___1:22)
               \/ (x:4 <= y:5 /\ (y:5 + -x:4) = 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(22)
    )
    ,
    Weight(Base relation: 
      {return := havoc:56
       return@pos := type_err:59
       return@width := type_err:60}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':199
   return := havoc:201
   return@pos := type_err:202
   return@width := type_err:203
   when ((!(0 <= K:174) \/ mid_x:175 = (param0:73 + K:174))
           /\ (!(0 <= K:174) \/ mid___cost:176 = (__cost:96 + K:174))
           /\ ((K:174 = 0 /\ param0:73 = mid_x:175
                  /\ __cost:96 = mid___cost:176)
                 \/ (1 <= K:174 /\ 0 <= (-1 + -param0:73 + param1:76)
                       /\ 0 <= __cost:96 /\ 0 <= (-1 + mid___cost:176)
                       /\ 0 <= (param1:76 + -mid_x:175))) /\ K:177 = 0
           /\ mid_x:175 = x':178 /\ mid___cost:176 = __cost':179 /\ 0 = K:177
           /\ (K:174 + K:177) = K:180 /\ 0 <= K:180 /\ param1:76 <= x':178
           /\ (!(0 <= K:194) \/ mid_y:195 = (param1:76 + K:194))
           /\ (!(0 <= K:194) \/ mid___cost:196 = (__cost':179 + K:194))
           /\ ((K:194 = 0 /\ param1:76 = mid_y:195
                  /\ __cost':179 = mid___cost:196)
                 \/ (1 <= K:194 /\ 0 <= (-1 + -param1:76 + x':178)
                       /\ 0 <= __cost':179 /\ 0 <= (-1 + mid___cost:196)
                       /\ 0 <= (x':178 + -mid_y:195))) /\ K:197 = 0
           /\ mid_y:195 = y':198 /\ mid___cost:196 = __cost':199 /\ 0 = K:197
           /\ (K:194 + K:197) = K:200 /\ 0 <= K:200 /\ y':198 <= x':178
           /\ x':178 <= y':198)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':236
   return := 0
   param0 := havoc:20
   param1 := havoc:21
   return@pos := type_err:246
   param0@pos := type_err:240
   param1@pos := type_err:241
   return@width := type_err:247
   param0@width := type_err:243
   param1@width := type_err:244
   when ((!(0 <= K:224) \/ mid_x:225 = (havoc:20 + K:224))
           /\ (!(0 <= K:224) \/ mid___cost:226 = K:224)
           /\ ((K:224 = 0 /\ havoc:20 = mid_x:225 /\ 0 = mid___cost:226)
                 \/ (1 <= K:224 /\ 0 <= (-1 + -havoc:20 + havoc:21)
                       /\ 0 <= (-1 + mid___cost:226)
                       /\ 0 <= (havoc:21 + -mid_x:225))) /\ K:227 = 0
           /\ mid_x:225 = x':228 /\ mid___cost:226 = __cost':229 /\ 0 = K:227
           /\ (K:224 + K:227) = K:230 /\ 0 <= K:230 /\ havoc:21 <= x':228
           /\ (!(0 <= K:231) \/ mid_y:232 = (havoc:21 + K:231))
           /\ (!(0 <= K:231) \/ mid___cost:233 = (__cost':229 + K:231))
           /\ ((K:231 = 0 /\ havoc:21 = mid_y:232
                  /\ __cost':229 = mid___cost:233)
                 \/ (1 <= K:231 /\ 0 <= (-1 + -havoc:21 + x':228)
                       /\ 0 <= __cost':229 /\ 0 <= (-1 + mid___cost:233)
                       /\ 0 <= (x':228 + -mid_y:232))) /\ K:234 = 0
           /\ mid_y:232 = y':235 /\ mid___cost:233 = __cost':236 /\ 0 = K:234
           /\ (K:231 + K:234) = K:237 /\ 0 <= K:237 /\ y':235 <= x':228
           /\ x':228 <= y':235
           /\ ((havoc:21 < havoc:20
                  /\ (havoc:20 + -havoc:21) = phi_tmp___1:245)
                 \/ (havoc:20 <= havoc:21
                       /\ (havoc:21 + -havoc:20) = phi_tmp___1:245)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':260
   return := havoc:265
   param0 := param0:73
   param1 := param1:76
   return@pos := type_err:266
   param0@pos := type_err:81
   param1@pos := type_err:82
   return@width := type_err:267
   param0@width := type_err:83
   param1@width := type_err:84
   when ((!(0 <= K:248) \/ mid_x:249 = (param0:73 + K:248))
           /\ (!(0 <= K:248) \/ mid___cost:250 = (__cost:96 + K:248))
           /\ ((K:248 = 0 /\ param0:73 = mid_x:249
                  /\ __cost:96 = mid___cost:250)
                 \/ (1 <= K:248 /\ 0 <= (-1 + -param0:73 + param1:76)
                       /\ 0 <= __cost:96 /\ 0 <= (-1 + mid___cost:250)
                       /\ 0 <= (param1:76 + -mid_x:249))) /\ K:251 = 0
           /\ mid_x:249 = x':252 /\ mid___cost:250 = __cost':253 /\ 0 = K:251
           /\ (K:248 + K:251) = K:254 /\ 0 <= K:254 /\ param1:76 <= x':252
           /\ (!(0 <= K:255) \/ mid_y:256 = (param1:76 + K:255))
           /\ (!(0 <= K:255) \/ mid___cost:257 = (__cost':253 + K:255))
           /\ ((K:255 = 0 /\ param1:76 = mid_y:256
                  /\ __cost':253 = mid___cost:257)
                 \/ (1 <= K:255 /\ 0 <= (-1 + -param1:76 + x':252)
                       /\ 0 <= __cost':253 /\ 0 <= (-1 + mid___cost:257)
                       /\ 0 <= (x':252 + -mid_y:256))) /\ K:258 = 0
           /\ mid_y:256 = y':259 /\ mid___cost:257 = __cost':260 /\ 0 = K:258
           /\ (K:255 + K:258) = K:261 /\ 0 <= K:261 /\ y':259 <= x':252
           /\ x':252 <= y':259)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=22: 
Weight(Base relation: 
  {__cost := __cost':199
   return := havoc:201
   return@pos := type_err:202
   return@width := type_err:203
   when ((!(0 <= K:174) \/ mid_x:175 = (param0:73 + K:174))
           /\ (!(0 <= K:174) \/ mid___cost:176 = (__cost:96 + K:174))
           /\ ((K:174 = 0 /\ param0:73 = mid_x:175
                  /\ __cost:96 = mid___cost:176)
                 \/ (1 <= K:174 /\ 0 <= (-1 + -param0:73 + param1:76)
                       /\ 0 <= __cost:96 /\ 0 <= (-1 + mid___cost:176)
                       /\ 0 <= (param1:76 + -mid_x:175))) /\ K:177 = 0
           /\ mid_x:175 = x':178 /\ mid___cost:176 = __cost':179 /\ 0 = K:177
           /\ (K:174 + K:177) = K:180 /\ 0 <= K:180 /\ param1:76 <= x':178
           /\ (!(0 <= K:194) \/ mid_y:195 = (param1:76 + K:194))
           /\ (!(0 <= K:194) \/ mid___cost:196 = (__cost':179 + K:194))
           /\ ((K:194 = 0 /\ param1:76 = mid_y:195
                  /\ __cost':179 = mid___cost:196)
                 \/ (1 <= K:194 /\ 0 <= (-1 + -param1:76 + x':178)
                       /\ 0 <= __cost':179 /\ 0 <= (-1 + mid___cost:196)
                       /\ 0 <= (x':178 + -mid_y:195))) /\ K:197 = 0
           /\ mid_y:195 = y':198 /\ mid___cost:196 = __cost':199 /\ 0 = K:197
           /\ (K:194 + K:197) = K:200 /\ 0 <= K:200 /\ y':198 <= x':178
           /\ x':178 <= y':198)})


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':236
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:246
 param0@pos := type_err:240
 param1@pos := type_err:241
 return@width := type_err:247
 param0@width := type_err:243
 param1@width := type_err:244
 when ((!(0 <= K:224) \/ mid_x:225 = (havoc:20 + K:224))
         /\ (!(0 <= K:224) \/ mid___cost:226 = K:224)
         /\ ((K:224 = 0 /\ havoc:20 = mid_x:225 /\ 0 = mid___cost:226)
               \/ (1 <= K:224 /\ 0 <= (-1 + -havoc:20 + havoc:21)
                     /\ 0 <= (-1 + mid___cost:226)
                     /\ 0 <= (havoc:21 + -mid_x:225))) /\ K:227 = 0
         /\ mid_x:225 = x':228 /\ mid___cost:226 = __cost':229 /\ 0 = K:227
         /\ (K:224 + K:227) = K:230 /\ 0 <= K:230 /\ havoc:21 <= x':228
         /\ (!(0 <= K:231) \/ mid_y:232 = (havoc:21 + K:231))
         /\ (!(0 <= K:231) \/ mid___cost:233 = (__cost':229 + K:231))
         /\ ((K:231 = 0 /\ havoc:21 = mid_y:232
                /\ __cost':229 = mid___cost:233)
               \/ (1 <= K:231 /\ 0 <= (-1 + -havoc:21 + x':228)
                     /\ 0 <= __cost':229 /\ 0 <= (-1 + mid___cost:233)
                     /\ 0 <= (x':228 + -mid_y:232))) /\ K:234 = 0
         /\ mid_y:232 = y':235 /\ mid___cost:233 = __cost':236 /\ 0 = K:234
         /\ (K:231 + K:234) = K:237 /\ 0 <= K:237 /\ y':235 <= x':228
         /\ x':228 <= y':235
         /\ ((havoc:21 < havoc:20 /\ (havoc:20 + -havoc:21) = phi_tmp___1:245)
               \/ (havoc:20 <= havoc:21
                     /\ (havoc:21 + -havoc:20) = phi_tmp___1:245)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':260
 return := havoc:265
 param0 := param0:73
 param1 := param1:76
 return@pos := type_err:266
 param0@pos := type_err:81
 param1@pos := type_err:82
 return@width := type_err:267
 param0@width := type_err:83
 param1@width := type_err:84
 when ((!(0 <= K:248) \/ mid_x:249 = (param0:73 + K:248))
         /\ (!(0 <= K:248) \/ mid___cost:250 = (__cost:96 + K:248))
         /\ ((K:248 = 0 /\ param0:73 = mid_x:249
                /\ __cost:96 = mid___cost:250)
               \/ (1 <= K:248 /\ 0 <= (-1 + -param0:73 + param1:76)
                     /\ 0 <= __cost:96 /\ 0 <= (-1 + mid___cost:250)
                     /\ 0 <= (param1:76 + -mid_x:249))) /\ K:251 = 0
         /\ mid_x:249 = x':252 /\ mid___cost:250 = __cost':253 /\ 0 = K:251
         /\ (K:248 + K:251) = K:254 /\ 0 <= K:254 /\ param1:76 <= x':252
         /\ (!(0 <= K:255) \/ mid_y:256 = (param1:76 + K:255))
         /\ (!(0 <= K:255) \/ mid___cost:257 = (__cost':253 + K:255))
         /\ ((K:255 = 0 /\ param1:76 = mid_y:256
                /\ __cost':253 = mid___cost:257)
               \/ (1 <= K:255 /\ 0 <= (-1 + -param1:76 + x':252)
                     /\ 0 <= __cost':253 /\ 0 <= (-1 + mid___cost:257)
                     /\ 0 <= (x':252 + -mid_y:256))) /\ K:258 = 0
         /\ mid_y:256 = y':259 /\ mid___cost:257 = __cost':260 /\ 0 = K:258
         /\ (K:255 + K:258) = K:261 /\ 0 <= K:261 /\ y':259 <= x':252
         /\ x':252 <= y':259)}

Evaluating variable number 22 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':199
 return := havoc:201
 return@pos := type_err:202
 return@width := type_err:203
 when ((!(0 <= K:174) \/ mid_x:175 = (param0:73 + K:174))
         /\ (!(0 <= K:174) \/ mid___cost:176 = (__cost:96 + K:174))
         /\ ((K:174 = 0 /\ param0:73 = mid_x:175
                /\ __cost:96 = mid___cost:176)
               \/ (1 <= K:174 /\ 0 <= (-1 + -param0:73 + param1:76)
                     /\ 0 <= __cost:96 /\ 0 <= (-1 + mid___cost:176)
                     /\ 0 <= (param1:76 + -mid_x:175))) /\ K:177 = 0
         /\ mid_x:175 = x':178 /\ mid___cost:176 = __cost':179 /\ 0 = K:177
         /\ (K:174 + K:177) = K:180 /\ 0 <= K:180 /\ param1:76 <= x':178
         /\ (!(0 <= K:194) \/ mid_y:195 = (param1:76 + K:194))
         /\ (!(0 <= K:194) \/ mid___cost:196 = (__cost':179 + K:194))
         /\ ((K:194 = 0 /\ param1:76 = mid_y:195
                /\ __cost':179 = mid___cost:196)
               \/ (1 <= K:194 /\ 0 <= (-1 + -param1:76 + x':178)
                     /\ 0 <= __cost':179 /\ 0 <= (-1 + mid___cost:196)
                     /\ 0 <= (x':178 + -mid_y:195))) /\ K:197 = 0
         /\ mid_y:195 = y':198 /\ mid___cost:196 = __cost':199 /\ 0 = K:197
         /\ (K:194 + K:197) = K:200 /\ 0 <= K:200 /\ y':198 <= x':178
         /\ x':178 <= y':198)}

    (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,56)_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,62)_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: 
__pstate 0x10a2e00: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x10d2050: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
##### ANS
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}
    ( __pstate , (Unique State Name,56)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:20
 y := havoc:21
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:312
 param1@pos := type_err:313
 param0@width := type_err:314
 param1@width := type_err:315}
    ( __pstate , (Unique State Name,62)_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: 
__pstate 0x3292890: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x3284ef0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
================================================
Procedure Summaries

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

Base relation: 
{__cost := __cost':280
 x := havoc:20
 y := havoc:21
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:290
 param0@pos := type_err:284
 param1@pos := type_err:285
 return@width := type_err:291
 param0@width := type_err:287
 param1@width := type_err:288
 when ((!(0 <= K:268) \/ mid_x:269 = (havoc:20 + K:268))
         /\ (!(0 <= K:268) \/ mid___cost:270 = K:268)
         /\ ((K:268 = 0 /\ havoc:20 = mid_x:269 /\ 0 = mid___cost:270)
               \/ (1 <= K:268 /\ 0 <= (-1 + -havoc:20 + havoc:21)
                     /\ 0 <= (-1 + mid___cost:270)
                     /\ 0 <= (havoc:21 + -mid_x:269))) /\ K:271 = 0
         /\ mid_x:269 = x':272 /\ mid___cost:270 = __cost':273 /\ 0 = K:271
         /\ (K:268 + K:271) = K:274 /\ 0 <= K:274 /\ havoc:21 <= x':272
         /\ (!(0 <= K:275) \/ mid_y:276 = (havoc:21 + K:275))
         /\ (!(0 <= K:275) \/ mid___cost:277 = (__cost':273 + K:275))
         /\ ((K:275 = 0 /\ havoc:21 = mid_y:276
                /\ __cost':273 = mid___cost:277)
               \/ (1 <= K:275 /\ 0 <= (-1 + -havoc:21 + x':272)
                     /\ 0 <= __cost':273 /\ 0 <= (-1 + mid___cost:277)
                     /\ 0 <= (x':272 + -mid_y:276))) /\ K:278 = 0
         /\ mid_y:276 = y':279 /\ mid___cost:277 = __cost':280 /\ 0 = K:278
         /\ (K:275 + K:278) = K:281 /\ 0 <= K:281 /\ y':279 <= x':272
         /\ x':272 <= y':279
         /\ ((havoc:21 < havoc:20 /\ (havoc:20 + -havoc:21) = phi_tmp___1:289)
               \/ (havoc:20 <= havoc:21
                     /\ (havoc:21 + -havoc:20) = phi_tmp___1:289)))}

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

Base relation: 
{__cost := __cost':304
 return := havoc:309
 param0 := param0:73
 param1 := param1:76
 return@pos := type_err:310
 param0@pos := type_err:81
 param1@pos := type_err:82
 return@width := type_err:311
 param0@width := type_err:83
 param1@width := type_err:84
 when ((!(0 <= K:292) \/ mid_x:293 = (param0:73 + K:292))
         /\ (!(0 <= K:292) \/ mid___cost:294 = (__cost:96 + K:292))
         /\ ((K:292 = 0 /\ param0:73 = mid_x:293
                /\ __cost:96 = mid___cost:294)
               \/ (1 <= K:292 /\ 0 <= (-1 + -param0:73 + param1:76)
                     /\ 0 <= __cost:96 /\ 0 <= (-1 + mid___cost:294)
                     /\ 0 <= (param1:76 + -mid_x:293))) /\ K:295 = 0
         /\ mid_x:293 = x':296 /\ mid___cost:294 = __cost':297 /\ 0 = K:295
         /\ (K:292 + K:295) = K:298 /\ 0 <= K:298 /\ param1:76 <= x':296
         /\ (!(0 <= K:299) \/ mid_y:300 = (param1:76 + K:299))
         /\ (!(0 <= K:299) \/ mid___cost:301 = (__cost':297 + K:299))
         /\ ((K:299 = 0 /\ param1:76 = mid_y:300
                /\ __cost':297 = mid___cost:301)
               \/ (1 <= K:299 /\ 0 <= (-1 + -param1:76 + x':296)
                     /\ 0 <= __cost':297 /\ 0 <= (-1 + mid___cost:301)
                     /\ 0 <= (x':296 + -mid_y:300))) /\ K:302 = 0
         /\ mid_y:300 = y':303 /\ mid___cost:301 = __cost':304 /\ 0 = K:302
         /\ (K:299 + K:302) = K:305 /\ 0 <= K:305 /\ y':303 <= x':296
         /\ x':296 <= y':303)}

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

Base relation: 
{__cost := __cost':199
 x := x':178
 y := y':198
 return := havoc:201
 return@pos := type_err:202
 return@width := type_err:203
 when ((!(0 <= K:174) \/ mid_x:175 = (param0:73 + K:174))
         /\ (!(0 <= K:174) \/ mid___cost:176 = (__cost:96 + K:174))
         /\ ((K:174 = 0 /\ param0:73 = mid_x:175
                /\ __cost:96 = mid___cost:176)
               \/ (1 <= K:174 /\ 0 <= (-1 + -param0:73 + param1:76)
                     /\ 0 <= __cost:96 /\ 0 <= (-1 + mid___cost:176)
                     /\ 0 <= (param1:76 + -mid_x:175))) /\ K:177 = 0
         /\ mid_x:175 = x':178 /\ mid___cost:176 = __cost':179 /\ 0 = K:177
         /\ (K:174 + K:177) = K:180 /\ 0 <= K:180 /\ param1:76 <= x':178
         /\ (!(0 <= K:194) \/ mid_y:195 = (param1:76 + K:194))
         /\ (!(0 <= K:194) \/ mid___cost:196 = (__cost':179 + K:194))
         /\ ((K:194 = 0 /\ param1:76 = mid_y:195
                /\ __cost':179 = mid___cost:196)
               \/ (1 <= K:194 /\ 0 <= (-1 + -param1:76 + x':178)
                     /\ 0 <= __cost':179 /\ 0 <= (-1 + mid___cost:196)
                     /\ 0 <= (x':178 + -mid_y:195))) /\ K:197 = 0
         /\ mid_y:195 = y':198 /\ mid___cost:196 = __cost':199 /\ 0 = K:197
         /\ (K:194 + K:197) = K:200 /\ 0 <= K:200 /\ y':198 <= x':178
         /\ x':178 <= y':198)}

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

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

Variable bounds at line 20 in run

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

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