/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, 37> -> <Unique State Name, 18>	Base relation: 
{i := 0
 n := param0:27}	
<Unique State Name, 22> -> <Unique State Name, 18>	Base relation: 
{__cost := (__cost:66 + 1)
 i := (i:64 + 1)
 when (i:64 < n:65 /\ 0 <= __cost:66 /\ 0 <= (__cost:66 + 1))}	
<Unique State Name, 22> -> <Unique State Name, 33>	Base relation: 
{when n:65 <= i:64}	
<Unique State Name, 45> -> <Unique State Name, 8>	Base relation: 
{__cost := 0
 argv := param1:30
 argv@pos := param1@pos:29
 argv@width := param1@width:28}	
<Unique State Name, 8> -> <Unique State Name, 9>	Base relation: 
{tmp___0 := 0
 when (0 <= tr:7 /\ tr:6 <= 0)}	
<Unique State Name, 8> -> <Unique State Name, 44>	Base relation: 
{param0 := tr:39
 param0@pos := type_err:40
 param0@width := type_err:41
 when (tr:5 < 0 \/ 0 < tr:4)}	
<Unique State Name, 9> -> <Unique State Name, 40>	Base relation: 
{param0 := tmp___0:8
 param0@pos := type_err:37
 param0@width := type_err:38}	
<Unique State Name, 18> -> <Unique State Name, 50>	Base relation: 
{when 0 <= i:64}	
<Unique State Name, 47> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 48> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 39> -> <Unique State Name, 48>	Base relation: 
{return := 0
 return@pos := type_err:35
 return@width := type_err:36}	
<Unique State Name, 33> -> <Unique State Name, 47>	Base relation: 
{return := havoc:67
 return@pos := type_err:70
 return@width := type_err:71}	
<Unique State Name, 44> -> <Unique State Name, 49 43>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 50> -> <Unique State Name, 22>	Base relation: 
{}	
<Unique State Name, 40> -> <Unique State Name, 37 39>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 49> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 43> -> <Unique State Name, 9>	Base relation: 
{tmp___0 := havoc:19}	
#################################################################
           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:66 + 1)
 i := (i:64 + 1)
 when (0 <= i:64 /\ i:64 < n:65 /\ 0 <= __cost:66 /\ 0 <= (__cost:66 + 1))}
**** alpha hat: 
  {<Split [true
            (i':140) = (1)*(i:64) + 1
           (__cost':139) = (1)*(__cost:66) + 1
           }
          pre:
            [|-i:64+n:65-1>=0; __cost:66>=0; i:64>=0|]
          post:
            [|i':140-1>=0; __cost':139-1>=0; n:65-i':140>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':139
   i := i':140
   when ((!(0 <= K:149) \/ mid_i:151 = (i:64 + K:149))
           /\ (!(0 <= K:149) \/ mid___cost:152 = (__cost:66 + K:149))
           /\ ((K:149 = 0 /\ i:64 = mid_i:151 /\ __cost:66 = mid___cost:152)
                 \/ (1 <= K:149 /\ 0 <= (-1 + -i:64 + n:65) /\ 0 <= __cost:66
                       /\ 0 <= i:64 /\ 0 <= (-1 + mid_i:151)
                       /\ 0 <= (-1 + mid___cost:152)
                       /\ 0 <= (n:65 + -mid_i:151))) /\ K:150 = 0
           /\ mid_i:151 = i':140 /\ mid___cost:152 = __cost':139 /\ 0 = K:150
           /\ (K:149 + K:150) = K:148 /\ 0 <= K:148)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
11  13  20  


New-style (IRE) regular expression in IREregExpMap for reID=11: 
Dot(
  Dot(
    Dot(
      Plus(
        Weight(Base relation: 
          {__cost := 0
           tmp___0 := 0
           argv := param1:30
           argv@pos := param1@pos:29
           argv@width := param1@width:28
           when (0 <= tr:137 /\ tr:138 <= 0)}        )
        ,
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := 0
               argv := param1:30
               param0 := tr:134
               argv@pos := param1@pos:29
               param0@pos := type_err:135
               argv@width := param1@width:28
               param0@width := type_err:136
               when (tr:132 < 0 \/ 0 < tr:133)}            )
            ,
            Var(13)
          )
          ,
          Weight(Base relation: 
            {tmp___0 := havoc:19}          )
        )
      )
      ,
      Weight(Base relation: 
        {param0 := tmp___0:8
         param0@pos := type_err:37
         param0@width := type_err:38}      )
    )
    ,
    Var(20)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:35
     return@width := type_err:36}  )
)


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


