/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, 53> -> <Unique State Name, 50 52>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 15> -> <Unique State Name, 53>	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
<Unique State Name, 56> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 46> -> <Unique State Name, 22>	Base relation: 
{x := 0
 n := param0:53}	
<Unique State Name, 22> -> <Unique State Name, 57>	Base relation: 
{when 0 <= x:62}	
<Unique State Name, 48> -> <Unique State Name, 17>	Base relation: 
{}	
<Unique State Name, 54> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 49> -> <Unique State Name, 46 48>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 57> -> <Unique State Name, 26>	Base relation: 
{}	
<Unique State Name, 17> -> <Unique State Name, 55>	Base relation: 
{return := havoc:41
 return@pos := type_err:44
 return@width := type_err:45}	
<Unique State Name, 50> -> <Unique State Name, 49>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
<Unique State Name, 52> -> <Unique State Name, 56>	Base relation: 
{return := 0
 return@pos := type_err:19
 return@width := type_err:20
 when ((0 < n:2 /\ n:2 = phi_tmp___0:14) \/ (n:2 <= 0 /\ 0 = phi_tmp___0:14))}	
<Unique State Name, 26> -> <Unique State Name, 22>	Base relation: 
{__cost := (__cost:64 + 1)
 x := (x:62 + 1)
 when (x:62 < n:63 /\ 0 <= __cost:64 /\ 0 <= (__cost:64 + 1)
         /\ (!(havoc:72 = 0) \/ havoc:72 = 0))}	
<Unique State Name, 26> -> <Unique State Name, 54>	Base relation: 
{return := havoc:73
 return@pos := type_err:74
 return@width := type_err:75
 when n:63 <= x:62}	
<Unique State Name, 55> -> <Unique State Name, >	Base relation: 
{}	
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:64 + 1)
 x := (x:62 + 1)
 when (0 <= x:62 /\ x:62 < n:63 /\ 0 <= __cost:64 /\ 0 <= (__cost:64 + 1)
         /\ (!(havoc:131 = 0) \/ havoc:131 = 0))}
