/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, 6> -> <Unique State Name, 36>	Base relation: 
{}	
<Unique State Name, 14> -> <Unique State Name, 19>	Base relation: 
{M_ii := 0
 when tmp:16 = 0}	
<Unique State Name, 14> -> <Unique State Name, 33>	Base relation: 
{M_responseLength := 30
 when !(tmp:16 = 0)}	
<Unique State Name, 23> -> <Unique State Name, 19>	Base relation: 
{M_responseLength := (M_responseLength:18 + 1)
 M_ii := (M_ii:17 + 1)
 when M_ii:17 < 4}	
<Unique State Name, 23> -> <Unique State Name, 33>	Base relation: 
{when 4 <= M_ii:17}	
<Unique State Name, 37> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 39> -> <Unique State Name, 23>	Base relation: 
{}	
<Unique State Name, 19> -> <Unique State Name, 39>	Base relation: 
{when (M_ii:17 <= 4 /\ 0 <= M_ii:17 /\ 0 <= M_responseLength:18)}	
<Unique State Name, 3> -> <Unique State Name, 38>	Base relation: 
{return := havoc:0
 return@pos := type_err:3
 return@width := type_err:4}	
<Unique State Name, 34> -> <Unique State Name, 14>	Base relation: 
{M_responseLength := 0
 tmp := havoc:24}	
<Unique State Name, 38> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 33> -> <Unique State Name, 37>	Base relation: 
{return := havoc:19
 return@pos := type_err:22
 return@width := type_err:23}	
<Unique State Name, 36> -> <Unique State Name, 34 35>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 35> -> <Unique State Name, 3>	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: 
{M_responseLength := (M_responseLength:18 + 1)
 M_ii := (M_ii:17 + 1)
 when (M_ii:17 <= 4 /\ 0 <= M_ii:17 /\ 0 <= M_responseLength:18
         /\ M_ii:17 < 4)}
