/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, 25> -> <Unique State Name, 3>	Base relation: 
{}	
<Unique State Name, 27> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 9> -> <Unique State Name, 29>	Base relation: 
{when (M_ii:15 <= 4 /\ 0 <= M_ii:15 /\ 0 <= M_responseLength:16)}	
<Unique State Name, 6> -> <Unique State Name, 26>	Base relation: 
{}	
<Unique State Name, 24> -> <Unique State Name, 9>	Base relation: 
{M_responseLength := 0
 M_ii := 0}	
<Unique State Name, 3> -> <Unique State Name, 28>	Base relation: 
{return := havoc:0
 return@pos := type_err:3
 return@width := type_err:4}	
<Unique State Name, 29> -> <Unique State Name, 13>	Base relation: 
{}	
<Unique State Name, 28> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 26> -> <Unique State Name, 24 25>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 13> -> <Unique State Name, 9>	Base relation: 
{M_responseLength := (M_responseLength:16 + 1)
 M_ii := (M_ii:15 + 1)
 when M_ii:15 < 4}	
<Unique State Name, 13> -> <Unique State Name, 27>	Base relation: 
{return := havoc:22
 return@pos := type_err:23
 return@width := type_err:24
 when 4 <= M_ii:15}	
#################################################################
           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:16 + 1)
 M_ii := (M_ii:15 + 1)
 when (M_ii:15 <= 4 /\ 0 <= M_ii:15 /\ 0 <= M_responseLength:16
         /\ M_ii:15 < 4)}
