/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, 45>	Base relation: 
{}	
<Unique State Name, 25> -> <Unique State Name, 80>	Base relation: 
{return := 0
 return@pos := type_err:84
 return@width := type_err:85}	
<Unique State Name, 23> -> <Unique State Name, 78>	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, 33> -> <Unique State Name, 41>	Base relation: 
{when 0 < x:104}	
<Unique State Name, 33> -> <Unique State Name, 65>	Base relation: 
{__retres3 := y:103
 when x:104 <= 0}	
<Unique State Name, 79> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 77> -> <Unique State Name, 81>	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, 73> -> <Unique State Name, 72>	Base relation: 
{param0 := param0:80
 param1 := param1:83
 param0@pos := type_err:90
 param1@pos := type_err:91
 param0@width := type_err:92
 param1@width := type_err:93}	
<Unique State Name, 81> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 71> -> <Unique State Name, 25>	Base relation: 
{}	
<Unique State Name, 82> -> <Unique State Name, 57>	Base relation: 
{__cost := (__cost:105 + 1)
 when (0 <= __cost:105 /\ 0 <= (__cost:105 + 1))}	
<Unique State Name, 57> -> <Unique State Name, 52>	Base relation: 
{when x:104 <= y:103}	
<Unique State Name, 57> -> <Unique State Name, 58>	Base relation: 
{x := (x:104 + -y:103)
 when y:103 < x:104}	
<Unique State Name, 80> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 52> -> <Unique State Name, 58>	Base relation: 
{y := (y:103 + -x:104)
 when x:104 < y:103}	
<Unique State Name, 52> -> <Unique State Name, 65>	Base relation: 
{__retres3 := x:104
 when y:103 <= x:104}	
<Unique State Name, 72> -> <Unique State Name, 67 71>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 67> -> <Unique State Name, 33>	Base relation: 
{x := param0:80
 y := param1:83}	
<Unique State Name, 41> -> <Unique State Name, 45>	Base relation: 
{when 0 < y:103}	
<Unique State Name, 41> -> <Unique State Name, 65>	Base relation: 
{__retres3 := x:104
 when y:103 <= 0}	
<Unique State Name, 78> -> <Unique State Name, 73 77>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 45> -> <Unique State Name, 82>	Base relation: 
{when (1 <= y:103 /\ 1 <= x:104 /\ 0 < x:104 /\ 0 < y:103)}	
<Unique State Name, 65> -> <Unique State Name, 79>	Base relation: 
{return := __retres3:106
 return@pos := type_err:109
 return@width := type_err:110}	
#################################################################
           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:105 + 1)
 x := phi_x:213
 y := phi_y:214
 when (1 <= y:103 /\ 1 <= x:104 /\ 0 < x:104 /\ 0 < y:103 /\ 0 <= __cost:105
         /\ 0 <= (__cost:105 + 1)
         /\ ((y:103 < x:104 /\ (x:104 + -y:103) = phi_x:213
                /\ y:103 = phi_y:214)
               \/ (x:104 <= y:103 /\ x:104 < y:103 /\ x:104 = phi_x:213
                     /\ (y:103 + -x:104) = phi_y:214)))}