New-style (IRE) regular expression in IREregExpMap for reID=20: 
Weight(Base relation: 
  {__cost := __cost':158
   i := i':157
   n := param0:27
   return := havoc:160
   return@pos := type_err:161
   return@width := type_err:162
   when ((!(0 <= K:153) \/ mid_i:154 = K:153)
           /\ (!(0 <= K:153) \/ mid___cost:155 = (__cost:66 + K:153))
           /\ ((K:153 = 0 /\ 0 = mid_i:154 /\ __cost:66 = mid___cost:155)
                 \/ (1 <= K:153 /\ 0 <= (-1 + param0:27) /\ 0 <= __cost:66
                       /\ 0 <= (-1 + mid_i:154) /\ 0 <= (-1 + mid___cost:155)
                       /\ 0 <= (param0:27 + -mid_i:154))) /\ K:156 = 0
           /\ mid_i:154 = i':157 /\ mid___cost:155 = __cost':158 /\ 0 = K:156
           /\ (K:153 + K:156) = K:159 /\ 0 <= K:159 /\ 0 <= i':157
           /\ param0:27 <= i':157)})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Dot(
      Dot(
        Plus(
          Weight(Base relation: 
            {__cost := 0
             tmp___0 := 0
             argv := param1:30
             argv@pos := param1@pos:29
             argv@width := param1@width:28
             when (0 <= tr:137 /\ tr:138 <= 0)}          )
          ,
          Dot(
            Dot(
              Weight(Base relation: 
                {__cost := 0
                 argv := param1:30
                 param0 := tr:134
                 argv@pos := param1@pos:29
                 param0@pos := type_err:135
                 argv@width := param1@width:28
                 param0@width := type_err:136
                 when (tr:132 < 0 \/ 0 < tr:133)}              )
              ,
              Var(13)
            )
            ,
            Weight(Base relation: 
              {tmp___0 := havoc:19}            )
          )
        )
        ,
        Weight(Base relation: 
          {param0 := tmp___0:8
           param0@pos := type_err:37
           param0@width := type_err:38}        )
      )
      ,
      Var(20)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:35
       return@width := type_err:36}    )
  )
)



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

One()



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