**** alpha hat: 
  {<Split [true
            (M_responseLength':80) = (1)*(M_responseLength:16) + 1
           (M_ii':81) = (1)*(M_ii:15) + 1
           }
          pre:
            [|-M_ii:15+3>=0; M_responseLength:16>=0; M_ii:15>=0|]
          post:
            [|-M_ii':81+4>=0; M_ii':81-1>=0; M_responseLength':80-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {M_responseLength := M_responseLength':80
   M_ii := M_ii':81
   when ((!(0 <= K:89)
            \/ mid_M_responseLength:92 = (M_responseLength:16 + K:89))
           /\ (!(0 <= K:89) \/ mid_M_ii:91 = (M_ii:15 + K:89))
           /\ ((K:89 = 0 /\ M_ii:15 = mid_M_ii:91
                  /\ M_responseLength:16 = mid_M_responseLength:92)
                 \/ (1 <= K:89 /\ 0 <= (3 + -M_ii:15)
                       /\ 0 <= M_responseLength:16 /\ 0 <= M_ii:15
                       /\ 0 <= (4 + -mid_M_ii:91) /\ 0 <= (-1 + mid_M_ii:91)
                       /\ 0 <= (-1 + mid_M_responseLength:92))) /\ K:90 = 0
           /\ mid_M_ii:91 = M_ii':81
           /\ mid_M_responseLength:92 = M_responseLength':80 /\ 0 = K:90
           /\ (K:89 + K:90) = K:88 /\ 0 <= K:88)}
}
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 := M_responseLength':98
   M_ii := M_ii':97
   return := havoc:100
   return@pos := type_err:101
   return@width := type_err:102
   when ((!(0 <= K:93) \/ mid_M_responseLength:94 = K:93)
           /\ (!(0 <= K:93) \/ mid_M_ii:95 = K:93)
           /\ ((K:93 = 0 /\ 0 = mid_M_ii:95 /\ 0 = mid_M_responseLength:94)
                 \/ (1 <= K:93 /\ 0 <= (4 + -mid_M_ii:95)
                       /\ 0 <= (-1 + mid_M_ii:95)
                       /\ 0 <= (-1 + mid_M_responseLength:94))) /\ K:96 = 0
           /\ mid_M_ii:95 = M_ii':97
           /\ mid_M_responseLength:94 = M_responseLength':98 /\ 0 = K:96
           /\ (K:93 + K:96) = K:99 /\ 0 <= K:99 /\ M_ii':97 <= 4
           /\ 0 <= M_ii':97 /\ 0 <= M_responseLength':98 /\ 4 <= M_ii':97)})



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 := M_responseLength':98
   return := havoc:100
   return@pos := type_err:101
   return@width := type_err:102
   when ((!(0 <= K:93) \/ mid_M_responseLength:94 = K:93)
           /\ (!(0 <= K:93) \/ mid_M_ii:95 = K:93)
           /\ ((K:93 = 0 /\ 0 = mid_M_ii:95 /\ 0 = mid_M_responseLength:94)
                 \/ (1 <= K:93 /\ 0 <= (4 + -mid_M_ii:95)
                       /\ 0 <= (-1 + mid_M_ii:95)
                       /\ 0 <= (-1 + mid_M_responseLength:94))) /\ K:96 = 0
           /\ mid_M_ii:95 = M_ii':97
           /\ mid_M_responseLength:94 = M_responseLength':98 /\ 0 = K:96
           /\ (K:93 + K:96) = K:99 /\ 0 <= K:99 /\ M_ii':97 <= 4
           /\ 0 <= M_ii':97 /\ 0 <= M_responseLength':98 /\ 4 <= M_ii':97)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=7: 
Weight(Base relation: 
  {M_responseLength := M_responseLength':98
   return := havoc:103
   return@pos := type_err:104
   return@width := type_err:105
   when ((!(0 <= K:93) \/ mid_M_responseLength:94 = K:93)
           /\ (!(0 <= K:93) \/ mid_M_ii:95 = K:93)
           /\ ((K:93 = 0 /\ 0 = mid_M_ii:95 /\ 0 = mid_M_responseLength:94)
                 \/ (1 <= K:93 /\ 0 <= (4 + -mid_M_ii:95)
                       /\ 0 <= (-1 + mid_M_ii:95)
                       /\ 0 <= (-1 + mid_M_responseLength:94))) /\ K:96 = 0
           /\ mid_M_ii:95 = M_ii':97
           /\ mid_M_responseLength:94 = M_responseLength':98 /\ 0 = K:96
           /\ (K:93 + K:96) = K:99 /\ 0 <= K:99 /\ M_ii':97 <= 4
           /\ 0 <= M_ii':97 /\ 0 <= M_responseLength':98 /\ 4 <= M_ii':97)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {M_responseLength := M_responseLength':98
   return := havoc:100
   return@pos := type_err:101
   return@width := type_err:102
   when ((!(0 <= K:93) \/ mid_M_responseLength:94 = K:93)
           /\ (!(0 <= K:93) \/ mid_M_ii:95 = K:93)
           /\ ((K:93 = 0 /\ 0 = mid_M_ii:95 /\ 0 = mid_M_responseLength:94)
                 \/ (1 <= K:93 /\ 0 <= (4 + -mid_M_ii:95)
                       /\ 0 <= (-1 + mid_M_ii:95)
                       /\ 0 <= (-1 + mid_M_responseLength:94))) /\ K:96 = 0
           /\ mid_M_ii:95 = M_ii':97
           /\ mid_M_responseLength:94 = M_responseLength':98 /\ 0 = K:96
           /\ (K:93 + K:96) = K:99 /\ 0 <= K:99 /\ M_ii':97 <= 4
           /\ 0 <= M_ii':97 /\ 0 <= M_responseLength':98 /\ 4 <= M_ii':97)})


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 := M_responseLength':98
 return := havoc:103
 return@pos := type_err:104
 return@width := type_err:105
 when ((!(0 <= K:93) \/ mid_M_responseLength:94 = K:93)
         /\ (!(0 <= K:93) \/ mid_M_ii:95 = K:93)
         /\ ((K:93 = 0 /\ 0 = mid_M_ii:95 /\ 0 = mid_M_responseLength:94)
               \/ (1 <= K:93 /\ 0 <= (4 + -mid_M_ii:95)
                     /\ 0 <= (-1 + mid_M_ii:95)
                     /\ 0 <= (-1 + mid_M_responseLength:94))) /\ K:96 = 0
         /\ mid_M_ii:95 = M_ii':97
         /\ mid_M_responseLength:94 = M_responseLength':98 /\ 0 = K:96
         /\ (K:93 + K:96) = K:99 /\ 0 <= K:99 /\ M_ii':97 <= 4
         /\ 0 <= M_ii':97 /\ 0 <= M_responseLength':98 /\ 4 <= M_ii':97)}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{M_responseLength := M_responseLength':98
 return := havoc:100
 return@pos := type_err:101
 return@width := type_err:102
 when ((!(0 <= K:93) \/ mid_M_responseLength:94 = K:93)
         /\ (!(0 <= K:93) \/ mid_M_ii:95 = K:93)
         /\ ((K:93 = 0 /\ 0 = mid_M_ii:95 /\ 0 = mid_M_responseLength:94)
               \/ (1 <= K:93 /\ 0 <= (4 + -mid_M_ii:95)
                     /\ 0 <= (-1 + mid_M_ii:95)
                     /\ 0 <= (-1 + mid_M_responseLength:94))) /\ K:96 = 0
         /\ mid_M_ii:95 = M_ii':97
         /\ mid_M_responseLength:94 = M_responseLength':98 /\ 0 = K:96
         /\ (K:93 + K:96) = K:99 /\ 0 <= K:99 /\ M_ii':97 <= 4
         /\ 0 <= M_ii':97 /\ 0 <= M_responseLength':98 /\ 4 <= M_ii':97)}

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

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

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

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

Base relation: 
{M_responseLength := M_responseLength':98
 return := havoc:106
 return@pos := type_err:107
 return@width := type_err:108
 when ((!(0 <= K:93) \/ mid_M_responseLength:94 = K:93)
         /\ (!(0 <= K:93) \/ mid_M_ii:95 = K:93)
         /\ ((K:93 = 0 /\ 0 = mid_M_ii:95 /\ 0 = mid_M_responseLength:94)
               \/ (1 <= K:93 /\ 0 <= (4 + -mid_M_ii:95)
                     /\ 0 <= (-1 + mid_M_ii:95)
                     /\ 0 <= (-1 + mid_M_responseLength:94))) /\ K:96 = 0
         /\ mid_M_ii:95 = M_ii':97
         /\ mid_M_responseLength:94 = M_responseLength':98 /\ 0 = K:96
         /\ (K:93 + K:96) = K:99 /\ 0 <= K:99 /\ M_ii':97 <= 4
         /\ 0 <= M_ii':97 /\ 0 <= M_responseLength':98 /\ 4 <= M_ii':97)}

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

Base relation: 
{M_responseLength := M_responseLength':98
 M_ii := M_ii':97
 return := havoc:100
 return@pos := type_err:101
 return@width := type_err:102
 when ((!(0 <= K:93) \/ mid_M_responseLength:94 = K:93)
         /\ (!(0 <= K:93) \/ mid_M_ii:95 = K:93)
         /\ ((K:93 = 0 /\ 0 = mid_M_ii:95 /\ 0 = mid_M_responseLength:94)
               \/ (1 <= K:93 /\ 0 <= (4 + -mid_M_ii:95)
                     /\ 0 <= (-1 + mid_M_ii:95)
                     /\ 0 <= (-1 + mid_M_responseLength:94))) /\ K:96 = 0
         /\ mid_M_ii:95 = M_ii':97
         /\ mid_M_responseLength:94 = M_responseLength':98 /\ 0 = K:96
         /\ (K:93 + K:96) = K:99 /\ 0 <= K:99 /\ M_ii':97 <= 4
         /\ 0 <= M_ii':97 /\ 0 <= M_responseLength':98 /\ 4 <= M_ii':97)}

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

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

Variable bounds at line 12 in main

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

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