**** alpha hat: 
  {<Split [true
            (__cost':215) = (1)*(__cost:105) + 1
           ((x':216 + y':217)) <= (1)*((x:104 + y:103)) + (-1)*1
           (y':217) <= (1)*(y:103) + 0
           (x':216) <= (1)*(x:104) + 0
           }
          pre:
            [|y:103-1>=0; __cost:105>=0; x:104-1>=0; x:104+y:103-3>=0|]
          post:
            [|y':217-1>=0; __cost':215-1>=0; x':216-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':215
   x := x':216
   y := y':217
   when ((!(0 <= K:226) \/ mid___cost:230 = (__cost:105 + K:226))
           /\ (!(0 <= K:226)
                 \/ (mid_x:229 + mid_y:228) <= ((x:104 + y:103) + -K:226))
           /\ (!(0 <= K:226) \/ mid_y:228 <= y:103)
           /\ (!(0 <= K:226) \/ mid_x:229 <= x:104)
           /\ ((K:226 = 0 /\ y:103 = mid_y:228 /\ x:104 = mid_x:229
                  /\ __cost:105 = mid___cost:230)
                 \/ (1 <= K:226 /\ 0 <= (-1 + y:103) /\ 0 <= __cost:105
                       /\ 0 <= (-1 + x:104) /\ 0 <= (-3 + x:104 + y:103)
                       /\ 0 <= (-1 + mid_y:228) /\ 0 <= (-1 + mid___cost:230)
                       /\ 0 <= (-1 + mid_x:229))) /\ K:227 = 0
           /\ mid_y:228 = y':217 /\ mid_x:229 = x':216
           /\ mid___cost:230 = __cost':215 /\ 0 = K:227
           /\ (K:226 + K:227) = K:225 /\ 0 <= K:225)}
}
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:90
       param1@pos := type_err:91
       param0@width := type_err:92
       param1@width := type_err:93}    )
    ,
    Var(19)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:84
     return@width := type_err:85}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=19: 
Weight(Base relation: 
  {__cost := phi___cost:243
   __retres3 := phi___retres3:242
   x := phi_x:241
   y := phi_y:240
   return := phi___retres3:242
   return@pos := type_err:244
   return@width := type_err:245
   when ((((param0:80 <= 0 /\ param1:83 = phi___retres3:210)
             \/ (0 < param0:80 /\ param1:83 <= 0
                   /\ param0:80 = phi___retres3:210))
            /\ __cost:105 = phi___cost:243
            /\ phi___retres3:210 = phi___retres3:242 /\ param0:80 = phi_x:241
            /\ param1:83 = phi_y:240)
           \/ (0 < param0:80 /\ 0 < param1:83
                 /\ (!(0 <= K:231) \/ mid___cost:232 = (__cost:105 + K:231))
                 /\ (!(0 <= K:231)
                       \/ (mid_x:233 + mid_y:234) <= ((param0:80 + param1:83)
                                                        + -K:231))
                 /\ (!(0 <= K:231) \/ mid_y:234 <= param1:83)
                 /\ (!(0 <= K:231) \/ mid_x:233 <= param0:80)
                 /\ ((K:231 = 0 /\ param1:83 = mid_y:234
                        /\ param0:80 = mid_x:233
                        /\ __cost:105 = mid___cost:232)
                       \/ (1 <= K:231 /\ 0 <= (-1 + param1:83)
                             /\ 0 <= __cost:105 /\ 0 <= (-1 + param0:80)
                             /\ 0 <= (-3 + param0:80 + param1:83)
                             /\ 0 <= (-1 + mid_y:234)
                             /\ 0 <= (-1 + mid___cost:232)
                             /\ 0 <= (-1 + mid_x:233))) /\ K:235 = 0
                 /\ mid_y:234 = y':236 /\ mid_x:233 = x':237
                 /\ mid___cost:232 = __cost':238 /\ 0 = K:235
                 /\ (K:231 + K:235) = K:239 /\ 0 <= K:239 /\ 1 <= y':236
                 /\ 1 <= x':237 /\ 0 < x':237 /\ 0 < y':236
                 /\ 0 <= __cost':238 /\ 0 <= (__cost':238 + 1)
                 /\ x':237 <= y':236 /\ y':236 <= x':237
                 /\ (__cost':238 + 1) = phi___cost:243
                 /\ x':237 = phi___retres3:242 /\ x':237 = phi_x:241
                 /\ y':236 = phi_y:240))})



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:90
         param1@pos := type_err:91
         param0@width := type_err:92
         param1@width := type_err:93}      )
      ,
      Var(19)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:84
       return@width := type_err:85}    )
  )
)



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