**** alpha hat: 
  {<Split [true
            (x':133) = (1)*(x:62) + 1
           (__cost':132) = (1)*(__cost:64) + 1
           }
          pre:
            [|-x:62+n:63-1>=0; __cost:64>=0; x:62>=0|]
          post:
            [|x':133-1>=0; __cost':132-1>=0; n:63-x':133>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':132
   x := x':133
   when ((!(0 <= K:142) \/ mid_x:144 = (x:62 + K:142))
           /\ (!(0 <= K:142) \/ mid___cost:145 = (__cost:64 + K:142))
           /\ ((K:142 = 0 /\ x:62 = mid_x:144 /\ __cost:64 = mid___cost:145)
                 \/ (1 <= K:142 /\ 0 <= (-1 + -x:62 + n:63) /\ 0 <= __cost:64
                       /\ 0 <= x:62 /\ 0 <= (-1 + mid_x:144)
                       /\ 0 <= (-1 + mid___cost:145)
                       /\ 0 <= (n:63 + -mid_x:144))) /\ K:143 = 0
           /\ mid_x:144 = x':133 /\ mid___cost:145 = __cost':132 /\ 0 = K:143
           /\ (K:142 + K:143) = K:141 /\ 0 <= K:141)}
}
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
       n := havoc:13
       param0 := havoc:13
       param0@pos := type_err:17
       param0@width := type_err:18}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:19
     return@width := type_err:20
     when ((0 < n:2 /\ n:2 = phi_tmp___0:14)
             \/ (n:2 <= 0 /\ 0 = phi_tmp___0:14))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:53
       param0@pos := type_err:54
       param0@width := type_err:55}    )
    ,
    Var(19)
  )
  ,
  Weight(Base relation: 
    {return := havoc:41
     return@pos := type_err:44
     return@width := type_err:45}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=19: 
Weight(Base relation: 
  {__cost := __cost':151
   x := x':150
   n := param0:53
   return := havoc:153
   return@pos := type_err:154
   return@width := type_err:155
   when ((!(0 <= K:146) \/ mid_x:147 = K:146)
           /\ (!(0 <= K:146) \/ mid___cost:148 = (__cost:64 + K:146))
           /\ ((K:146 = 0 /\ 0 = mid_x:147 /\ __cost:64 = mid___cost:148)
                 \/ (1 <= K:146 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:64
                       /\ 0 <= (-1 + mid_x:147) /\ 0 <= (-1 + mid___cost:148)
                       /\ 0 <= (param0:53 + -mid_x:147))) /\ K:149 = 0
           /\ mid_x:147 = x':150 /\ mid___cost:148 = __cost':151 /\ 0 = K:149
           /\ (K:146 + K:149) = K:152 /\ 0 <= K:152 /\ 0 <= x':150
           /\ param0:53 <= x':150)})



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
         n := havoc:13
         param0 := havoc:13
         param0@pos := type_err:17
         param0@width := type_err:18}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:19
       return@width := type_err:20
       when ((0 < n:2 /\ n:2 = phi_tmp___0:14)
               \/ (n:2 <= 0 /\ 0 = phi_tmp___0:14))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:53
         param0@pos := type_err:54
         param0@width := type_err:55}      )
      ,
      Var(19)
    )
    ,
    Weight(Base relation: 
      {return := havoc:41
       return@pos := type_err:44
       return@width := type_err:45}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':151
   return := havoc:153
   return@pos := type_err:154
   return@width := type_err:155
   when ((!(0 <= K:146) \/ mid_x:147 = K:146)
           /\ (!(0 <= K:146) \/ mid___cost:148 = (__cost:64 + K:146))
           /\ ((K:146 = 0 /\ 0 = mid_x:147 /\ __cost:64 = mid___cost:148)
                 \/ (1 <= K:146 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:64
                       /\ 0 <= (-1 + mid_x:147) /\ 0 <= (-1 + mid___cost:148)
                       /\ 0 <= (param0:53 + -mid_x:147))) /\ K:149 = 0
           /\ mid_x:147 = x':150 /\ mid___cost:148 = __cost':151 /\ 0 = K:149
           /\ (K:146 + K:149) = K:152 /\ 0 <= K:152 /\ 0 <= x':150
           /\ param0:53 <= x':150)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':174
   return := 0
   param0 := havoc:13
   return@pos := type_err:182
   param0@pos := type_err:178
   return@width := type_err:183
   param0@width := type_err:180
   when ((!(0 <= K:169) \/ mid_x:170 = K:169)
           /\ (!(0 <= K:169) \/ mid___cost:171 = K:169)
           /\ ((K:169 = 0 /\ 0 = mid_x:170 /\ 0 = mid___cost:171)
                 \/ (1 <= K:169 /\ 0 <= (-1 + havoc:13)
                       /\ 0 <= (-1 + mid_x:170) /\ 0 <= (-1 + mid___cost:171)
                       /\ 0 <= (havoc:13 + -mid_x:170))) /\ K:172 = 0
           /\ mid_x:170 = x':173 /\ mid___cost:171 = __cost':174 /\ 0 = K:172
           /\ (K:169 + K:172) = K:175 /\ 0 <= K:175 /\ 0 <= x':173
           /\ havoc:13 <= x':173
           /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:181)
                 \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:181)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':189
   return := havoc:194
   param0 := param0:53
   return@pos := type_err:195
   param0@pos := type_err:54
   return@width := type_err:196
   param0@width := type_err:55
   when ((!(0 <= K:184) \/ mid_x:185 = K:184)
           /\ (!(0 <= K:184) \/ mid___cost:186 = (__cost:64 + K:184))
           /\ ((K:184 = 0 /\ 0 = mid_x:185 /\ __cost:64 = mid___cost:186)
                 \/ (1 <= K:184 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:64
                       /\ 0 <= (-1 + mid_x:185) /\ 0 <= (-1 + mid___cost:186)
                       /\ 0 <= (param0:53 + -mid_x:185))) /\ K:187 = 0
           /\ mid_x:185 = x':188 /\ mid___cost:186 = __cost':189 /\ 0 = K:187
           /\ (K:184 + K:187) = K:190 /\ 0 <= K:190 /\ 0 <= x':188
           /\ param0:53 <= x':188)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=19: 
Weight(Base relation: 
  {__cost := __cost':151
   return := havoc:153
   return@pos := type_err:154
   return@width := type_err:155
   when ((!(0 <= K:146) \/ mid_x:147 = K:146)
           /\ (!(0 <= K:146) \/ mid___cost:148 = (__cost:64 + K:146))
           /\ ((K:146 = 0 /\ 0 = mid_x:147 /\ __cost:64 = mid___cost:148)
                 \/ (1 <= K:146 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:64
                       /\ 0 <= (-1 + mid_x:147) /\ 0 <= (-1 + mid___cost:148)
                       /\ 0 <= (param0:53 + -mid_x:147))) /\ K:149 = 0
           /\ mid_x:147 = x':150 /\ mid___cost:148 = __cost':151 /\ 0 = K:149
           /\ (K:146 + K:149) = K:152 /\ 0 <= K:152 /\ 0 <= x':150
           /\ param0:53 <= x':150)})


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':174
 return := 0
 param0 := havoc:13
 return@pos := type_err:182
 param0@pos := type_err:178
 return@width := type_err:183
 param0@width := type_err:180
 when ((!(0 <= K:169) \/ mid_x:170 = K:169)
         /\ (!(0 <= K:169) \/ mid___cost:171 = K:169)
         /\ ((K:169 = 0 /\ 0 = mid_x:170 /\ 0 = mid___cost:171)
               \/ (1 <= K:169 /\ 0 <= (-1 + havoc:13)
                     /\ 0 <= (-1 + mid_x:170) /\ 0 <= (-1 + mid___cost:171)
                     /\ 0 <= (havoc:13 + -mid_x:170))) /\ K:172 = 0
         /\ mid_x:170 = x':173 /\ mid___cost:171 = __cost':174 /\ 0 = K:172
         /\ (K:169 + K:172) = K:175 /\ 0 <= K:175 /\ 0 <= x':173
         /\ havoc:13 <= x':173
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:181)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:181)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':189
 return := havoc:194
 param0 := param0:53
 return@pos := type_err:195
 param0@pos := type_err:54
 return@width := type_err:196
 param0@width := type_err:55
 when ((!(0 <= K:184) \/ mid_x:185 = K:184)
         /\ (!(0 <= K:184) \/ mid___cost:186 = (__cost:64 + K:184))
         /\ ((K:184 = 0 /\ 0 = mid_x:185 /\ __cost:64 = mid___cost:186)
               \/ (1 <= K:184 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:64
                     /\ 0 <= (-1 + mid_x:185) /\ 0 <= (-1 + mid___cost:186)
                     /\ 0 <= (param0:53 + -mid_x:185))) /\ K:187 = 0
         /\ mid_x:185 = x':188 /\ mid___cost:186 = __cost':189 /\ 0 = K:187
         /\ (K:184 + K:187) = K:190 /\ 0 <= K:190 /\ 0 <= x':188
         /\ param0:53 <= x':188)}

Evaluating variable number 19 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':151
 return := havoc:153
 return@pos := type_err:154
 return@width := type_err:155
 when ((!(0 <= K:146) \/ mid_x:147 = K:146)
         /\ (!(0 <= K:146) \/ mid___cost:148 = (__cost:64 + K:146))
         /\ ((K:146 = 0 /\ 0 = mid_x:147 /\ __cost:64 = mid___cost:148)
               \/ (1 <= K:146 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:64
                     /\ 0 <= (-1 + mid_x:147) /\ 0 <= (-1 + mid___cost:148)
                     /\ 0 <= (param0:53 + -mid_x:147))) /\ K:149 = 0
         /\ mid_x:147 = x':150 /\ mid___cost:148 = __cost':151 /\ 0 = K:149
         /\ (K:146 + K:149) = K:152 /\ 0 <= K:152 /\ 0 <= x':150
         /\ param0:53 <= x':150)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,50)_g1> -> <__pstate, (Unique State Name,46)_g1>	Base relation: 
{param0 := param0:53
 param0@pos := type_err:54
 param0@width := type_err:55}	
<__pstate, accept> -> <__pstate, (Unique State Name,50)_g1>	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x530fe40: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x531b600: 
	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,46)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:225
 param0@width := type_err:226}
    ( __pstate , (Unique State Name,50)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:13
 param0 := havoc:13
 param0@pos := type_err:17
 param0@width := type_err:18}

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

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

Base relation: 
{__cost := __cost':202
 n := havoc:13
 return := 0
 param0 := havoc:13
 return@pos := type_err:210
 param0@pos := type_err:206
 return@width := type_err:211
 param0@width := type_err:208
 when ((!(0 <= K:197) \/ mid_x:198 = K:197)
         /\ (!(0 <= K:197) \/ mid___cost:199 = K:197)
         /\ ((K:197 = 0 /\ 0 = mid_x:198 /\ 0 = mid___cost:199)
               \/ (1 <= K:197 /\ 0 <= (-1 + havoc:13)
                     /\ 0 <= (-1 + mid_x:198) /\ 0 <= (-1 + mid___cost:199)
                     /\ 0 <= (havoc:13 + -mid_x:198))) /\ K:200 = 0
         /\ mid_x:198 = x':201 /\ mid___cost:199 = __cost':202 /\ 0 = K:200
         /\ (K:197 + K:200) = K:203 /\ 0 <= K:203 /\ 0 <= x':201
         /\ havoc:13 <= x':201
         /\ ((0 < havoc:13 /\ havoc:13 = phi_tmp___0:209)
               \/ (havoc:13 <= 0 /\ 0 = phi_tmp___0:209)))}

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

Base relation: 
{__cost := __cost':217
 return := havoc:222
 param0 := param0:53
 return@pos := type_err:223
 param0@pos := type_err:54
 return@width := type_err:224
 param0@width := type_err:55
 when ((!(0 <= K:212) \/ mid_x:213 = K:212)
         /\ (!(0 <= K:212) \/ mid___cost:214 = (__cost:64 + K:212))
         /\ ((K:212 = 0 /\ 0 = mid_x:213 /\ __cost:64 = mid___cost:214)
               \/ (1 <= K:212 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:64
                     /\ 0 <= (-1 + mid_x:213) /\ 0 <= (-1 + mid___cost:214)
                     /\ 0 <= (param0:53 + -mid_x:213))) /\ K:215 = 0
         /\ mid_x:213 = x':216 /\ mid___cost:214 = __cost':217 /\ 0 = K:215
         /\ (K:212 + K:215) = K:218 /\ 0 <= K:218 /\ 0 <= x':216
         /\ param0:53 <= x':216)}

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

Base relation: 
{__cost := __cost':151
 x := x':150
 n := param0:53
 return := havoc:153
 return@pos := type_err:154
 return@width := type_err:155
 when ((!(0 <= K:146) \/ mid_x:147 = K:146)
         /\ (!(0 <= K:146) \/ mid___cost:148 = (__cost:64 + K:146))
         /\ ((K:146 = 0 /\ 0 = mid_x:147 /\ __cost:64 = mid___cost:148)
               \/ (1 <= K:146 /\ 0 <= (-1 + param0:53) /\ 0 <= __cost:64
                     /\ 0 <= (-1 + mid_x:147) /\ 0 <= (-1 + mid___cost:148)
                     /\ 0 <= (param0:53 + -mid_x:147))) /\ K:149 = 0
         /\ mid_x:147 = x':150 /\ mid___cost:148 = __cost':151 /\ 0 = K:149
         /\ (K:146 + K:149) = K:152 /\ 0 <= K:152 /\ 0 <= x':150
         /\ param0:53 <= x':150)}

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

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

Variable bounds at line 21 in run

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

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