/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, 65> -> <Unique State Name, 59>	Base relation: 
{__cost := phi___cost:118
 when (((havoc:109 < 0 \/ 0 < havoc:109) /\ 0 <= __cost:102
          /\ 0 <= (__cost:102 + 10000)
          /\ (__cost:102 + 10000) = phi___cost:118)
         \/ (0 <= havoc:109 /\ havoc:109 <= 0 /\ __cost:102 = phi___cost:118))}	
<Unique State Name, 31> -> <Unique State Name, 78>	Base relation: 
{return := __retres5:6
 return@pos := type_err:9
 return@width := type_err:10}	
<Unique State Name, 75> -> <Unique State Name, 7>	Base relation: 
{__cost := 0
 argc := param0:23
 argv := param1:26
 argv@pos := param1@pos:25
 argv@width := param1@width:24}	
<Unique State Name, 7> -> <Unique State Name, 31>	Base relation: 
{__retres5 := -1
 when (argc:0 < 2 \/ 2 < argc:0)}	
<Unique State Name, 7> -> <Unique State Name, 71>	Base relation: 
{param0 := tr:27
 param0@pos := type_err:28
 param0@width := type_err:29
 when (2 <= argc:0 /\ argc:0 <= 2)}	
<Unique State Name, 71> -> <Unique State Name, 79 70>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 70> -> <Unique State Name, 25>	Base relation: 
{val := havoc:11}	
<Unique State Name, 67> -> <Unique State Name, 36>	Base relation: 
{N := 10000000005
 z := 0
 i := 0
 x := param0:23}	
<Unique State Name, 77> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 78> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 80> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 81> -> <Unique State Name, 40>	Base relation: 
{}	
<Unique State Name, 79> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 74> -> <Unique State Name, 67 73>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 18> -> <Unique State Name, 31>	Base relation: 
{__retres5 := -1
 when 10000000 < val:5}	
<Unique State Name, 18> -> <Unique State Name, 74>	Base relation: 
{param0 := val:5
 param0@pos := type_err:30
 param0@width := type_err:31
 when val:5 <= 10000000}	
<Unique State Name, 59> -> <Unique State Name, 77>	Base relation: 
{return := havoc:104
 return@pos := type_err:107
 return@width := type_err:108}	
<Unique State Name, 25> -> <Unique State Name, 18>	Base relation: 
{when 1 <= val:5}	
<Unique State Name, 25> -> <Unique State Name, 31>	Base relation: 
{__retres5 := -1
 when val:5 < 1}	
<Unique State Name, 73> -> <Unique State Name, 31>	Base relation: 
{__retres5 := 0}	
<Unique State Name, 36> -> <Unique State Name, 81>	Base relation: 
{when (0 <= i:98 /\ 0 <= z:101 /\ N:100 <= 10000000005
         /\ 10000000005 <= N:100)}	
<Unique State Name, 40> -> <Unique State Name, 36>	Base relation: 
{z := (z:101 + N:100)
 i := (i:98 + 1)
 when i:98 < x:99}	
<Unique State Name, 40> -> <Unique State Name, 66>	Base relation: 
{param0 := (N:100
              + -(ite(((0 <= z:101 /\ 0 <= x:99)
                         \/ (!(0 <= z:101) /\ !(0 <= x:99))),
                      floor((z:101 / x:99)), -(floor(-((z:101 / x:99)))))))
 param0@pos := type_err:116
 param0@width := type_err:117
 when x:99 <= i:98}	
<Unique State Name, 66> -> <Unique State Name, 80 65>	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: 
{z := (z:101 + N:100)
 i := (i:98 + 1)
 when (0 <= i:98 /\ 0 <= z:101 /\ N:100 <= 10000000005
         /\ 10000000005 <= N:100 /\ i:98 < x:99)}