**** alpha hat: 
  {<Split [true
            (M_responseLength':113) = (1)*(M_responseLength:18) + 1
           (M_ii':114) = (1)*(M_ii:17) + 1
           }
          pre:
            [|-M_ii:17+3>=0; M_responseLength:18>=0; M_ii:17>=0|]
          post:
            [|-M_ii':114+4>=0; M_ii':114-1>=0; M_responseLength':113-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {M_responseLength := M_responseLength':113
   M_ii := M_ii':114
   when ((!(0 <= K:122)
            \/ mid_M_responseLength:125 = (M_responseLength:18 + K:122))
           /\ (!(0 <= K:122) \/ mid_M_ii:124 = (M_ii:17 + K:122))
           /\ ((K:122 = 0 /\ M_ii:17 = mid_M_ii:124
                  /\ M_responseLength:18 = mid_M_responseLength:125)
                 \/ (1 <= K:122 /\ 0 <= (3 + -M_ii:17)
                       /\ 0 <= M_responseLength:18 /\ 0 <= M_ii:17
                       /\ 0 <= (4 + -mid_M_ii:124)
                       /\ 0 <= (-1 + mid_M_ii:124)
                       /\ 0 <= (-1 + mid_M_responseLength:125))) /\ K:123 = 0
           /\ mid_M_ii:124 = M_ii':114
           /\ mid_M_responseLength:125 = M_responseLength':113 /\ 0 = K:123
           /\ (K:122 + K:123) = K:121 /\ 0 <= K:121)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
7  13  


New-style (IRE) regular expression in IREregExpMap for reID=7: 
Dot(
  Var(13)
  ,
  Weight(Base relation: 
    {return := havoc:0
     return@pos := type_err:3
     return@width := type_err:4}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Weight(Base relation: 
  {M_responseLength := phi_M_responseLength:134
   tmp := havoc:24
   M_ii := phi_M_ii:133
   return := havoc:135
   return@pos := type_err:136
   return@width := type_err:137
   when ((!(havoc:24 = 0) /\ 30 = phi_M_responseLength:134
            /\ M_ii:17 = phi_M_ii:133)
           \/ (havoc:24 = 0
                 /\ (!(0 <= K:126) \/ mid_M_responseLength:127 = K:126)
                 /\ (!(0 <= K:126) \/ mid_M_ii:128 = K:126)
                 /\ ((K:126 = 0 /\ 0 = mid_M_ii:128
                        /\ 0 = mid_M_responseLength:127)
                       \/ (1 <= K:126 /\ 0 <= (4 + -mid_M_ii:128)
                             /\ 0 <= (-1 + mid_M_ii:128)
                             /\ 0 <= (-1 + mid_M_responseLength:127)))
                 /\ K:129 = 0 /\ mid_M_ii:128 = M_ii':130
                 /\ mid_M_responseLength:127 = M_responseLength':131
                 /\ 0 = K:129 /\ (K:126 + K:129) = K:132 /\ 0 <= K:132
                 /\ M_ii':130 <= 4 /\ 0 <= M_ii':130
                 /\ 0 <= M_responseLength':131 /\ 4 <= M_ii':130
                 /\ M_responseLength':131 = phi_M_responseLength:134
                 /\ M_ii':130 = phi_M_ii:133))})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Var(13)
    ,
    Weight(Base relation: 
      {return := havoc:0
       return@pos := type_err:3
       return@width := type_err:4}    )
  )
)



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

Weight(Base relation: 
  {M_responseLength := phi_M_responseLength:134
   return := havoc:135
   return@pos := type_err:136
   return@width := type_err:137
   when ((!(havoc:24 = 0) /\ 30 = phi_M_responseLength:134
            /\ M_ii:138 = phi_M_ii:133)
           \/ (havoc:24 = 0
                 /\ (!(0 <= K:126) \/ mid_M_responseLength:127 = K:126)
                 /\ (!(0 <= K:126) \/ mid_M_ii:128 = K:126)
                 /\ ((K:126 = 0 /\ 0 = mid_M_ii:128
                        /\ 0 = mid_M_responseLength:127)
                       \/ (1 <= K:126 /\ 0 <= (4 + -mid_M_ii:128)
                             /\ 0 <= (-1 + mid_M_ii:128)
                             /\ 0 <= (-1 + mid_M_responseLength:127)))
                 /\ K:129 = 0 /\ mid_M_ii:128 = M_ii':130
                 /\ mid_M_responseLength:127 = M_responseLength':131
                 /\ 0 = K:129 /\ (K:126 + K:129) = K:132 /\ 0 <= K:132
                 /\ M_ii':130 <= 4 /\ 0 <= M_ii':130
                 /\ 0 <= M_responseLength':131 /\ 4 <= M_ii':130
                 /\ M_responseLength':131 = phi_M_responseLength:134
                 /\ M_ii':130 = phi_M_ii:133))})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=7: 
Weight(Base relation: 
  {M_responseLength := phi_M_responseLength:134
   return := havoc:139
   return@pos := type_err:140
   return@width := type_err:141
   when ((!(havoc:24 = 0) /\ 30 = phi_M_responseLength:134
            /\ M_ii:138 = phi_M_ii:133)
           \/ (havoc:24 = 0
                 /\ (!(0 <= K:126) \/ mid_M_responseLength:127 = K:126)
                 /\ (!(0 <= K:126) \/ mid_M_ii:128 = K:126)
                 /\ ((K:126 = 0 /\ 0 = mid_M_ii:128
                        /\ 0 = mid_M_responseLength:127)
                       \/ (1 <= K:126 /\ 0 <= (4 + -mid_M_ii:128)
                             /\ 0 <= (-1 + mid_M_ii:128)
                             /\ 0 <= (-1 + mid_M_responseLength:127)))
                 /\ K:129 = 0 /\ mid_M_ii:128 = M_ii':130
                 /\ mid_M_responseLength:127 = M_responseLength':131
                 /\ 0 = K:129 /\ (K:126 + K:129) = K:132 /\ 0 <= K:132
                 /\ M_ii':130 <= 4 /\ 0 <= M_ii':130
                 /\ 0 <= M_responseLength':131 /\ 4 <= M_ii':130
                 /\ M_responseLength':131 = phi_M_responseLength:134
                 /\ M_ii':130 = phi_M_ii:133))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {M_responseLength := phi_M_responseLength:134
   return := havoc:135
   return@pos := type_err:136
   return@width := type_err:137
   when ((!(havoc:24 = 0) /\ 30 = phi_M_responseLength:134
            /\ M_ii:138 = phi_M_ii:133)
           \/ (havoc:24 = 0
                 /\ (!(0 <= K:126) \/ mid_M_responseLength:127 = K:126)
                 /\ (!(0 <= K:126) \/ mid_M_ii:128 = K:126)
                 /\ ((K:126 = 0 /\ 0 = mid_M_ii:128
                        /\ 0 = mid_M_responseLength:127)
                       \/ (1 <= K:126 /\ 0 <= (4 + -mid_M_ii:128)
                             /\ 0 <= (-1 + mid_M_ii:128)
                             /\ 0 <= (-1 + mid_M_responseLength:127)))
                 /\ K:129 = 0 /\ mid_M_ii:128 = M_ii':130
                 /\ mid_M_responseLength:127 = M_responseLength':131
                 /\ 0 = K:129 /\ (K:126 + K:129) = K:132 /\ 0 <= K:132
                 /\ M_ii':130 <= 4 /\ 0 <= M_ii':130
                 /\ 0 <= M_responseLength':131 /\ 4 <= M_ii':130
                 /\ M_responseLength':131 = phi_M_responseLength:134
                 /\ M_ii':130 = phi_M_ii:133))})


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

  The IRE-evaluated value on this round is: 

Base relation: 
{M_responseLength := phi_M_responseLength:134
 return := havoc:139
 return@pos := type_err:140
 return@width := type_err:141
 when ((!(havoc:24 = 0) /\ 30 = phi_M_responseLength:134
          /\ M_ii:138 = phi_M_ii:133)
         \/ (havoc:24 = 0
               /\ (!(0 <= K:126) \/ mid_M_responseLength:127 = K:126)
               /\ (!(0 <= K:126) \/ mid_M_ii:128 = K:126)
               /\ ((K:126 = 0 /\ 0 = mid_M_ii:128
                      /\ 0 = mid_M_responseLength:127)
                     \/ (1 <= K:126 /\ 0 <= (4 + -mid_M_ii:128)
                           /\ 0 <= (-1 + mid_M_ii:128)
                           /\ 0 <= (-1 + mid_M_responseLength:127)))
               /\ K:129 = 0 /\ mid_M_ii:128 = M_ii':130
               /\ mid_M_responseLength:127 = M_responseLength':131
               /\ 0 = K:129 /\ (K:126 + K:129) = K:132 /\ 0 <= K:132
               /\ M_ii':130 <= 4 /\ 0 <= M_ii':130
               /\ 0 <= M_responseLength':131 /\ 4 <= M_ii':130
               /\ M_responseLength':131 = phi_M_responseLength:134
               /\ M_ii':130 = phi_M_ii:133))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{M_responseLength := phi_M_responseLength:134
 return := havoc:135
 return@pos := type_err:136
 return@width := type_err:137
 when ((!(havoc:24 = 0) /\ 30 = phi_M_responseLength:134
          /\ M_ii:138 = phi_M_ii:133)
         \/ (havoc:24 = 0
               /\ (!(0 <= K:126) \/ mid_M_responseLength:127 = K:126)
               /\ (!(0 <= K:126) \/ mid_M_ii:128 = K:126)
               /\ ((K:126 = 0 /\ 0 = mid_M_ii:128
                      /\ 0 = mid_M_responseLength:127)
                     \/ (1 <= K:126 /\ 0 <= (4 + -mid_M_ii:128)
                           /\ 0 <= (-1 + mid_M_ii:128)
                           /\ 0 <= (-1 + mid_M_responseLength:127)))
               /\ K:129 = 0 /\ mid_M_ii:128 = M_ii':130
               /\ mid_M_responseLength:127 = M_responseLength':131
               /\ 0 = K:129 /\ (K:126 + K:129) = K:132 /\ 0 <= K:132
               /\ M_ii':130 <= 4 /\ 0 <= M_ii':130
               /\ 0 <= M_responseLength':131 /\ 4 <= M_ii':130
               /\ M_responseLength':131 = phi_M_responseLength:134
               /\ M_ii':130 = phi_M_ii:133))}

    (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,34)_g1>	Base relation: 
{}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x65f1400: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x6212e50: 
	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,34)_g1 , __done )	Base relation: 
{}

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

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

Base relation: 
{M_responseLength := phi_M_responseLength:134
 return := havoc:142
 return@pos := type_err:143
 return@width := type_err:144
 when ((!(havoc:24 = 0) /\ 30 = phi_M_responseLength:134
          /\ M_ii:138 = phi_M_ii:133)
         \/ (havoc:24 = 0
               /\ (!(0 <= K:126) \/ mid_M_responseLength:127 = K:126)
               /\ (!(0 <= K:126) \/ mid_M_ii:128 = K:126)
               /\ ((K:126 = 0 /\ 0 = mid_M_ii:128
                      /\ 0 = mid_M_responseLength:127)
                     \/ (1 <= K:126 /\ 0 <= (4 + -mid_M_ii:128)
                           /\ 0 <= (-1 + mid_M_ii:128)
                           /\ 0 <= (-1 + mid_M_responseLength:127)))
               /\ K:129 = 0 /\ mid_M_ii:128 = M_ii':130
               /\ mid_M_responseLength:127 = M_responseLength':131
               /\ 0 = K:129 /\ (K:126 + K:129) = K:132 /\ 0 <= K:132
               /\ M_ii':130 <= 4 /\ 0 <= M_ii':130
               /\ 0 <= M_responseLength':131 /\ 4 <= M_ii':130
               /\ M_responseLength':131 = phi_M_responseLength:134
               /\ M_ii':130 = phi_M_ii:133))}

------------------------------------------------
Procedure summary for serve

Base relation: 
{M_responseLength := phi_M_responseLength:134
 tmp := havoc:24
 M_ii := phi_M_ii:133
 return := havoc:135
 return@pos := type_err:136
 return@width := type_err:137
 when ((!(havoc:24 = 0) /\ 30 = phi_M_responseLength:134
          /\ M_ii:17 = phi_M_ii:133)
         \/ (havoc:24 = 0
               /\ (!(0 <= K:126) \/ mid_M_responseLength:127 = K:126)
               /\ (!(0 <= K:126) \/ mid_M_ii:128 = K:126)
               /\ ((K:126 = 0 /\ 0 = mid_M_ii:128
                      /\ 0 = mid_M_responseLength:127)
                     \/ (1 <= K:126 /\ 0 <= (4 + -mid_M_ii:128)
                           /\ 0 <= (-1 + mid_M_ii:128)
                           /\ 0 <= (-1 + mid_M_responseLength:127)))
               /\ K:129 = 0 /\ mid_M_ii:128 = M_ii':130
               /\ mid_M_responseLength:127 = M_responseLength':131
               /\ 0 = K:129 /\ (K:126 + K:129) = K:132 /\ 0 <= K:132
               /\ M_ii':130 <= 4 /\ 0 <= M_ii':130
               /\ 0 <= M_responseLength':131 /\ 4 <= M_ii':130
               /\ M_responseLength':131 = phi_M_responseLength:134
               /\ M_ii':130 = phi_M_ii:133))}

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

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

Variable bounds at line 16 in main

4 <= M_responseLength
M_responseLength is o(1)
M_responseLength <= 30
M_responseLength is O(1)

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