/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, 71> -> <Unique State Name, 8>	Base relation: 
{__cost := 0
 argv := param1:30
 argv@pos := param1@pos:29
 argv@width := param1@width:28}	
<Unique State Name, 77> -> <Unique State Name, 31>	Base relation: 
{}	
<Unique State Name, 73> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 59> -> <Unique State Name, 73>	Base relation: 
{return := havoc:69
 return@pos := type_err:72
 return@width := type_err:73}	
<Unique State Name, 18> -> <Unique State Name, 78>	Base relation: 
{when 0 <= i:64}	
<Unique State Name, 74> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 63> -> <Unique State Name, 18>	Base relation: 
{i := 0
 n := param0:27}	
<Unique State Name, 70> -> <Unique State Name, 75 69>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 76> -> <Unique State Name, 40>	Base relation: 
{}	
<Unique State Name, 9> -> <Unique State Name, 66>	Base relation: 
{param0 := tmp___0:8
 param0@pos := type_err:37
 param0@width := type_err:38}	
<Unique State Name, 22> -> <Unique State Name, 27>	Base relation: 
{j := 0
 when i:64 < n:65}	
<Unique State Name, 22> -> <Unique State Name, 59>	Base relation: 
{when n:65 <= i:64}	
<Unique State Name, 40> -> <Unique State Name, 27>	Base relation: 
{j := (j:66 + 1)
 when n:65 <= k:67}	
<Unique State Name, 40> -> <Unique State Name, 36>	Base relation: 
{__cost := (__cost:68 + 1)
 k := (k:67 + 1)
 when (k:67 < n:65 /\ 0 <= __cost:68 /\ 0 <= (__cost:68 + 1))}	
<Unique State Name, 78> -> <Unique State Name, 22>	Base relation: 
{}	
<Unique State Name, 69> -> <Unique State Name, 9>	Base relation: 
{tmp___0 := havoc:19}	
<Unique State Name, 27> -> <Unique State Name, 77>	Base relation: 
{when (1 <= n:65 /\ 0 <= j:66 /\ i:64 < n:65)}	
<Unique State Name, 31> -> <Unique State Name, 18>	Base relation: 
{i := (i:64 + 1)
 when n:65 <= j:66}	
<Unique State Name, 31> -> <Unique State Name, 36>	Base relation: 
{k := 0
 when j:66 < n:65}	
<Unique State Name, 75> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 36> -> <Unique State Name, 76>	Base relation: 
{when (1 <= n:65 /\ 0 <= k:67 /\ i:64 < n:65 /\ j:66 < n:65)}	
<Unique State Name, 66> -> <Unique State Name, 63 65>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 65> -> <Unique State Name, 74>	Base relation: 
{return := 0
 return@pos := type_err:35
 return@width := type_err:36}	
<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, 70>	Base relation: 
{param0 := tr:39
 param0@pos := type_err:40
 param0@width := type_err:41
 when (tr:5 < 0 \/ 0 < tr:4)}	
#################################################################
           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:68 + 1)
 k := (k:67 + 1)
 when (1 <= n:65 /\ 0 <= k:67 /\ i:64 < n:65 /\ j:66 < n:65 /\ k:67 < n:65
         /\ 0 <= __cost:68 /\ 0 <= (__cost:68 + 1))}