**** alpha hat: 
  {<Split [true
            (i':199) = (1)*(i:98) + 1
           (z':198) = (1)*(z:101) + 10000000005*1
           }
          pre:
            [|N:100-10000000005=0; -i:98+x:99-1>=0; z:101>=0; i:98>=0|]
          post:
            [|N:100-10000000005=0; z':198-10000000005>=0; i':199-1>=0;
              x:99-i':199>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {z := z':198
   i := i':199
   when ((!(0 <= K:209) \/ mid_i:211 = (i:98 + K:209))
           /\ (!(0 <= K:209) \/ mid_z:212 = (z:101 + (10000000005 * K:209)))
           /\ ((K:209 = 0 /\ i:98 = mid_i:211 /\ z:101 = mid_z:212)
                 \/ (1 <= K:209 /\ (-10000000005 + N:100) = 0
                       /\ 0 <= (-1 + -i:98 + x:99) /\ 0 <= z:101 /\ 0 <= i:98
                       /\ (-10000000005 + N:100) = 0
                       /\ 0 <= (-10000000005 + mid_z:212)
                       /\ 0 <= (-1 + mid_i:211) /\ 0 <= (x:99 + -mid_i:211)))
           /\ K:210 = 0 /\ mid_i:211 = i':199 /\ mid_z:212 = z':198
           /\ 0 = K:210 /\ (K:209 + K:210) = K:208 /\ 0 <= K:208)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
13  15  25  27  


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Plus(
    Plus(
      Plus(
        Weight(Base relation: 
          {__cost := 0
           __retres5 := -1
           argc := param0:23
           argv := param1:26
           argv@pos := param1@pos:25
           argv@width := param1@width:24
           when (param0:23 < 2 \/ 2 < param0:23)}        )
        ,
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := 0
               argc := param0:23
               argv := param1:26
               param0 := tr:193
               argv@pos := param1@pos:25
               param0@pos := type_err:194
               argv@width := param1@width:24
               param0@width := type_err:195
               when (2 <= param0:23 /\ param0:23 <= 2)}            )
            ,
            Var(15)
          )
          ,
          Weight(Base relation: 
            {val := havoc:11
             __retres5 := -1
             when havoc:11 < 1}          )
        )
      )
      ,
      Dot(
        Dot(
          Weight(Base relation: 
            {__cost := 0
             argc := param0:23
             argv := param1:26
             param0 := tr:193
             argv@pos := param1@pos:25
             param0@pos := type_err:194
             argv@width := param1@width:24
             param0@width := type_err:195
             when (2 <= param0:23 /\ param0:23 <= 2)}          )
          ,
          Var(15)
        )
        ,
        Weight(Base relation: 
          {val := havoc:11
           __retres5 := -1
           when (1 <= havoc:11 /\ 10000000 < havoc:11)}        )
      )
    )
    ,
    Dot(
      Dot(
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := 0
               argc := param0:23
               argv := param1:26
               param0 := tr:193
               argv@pos := param1@pos:25
               param0@pos := type_err:194
               argv@width := param1@width:24
               param0@width := type_err:195
               when (2 <= param0:23 /\ param0:23 <= 2)}            )
            ,
            Var(15)
          )
          ,
          Weight(Base relation: 
            {val := havoc:11
             param0 := havoc:11
             param0@pos := type_err:196
             param0@width := type_err:197
             when (1 <= havoc:11 /\ havoc:11 <= 10000000)}          )
        )
        ,
        Var(25)
      )
      ,
      Weight(Base relation: 
        {__retres5 := 0}      )
    )
  )
  ,
  Weight(Base relation: 
    {return := __retres5:6
     return@pos := type_err:9
     return@width := type_err:10}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=15: 
One()


New-style (IRE) regular expression in IREregExpMap for reID=25: 
Dot(
  Dot(
    Weight(Base relation: 
      {N := 10000000005
       z := z':218
       i := i':217
       x := param0:23
       param0 := (10000000005
                    + -(ite(((0 <= z':218 /\ 0 <= param0:23)
                               \/ (!(0 <= z':218) /\ !(0 <= param0:23))),
                            floor((z':218 / param0:23)),
                            -(floor(-((z':218 / param0:23)))))))
       param0@pos := type_err:220
       param0@width := type_err:221
       when ((!(0 <= K:213) \/ mid_i:214 = K:213)
               /\ (!(0 <= K:213) \/ mid_z:215 = (10000000005 * K:213))
               /\ ((K:213 = 0 /\ 0 = mid_i:214 /\ 0 = mid_z:215)
                     \/ (1 <= K:213 /\ (-10000000005 + 10000000005) = 0
                           /\ 0 <= (-1 + param0:23)
                           /\ (-10000000005 + 10000000005) = 0
                           /\ 0 <= (-10000000005 + mid_z:215)
                           /\ 0 <= (-1 + mid_i:214)
                           /\ 0 <= (param0:23 + -mid_i:214))) /\ K:216 = 0
               /\ mid_i:214 = i':217 /\ mid_z:215 = z':218 /\ 0 = K:216
               /\ (K:213 + K:216) = K:219 /\ 0 <= K:219 /\ 0 <= i':217
               /\ 0 <= z':218 /\ param0:23 <= i':217)}    )
    ,
    Var(27)
  )
  ,
  Weight(Base relation: 
    {__cost := phi___cost:118
     return := havoc:222
     return@pos := type_err:223
     return@width := type_err:224
     when (((havoc:109 < 0 \/ 0 < havoc:109) /\ 0 <= __cost:102
              /\ 0 <= (__cost:102 + 10000)
              /\ (__cost:102 + 10000) = phi___cost:118)
             \/ (0 <= havoc:109 /\ havoc:109 <= 0
                   /\ __cost:102 = phi___cost:118))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=27: 
One()



Performing Gaussian Elimination.


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

Project(
  Dot(
    Plus(
      Plus(
        Plus(
          Weight(Base relation: 
            {__cost := 0
             __retres5 := -1
             argc := param0:23
             argv := param1:26
             argv@pos := param1@pos:25
             argv@width := param1@width:24
             when (param0:23 < 2 \/ 2 < param0:23)}          )
          ,
          Dot(
            Dot(
              Weight(Base relation: 
                {__cost := 0
                 argc := param0:23
                 argv := param1:26
                 param0 := tr:193
                 argv@pos := param1@pos:25
                 param0@pos := type_err:194
                 argv@width := param1@width:24
                 param0@width := type_err:195
                 when (2 <= param0:23 /\ param0:23 <= 2)}              )
              ,
              Var(15)
            )
            ,
            Weight(Base relation: 
              {val := havoc:11
               __retres5 := -1
               when havoc:11 < 1}            )
          )
        )
        ,
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := 0
               argc := param0:23
               argv := param1:26
               param0 := tr:193
               argv@pos := param1@pos:25
               param0@pos := type_err:194
               argv@width := param1@width:24
               param0@width := type_err:195
               when (2 <= param0:23 /\ param0:23 <= 2)}            )
            ,
            Var(15)
          )
          ,
          Weight(Base relation: 
            {val := havoc:11
             __retres5 := -1
             when (1 <= havoc:11 /\ 10000000 < havoc:11)}          )
        )
      )
      ,
      Dot(
        Dot(
          Dot(
            Dot(
              Weight(Base relation: 
                {__cost := 0
                 argc := param0:23
                 argv := param1:26
                 param0 := tr:193
                 argv@pos := param1@pos:25
                 param0@pos := type_err:194
                 argv@width := param1@width:24
                 param0@width := type_err:195
                 when (2 <= param0:23 /\ param0:23 <= 2)}              )
              ,
              Var(15)
            )
            ,
            Weight(Base relation: 
              {val := havoc:11
               param0 := havoc:11
               param0@pos := type_err:196
               param0@width := type_err:197
               when (1 <= havoc:11 /\ havoc:11 <= 10000000)}            )
          )
          ,
          Var(25)
        )
        ,
        Weight(Base relation: 
          {__retres5 := 0}        )
      )
    )
    ,
    Weight(Base relation: 
      {return := __retres5:6
       return@pos := type_err:9
       return@width := type_err:10}    )
  )
)



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

One()



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {N := 10000000005
         z := z':218
         i := i':217
         x := param0:23
         param0 := (10000000005
                      + -(ite(((0 <= z':218 /\ 0 <= param0:23)
                                 \/ (!(0 <= z':218) /\ !(0 <= param0:23))),
                              floor((z':218 / param0:23)),
                              -(floor(-((z':218 / param0:23)))))))
         param0@pos := type_err:220
         param0@width := type_err:221
         when ((!(0 <= K:213) \/ mid_i:214 = K:213)
                 /\ (!(0 <= K:213) \/ mid_z:215 = (10000000005 * K:213))
                 /\ ((K:213 = 0 /\ 0 = mid_i:214 /\ 0 = mid_z:215)
                       \/ (1 <= K:213 /\ (-10000000005 + 10000000005) = 0
                             /\ 0 <= (-1 + param0:23)
                             /\ (-10000000005 + 10000000005) = 0
                             /\ 0 <= (-10000000005 + mid_z:215)
                             /\ 0 <= (-1 + mid_i:214)
                             /\ 0 <= (param0:23 + -mid_i:214))) /\ K:216 = 0
                 /\ mid_i:214 = i':217 /\ mid_z:215 = z':218 /\ 0 = K:216
                 /\ (K:213 + K:216) = K:219 /\ 0 <= K:219 /\ 0 <= i':217
                 /\ 0 <= z':218 /\ param0:23 <= i':217)}      )
      ,
      Var(27)
    )
    ,
    Weight(Base relation: 
      {__cost := phi___cost:118
       return := havoc:222
       return@pos := type_err:223
       return@width := type_err:224
       when (((havoc:109 < 0 \/ 0 < havoc:109) /\ 0 <= __cost:102
                /\ 0 <= (__cost:102 + 10000)
                /\ (__cost:102 + 10000) = phi___cost:118)
               \/ (0 <= havoc:109 /\ havoc:109 <= 0
                     /\ __cost:102 = phi___cost:118))}    )
  )
)



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

One()



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := phi___cost:268
   return := phi___retres5:266
   param0 := phi_param0:263
   return@pos := type_err:269
   param0@pos := phi_param0@pos:260
   return@width := type_err:270
   param0@width := phi_param0@width:257
   when (((((((param0:23 < 2 \/ 2 < param0:23) /\ val:271 = phi_val:233
                /\ param0:23 = phi_param0:232
                /\ param0@pos:22 = phi_param0@pos:231
                /\ param0@width:21 = phi_param0@width:230)
               \/ (2 <= param0:23 /\ param0:23 <= 2 /\ havoc:229 < 1
                     /\ havoc:229 = phi_val:233 /\ tr:193 = phi_param0:232
                     /\ type_err:194 = phi_param0@pos:231
                     /\ type_err:195 = phi_param0@width:230))
              /\ phi_val:233 = phi_val:237 /\ phi_param0:232 = phi_param0:236
              /\ phi_param0@pos:231 = phi_param0@pos:235
              /\ phi_param0@width:230 = phi_param0@width:234)
             \/ (2 <= param0:23 /\ param0:23 <= 2 /\ 1 <= havoc:228
                   /\ 10000000 < havoc:228 /\ havoc:228 = phi_val:237
                   /\ tr:193 = phi_param0:236
                   /\ type_err:194 = phi_param0@pos:235
                   /\ type_err:195 = phi_param0@width:234))
            /\ 0 = phi___cost:268 /\ phi_val:237 = phi_val:267
            /\ -1 = phi___retres5:266 /\ return:265 = phi_return:264
            /\ phi_param0:236 = phi_param0:263
            /\ return@pos:262 = phi_return@pos:261
            /\ phi_param0@pos:235 = phi_param0@pos:260
            /\ return@width:259 = phi_return@width:258
            /\ phi_param0@width:234 = phi_param0@width:257)
           \/ (2 <= param0:23 /\ param0:23 <= 2 /\ 1 <= havoc:225
                 /\ havoc:225 <= 10000000
                 /\ (!(0 <= K:243) \/ mid_i:244 = K:243)
                 /\ (!(0 <= K:243) \/ mid_z:245 = (10000000005 * K:243))
                 /\ ((K:243 = 0 /\ 0 = mid_i:244 /\ 0 = mid_z:245)
                       \/ (1 <= K:243 /\ (-10000000005 + 10000000005) = 0
                             /\ 0 <= (-1 + havoc:225)
                             /\ (-10000000005 + 10000000005) = 0
                             /\ 0 <= (-10000000005 + mid_z:245)
                             /\ 0 <= (-1 + mid_i:244)
                             /\ 0 <= (havoc:225 + -mid_i:244))) /\ K:246 = 0
                 /\ mid_i:244 = i':247 /\ mid_z:245 = z':248 /\ 0 = K:246
                 /\ (K:243 + K:246) = K:249 /\ 0 <= K:249 /\ 0 <= i':247
                 /\ 0 <= z':248 /\ havoc:225 <= i':247
                 /\ (((havoc:250 < 0 \/ 0 < havoc:250)
                        /\ 10000 = phi___cost:251)
                       \/ (0 <= havoc:250 /\ havoc:250 <= 0
                             /\ 0 = phi___cost:251))
                 /\ phi___cost:251 = phi___cost:268
                 /\ havoc:225 = phi_val:267 /\ 0 = phi___retres5:266
                 /\ havoc:252 = phi_return:264
                 /\ (10000000005
                       + -(ite(((0 <= z':248 /\ 0 <= havoc:225)
                                  \/ (!(0 <= z':248) /\ !(0 <= havoc:225))),
                               floor((z':248 / havoc:225)),
                               -(floor(-((z':248 / havoc:225))))))) = phi_param0:263
                 /\ type_err:253 = phi_return@pos:261
                 /\ type_err:254 = phi_param0@pos:260
                 /\ type_err:255 = phi_return@width:258
                 /\ type_err:256 = phi_param0@width:257))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=15: 
One()


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=25: 
Weight(Base relation: 
  {__cost := phi___cost:273
   return := havoc:274
   param0 := (10000000005
                + -(ite(((0 <= z':218 /\ 0 <= param0:23)
                           \/ (!(0 <= z':218) /\ !(0 <= param0:23))),
                        floor((z':218 / param0:23)),
                        -(floor(-((z':218 / param0:23)))))))
   return@pos := type_err:275
   param0@pos := type_err:220
   return@width := type_err:276
   param0@width := type_err:221
   when ((!(0 <= K:213) \/ mid_i:214 = K:213)
           /\ (!(0 <= K:213) \/ mid_z:215 = (10000000005 * K:213))
           /\ ((K:213 = 0 /\ 0 = mid_i:214 /\ 0 = mid_z:215)
                 \/ (1 <= K:213 /\ (-10000000005 + 10000000005) = 0
                       /\ 0 <= (-1 + param0:23)
                       /\ (-10000000005 + 10000000005) = 0
                       /\ 0 <= (-10000000005 + mid_z:215)
                       /\ 0 <= (-1 + mid_i:214)
                       /\ 0 <= (param0:23 + -mid_i:214))) /\ K:216 = 0
           /\ mid_i:214 = i':217 /\ mid_z:215 = z':218 /\ 0 = K:216
           /\ (K:213 + K:216) = K:219 /\ 0 <= K:219 /\ 0 <= i':217
           /\ 0 <= z':218 /\ param0:23 <= i':217
           /\ (((havoc:272 < 0 \/ 0 < havoc:272) /\ 0 <= __cost:102
                  /\ 0 <= (__cost:102 + 10000)
                  /\ (__cost:102 + 10000) = phi___cost:273)
                 \/ (0 <= havoc:272 /\ havoc:272 <= 0
                       /\ __cost:102 = phi___cost:273)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=27: 
One()


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

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:268
 return := phi___retres5:266
 param0 := phi_param0:263
 return@pos := type_err:269
 param0@pos := phi_param0@pos:260
 return@width := type_err:270
 param0@width := phi_param0@width:257
 when (((((((param0:23 < 2 \/ 2 < param0:23) /\ val:271 = phi_val:233
              /\ param0:23 = phi_param0:232
              /\ param0@pos:22 = phi_param0@pos:231
              /\ param0@width:21 = phi_param0@width:230)
             \/ (2 <= param0:23 /\ param0:23 <= 2 /\ havoc:229 < 1
                   /\ havoc:229 = phi_val:233 /\ tr:193 = phi_param0:232
                   /\ type_err:194 = phi_param0@pos:231
                   /\ type_err:195 = phi_param0@width:230))
            /\ phi_val:233 = phi_val:237 /\ phi_param0:232 = phi_param0:236
            /\ phi_param0@pos:231 = phi_param0@pos:235
            /\ phi_param0@width:230 = phi_param0@width:234)
           \/ (2 <= param0:23 /\ param0:23 <= 2 /\ 1 <= havoc:228
                 /\ 10000000 < havoc:228 /\ havoc:228 = phi_val:237
                 /\ tr:193 = phi_param0:236
                 /\ type_err:194 = phi_param0@pos:235
                 /\ type_err:195 = phi_param0@width:234))
          /\ 0 = phi___cost:268 /\ phi_val:237 = phi_val:267
          /\ -1 = phi___retres5:266 /\ return:265 = phi_return:264
          /\ phi_param0:236 = phi_param0:263
          /\ return@pos:262 = phi_return@pos:261
          /\ phi_param0@pos:235 = phi_param0@pos:260
          /\ return@width:259 = phi_return@width:258
          /\ phi_param0@width:234 = phi_param0@width:257)
         \/ (2 <= param0:23 /\ param0:23 <= 2 /\ 1 <= havoc:225
               /\ havoc:225 <= 10000000
               /\ (!(0 <= K:243) \/ mid_i:244 = K:243)
               /\ (!(0 <= K:243) \/ mid_z:245 = (10000000005 * K:243))
               /\ ((K:243 = 0 /\ 0 = mid_i:244 /\ 0 = mid_z:245)
                     \/ (1 <= K:243 /\ (-10000000005 + 10000000005) = 0
                           /\ 0 <= (-1 + havoc:225)
                           /\ (-10000000005 + 10000000005) = 0
                           /\ 0 <= (-10000000005 + mid_z:245)
                           /\ 0 <= (-1 + mid_i:244)
                           /\ 0 <= (havoc:225 + -mid_i:244))) /\ K:246 = 0
               /\ mid_i:244 = i':247 /\ mid_z:245 = z':248 /\ 0 = K:246
               /\ (K:243 + K:246) = K:249 /\ 0 <= K:249 /\ 0 <= i':247
               /\ 0 <= z':248 /\ havoc:225 <= i':247
               /\ (((havoc:250 < 0 \/ 0 < havoc:250)
                      /\ 10000 = phi___cost:251)
                     \/ (0 <= havoc:250 /\ havoc:250 <= 0
                           /\ 0 = phi___cost:251))
               /\ phi___cost:251 = phi___cost:268 /\ havoc:225 = phi_val:267
               /\ 0 = phi___retres5:266 /\ havoc:252 = phi_return:264
               /\ (10000000005
                     + -(ite(((0 <= z':248 /\ 0 <= havoc:225)
                                \/ (!(0 <= z':248) /\ !(0 <= havoc:225))),
                             floor((z':248 / havoc:225)),
                             -(floor(-((z':248 / havoc:225))))))) = phi_param0:263
               /\ type_err:253 = phi_return@pos:261
               /\ type_err:254 = phi_param0@pos:260
               /\ type_err:255 = phi_return@width:258
               /\ type_err:256 = phi_param0@width:257))}

Evaluating variable number 15 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

Evaluating variable number 25 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:273
 return := havoc:274
 param0 := (10000000005
              + -(ite(((0 <= z':218 /\ 0 <= param0:23)
                         \/ (!(0 <= z':218) /\ !(0 <= param0:23))),
                      floor((z':218 / param0:23)),
                      -(floor(-((z':218 / param0:23)))))))
 return@pos := type_err:275
 param0@pos := type_err:220
 return@width := type_err:276
 param0@width := type_err:221
 when ((!(0 <= K:213) \/ mid_i:214 = K:213)
         /\ (!(0 <= K:213) \/ mid_z:215 = (10000000005 * K:213))
         /\ ((K:213 = 0 /\ 0 = mid_i:214 /\ 0 = mid_z:215)
               \/ (1 <= K:213 /\ (-10000000005 + 10000000005) = 0
                     /\ 0 <= (-1 + param0:23)
                     /\ (-10000000005 + 10000000005) = 0
                     /\ 0 <= (-10000000005 + mid_z:215)
                     /\ 0 <= (-1 + mid_i:214)
                     /\ 0 <= (param0:23 + -mid_i:214))) /\ K:216 = 0
         /\ mid_i:214 = i':217 /\ mid_z:215 = z':218 /\ 0 = K:216
         /\ (K:213 + K:216) = K:219 /\ 0 <= K:219 /\ 0 <= i':217
         /\ 0 <= z':218 /\ param0:23 <= i':217
         /\ (((havoc:272 < 0 \/ 0 < havoc:272) /\ 0 <= __cost:102
                /\ 0 <= (__cost:102 + 10000)
                /\ (__cost:102 + 10000) = phi___cost:273)
               \/ (0 <= havoc:272 /\ havoc:272 <= 0
                     /\ __cost:102 = phi___cost:273)))}

Evaluating variable number 27 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,67)_g1> -> <__pstate, (Unique State Name,80)_g1>	Base relation: 
{N := 10000000005
 z := z':218
 i := i':217
 x := param0:23
 param0 := (10000000005
              + -(ite(((0 <= z':218 /\ 0 <= param0:23)
                         \/ (!(0 <= z':218) /\ !(0 <= param0:23))),
                      floor((z':218 / param0:23)),
                      -(floor(-((z':218 / param0:23)))))))
 param0@pos := type_err:220
 param0@width := type_err:221
 when ((!(0 <= K:213) \/ mid_i:214 = K:213)
         /\ (!(0 <= K:213) \/ mid_z:215 = (10000000005 * K:213))
         /\ ((K:213 = 0 /\ 0 = mid_i:214 /\ 0 = mid_z:215)
               \/ (1 <= K:213 /\ (-10000000005 + 10000000005) = 0
                     /\ 0 <= (-1 + param0:23)
                     /\ (-10000000005 + 10000000005) = 0
                     /\ 0 <= (-10000000005 + mid_z:215)
                     /\ 0 <= (-1 + mid_i:214)
                     /\ 0 <= (param0:23 + -mid_i:214))) /\ K:216 = 0
         /\ mid_i:214 = i':217 /\ mid_z:215 = z':218 /\ 0 = K:216
         /\ (K:213 + K:216) = K:219 /\ 0 <= K:219 /\ 0 <= i':217
         /\ 0 <= z':218 /\ param0:23 <= i':217)}	
<__pstate, accept> -> <__pstate, (Unique State Name,79)_g1>	Base relation: 
{__cost := 0
 argc := param0:23
 argv := param1:26
 param0 := tr:193
 argv@pos := param1@pos:25
 param0@pos := type_err:194
 argv@width := param1@width:24
 param0@width := type_err:195
 when (2 <= param0:23 /\ param0:23 <= 2)}	
<__pstate, accept> -> <__pstate, (Unique State Name,67)_g1>	Base relation: 
{__cost := 0
 val := havoc:287
 argc := param0:23
 argv := param1:26
 param0 := havoc:287
 argv@pos := param1@pos:25
 param0@pos := type_err:288
 argv@width := param1@width:24
 param0@width := type_err:289
 when (2 <= param0:23 /\ param0:23 <= 2 /\ 1 <= havoc:287
         /\ havoc:287 <= 10000000)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x5b04c70: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x514f630: 
	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,80)_g1 , __done )	Base relation: 
{__cost := 0
 val := havoc:287
 argc := param0:23
 argv := param1:26
 N := 10000000005
 z := z':329
 i := i':328
 x := havoc:287
 param0 := (10000000005
              + -(ite(((0 <= z':329 /\ 0 <= havoc:287)
                         \/ (!(0 <= z':329) /\ !(0 <= havoc:287))),
                      floor((z':329 / havoc:287)),
                      -(floor(-((z':329 / havoc:287)))))))
 argv@pos := param1@pos:25
 param0@pos := type_err:331
 argv@width := param1@width:24
 param0@width := type_err:332
 when (2 <= param0:23 /\ param0:23 <= 2 /\ 1 <= havoc:287
         /\ havoc:287 <= 10000000 /\ (!(0 <= K:324) \/ mid_i:325 = K:324)
         /\ (!(0 <= K:324) \/ mid_z:326 = (10000000005 * K:324))
         /\ ((K:324 = 0 /\ 0 = mid_i:325 /\ 0 = mid_z:326)
               \/ (1 <= K:324 /\ (-10000000005 + 10000000005) = 0
                     /\ 0 <= (-1 + havoc:287)
                     /\ (-10000000005 + 10000000005) = 0
                     /\ 0 <= (-10000000005 + mid_z:326)
                     /\ 0 <= (-1 + mid_i:325)
                     /\ 0 <= (havoc:287 + -mid_i:325))) /\ K:327 = 0
         /\ mid_i:325 = i':328 /\ mid_z:326 = z':329 /\ 0 = K:327
         /\ (K:324 + K:327) = K:330 /\ 0 <= K:330 /\ 0 <= i':328
         /\ 0 <= z':329 /\ havoc:287 <= i':328)}
    ( __pstate , (Unique State Name,79)_g1 , __done )	Base relation: 
{__cost := 0
 argc := param0:23
 argv := param1:26
 param0 := tr:193
 argv@pos := param1@pos:25
 param0@pos := type_err:194
 argv@width := param1@width:24
 param0@width := type_err:195
 when (2 <= param0:23 /\ param0:23 <= 2)}
    ( __pstate , (Unique State Name,67)_g1 , __done )	Base relation: 
{__cost := 0
 val := havoc:287
 argc := param0:23
 argv := param1:26
 param0 := havoc:287
 argv@pos := param1@pos:25
 param0@pos := type_err:288
 argv@width := param1@width:24
 param0@width := type_err:289
 when (2 <= param0:23 /\ param0:23 <= 2 /\ 1 <= havoc:287
         /\ havoc:287 <= 10000000)}

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

------------------------------------------------
Procedure summary for atoi

Base relation: 
{}

------------------------------------------------
Procedure summary for fabs

Base relation: 
{}

------------------------------------------------
Procedure summary for function

Base relation: 
{__cost := phi___cost:316
 N := 10000000005
 z := z':218
 i := i':217
 x := param0:23
 return := havoc:317
 param0 := (10000000005
              + -(ite(((0 <= z':218 /\ 0 <= param0:23)
                         \/ (!(0 <= z':218) /\ !(0 <= param0:23))),
                      floor((z':218 / param0:23)),
                      -(floor(-((z':218 / param0:23)))))))
 return@pos := type_err:318
 param0@pos := type_err:220
 return@width := type_err:319
 param0@width := type_err:221
 when ((!(0 <= K:213) \/ mid_i:214 = K:213)
         /\ (!(0 <= K:213) \/ mid_z:215 = (10000000005 * K:213))
         /\ ((K:213 = 0 /\ 0 = mid_i:214 /\ 0 = mid_z:215)
               \/ (1 <= K:213 /\ (-10000000005 + 10000000005) = 0
                     /\ 0 <= (-1 + param0:23)
                     /\ (-10000000005 + 10000000005) = 0
                     /\ 0 <= (-10000000005 + mid_z:215)
                     /\ 0 <= (-1 + mid_i:214)
                     /\ 0 <= (param0:23 + -mid_i:214))) /\ K:216 = 0
         /\ mid_i:214 = i':217 /\ mid_z:215 = z':218 /\ 0 = K:216
         /\ (K:213 + K:216) = K:219 /\ 0 <= K:219 /\ 0 <= i':217
         /\ 0 <= z':218 /\ param0:23 <= i':217
         /\ (((havoc:315 < 0 \/ 0 < havoc:315) /\ 0 <= __cost:102
                /\ 0 <= (__cost:102 + 10000)
                /\ (__cost:102 + 10000) = phi___cost:316)
               \/ (0 <= havoc:315 /\ havoc:315 <= 0
                     /\ __cost:102 = phi___cost:316)))}

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

Base relation: 
{__cost := phi___cost:312
 val := phi_val:311
 __retres5 := phi___retres5:310
 argc := param0:23
 argv := param1:26
 return := phi___retres5:310
 param0 := phi_param0:308
 argv@pos := param1@pos:25
 return@pos := type_err:313
 param0@pos := phi_param0@pos:306
 argv@width := param1@width:24
 return@width := type_err:314
 param0@width := phi_param0@width:304
 when (((((((param0:23 < 2 \/ 2 < param0:23) /\ val:5 = phi_val:281
              /\ param0:23 = phi_param0:280
              /\ param0@pos:22 = phi_param0@pos:279
              /\ param0@width:21 = phi_param0@width:278)
             \/ (2 <= param0:23 /\ param0:23 <= 2 /\ havoc:277 < 1
                   /\ havoc:277 = phi_val:281 /\ tr:193 = phi_param0:280
                   /\ type_err:194 = phi_param0@pos:279
                   /\ type_err:195 = phi_param0@width:278))
            /\ phi_val:281 = phi_val:286 /\ phi_param0:280 = phi_param0:285
            /\ phi_param0@pos:279 = phi_param0@pos:284
            /\ phi_param0@width:278 = phi_param0@width:283)
           \/ (2 <= param0:23 /\ param0:23 <= 2 /\ 1 <= havoc:282
                 /\ 10000000 < havoc:282 /\ havoc:282 = phi_val:286
                 /\ tr:193 = phi_param0:285
                 /\ type_err:194 = phi_param0@pos:284
                 /\ type_err:195 = phi_param0@width:283))
          /\ 0 = phi___cost:312 /\ phi_val:286 = phi_val:311
          /\ -1 = phi___retres5:310 /\ return:265 = phi_return:309
          /\ phi_param0:285 = phi_param0:308
          /\ return@pos:262 = phi_return@pos:307
          /\ phi_param0@pos:284 = phi_param0@pos:306
          /\ return@width:259 = phi_return@width:305
          /\ phi_param0@width:283 = phi_param0@width:304)
         \/ (2 <= param0:23 /\ param0:23 <= 2 /\ 1 <= havoc:287
               /\ havoc:287 <= 10000000
               /\ (!(0 <= K:290) \/ mid_i:291 = K:290)
               /\ (!(0 <= K:290) \/ mid_z:292 = (10000000005 * K:290))
               /\ ((K:290 = 0 /\ 0 = mid_i:291 /\ 0 = mid_z:292)
                     \/ (1 <= K:290 /\ (-10000000005 + 10000000005) = 0
                           /\ 0 <= (-1 + havoc:287)
                           /\ (-10000000005 + 10000000005) = 0
                           /\ 0 <= (-10000000005 + mid_z:292)
                           /\ 0 <= (-1 + mid_i:291)
                           /\ 0 <= (havoc:287 + -mid_i:291))) /\ K:293 = 0
               /\ mid_i:291 = i':294 /\ mid_z:292 = z':295 /\ 0 = K:293
               /\ (K:290 + K:293) = K:296 /\ 0 <= K:296 /\ 0 <= i':294
               /\ 0 <= z':295 /\ havoc:287 <= i':294
               /\ (((havoc:297 < 0 \/ 0 < havoc:297)
                      /\ 10000 = phi___cost:298)
                     \/ (0 <= havoc:297 /\ havoc:297 <= 0
                           /\ 0 = phi___cost:298))
               /\ phi___cost:298 = phi___cost:312 /\ havoc:287 = phi_val:311
               /\ 0 = phi___retres5:310 /\ havoc:299 = phi_return:309
               /\ (10000000005
                     + -(ite(((0 <= z':295 /\ 0 <= havoc:287)
                                \/ (!(0 <= z':295) /\ !(0 <= havoc:287))),
                             floor((z':295 / havoc:287)),
                             -(floor(-((z':295 / havoc:287))))))) = phi_param0:308
               /\ type_err:300 = phi_return@pos:307
               /\ type_err:301 = phi_param0@pos:306
               /\ type_err:302 = phi_return@width:305
               /\ type_err:303 = phi_param0@width:304))}

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

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

Variable bounds at line 13 in function

min((10000 + __cost), __cost) <= __cost
__cost is o(1)
__cost <= max((10000 + __cost), __cost)
__cost is O(1)

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