Weight(Base relation: 
  {__cost := __cost':158
   return := havoc:160
   return@pos := type_err:161
   return@width := type_err:162
   when ((!(0 <= K:153) \/ mid_i:154 = K:153)
           /\ (!(0 <= K:153) \/ mid___cost:155 = (__cost:66 + K:153))
           /\ ((K:153 = 0 /\ 0 = mid_i:154 /\ __cost:66 = mid___cost:155)
                 \/ (1 <= K:153 /\ 0 <= (-1 + param0:27) /\ 0 <= __cost:66
                       /\ 0 <= (-1 + mid_i:154) /\ 0 <= (-1 + mid___cost:155)
                       /\ 0 <= (param0:27 + -mid_i:154))) /\ K:156 = 0
           /\ mid_i:154 = i':157 /\ mid___cost:155 = __cost':158 /\ 0 = K:156
           /\ (K:153 + K:156) = K:159 /\ 0 <= K:159 /\ 0 <= i':157
           /\ param0:27 <= i':157)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=11: 
Weight(Base relation: 
  {__cost := __cost':175
   return := 0
   param0 := phi_tmp___0:167
   return@pos := type_err:180
   param0@pos := type_err:168
   return@width := type_err:181
   param0@width := type_err:169
   when (((0 <= tr:137 /\ tr:138 <= 0 /\ 0 = phi_tmp___0:167
             /\ param0:27 = phi_param0:166
             /\ param0@pos:26 = phi_param0@pos:165
             /\ param0@width:25 = phi_param0@width:164)
            \/ ((tr:132 < 0 \/ 0 < tr:133) /\ havoc:163 = phi_tmp___0:167
                  /\ tr:134 = phi_param0:166
                  /\ type_err:135 = phi_param0@pos:165
                  /\ type_err:136 = phi_param0@width:164))
           /\ (!(0 <= K:170) \/ mid_i:171 = K:170)
           /\ (!(0 <= K:170) \/ mid___cost:172 = K:170)
           /\ ((K:170 = 0 /\ 0 = mid_i:171 /\ 0 = mid___cost:172)
                 \/ (1 <= K:170 /\ 0 <= (-1 + phi_tmp___0:167)
                       /\ 0 <= (-1 + mid_i:171) /\ 0 <= (-1 + mid___cost:172)
                       /\ 0 <= (phi_tmp___0:167 + -mid_i:171))) /\ K:173 = 0
           /\ mid_i:171 = i':174 /\ mid___cost:172 = __cost':175 /\ 0 = K:173
           /\ (K:170 + K:173) = K:176 /\ 0 <= K:176 /\ 0 <= i':174
           /\ phi_tmp___0:167 <= i':174)})


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


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=20: 
Weight(Base relation: 
  {__cost := __cost':158
   return := havoc:160
   return@pos := type_err:161
   return@width := type_err:162
   when ((!(0 <= K:153) \/ mid_i:154 = K:153)
           /\ (!(0 <= K:153) \/ mid___cost:155 = (__cost:66 + K:153))
           /\ ((K:153 = 0 /\ 0 = mid_i:154 /\ __cost:66 = mid___cost:155)
                 \/ (1 <= K:153 /\ 0 <= (-1 + param0:27) /\ 0 <= __cost:66
                       /\ 0 <= (-1 + mid_i:154) /\ 0 <= (-1 + mid___cost:155)
                       /\ 0 <= (param0:27 + -mid_i:154))) /\ K:156 = 0
           /\ mid_i:154 = i':157 /\ mid___cost:155 = __cost':158 /\ 0 = K:156
           /\ (K:153 + K:156) = K:159 /\ 0 <= K:159 /\ 0 <= i':157
           /\ param0:27 <= i':157)})


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

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':175
 return := 0
 param0 := phi_tmp___0:167
 return@pos := type_err:180
 param0@pos := type_err:168
 return@width := type_err:181
 param0@width := type_err:169
 when (((0 <= tr:137 /\ tr:138 <= 0 /\ 0 = phi_tmp___0:167
           /\ param0:27 = phi_param0:166
           /\ param0@pos:26 = phi_param0@pos:165
           /\ param0@width:25 = phi_param0@width:164)
          \/ ((tr:132 < 0 \/ 0 < tr:133) /\ havoc:163 = phi_tmp___0:167
                /\ tr:134 = phi_param0:166
                /\ type_err:135 = phi_param0@pos:165
                /\ type_err:136 = phi_param0@width:164))
         /\ (!(0 <= K:170) \/ mid_i:171 = K:170)
         /\ (!(0 <= K:170) \/ mid___cost:172 = K:170)
         /\ ((K:170 = 0 /\ 0 = mid_i:171 /\ 0 = mid___cost:172)
               \/ (1 <= K:170 /\ 0 <= (-1 + phi_tmp___0:167)
                     /\ 0 <= (-1 + mid_i:171) /\ 0 <= (-1 + mid___cost:172)
                     /\ 0 <= (phi_tmp___0:167 + -mid_i:171))) /\ K:173 = 0
         /\ mid_i:171 = i':174 /\ mid___cost:172 = __cost':175 /\ 0 = K:173
         /\ (K:170 + K:173) = K:176 /\ 0 <= K:176 /\ 0 <= i':174
         /\ phi_tmp___0:167 <= i':174)}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

Evaluating variable number 20 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':158
 return := havoc:160
 return@pos := type_err:161
 return@width := type_err:162
 when ((!(0 <= K:153) \/ mid_i:154 = K:153)
         /\ (!(0 <= K:153) \/ mid___cost:155 = (__cost:66 + K:153))
         /\ ((K:153 = 0 /\ 0 = mid_i:154 /\ __cost:66 = mid___cost:155)
               \/ (1 <= K:153 /\ 0 <= (-1 + param0:27) /\ 0 <= __cost:66
                     /\ 0 <= (-1 + mid_i:154) /\ 0 <= (-1 + mid___cost:155)
                     /\ 0 <= (param0:27 + -mid_i:154))) /\ K:156 = 0
         /\ mid_i:154 = i':157 /\ mid___cost:155 = __cost':158 /\ 0 = K:156
         /\ (K:153 + K:156) = K:159 /\ 0 <= K:159 /\ 0 <= i':157
         /\ param0:27 <= i':157)}

    (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,37)_g1>	Base relation: 
{__cost := 0
 tmp___0 := phi_tmp___0:186
 argv := param1:30
 param0 := phi_tmp___0:186
 argv@pos := param1@pos:29
 param0@pos := type_err:187
 argv@width := param1@width:28
 param0@width := type_err:188
 when ((0 <= tr:137 /\ tr:138 <= 0 /\ 0 = phi_tmp___0:186
          /\ param0:27 = phi_param0:185 /\ param0@pos:26 = phi_param0@pos:184
          /\ param0@width:25 = phi_param0@width:183)
         \/ ((tr:132 < 0 \/ 0 < tr:133) /\ havoc:182 = phi_tmp___0:186
               /\ tr:134 = phi_param0:185
               /\ type_err:135 = phi_param0@pos:184
               /\ type_err:136 = phi_param0@width:183))}	
<__pstate, accept> -> <__pstate, (Unique State Name,49)_g1>	Base relation: 
{__cost := 0
 argv := param1:30
 param0 := tr:134
 argv@pos := param1@pos:29
 param0@pos := type_err:135
 argv@width := param1@width:28
 param0@width := type_err:136
 when (tr:132 < 0 \/ 0 < tr:133)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x160ccd0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x52fbb50: 
	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,37)_g1 , __done )	Base relation: 
{__cost := 0
 tmp___0 := phi_tmp___0:186
 argv := param1:30
 param0 := phi_tmp___0:186
 argv@pos := param1@pos:29
 param0@pos := type_err:187
 argv@width := param1@width:28
 param0@width := type_err:188
 when ((0 <= tr:137 /\ tr:138 <= 0 /\ 0 = phi_tmp___0:186
          /\ param0:27 = phi_param0:185 /\ param0@pos:26 = phi_param0@pos:184
          /\ param0@width:25 = phi_param0@width:183)
         \/ ((tr:132 < 0 \/ 0 < tr:133) /\ havoc:182 = phi_tmp___0:186
               /\ tr:134 = phi_param0:185
               /\ type_err:135 = phi_param0@pos:184
               /\ type_err:136 = phi_param0@width:183))}
    ( __pstate , (Unique State Name,49)_g1 , __done )	Base relation: 
{__cost := 0
 argv := param1:30
 param0 := tr:134
 argv@pos := param1@pos:29
 param0@pos := type_err:135
 argv@width := param1@width:28
 param0@width := type_err:136
 when (tr:132 < 0 \/ 0 < tr:133)}

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

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

Base relation: 
{}

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

Base relation: 
{__cost := __cost':194
 tmp___0 := phi_tmp___0:186
 argv := param1:30
 return := 0
 param0 := phi_tmp___0:186
 argv@pos := param1@pos:29
 return@pos := type_err:199
 param0@pos := type_err:187
 argv@width := param1@width:28
 return@width := type_err:200
 param0@width := type_err:188
 when (((0 <= tr:137 /\ tr:138 <= 0 /\ 0 = phi_tmp___0:186
           /\ param0:27 = phi_param0:185
           /\ param0@pos:26 = phi_param0@pos:184
           /\ param0@width:25 = phi_param0@width:183)
          \/ ((tr:132 < 0 \/ 0 < tr:133) /\ havoc:182 = phi_tmp___0:186
                /\ tr:134 = phi_param0:185
                /\ type_err:135 = phi_param0@pos:184
                /\ type_err:136 = phi_param0@width:183))
         /\ (!(0 <= K:189) \/ mid_i:190 = K:189)
         /\ (!(0 <= K:189) \/ mid___cost:191 = K:189)
         /\ ((K:189 = 0 /\ 0 = mid_i:190 /\ 0 = mid___cost:191)
               \/ (1 <= K:189 /\ 0 <= (-1 + phi_tmp___0:186)
                     /\ 0 <= (-1 + mid_i:190) /\ 0 <= (-1 + mid___cost:191)
                     /\ 0 <= (phi_tmp___0:186 + -mid_i:190))) /\ K:192 = 0
         /\ mid_i:190 = i':193 /\ mid___cost:191 = __cost':194 /\ 0 = K:192
         /\ (K:189 + K:192) = K:195 /\ 0 <= K:195 /\ 0 <= i':193
         /\ phi_tmp___0:186 <= i':193)}

------------------------------------------------
Procedure summary for work

Base relation: 
{__cost := __cost':158
 i := i':157
 n := param0:27
 return := havoc:160
 return@pos := type_err:161
 return@width := type_err:162
 when ((!(0 <= K:153) \/ mid_i:154 = K:153)
         /\ (!(0 <= K:153) \/ mid___cost:155 = (__cost:66 + K:153))
         /\ ((K:153 = 0 /\ 0 = mid_i:154 /\ __cost:66 = mid___cost:155)
               \/ (1 <= K:153 /\ 0 <= (-1 + param0:27) /\ 0 <= __cost:66
                     /\ 0 <= (-1 + mid_i:154) /\ 0 <= (-1 + mid___cost:155)
                     /\ 0 <= (param0:27 + -mid_i:154))) /\ K:156 = 0
         /\ mid_i:154 = i':157 /\ mid___cost:155 = __cost':158 /\ 0 = K:156
         /\ (K:153 + K:156) = K:159 /\ 0 <= K:159 /\ 0 <= i':157
         /\ param0:27 <= i':157)}

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

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

Variable bounds at line 7 in work

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

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