**** alpha hat: 
  {<Split [true
            (k':733) = (1)*(k:67) + 1
           (__cost':732) = (1)*(__cost:68) + 1
           }
          pre:
            [|__cost:68>=0; k:67>=0; n:65-j:66-1>=0; n:65-i:64-1>=0;
              n:65-k:67-1>=0|]
          post:
            [|k':733-1>=0; __cost':732-1>=0; n:65-j:66-1>=0; n:65-i:64-1>=0;
              n:65-k':733>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':732
   k := k':733
   when ((!(0 <= K:744) \/ mid_k:746 = (k:67 + K:744))
           /\ (!(0 <= K:744) \/ mid___cost:747 = (__cost:68 + K:744))
           /\ ((K:744 = 0 /\ k:67 = mid_k:746 /\ __cost:68 = mid___cost:747)
                 \/ (1 <= K:744 /\ 0 <= __cost:68 /\ 0 <= k:67
                       /\ 0 <= (-1 + n:65 + -j:66)
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (-1 + n:65 + -k:67) /\ 0 <= (-1 + mid_k:746)
                       /\ 0 <= (-1 + mid___cost:747)
                       /\ 0 <= (-1 + n:65 + -j:66)
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (n:65 + -mid_k:746))) /\ K:745 = 0
           /\ mid_k:746 = k':733 /\ mid___cost:747 = __cost':732 /\ 0 = K:745
           /\ (K:744 + K:745) = K:743 /\ 0 <= K:743)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':760
 j := (j:66 + 1)
 k := k':759
 when (1 <= n:65 /\ 0 <= j:66 /\ i:64 < n:65 /\ j:66 < n:65
         /\ (!(0 <= K:755) \/ mid_k:756 = K:755)
         /\ (!(0 <= K:755) \/ mid___cost:757 = (__cost:68 + K:755))
         /\ ((K:755 = 0 /\ 0 = mid_k:756 /\ __cost:68 = mid___cost:757)
               \/ (1 <= K:755 /\ 0 <= __cost:68 /\ 0 <= (-1 + n:65 + -j:66)
                     /\ 0 <= (-1 + n:65 + -i:64) /\ 0 <= (-1 + n:65)
                     /\ 0 <= (-1 + mid_k:756) /\ 0 <= (-1 + mid___cost:757)
                     /\ 0 <= (-1 + n:65 + -j:66) /\ 0 <= (-1 + n:65 + -i:64)
                     /\ 0 <= (n:65 + -mid_k:756))) /\ K:758 = 0
         /\ mid_k:756 = k':759 /\ mid___cost:757 = __cost':760 /\ 0 = K:758
         /\ (K:755 + K:758) = K:761 /\ 0 <= K:761 /\ 1 <= n:65 /\ 0 <= k':759
         /\ i:64 < n:65 /\ j:66 < n:65 /\ n:65 <= k':759)}
**** alpha hat: 
  {<Split [true
            (__cost':732) = (1)*(__cost:68) + n:65
           (k':733) = n:65
           (j':762) = (1)*(j:66) + 1
           (-__cost':732) <= (1)*(-__cost:68) + (-1)*1 + (-1)*i:64
           (-__cost':732) <= (1)*(-__cost:68) + (-1)*1 + (-1)*j:66
           }
          pre:
            [|__cost:68>=0; j:66>=0; n:65-i:64-1>=0; n:65-j:66-1>=0|]
          post:
            [|-n:65+k':733=0; -n:65+__cost':732>=0; j':762-1>=0;
              n:65-i:64-1>=0; n:65-j':762>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':732
   j := j':762
   k := k':733
   when ((!(0 <= K:775) \/ mid___cost:779 = (__cost:68 + (n:65 * K:775)))
           /\ (!((0 <= K:775 /\ K:775 <= 0)) \/ mid_k:777 = k:67)
           /\ (!(1 <= K:775) \/ mid_k:777 = n:65)
           /\ (!(0 <= K:775) \/ mid_j:778 = (j:66 + K:775))
           /\ (!(0 <= K:775)
                 \/ -mid___cost:779 <= (-__cost:68 + -K:775
                                          + -((i:64 * K:775))))
           /\ (!(0 <= K:775)
                 \/ -mid___cost:779 <= (-__cost:68 + (-1/2 * K:775)
                                          + -((j:66 * K:775))
                                          + (-1/2 * (K:775 * K:775))))
           /\ ((K:775 = 0 /\ k:67 = mid_k:777 /\ j:66 = mid_j:778
                  /\ __cost:68 = mid___cost:779)
                 \/ (1 <= K:775 /\ 0 <= __cost:68 /\ 0 <= j:66
                       /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (-1 + n:65 + -j:66) /\ (-n:65 + mid_k:777) = 0
                       /\ 0 <= (-n:65 + mid___cost:779)
                       /\ 0 <= (-1 + mid_j:778) /\ 0 <= (-1 + n:65 + -i:64)
                       /\ 0 <= (n:65 + -mid_j:778))) /\ K:776 = 0
           /\ mid_k:777 = k':733 /\ mid_j:778 = j':762
           /\ mid___cost:779 = __cost':732 /\ 0 = K:776
           /\ (K:775 + K:776) = K:774 /\ 0 <= K:774)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':796
 i := (i:64 + 1)
 j := j':795
 k := k':794
 when (0 <= i:64 /\ i:64 < n:65
         /\ (!(0 <= K:789) \/ mid___cost:790 = (__cost:68 + (n:65 * K:789)))
         /\ (!((0 <= K:789 /\ K:789 <= 0)) \/ mid_k:791 = k:67)
         /\ (!(1 <= K:789) \/ mid_k:791 = n:65)
         /\ (!(0 <= K:789) \/ mid_j:792 = K:789)
         /\ (!(0 <= K:789)
               \/ -mid___cost:790 <= (-__cost:68 + -K:789 + -((i:64 * K:789))))
         /\ (!(0 <= K:789)
               \/ -mid___cost:790 <= (-__cost:68 + (-1/2 * K:789)
                                        + (-1/2 * (K:789 * K:789))))
         /\ ((K:789 = 0 /\ k:67 = mid_k:791 /\ 0 = mid_j:792
                /\ __cost:68 = mid___cost:790)
               \/ (1 <= K:789 /\ 0 <= __cost:68 /\ 0 <= (-1 + n:65 + -i:64)
                     /\ 0 <= (-1 + n:65) /\ (-n:65 + mid_k:791) = 0
                     /\ 0 <= (-n:65 + mid___cost:790)
                     /\ 0 <= (-1 + mid_j:792) /\ 0 <= (-1 + n:65 + -i:64)
                     /\ 0 <= (n:65 + -mid_j:792))) /\ K:793 = 0
         /\ mid_k:791 = k':794 /\ mid_j:792 = j':795
         /\ mid___cost:790 = __cost':796 /\ 0 = K:793
         /\ (K:789 + K:793) = K:797 /\ 0 <= K:797 /\ 1 <= n:65 /\ 0 <= j':795
         /\ i:64 < n:65 /\ n:65 <= j':795)}
**** alpha hat: 
  {<Split [true
            (i':798) = (1)*(i:64) + 1
           (k':733) = n:65
           (__cost':732) = (1)*(__cost:68) + n:65^2
           (j':762) = n:65
           (-__cost':732) <= (1)*(-__cost:68) + (-1)*n:65 + (-1)*n:65*i:64
           }
          pre:
            [|-i:64+(n:65 * i:64)>=0; -i:64+n:65-1>=0;
              -n:65+(n:65 * n:65)-(n:65 * i:64)>=0; __cost:68>=0; i:64>=0|]
          post:
            [|-n:65+k':733=0; -n:65+j':762=0;
              -n:65+(n:65 * n:65)-(n:65 * (-1 + i':798))>=0;
              -(n:65 * n:65)+__cost':732>=0;
              -i':798+(n:65 * (-1 + i':798))+1>=0; i':798-1>=0;
              n:65-i':798>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':732
   i := i':798
   j := j':762
   k := k':733
   when ((!(0 <= K:817) \/ mid_i:821 = (i:64 + K:817))
           /\ (!((0 <= K:817 /\ K:817 <= 0)) \/ mid_k:819 = k:67)
           /\ (!(1 <= K:817) \/ mid_k:819 = n:65)
           /\ (!(0 <= K:817)
                 \/ mid___cost:822 = (__cost:68 + ((n:65 * n:65) * K:817)))
           /\ (!((0 <= K:817 /\ K:817 <= 0)) \/ mid_j:820 = j:66)
           /\ (!(1 <= K:817) \/ mid_j:820 = n:65)
           /\ (!(0 <= K:817)
                 \/ -mid___cost:822 <= (-__cost:68 + (-1/2 * n:65 * K:817)
                                          + -((n:65 * i:64 * K:817))
                                          + (-1/2 * n:65 * (K:817 * K:817))))
           /\ ((K:817 = 0 /\ k:67 = mid_k:819 /\ j:66 = mid_j:820
                  /\ i:64 = mid_i:821 /\ __cost:68 = mid___cost:822)
                 \/ (1 <= K:817 /\ 0 <= (-i:64 + (n:65 * i:64))
                       /\ 0 <= (-1 + -i:64 + n:65)
                       /\ 0 <= (-n:65 + (n:65 * n:65) + -((n:65 * i:64)))
                       /\ 0 <= __cost:68 /\ 0 <= i:64
                       /\ (-n:65 + mid_k:819) = 0 /\ (-n:65 + mid_j:820) = 0
                       /\ 0 <= (-n:65 + (n:65 * n:65)
                                  + -((n:65 * (-1 + mid_i:821))))
                       /\ 0 <= (-((n:65 * n:65)) + mid___cost:822)
                       /\ 0 <= (1 + -mid_i:821 + (n:65 * (-1 + mid_i:821)))
                       /\ 0 <= (-1 + mid_i:821) /\ 0 <= (n:65 + -mid_i:821)))
           /\ K:818 = 0 /\ mid_k:819 = k':733 /\ mid_j:820 = j':762
           /\ mid_i:821 = i':798 /\ mid___cost:822 = __cost':732 /\ 0 = K:818
           /\ (K:817 + K:818) = K:816 /\ 0 <= K:816)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
11  13  21  


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:730 /\ tr:731 <= 0)}        )
        ,
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := 0
               argv := param1:30
               param0 := tr:727
               argv@pos := param1@pos:29
               param0@pos := type_err:728
               argv@width := param1@width:28
               param0@width := type_err:729
               when (tr:725 < 0 \/ 0 < tr:726)}            )
            ,
            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(21)
  )
  ,
  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=21: 
Weight(Base relation: 
  {__cost := __cost':832
   i := i':831
   j := j':830
   k := k':829
   n := param0:27
   return := havoc:834
   return@pos := type_err:835
   return@width := type_err:836
   when ((!(0 <= K:823) \/ mid_i:824 = K:823)
           /\ (!((0 <= K:823 /\ K:823 <= 0)) \/ mid_k:825 = k:67)
           /\ (!(1 <= K:823) \/ mid_k:825 = param0:27)
           /\ (!(0 <= K:823)
                 \/ mid___cost:826 = (__cost:68
                                        + ((param0:27 * param0:27) * K:823)))
           /\ (!((0 <= K:823 /\ K:823 <= 0)) \/ mid_j:827 = j:66)
           /\ (!(1 <= K:823) \/ mid_j:827 = param0:27)
           /\ (!(0 <= K:823)
                 \/ -mid___cost:826 <= (-__cost:68
                                          + (-1/2 * param0:27 * K:823)
                                          + (-1/2 * param0:27
                                               * (K:823 * K:823))))
           /\ ((K:823 = 0 /\ k:67 = mid_k:825 /\ j:66 = mid_j:827
                  /\ 0 = mid_i:824 /\ __cost:68 = mid___cost:826)
                 \/ (1 <= K:823 /\ 0 <= (-1 + param0:27)
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27))
                       /\ 0 <= __cost:68 /\ (-param0:27 + mid_k:825) = 0
                       /\ (-param0:27 + mid_j:827) = 0
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                  + -((param0:27 * (-1 + mid_i:824))))
                       /\ 0 <= (-((param0:27 * param0:27)) + mid___cost:826)
                       /\ 0 <= (1 + -mid_i:824
                                  + (param0:27 * (-1 + mid_i:824)))
                       /\ 0 <= (-1 + mid_i:824)
                       /\ 0 <= (param0:27 + -mid_i:824))) /\ K:828 = 0
           /\ mid_k:825 = k':829 /\ mid_j:827 = j':830 /\ mid_i:824 = i':831
           /\ mid___cost:826 = __cost':832 /\ 0 = K:828
           /\ (K:823 + K:828) = K:833 /\ 0 <= K:833 /\ 0 <= i':831
           /\ param0:27 <= i':831)})



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:730 /\ tr:731 <= 0)}          )
          ,
          Dot(
            Dot(
              Weight(Base relation: 
                {__cost := 0
                 argv := param1:30
                 param0 := tr:727
                 argv@pos := param1@pos:29
                 param0@pos := type_err:728
                 argv@width := param1@width:28
                 param0@width := type_err:729
                 when (tr:725 < 0 \/ 0 < tr:726)}              )
              ,
              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(21)
    )
    ,
    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 21
  New-style (IRE) regular expression for 21 just before isolating it: 

Weight(Base relation: 
  {__cost := __cost':832
   return := havoc:834
   return@pos := type_err:835
   return@width := type_err:836
   when ((!(0 <= K:823) \/ mid_i:824 = K:823)
           /\ (!((0 <= K:823 /\ K:823 <= 0)) \/ mid_k:825 = k:869)
           /\ (!(1 <= K:823) \/ mid_k:825 = param0:27)
           /\ (!(0 <= K:823)
                 \/ mid___cost:826 = (__cost:68
                                        + ((param0:27 * param0:27) * K:823)))
           /\ (!((0 <= K:823 /\ K:823 <= 0)) \/ mid_j:827 = j:870)
           /\ (!(1 <= K:823) \/ mid_j:827 = param0:27)
           /\ (!(0 <= K:823)
                 \/ -mid___cost:826 <= (-__cost:68
                                          + (-1/2 * param0:27 * K:823)
                                          + (-1/2 * param0:27
                                               * (K:823 * K:823))))
           /\ ((K:823 = 0 /\ k:869 = mid_k:825 /\ j:870 = mid_j:827
                  /\ 0 = mid_i:824 /\ __cost:68 = mid___cost:826)
                 \/ (1 <= K:823 /\ 0 <= (-1 + param0:27)
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27))
                       /\ 0 <= __cost:68 /\ (-param0:27 + mid_k:825) = 0
                       /\ (-param0:27 + mid_j:827) = 0
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                  + -((param0:27 * (-1 + mid_i:824))))
                       /\ 0 <= (-((param0:27 * param0:27)) + mid___cost:826)
                       /\ 0 <= (1 + -mid_i:824
                                  + (param0:27 * (-1 + mid_i:824)))
                       /\ 0 <= (-1 + mid_i:824)
                       /\ 0 <= (param0:27 + -mid_i:824))) /\ K:828 = 0
           /\ mid_k:825 = k':829 /\ mid_j:827 = j':830 /\ mid_i:824 = i':831
           /\ mid___cost:826 = __cost':832 /\ 0 = K:828
           /\ (K:823 + K:828) = K:833 /\ 0 <= K:833 /\ 0 <= i':831
           /\ param0:27 <= i':831)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=11: 
Weight(Base relation: 
  {__cost := __cost':889
   return := 0
   param0 := phi_tmp___0:875
   return@pos := type_err:894
   param0@pos := type_err:876
   return@width := type_err:895
   param0@width := type_err:877
   when (((0 <= tr:730 /\ tr:731 <= 0 /\ 0 = phi_tmp___0:875
             /\ param0:27 = phi_param0:874
             /\ param0@pos:26 = phi_param0@pos:873
             /\ param0@width:25 = phi_param0@width:872)
            \/ ((tr:725 < 0 \/ 0 < tr:726) /\ havoc:871 = phi_tmp___0:875
                  /\ tr:727 = phi_param0:874
                  /\ type_err:728 = phi_param0@pos:873
                  /\ type_err:729 = phi_param0@width:872))
           /\ (!(0 <= K:878) \/ mid_i:879 = K:878)
           /\ (!((0 <= K:878 /\ K:878 <= 0)) \/ mid_k:880 = k:881)
           /\ (!(1 <= K:878) \/ mid_k:880 = phi_tmp___0:875)
           /\ (!(0 <= K:878)
                 \/ mid___cost:882 = ((phi_tmp___0:875 * phi_tmp___0:875)
                                        * K:878))
           /\ (!((0 <= K:878 /\ K:878 <= 0)) \/ mid_j:883 = j:884)
           /\ (!(1 <= K:878) \/ mid_j:883 = phi_tmp___0:875)
           /\ (!(0 <= K:878)
                 \/ -mid___cost:882 <= ((-1/2 * phi_tmp___0:875 * K:878)
                                          + (-1/2 * phi_tmp___0:875
                                               * (K:878 * K:878))))
           /\ ((K:878 = 0 /\ k:881 = mid_k:880 /\ j:884 = mid_j:883
                  /\ 0 = mid_i:879 /\ 0 = mid___cost:882)
                 \/ (1 <= K:878 /\ 0 <= (-1 + phi_tmp___0:875)
                       /\ 0 <= (-phi_tmp___0:875
                                  + (phi_tmp___0:875 * phi_tmp___0:875))
                       /\ (-phi_tmp___0:875 + mid_k:880) = 0
                       /\ (-phi_tmp___0:875 + mid_j:883) = 0
                       /\ 0 <= (-phi_tmp___0:875
                                  + (phi_tmp___0:875 * phi_tmp___0:875)
                                  + -((phi_tmp___0:875 * (-1 + mid_i:879))))
                       /\ 0 <= (-((phi_tmp___0:875 * phi_tmp___0:875))
                                  + mid___cost:882)
                       /\ 0 <= (1 + -mid_i:879
                                  + (phi_tmp___0:875 * (-1 + mid_i:879)))
                       /\ 0 <= (-1 + mid_i:879)
                       /\ 0 <= (phi_tmp___0:875 + -mid_i:879))) /\ K:885 = 0
           /\ mid_k:880 = k':886 /\ mid_j:883 = j':887 /\ mid_i:879 = i':888
           /\ mid___cost:882 = __cost':889 /\ 0 = K:885
           /\ (K:878 + K:885) = K:890 /\ 0 <= K:890 /\ 0 <= i':888
           /\ phi_tmp___0:875 <= i':888)})


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


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=21: 
Weight(Base relation: 
  {__cost := __cost':832
   return := havoc:834
   return@pos := type_err:835
   return@width := type_err:836
   when ((!(0 <= K:823) \/ mid_i:824 = K:823)
           /\ (!((0 <= K:823 /\ K:823 <= 0)) \/ mid_k:825 = k:869)
           /\ (!(1 <= K:823) \/ mid_k:825 = param0:27)
           /\ (!(0 <= K:823)
                 \/ mid___cost:826 = (__cost:68
                                        + ((param0:27 * param0:27) * K:823)))
           /\ (!((0 <= K:823 /\ K:823 <= 0)) \/ mid_j:827 = j:870)
           /\ (!(1 <= K:823) \/ mid_j:827 = param0:27)
           /\ (!(0 <= K:823)
                 \/ -mid___cost:826 <= (-__cost:68
                                          + (-1/2 * param0:27 * K:823)
                                          + (-1/2 * param0:27
                                               * (K:823 * K:823))))
           /\ ((K:823 = 0 /\ k:869 = mid_k:825 /\ j:870 = mid_j:827
                  /\ 0 = mid_i:824 /\ __cost:68 = mid___cost:826)
                 \/ (1 <= K:823 /\ 0 <= (-1 + param0:27)
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27))
                       /\ 0 <= __cost:68 /\ (-param0:27 + mid_k:825) = 0
                       /\ (-param0:27 + mid_j:827) = 0
                       /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                  + -((param0:27 * (-1 + mid_i:824))))
                       /\ 0 <= (-((param0:27 * param0:27)) + mid___cost:826)
                       /\ 0 <= (1 + -mid_i:824
                                  + (param0:27 * (-1 + mid_i:824)))
                       /\ 0 <= (-1 + mid_i:824)
                       /\ 0 <= (param0:27 + -mid_i:824))) /\ K:828 = 0
           /\ mid_k:825 = k':829 /\ mid_j:827 = j':830 /\ mid_i:824 = i':831
           /\ mid___cost:826 = __cost':832 /\ 0 = K:828
           /\ (K:823 + K:828) = K:833 /\ 0 <= K:833 /\ 0 <= i':831
           /\ param0:27 <= i':831)})


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':889
 return := 0
 param0 := phi_tmp___0:875
 return@pos := type_err:894
 param0@pos := type_err:876
 return@width := type_err:895
 param0@width := type_err:877
 when (((0 <= tr:730 /\ tr:731 <= 0 /\ 0 = phi_tmp___0:875
           /\ param0:27 = phi_param0:874
           /\ param0@pos:26 = phi_param0@pos:873
           /\ param0@width:25 = phi_param0@width:872)
          \/ ((tr:725 < 0 \/ 0 < tr:726) /\ havoc:871 = phi_tmp___0:875
                /\ tr:727 = phi_param0:874
                /\ type_err:728 = phi_param0@pos:873
                /\ type_err:729 = phi_param0@width:872))
         /\ (!(0 <= K:878) \/ mid_i:879 = K:878)
         /\ (!((0 <= K:878 /\ K:878 <= 0)) \/ mid_k:880 = k:881)
         /\ (!(1 <= K:878) \/ mid_k:880 = phi_tmp___0:875)
         /\ (!(0 <= K:878)
               \/ mid___cost:882 = ((phi_tmp___0:875 * phi_tmp___0:875)
                                      * K:878))
         /\ (!((0 <= K:878 /\ K:878 <= 0)) \/ mid_j:883 = j:884)
         /\ (!(1 <= K:878) \/ mid_j:883 = phi_tmp___0:875)
         /\ (!(0 <= K:878)
               \/ -mid___cost:882 <= ((-1/2 * phi_tmp___0:875 * K:878)
                                        + (-1/2 * phi_tmp___0:875
                                             * (K:878 * K:878))))
         /\ ((K:878 = 0 /\ k:881 = mid_k:880 /\ j:884 = mid_j:883
                /\ 0 = mid_i:879 /\ 0 = mid___cost:882)
               \/ (1 <= K:878 /\ 0 <= (-1 + phi_tmp___0:875)
                     /\ 0 <= (-phi_tmp___0:875
                                + (phi_tmp___0:875 * phi_tmp___0:875))
                     /\ (-phi_tmp___0:875 + mid_k:880) = 0
                     /\ (-phi_tmp___0:875 + mid_j:883) = 0
                     /\ 0 <= (-phi_tmp___0:875
                                + (phi_tmp___0:875 * phi_tmp___0:875)
                                + -((phi_tmp___0:875 * (-1 + mid_i:879))))
                     /\ 0 <= (-((phi_tmp___0:875 * phi_tmp___0:875))
                                + mid___cost:882)
                     /\ 0 <= (1 + -mid_i:879
                                + (phi_tmp___0:875 * (-1 + mid_i:879)))
                     /\ 0 <= (-1 + mid_i:879)
                     /\ 0 <= (phi_tmp___0:875 + -mid_i:879))) /\ K:885 = 0
         /\ mid_k:880 = k':886 /\ mid_j:883 = j':887 /\ mid_i:879 = i':888
         /\ mid___cost:882 = __cost':889 /\ 0 = K:885
         /\ (K:878 + K:885) = K:890 /\ 0 <= K:890 /\ 0 <= i':888
         /\ phi_tmp___0:875 <= i':888)}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

Evaluating variable number 21 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':832
 return := havoc:834
 return@pos := type_err:835
 return@width := type_err:836
 when ((!(0 <= K:823) \/ mid_i:824 = K:823)
         /\ (!((0 <= K:823 /\ K:823 <= 0)) \/ mid_k:825 = k:869)
         /\ (!(1 <= K:823) \/ mid_k:825 = param0:27)
         /\ (!(0 <= K:823)
               \/ mid___cost:826 = (__cost:68
                                      + ((param0:27 * param0:27) * K:823)))
         /\ (!((0 <= K:823 /\ K:823 <= 0)) \/ mid_j:827 = j:870)
         /\ (!(1 <= K:823) \/ mid_j:827 = param0:27)
         /\ (!(0 <= K:823)
               \/ -mid___cost:826 <= (-__cost:68 + (-1/2 * param0:27 * K:823)
                                        + (-1/2 * param0:27 * (K:823 * K:823))))
         /\ ((K:823 = 0 /\ k:869 = mid_k:825 /\ j:870 = mid_j:827
                /\ 0 = mid_i:824 /\ __cost:68 = mid___cost:826)
               \/ (1 <= K:823 /\ 0 <= (-1 + param0:27)
                     /\ 0 <= (-param0:27 + (param0:27 * param0:27))
                     /\ 0 <= __cost:68 /\ (-param0:27 + mid_k:825) = 0
                     /\ (-param0:27 + mid_j:827) = 0
                     /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                + -((param0:27 * (-1 + mid_i:824))))
                     /\ 0 <= (-((param0:27 * param0:27)) + mid___cost:826)
                     /\ 0 <= (1 + -mid_i:824 + (param0:27 * (-1 + mid_i:824)))
                     /\ 0 <= (-1 + mid_i:824)
                     /\ 0 <= (param0:27 + -mid_i:824))) /\ K:828 = 0
         /\ mid_k:825 = k':829 /\ mid_j:827 = j':830 /\ mid_i:824 = i':831
         /\ mid___cost:826 = __cost':832 /\ 0 = K:828
         /\ (K:823 + K:828) = K:833 /\ 0 <= K:833 /\ 0 <= i':831
         /\ param0:27 <= i':831)}

    (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,75)_g1>	Base relation: 
{__cost := 0
 argv := param1:30
 param0 := tr:727
 argv@pos := param1@pos:29
 param0@pos := type_err:728
 argv@width := param1@width:28
 param0@width := type_err:729
 when (tr:725 < 0 \/ 0 < tr:726)}	
<__pstate, accept> -> <__pstate, (Unique State Name,63)_g1>	Base relation: 
{__cost := 0
 tmp___0 := phi_tmp___0:900
 argv := param1:30
 param0 := phi_tmp___0:900
 argv@pos := param1@pos:29
 param0@pos := type_err:901
 argv@width := param1@width:28
 param0@width := type_err:902
 when ((0 <= tr:730 /\ tr:731 <= 0 /\ 0 = phi_tmp___0:900
          /\ param0:27 = phi_param0:899 /\ param0@pos:26 = phi_param0@pos:898
          /\ param0@width:25 = phi_param0@width:897)
         \/ ((tr:725 < 0 \/ 0 < tr:726) /\ havoc:896 = phi_tmp___0:900
               /\ tr:727 = phi_param0:899
               /\ type_err:728 = phi_param0@pos:898
               /\ type_err:729 = phi_param0@width:897))}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x14a93c40: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x14a93b40: 
	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,63)_g1 , __done )	Base relation: 
{__cost := 0
 tmp___0 := phi_tmp___0:900
 argv := param1:30
 param0 := phi_tmp___0:900
 argv@pos := param1@pos:29
 param0@pos := type_err:901
 argv@width := param1@width:28
 param0@width := type_err:902
 when ((0 <= tr:730 /\ tr:731 <= 0 /\ 0 = phi_tmp___0:900
          /\ param0:27 = phi_param0:899 /\ param0@pos:26 = phi_param0@pos:898
          /\ param0@width:25 = phi_param0@width:897)
         \/ ((tr:725 < 0 \/ 0 < tr:726) /\ havoc:896 = phi_tmp___0:900
               /\ tr:727 = phi_param0:899
               /\ type_err:728 = phi_param0@pos:898
               /\ type_err:729 = phi_param0@width:897))}
    ( __pstate , (Unique State Name,75)_g1 , __done )	Base relation: 
{__cost := 0
 argv := param1:30
 param0 := tr:727
 argv@pos := param1@pos:29
 param0@pos := type_err:728
 argv@width := param1@width:28
 param0@width := type_err:729
 when (tr:725 < 0 \/ 0 < tr:726)}

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

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

Base relation: 
{}

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

Base relation: 
{__cost := __cost':914
 tmp___0 := phi_tmp___0:900
 argv := param1:30
 return := 0
 param0 := phi_tmp___0:900
 argv@pos := param1@pos:29
 return@pos := type_err:919
 param0@pos := type_err:901
 argv@width := param1@width:28
 return@width := type_err:920
 param0@width := type_err:902
 when (((0 <= tr:730 /\ tr:731 <= 0 /\ 0 = phi_tmp___0:900
           /\ param0:27 = phi_param0:899
           /\ param0@pos:26 = phi_param0@pos:898
           /\ param0@width:25 = phi_param0@width:897)
          \/ ((tr:725 < 0 \/ 0 < tr:726) /\ havoc:896 = phi_tmp___0:900
                /\ tr:727 = phi_param0:899
                /\ type_err:728 = phi_param0@pos:898
                /\ type_err:729 = phi_param0@width:897))
         /\ (!(0 <= K:903) \/ mid_i:904 = K:903)
         /\ (!((0 <= K:903 /\ K:903 <= 0)) \/ mid_k:905 = k:906)
         /\ (!(1 <= K:903) \/ mid_k:905 = phi_tmp___0:900)
         /\ (!(0 <= K:903)
               \/ mid___cost:907 = ((phi_tmp___0:900 * phi_tmp___0:900)
                                      * K:903))
         /\ (!((0 <= K:903 /\ K:903 <= 0)) \/ mid_j:908 = j:909)
         /\ (!(1 <= K:903) \/ mid_j:908 = phi_tmp___0:900)
         /\ (!(0 <= K:903)
               \/ -mid___cost:907 <= ((-1/2 * phi_tmp___0:900 * K:903)
                                        + (-1/2 * phi_tmp___0:900
                                             * (K:903 * K:903))))
         /\ ((K:903 = 0 /\ k:906 = mid_k:905 /\ j:909 = mid_j:908
                /\ 0 = mid_i:904 /\ 0 = mid___cost:907)
               \/ (1 <= K:903 /\ 0 <= (-1 + phi_tmp___0:900)
                     /\ 0 <= (-phi_tmp___0:900
                                + (phi_tmp___0:900 * phi_tmp___0:900))
                     /\ (-phi_tmp___0:900 + mid_k:905) = 0
                     /\ (-phi_tmp___0:900 + mid_j:908) = 0
                     /\ 0 <= (-phi_tmp___0:900
                                + (phi_tmp___0:900 * phi_tmp___0:900)
                                + -((phi_tmp___0:900 * (-1 + mid_i:904))))
                     /\ 0 <= (-((phi_tmp___0:900 * phi_tmp___0:900))
                                + mid___cost:907)
                     /\ 0 <= (1 + -mid_i:904
                                + (phi_tmp___0:900 * (-1 + mid_i:904)))
                     /\ 0 <= (-1 + mid_i:904)
                     /\ 0 <= (phi_tmp___0:900 + -mid_i:904))) /\ K:910 = 0
         /\ mid_k:905 = k':911 /\ mid_j:908 = j':912 /\ mid_i:904 = i':913
         /\ mid___cost:907 = __cost':914 /\ 0 = K:910
         /\ (K:903 + K:910) = K:915 /\ 0 <= K:915 /\ 0 <= i':913
         /\ phi_tmp___0:900 <= i':913)}

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

Base relation: 
{__cost := __cost':832
 i := i':831
 j := j':830
 k := k':829
 n := param0:27
 return := havoc:834
 return@pos := type_err:835
 return@width := type_err:836
 when ((!(0 <= K:823) \/ mid_i:824 = K:823)
         /\ (!((0 <= K:823 /\ K:823 <= 0)) \/ mid_k:825 = k:67)
         /\ (!(1 <= K:823) \/ mid_k:825 = param0:27)
         /\ (!(0 <= K:823)
               \/ mid___cost:826 = (__cost:68
                                      + ((param0:27 * param0:27) * K:823)))
         /\ (!((0 <= K:823 /\ K:823 <= 0)) \/ mid_j:827 = j:66)
         /\ (!(1 <= K:823) \/ mid_j:827 = param0:27)
         /\ (!(0 <= K:823)
               \/ -mid___cost:826 <= (-__cost:68 + (-1/2 * param0:27 * K:823)
                                        + (-1/2 * param0:27 * (K:823 * K:823))))
         /\ ((K:823 = 0 /\ k:67 = mid_k:825 /\ j:66 = mid_j:827
                /\ 0 = mid_i:824 /\ __cost:68 = mid___cost:826)
               \/ (1 <= K:823 /\ 0 <= (-1 + param0:27)
                     /\ 0 <= (-param0:27 + (param0:27 * param0:27))
                     /\ 0 <= __cost:68 /\ (-param0:27 + mid_k:825) = 0
                     /\ (-param0:27 + mid_j:827) = 0
                     /\ 0 <= (-param0:27 + (param0:27 * param0:27)
                                + -((param0:27 * (-1 + mid_i:824))))
                     /\ 0 <= (-((param0:27 * param0:27)) + mid___cost:826)
                     /\ 0 <= (1 + -mid_i:824 + (param0:27 * (-1 + mid_i:824)))
                     /\ 0 <= (-1 + mid_i:824)
                     /\ 0 <= (param0:27 + -mid_i:824))) /\ K:828 = 0
         /\ mid_k:825 = k':829 /\ mid_j:827 = j':830 /\ mid_i:824 = i':831
         /\ mid___cost:826 = __cost':832 /\ 0 = K:828
         /\ (K:823 + K:828) = K:833 /\ 0 <= K:833 /\ 0 <= i':831
         /\ param0:27 <= i':831)}

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

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

Variable bounds at line 11 in work

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

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