Weight(Base relation: 
  {__cost := phi___cost:243
   return := phi___retres3:242
   return@pos := type_err:244
   return@width := type_err:245
   when ((((param0:80 <= 0 /\ param1:83 = phi___retres3:210)
             \/ (0 < param0:80 /\ param1:83 <= 0
                   /\ param0:80 = phi___retres3:210))
            /\ __cost:105 = phi___cost:243
            /\ phi___retres3:210 = phi___retres3:242 /\ param0:80 = phi_x:241
            /\ param1:83 = phi_y:240)
           \/ (0 < param0:80 /\ 0 < param1:83
                 /\ (!(0 <= K:231) \/ mid___cost:232 = (__cost:105 + K:231))
                 /\ (!(0 <= K:231)
                       \/ (mid_x:233 + mid_y:234) <= ((param0:80 + param1:83)
                                                        + -K:231))
                 /\ (!(0 <= K:231) \/ mid_y:234 <= param1:83)
                 /\ (!(0 <= K:231) \/ mid_x:233 <= param0:80)
                 /\ ((K:231 = 0 /\ param1:83 = mid_y:234
                        /\ param0:80 = mid_x:233
                        /\ __cost:105 = mid___cost:232)
                       \/ (1 <= K:231 /\ 0 <= (-1 + param1:83)
                             /\ 0 <= __cost:105 /\ 0 <= (-1 + param0:80)
                             /\ 0 <= (-3 + param0:80 + param1:83)
                             /\ 0 <= (-1 + mid_y:234)
                             /\ 0 <= (-1 + mid___cost:232)
                             /\ 0 <= (-1 + mid_x:233))) /\ K:235 = 0
                 /\ mid_y:234 = y':236 /\ mid_x:233 = x':237
                 /\ mid___cost:232 = __cost':238 /\ 0 = K:235
                 /\ (K:231 + K:235) = K:239 /\ 0 <= K:239 /\ 1 <= y':236
                 /\ 1 <= x':237 /\ 0 < x':237 /\ 0 < y':236
                 /\ 0 <= __cost':238 /\ 0 <= (__cost':238 + 1)
                 /\ x':237 <= y':236 /\ y':236 <= x':237
                 /\ (__cost':238 + 1) = phi___cost:243
                 /\ x':237 = phi___retres3:242 /\ x':237 = phi_x:241
                 /\ y':236 = phi_y:240))})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := phi___cost:267
   return := 0
   param0 := havoc:21
   param1 := havoc:22
   return@pos := type_err:288
   param0@pos := type_err:281
   param1@pos := type_err:282
   return@width := type_err:289
   param0@width := type_err:284
   param1@width := type_err:285
   when (((((havoc:21 <= 0 /\ havoc:22 = phi___retres3:266)
              \/ (0 < havoc:21 /\ havoc:22 <= 0
                    /\ havoc:21 = phi___retres3:266)) /\ 0 = phi___cost:267
             /\ phi___retres3:266 = phi___retres3:268 /\ havoc:21 = phi_x:269
             /\ havoc:22 = phi_y:270)
            \/ (0 < havoc:21 /\ 0 < havoc:22
                  /\ (!(0 <= K:271) \/ mid___cost:272 = K:271)
                  /\ (!(0 <= K:271)
                        \/ (mid_x:273 + mid_y:274) <= ((havoc:21 + havoc:22)
                                                         + -K:271))
                  /\ (!(0 <= K:271) \/ mid_y:274 <= havoc:22)
                  /\ (!(0 <= K:271) \/ mid_x:273 <= havoc:21)
                  /\ ((K:271 = 0 /\ havoc:22 = mid_y:274
                         /\ havoc:21 = mid_x:273 /\ 0 = mid___cost:272)
                        \/ (1 <= K:271 /\ 0 <= (-1 + havoc:22)
                              /\ 0 <= (-1 + havoc:21)
                              /\ 0 <= (-3 + havoc:21 + havoc:22)
                              /\ 0 <= (-1 + mid_y:274)
                              /\ 0 <= (-1 + mid___cost:272)
                              /\ 0 <= (-1 + mid_x:273))) /\ K:275 = 0
                  /\ mid_y:274 = y':276 /\ mid_x:273 = x':277
                  /\ mid___cost:272 = __cost':278 /\ 0 = K:275
                  /\ (K:271 + K:275) = K:279 /\ 0 <= K:279 /\ 1 <= y':276
                  /\ 1 <= x':277 /\ 0 < x':277 /\ 0 < y':276
                  /\ 0 <= __cost':278 /\ 0 <= (__cost':278 + 1)
                  /\ x':277 <= y':276 /\ y':276 <= x':277
                  /\ (__cost':278 + 1) = phi___cost:267
                  /\ x':277 = phi___retres3:268 /\ x':277 = phi_x:269
                  /\ y':276 = phi_y:270))
           /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:286)
                 \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:286))
           /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:287)
                 \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:287)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := phi___cost:291
   return := 0
   param0 := param0:80
   param1 := param1:83
   return@pos := type_err:306
   param0@pos := type_err:90
   param1@pos := type_err:91
   return@width := type_err:307
   param0@width := type_err:92
   param1@width := type_err:93
   when ((((param0:80 <= 0 /\ param1:83 = phi___retres3:290)
             \/ (0 < param0:80 /\ param1:83 <= 0
                   /\ param0:80 = phi___retres3:290))
            /\ __cost:105 = phi___cost:291
            /\ phi___retres3:290 = phi___retres3:292 /\ param0:80 = phi_x:293
            /\ param1:83 = phi_y:294)
           \/ (0 < param0:80 /\ 0 < param1:83
                 /\ (!(0 <= K:295) \/ mid___cost:296 = (__cost:105 + K:295))
                 /\ (!(0 <= K:295)
                       \/ (mid_x:297 + mid_y:298) <= ((param0:80 + param1:83)
                                                        + -K:295))
                 /\ (!(0 <= K:295) \/ mid_y:298 <= param1:83)
                 /\ (!(0 <= K:295) \/ mid_x:297 <= param0:80)
                 /\ ((K:295 = 0 /\ param1:83 = mid_y:298
                        /\ param0:80 = mid_x:297
                        /\ __cost:105 = mid___cost:296)
                       \/ (1 <= K:295 /\ 0 <= (-1 + param1:83)
                             /\ 0 <= __cost:105 /\ 0 <= (-1 + param0:80)
                             /\ 0 <= (-3 + param0:80 + param1:83)
                             /\ 0 <= (-1 + mid_y:298)
                             /\ 0 <= (-1 + mid___cost:296)
                             /\ 0 <= (-1 + mid_x:297))) /\ K:299 = 0
                 /\ mid_y:298 = y':300 /\ mid_x:297 = x':301
                 /\ mid___cost:296 = __cost':302 /\ 0 = K:299
                 /\ (K:295 + K:299) = K:303 /\ 0 <= K:303 /\ 1 <= y':300
                 /\ 1 <= x':301 /\ 0 < x':301 /\ 0 < y':300
                 /\ 0 <= __cost':302 /\ 0 <= (__cost':302 + 1)
                 /\ x':301 <= y':300 /\ y':300 <= x':301
                 /\ (__cost':302 + 1) = phi___cost:291
                 /\ x':301 = phi___retres3:292 /\ x':301 = phi_x:293
                 /\ y':300 = phi_y:294))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=19: 
Weight(Base relation: 
  {__cost := phi___cost:243
   return := phi___retres3:242
   return@pos := type_err:244
   return@width := type_err:245
   when ((((param0:80 <= 0 /\ param1:83 = phi___retres3:210)
             \/ (0 < param0:80 /\ param1:83 <= 0
                   /\ param0:80 = phi___retres3:210))
            /\ __cost:105 = phi___cost:243
            /\ phi___retres3:210 = phi___retres3:242 /\ param0:80 = phi_x:241
            /\ param1:83 = phi_y:240)
           \/ (0 < param0:80 /\ 0 < param1:83
                 /\ (!(0 <= K:231) \/ mid___cost:232 = (__cost:105 + K:231))
                 /\ (!(0 <= K:231)
                       \/ (mid_x:233 + mid_y:234) <= ((param0:80 + param1:83)
                                                        + -K:231))
                 /\ (!(0 <= K:231) \/ mid_y:234 <= param1:83)
                 /\ (!(0 <= K:231) \/ mid_x:233 <= param0:80)
                 /\ ((K:231 = 0 /\ param1:83 = mid_y:234
                        /\ param0:80 = mid_x:233
                        /\ __cost:105 = mid___cost:232)
                       \/ (1 <= K:231 /\ 0 <= (-1 + param1:83)
                             /\ 0 <= __cost:105 /\ 0 <= (-1 + param0:80)
                             /\ 0 <= (-3 + param0:80 + param1:83)
                             /\ 0 <= (-1 + mid_y:234)
                             /\ 0 <= (-1 + mid___cost:232)
                             /\ 0 <= (-1 + mid_x:233))) /\ K:235 = 0
                 /\ mid_y:234 = y':236 /\ mid_x:233 = x':237
                 /\ mid___cost:232 = __cost':238 /\ 0 = K:235
                 /\ (K:231 + K:235) = K:239 /\ 0 <= K:239 /\ 1 <= y':236
                 /\ 1 <= x':237 /\ 0 < x':237 /\ 0 < y':236
                 /\ 0 <= __cost':238 /\ 0 <= (__cost':238 + 1)
                 /\ x':237 <= y':236 /\ y':236 <= x':237
                 /\ (__cost':238 + 1) = phi___cost:243
                 /\ x':237 = phi___retres3:242 /\ x':237 = phi_x:241
                 /\ y':236 = phi_y:240))})


Step 5: =========================================================
[Newton] Running Newton
-------------------------------------------------------------------------------
Round 0:
Evaluating variable number 6 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:267
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:288
 param0@pos := type_err:281
 param1@pos := type_err:282
 return@width := type_err:289
 param0@width := type_err:284
 param1@width := type_err:285
 when (((((havoc:21 <= 0 /\ havoc:22 = phi___retres3:266)
            \/ (0 < havoc:21 /\ havoc:22 <= 0 /\ havoc:21 = phi___retres3:266))
           /\ 0 = phi___cost:267 /\ phi___retres3:266 = phi___retres3:268
           /\ havoc:21 = phi_x:269 /\ havoc:22 = phi_y:270)
          \/ (0 < havoc:21 /\ 0 < havoc:22
                /\ (!(0 <= K:271) \/ mid___cost:272 = K:271)
                /\ (!(0 <= K:271)
                      \/ (mid_x:273 + mid_y:274) <= ((havoc:21 + havoc:22)
                                                       + -K:271))
                /\ (!(0 <= K:271) \/ mid_y:274 <= havoc:22)
                /\ (!(0 <= K:271) \/ mid_x:273 <= havoc:21)
                /\ ((K:271 = 0 /\ havoc:22 = mid_y:274
                       /\ havoc:21 = mid_x:273 /\ 0 = mid___cost:272)
                      \/ (1 <= K:271 /\ 0 <= (-1 + havoc:22)
                            /\ 0 <= (-1 + havoc:21)
                            /\ 0 <= (-3 + havoc:21 + havoc:22)
                            /\ 0 <= (-1 + mid_y:274)
                            /\ 0 <= (-1 + mid___cost:272)
                            /\ 0 <= (-1 + mid_x:273))) /\ K:275 = 0
                /\ mid_y:274 = y':276 /\ mid_x:273 = x':277
                /\ mid___cost:272 = __cost':278 /\ 0 = K:275
                /\ (K:271 + K:275) = K:279 /\ 0 <= K:279 /\ 1 <= y':276
                /\ 1 <= x':277 /\ 0 < x':277 /\ 0 < y':276
                /\ 0 <= __cost':278 /\ 0 <= (__cost':278 + 1)
                /\ x':277 <= y':276 /\ y':276 <= x':277
                /\ (__cost':278 + 1) = phi___cost:267
                /\ x':277 = phi___retres3:268 /\ x':277 = phi_x:269
                /\ y':276 = phi_y:270))
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:286)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:286))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:287)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:287)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:291
 return := 0
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:306
 param0@pos := type_err:90
 param1@pos := type_err:91
 return@width := type_err:307
 param0@width := type_err:92
 param1@width := type_err:93
 when ((((param0:80 <= 0 /\ param1:83 = phi___retres3:290)
           \/ (0 < param0:80 /\ param1:83 <= 0
                 /\ param0:80 = phi___retres3:290))
          /\ __cost:105 = phi___cost:291
          /\ phi___retres3:290 = phi___retres3:292 /\ param0:80 = phi_x:293
          /\ param1:83 = phi_y:294)
         \/ (0 < param0:80 /\ 0 < param1:83
               /\ (!(0 <= K:295) \/ mid___cost:296 = (__cost:105 + K:295))
               /\ (!(0 <= K:295)
                     \/ (mid_x:297 + mid_y:298) <= ((param0:80 + param1:83)
                                                      + -K:295))
               /\ (!(0 <= K:295) \/ mid_y:298 <= param1:83)
               /\ (!(0 <= K:295) \/ mid_x:297 <= param0:80)
               /\ ((K:295 = 0 /\ param1:83 = mid_y:298
                      /\ param0:80 = mid_x:297 /\ __cost:105 = mid___cost:296)
                     \/ (1 <= K:295 /\ 0 <= (-1 + param1:83)
                           /\ 0 <= __cost:105 /\ 0 <= (-1 + param0:80)
                           /\ 0 <= (-3 + param0:80 + param1:83)
                           /\ 0 <= (-1 + mid_y:298)
                           /\ 0 <= (-1 + mid___cost:296)
                           /\ 0 <= (-1 + mid_x:297))) /\ K:299 = 0
               /\ mid_y:298 = y':300 /\ mid_x:297 = x':301
               /\ mid___cost:296 = __cost':302 /\ 0 = K:299
               /\ (K:295 + K:299) = K:303 /\ 0 <= K:303 /\ 1 <= y':300
               /\ 1 <= x':301 /\ 0 < x':301 /\ 0 < y':300 /\ 0 <= __cost':302
               /\ 0 <= (__cost':302 + 1) /\ x':301 <= y':300
               /\ y':300 <= x':301 /\ (__cost':302 + 1) = phi___cost:291
               /\ x':301 = phi___retres3:292 /\ x':301 = phi_x:293
               /\ y':300 = phi_y:294))}

Evaluating variable number 19 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:243
 return := phi___retres3:242
 return@pos := type_err:244
 return@width := type_err:245
 when ((((param0:80 <= 0 /\ param1:83 = phi___retres3:210)
           \/ (0 < param0:80 /\ param1:83 <= 0
                 /\ param0:80 = phi___retres3:210))
          /\ __cost:105 = phi___cost:243
          /\ phi___retres3:210 = phi___retres3:242 /\ param0:80 = phi_x:241
          /\ param1:83 = phi_y:240)
         \/ (0 < param0:80 /\ 0 < param1:83
               /\ (!(0 <= K:231) \/ mid___cost:232 = (__cost:105 + K:231))
               /\ (!(0 <= K:231)
                     \/ (mid_x:233 + mid_y:234) <= ((param0:80 + param1:83)
                                                      + -K:231))
               /\ (!(0 <= K:231) \/ mid_y:234 <= param1:83)
               /\ (!(0 <= K:231) \/ mid_x:233 <= param0:80)
               /\ ((K:231 = 0 /\ param1:83 = mid_y:234
                      /\ param0:80 = mid_x:233 /\ __cost:105 = mid___cost:232)
                     \/ (1 <= K:231 /\ 0 <= (-1 + param1:83)
                           /\ 0 <= __cost:105 /\ 0 <= (-1 + param0:80)
                           /\ 0 <= (-3 + param0:80 + param1:83)
                           /\ 0 <= (-1 + mid_y:234)
                           /\ 0 <= (-1 + mid___cost:232)
                           /\ 0 <= (-1 + mid_x:233))) /\ K:235 = 0
               /\ mid_y:234 = y':236 /\ mid_x:233 = x':237
               /\ mid___cost:232 = __cost':238 /\ 0 = K:235
               /\ (K:231 + K:235) = K:239 /\ 0 <= K:239 /\ 1 <= y':236
               /\ 1 <= x':237 /\ 0 < x':237 /\ 0 < y':236 /\ 0 <= __cost':238
               /\ 0 <= (__cost':238 + 1) /\ x':237 <= y':236
               /\ y':236 <= x':237 /\ (__cost':238 + 1) = phi___cost:243
               /\ x':237 = phi___retres3:242 /\ x':237 = phi_x:241
               /\ y':236 = phi_y:240))}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, accept> -> <__pstate, (Unique State Name,73)_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}	
<__pstate, (Unique State Name,73)_g1> -> <__pstate, (Unique State Name,67)_g1>	Base relation: 
{param0 := param0:80
 param1 := param1:83
 param0@pos := type_err:90
 param1@pos := type_err:91
 param0@width := type_err:92
 param1@width := type_err:93}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x49536c0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x51e6680: 
	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,73)_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}
    ( __pstate , (Unique State Name,67)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:350
 param1@pos := type_err:351
 param0@width := type_err:352
 param1@width := type_err:353}

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

------------------------------------------------
Procedure summary for gcd

Base relation: 
{__cost := phi___cost:243
 __retres3 := phi___retres3:242
 x := phi_x:241
 y := phi_y:240
 return := phi___retres3:242
 return@pos := type_err:244
 return@width := type_err:245
 when ((((param0:80 <= 0 /\ param1:83 = phi___retres3:210)
           \/ (0 < param0:80 /\ param1:83 <= 0
                 /\ param0:80 = phi___retres3:210))
          /\ __cost:105 = phi___cost:243
          /\ phi___retres3:210 = phi___retres3:242 /\ param0:80 = phi_x:241
          /\ param1:83 = phi_y:240)
         \/ (0 < param0:80 /\ 0 < param1:83
               /\ (!(0 <= K:231) \/ mid___cost:232 = (__cost:105 + K:231))
               /\ (!(0 <= K:231)
                     \/ (mid_x:233 + mid_y:234) <= ((param0:80 + param1:83)
                                                      + -K:231))
               /\ (!(0 <= K:231) \/ mid_y:234 <= param1:83)
               /\ (!(0 <= K:231) \/ mid_x:233 <= param0:80)
               /\ ((K:231 = 0 /\ param1:83 = mid_y:234
                      /\ param0:80 = mid_x:233 /\ __cost:105 = mid___cost:232)
                     \/ (1 <= K:231 /\ 0 <= (-1 + param1:83)
                           /\ 0 <= __cost:105 /\ 0 <= (-1 + param0:80)
                           /\ 0 <= (-3 + param0:80 + param1:83)
                           /\ 0 <= (-1 + mid_y:234)
                           /\ 0 <= (-1 + mid___cost:232)
                           /\ 0 <= (-1 + mid_x:233))) /\ K:235 = 0
               /\ mid_y:234 = y':236 /\ mid_x:233 = x':237
               /\ mid___cost:232 = __cost':238 /\ 0 = K:235
               /\ (K:231 + K:235) = K:239 /\ 0 <= K:239 /\ 1 <= y':236
               /\ 1 <= x':237 /\ 0 < x':237 /\ 0 < y':236 /\ 0 <= __cost':238
               /\ 0 <= (__cost':238 + 1) /\ x':237 <= y':236
               /\ y':236 <= x':237 /\ (__cost':238 + 1) = phi___cost:243
               /\ x':237 = phi___retres3:242 /\ x':237 = phi_x:241
               /\ y':236 = phi_y:240))}

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

Base relation: 
{__cost := phi___cost:309
 x := havoc:21
 y := havoc:22
 return := 0
 param0 := havoc:21
 param1 := havoc:22
 return@pos := type_err:330
 param0@pos := type_err:323
 param1@pos := type_err:324
 return@width := type_err:331
 param0@width := type_err:326
 param1@width := type_err:327
 when (((((havoc:21 <= 0 /\ havoc:22 = phi___retres3:308)
            \/ (0 < havoc:21 /\ havoc:22 <= 0 /\ havoc:21 = phi___retres3:308))
           /\ 0 = phi___cost:309 /\ phi___retres3:308 = phi___retres3:310
           /\ havoc:21 = phi_x:311 /\ havoc:22 = phi_y:312)
          \/ (0 < havoc:21 /\ 0 < havoc:22
                /\ (!(0 <= K:313) \/ mid___cost:314 = K:313)
                /\ (!(0 <= K:313)
                      \/ (mid_x:315 + mid_y:316) <= ((havoc:21 + havoc:22)
                                                       + -K:313))
                /\ (!(0 <= K:313) \/ mid_y:316 <= havoc:22)
                /\ (!(0 <= K:313) \/ mid_x:315 <= havoc:21)
                /\ ((K:313 = 0 /\ havoc:22 = mid_y:316
                       /\ havoc:21 = mid_x:315 /\ 0 = mid___cost:314)
                      \/ (1 <= K:313 /\ 0 <= (-1 + havoc:22)
                            /\ 0 <= (-1 + havoc:21)
                            /\ 0 <= (-3 + havoc:21 + havoc:22)
                            /\ 0 <= (-1 + mid_y:316)
                            /\ 0 <= (-1 + mid___cost:314)
                            /\ 0 <= (-1 + mid_x:315))) /\ K:317 = 0
                /\ mid_y:316 = y':318 /\ mid_x:315 = x':319
                /\ mid___cost:314 = __cost':320 /\ 0 = K:317
                /\ (K:313 + K:317) = K:321 /\ 0 <= K:321 /\ 1 <= y':318
                /\ 1 <= x':319 /\ 0 < x':319 /\ 0 < y':318
                /\ 0 <= __cost':320 /\ 0 <= (__cost':320 + 1)
                /\ x':319 <= y':318 /\ y':318 <= x':319
                /\ (__cost':320 + 1) = phi___cost:309
                /\ x':319 = phi___retres3:310 /\ x':319 = phi_x:311
                /\ y':318 = phi_y:312))
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:328)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:328))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:329)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:329)))}

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

Base relation: 
{__cost := phi___cost:333
 return := 0
 param0 := param0:80
 param1 := param1:83
 return@pos := type_err:348
 param0@pos := type_err:90
 param1@pos := type_err:91
 return@width := type_err:349
 param0@width := type_err:92
 param1@width := type_err:93
 when ((((param0:80 <= 0 /\ param1:83 = phi___retres3:332)
           \/ (0 < param0:80 /\ param1:83 <= 0
                 /\ param0:80 = phi___retres3:332))
          /\ __cost:105 = phi___cost:333
          /\ phi___retres3:332 = phi___retres3:334 /\ param0:80 = phi_x:335
          /\ param1:83 = phi_y:336)
         \/ (0 < param0:80 /\ 0 < param1:83
               /\ (!(0 <= K:337) \/ mid___cost:338 = (__cost:105 + K:337))
               /\ (!(0 <= K:337)
                     \/ (mid_x:339 + mid_y:340) <= ((param0:80 + param1:83)
                                                      + -K:337))
               /\ (!(0 <= K:337) \/ mid_y:340 <= param1:83)
               /\ (!(0 <= K:337) \/ mid_x:339 <= param0:80)
               /\ ((K:337 = 0 /\ param1:83 = mid_y:340
                      /\ param0:80 = mid_x:339 /\ __cost:105 = mid___cost:338)
                     \/ (1 <= K:337 /\ 0 <= (-1 + param1:83)
                           /\ 0 <= __cost:105 /\ 0 <= (-1 + param0:80)
                           /\ 0 <= (-3 + param0:80 + param1:83)
                           /\ 0 <= (-1 + mid_y:340)
                           /\ 0 <= (-1 + mid___cost:338)
                           /\ 0 <= (-1 + mid_x:339))) /\ K:341 = 0
               /\ mid_y:340 = y':342 /\ mid_x:339 = x':343
               /\ mid___cost:338 = __cost':344 /\ 0 = K:341
               /\ (K:337 + K:341) = K:345 /\ 0 <= K:345 /\ 1 <= y':342
               /\ 1 <= x':343 /\ 0 < x':343 /\ 0 < y':342 /\ 0 <= __cost':344
               /\ 0 <= (__cost':344 + 1) /\ x':343 <= y':342
               /\ y':342 <= x':343 /\ (__cost':344 + 1) = phi___cost:333
               /\ x':343 = phi___retres3:334 /\ x':343 = phi_x:335
               /\ y':342 = phi_y:336))}

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

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

Variable bounds at line 22 in run

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

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