/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, 89> -> <Unique State Name, 86 88>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 94> -> <Unique State Name, 7>	Base relation: 
{n := 32
 secret := 1234
 __cost := 0
 argc := param0:23
 argv := param1:26
 argv@pos := param1@pos:25
 argv@width := param1@width:24}	
<Unique State Name, 23> -> <Unique State Name, 28>	Base relation: 
{t := 0
 when i:70 < n:71}	
<Unique State Name, 23> -> <Unique State Name, 77>	Base relation: 
{when n:71 <= i:70}	
<Unique State Name, 52> -> <Unique State Name, 57>	Base relation: 
{t := 0
 when i:70 < n:71}	
<Unique State Name, 52> -> <Unique State Name, 77>	Base relation: 
{when n:71 <= i:70}	
<Unique State Name, 61> -> <Unique State Name, 48>	Base relation: 
{i := (i:70 + 1)
 when n:71 <= t:72}	
<Unique State Name, 61> -> <Unique State Name, 57>	Base relation: 
{__cost := (__cost:73 + 1)
 t := (t:72 + 1)
 when (t:72 < n:71 /\ 0 <= __cost:73 /\ 0 <= (__cost:73 + 1))}	
<Unique State Name, 7> -> <Unique State Name, 16>	Base relation: 
{__retres5 := -1
 when (argc:0 < 2 \/ 2 < argc:0)}	
<Unique State Name, 7> -> <Unique State Name, 93>	Base relation: 
{param0 := tr:29
 param0@pos := type_err:30
 param0@width := type_err:31
 when (2 <= argc:0 /\ argc:0 <= 2)}	
<Unique State Name, 48> -> <Unique State Name, 102>	Base relation: 
{when 0 <= i:70}	
<Unique State Name, 86> -> <Unique State Name, 76>	Base relation: 
{guess := param0:23}	
<Unique State Name, 101> -> <Unique State Name, 61>	Base relation: 
{}	
<Unique State Name, 32> -> <Unique State Name, 19>	Base relation: 
{i := (i:70 + 1)
 when n:71 <= t:72}	
<Unique State Name, 32> -> <Unique State Name, 28>	Base relation: 
{__cost := (__cost:73 + 2)
 t := (t:72 + 1)
 when (t:72 < n:71 /\ 0 <= __cost:73 /\ 0 <= (__cost:73 + 2))}	
<Unique State Name, 28> -> <Unique State Name, 99>	Base relation: 
{when (0 <= t:72 /\ 1 <= n:71 /\ i:70 < n:71)}	
<Unique State Name, 88> -> <Unique State Name, 16>	Base relation: 
{__retres5 := 0}	
<Unique State Name, 98> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 93> -> <Unique State Name, 98 92>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 100> -> <Unique State Name, 23>	Base relation: 
{}	
<Unique State Name, 57> -> <Unique State Name, 101>	Base relation: 
{when (0 <= t:72 /\ 1 <= n:71 /\ i:70 < n:71)}	
<Unique State Name, 77> -> <Unique State Name, 80>	Base relation: 
{}	
<Unique State Name, 16> -> <Unique State Name, 97>	Base relation: 
{return := __retres5:5
 return@pos := type_err:8
 return@width := type_err:9}	
<Unique State Name, 102> -> <Unique State Name, 52>	Base relation: 
{}	
<Unique State Name, 19> -> <Unique State Name, 100>	Base relation: 
{when 0 <= i:70}	
<Unique State Name, 96> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 76> -> <Unique State Name, 19>	Base relation: 
{i := 0
 when secret:75 < guess:74}	
<Unique State Name, 76> -> <Unique State Name, 48>	Base relation: 
{i := 0
 when guess:74 <= secret:75}	
<Unique State Name, 99> -> <Unique State Name, 32>	Base relation: 
{}	
<Unique State Name, 92> -> <Unique State Name, 89>	Base relation: 
{param0 := havoc:15
 param0@pos := type_err:27
 param0@width := type_err:28}	
<Unique State Name, 80> -> <Unique State Name, 96>	Base relation: 
{return := havoc:76
 return@pos := type_err:79
 return@width := type_err:80}	
<Unique State Name, 97> -> <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:73 + 1)
 t := (t:72 + 1)
 when (0 <= t:72 /\ 1 <= n:71 /\ i:70 < n:71 /\ t:72 < n:71 /\ 0 <= __cost:73
         /\ 0 <= (__cost:73 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':767) = (1)*(__cost:73) + 1
           (t':768) = (1)*(t:72) + 1
           }
          pre:
            [|__cost:73>=0; t:72>=0; n:71-i:70-1>=0; n:71-t:72-1>=0|]
          post:
            [|t':768-1>=0; __cost':767-1>=0; n:71-i:70-1>=0; n:71-t':768>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':767
   t := t':768
   when ((!(0 <= K:778) \/ mid___cost:781 = (__cost:73 + K:778))
           /\ (!(0 <= K:778) \/ mid_t:780 = (t:72 + K:778))
           /\ ((K:778 = 0 /\ t:72 = mid_t:780 /\ __cost:73 = mid___cost:781)
                 \/ (1 <= K:778 /\ 0 <= __cost:73 /\ 0 <= t:72
                       /\ 0 <= (-1 + n:71 + -i:70)
                       /\ 0 <= (-1 + n:71 + -t:72) /\ 0 <= (-1 + mid_t:780)
                       /\ 0 <= (-1 + mid___cost:781)
                       /\ 0 <= (-1 + n:71 + -i:70)
                       /\ 0 <= (n:71 + -mid_t:780))) /\ K:779 = 0
           /\ mid_t:780 = t':768 /\ mid___cost:781 = __cost':767 /\ 0 = K:779
           /\ (K:778 + K:779) = K:777 /\ 0 <= K:777)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':794
 i := (i:70 + 1)
 t := t':793
 when (0 <= i:70 /\ i:70 < n:71
         /\ (!(0 <= K:789) \/ mid___cost:790 = (__cost:73 + K:789))
         /\ (!(0 <= K:789) \/ mid_t:791 = K:789)
         /\ ((K:789 = 0 /\ 0 = mid_t:791 /\ __cost:73 = mid___cost:790)
               \/ (1 <= K:789 /\ 0 <= __cost:73 /\ 0 <= (-1 + n:71 + -i:70)
                     /\ 0 <= (-1 + n:71) /\ 0 <= (-1 + mid_t:791)
                     /\ 0 <= (-1 + mid___cost:790)
                     /\ 0 <= (-1 + n:71 + -i:70) /\ 0 <= (n:71 + -mid_t:791)))
         /\ K:792 = 0 /\ mid_t:791 = t':793 /\ mid___cost:790 = __cost':794
         /\ 0 = K:792 /\ (K:789 + K:792) = K:795 /\ 0 <= K:795 /\ 0 <= t':793
         /\ 1 <= n:71 /\ i:70 < n:71 /\ n:71 <= t':793)}
**** alpha hat: 
  {<Split [true
            (i':796) = (1)*(i:70) + 1
           (__cost':767) = (1)*(__cost:73) + n:71
           (t':768) = n:71
           (-__cost':767) <= (1)*(-__cost:73) + (-1)*1 + (-1)*i:70
           }
          pre:
            [|-i:70+n:71-1>=0; __cost:73>=0; i:70>=0|]
          post:
            [|-n:71+t':768=0; -n:71+__cost':767>=0; i':796-1>=0;
              n:71-i':796>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':767
   i := i':796
   t := t':768
   when ((!(0 <= K:808) \/ mid_i:811 = (i:70 + K:808))
           /\ (!(0 <= K:808) \/ mid___cost:812 = (__cost:73 + (n:71 * K:808)))
           /\ (!((0 <= K:808 /\ K:808 <= 0)) \/ mid_t:810 = t:72)
           /\ (!(1 <= K:808) \/ mid_t:810 = n:71)
           /\ (!(0 <= K:808)
                 \/ -mid___cost:812 <= (-__cost:73 + (-1/2 * K:808)
                                          + -((i:70 * K:808))
                                          + (-1/2 * (K:808 * K:808))))
           /\ ((K:808 = 0 /\ t:72 = mid_t:810 /\ i:70 = mid_i:811
                  /\ __cost:73 = mid___cost:812)
                 \/ (1 <= K:808 /\ 0 <= (-1 + -i:70 + n:71) /\ 0 <= __cost:73
                       /\ 0 <= i:70 /\ (-n:71 + mid_t:810) = 0
                       /\ 0 <= (-n:71 + mid___cost:812)
                       /\ 0 <= (-1 + mid_i:811) /\ 0 <= (n:71 + -mid_i:811)))
           /\ K:809 = 0 /\ mid_t:810 = t':768 /\ mid_i:811 = i':796
           /\ mid___cost:812 = __cost':767 /\ 0 = K:809
           /\ (K:808 + K:809) = K:807 /\ 0 <= K:807)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:73 + 2)
 t := (t:72 + 1)
 when (0 <= t:72 /\ 1 <= n:71 /\ i:70 < n:71 /\ t:72 < n:71 /\ 0 <= __cost:73
         /\ 0 <= (__cost:73 + 2))}
**** alpha hat: 
  {<Split [true
            (__cost':767) = (1)*(__cost:73) + 2*1
           (t':768) = (1)*(t:72) + 1
           }
          pre:
            [|__cost:73>=0; t:72>=0; n:71-i:70-1>=0; n:71-t:72-1>=0|]
          post:
            [|t':768-1>=0; __cost':767-2>=0; n:71-i:70-1>=0; n:71-t':768>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':767
   t := t':768
   when ((!(0 <= K:831) \/ mid___cost:834 = (__cost:73 + (2 * K:831)))
           /\ (!(0 <= K:831) \/ mid_t:833 = (t:72 + K:831))
           /\ ((K:831 = 0 /\ t:72 = mid_t:833 /\ __cost:73 = mid___cost:834)
                 \/ (1 <= K:831 /\ 0 <= __cost:73 /\ 0 <= t:72
                       /\ 0 <= (-1 + n:71 + -i:70)
                       /\ 0 <= (-1 + n:71 + -t:72) /\ 0 <= (-1 + mid_t:833)
                       /\ 0 <= (-2 + mid___cost:834)
                       /\ 0 <= (-1 + n:71 + -i:70)
                       /\ 0 <= (n:71 + -mid_t:833))) /\ K:832 = 0
           /\ mid_t:833 = t':768 /\ mid___cost:834 = __cost':767 /\ 0 = K:832
           /\ (K:831 + K:832) = K:830 /\ 0 <= K:830)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':847
 i := (i:70 + 1)
 t := t':846
 when (0 <= i:70 /\ i:70 < n:71
         /\ (!(0 <= K:842) \/ mid___cost:843 = (__cost:73 + (2 * K:842)))
         /\ (!(0 <= K:842) \/ mid_t:844 = K:842)
         /\ ((K:842 = 0 /\ 0 = mid_t:844 /\ __cost:73 = mid___cost:843)
               \/ (1 <= K:842 /\ 0 <= __cost:73 /\ 0 <= (-1 + n:71 + -i:70)
                     /\ 0 <= (-1 + n:71) /\ 0 <= (-1 + mid_t:844)
                     /\ 0 <= (-2 + mid___cost:843)
                     /\ 0 <= (-1 + n:71 + -i:70) /\ 0 <= (n:71 + -mid_t:844)))
         /\ K:845 = 0 /\ mid_t:844 = t':846 /\ mid___cost:843 = __cost':847
         /\ 0 = K:845 /\ (K:842 + K:845) = K:848 /\ 0 <= K:848 /\ 0 <= t':846
         /\ 1 <= n:71 /\ i:70 < n:71 /\ n:71 <= t':846)}
**** alpha hat: 
  {<Split [true
            (i':796) = (1)*(i:70) + 1
           (__cost':767) = (1)*(__cost:73) + 2*n:71
           (t':768) = n:71
           (-__cost':767) <= (1)*(-__cost:73) + (-2)*1 + (-2)*i:70
           }
          pre:
            [|-i:70+n:71-1>=0; __cost:73>=0; i:70>=0|]
          post:
            [|-n:71+t':768=0; -2n:71+__cost':767>=0; i':796-1>=0;
              n:71-i':796>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':767
   i := i':796
   t := t':768
   when ((!(0 <= K:860) \/ mid_i:863 = (i:70 + K:860))
           /\ (!(0 <= K:860)
                 \/ mid___cost:864 = (__cost:73 + (2 * n:71 * K:860)))
           /\ (!((0 <= K:860 /\ K:860 <= 0)) \/ mid_t:862 = t:72)
           /\ (!(1 <= K:860) \/ mid_t:862 = n:71)
           /\ (!(0 <= K:860)
                 \/ -mid___cost:864 <= (-__cost:73 + -K:860
                                          + (-2 * i:70 * K:860)
                                          + -((K:860 * K:860))))
           /\ ((K:860 = 0 /\ t:72 = mid_t:862 /\ i:70 = mid_i:863
                  /\ __cost:73 = mid___cost:864)
                 \/ (1 <= K:860 /\ 0 <= (-1 + -i:70 + n:71) /\ 0 <= __cost:73
                       /\ 0 <= i:70 /\ (-n:71 + mid_t:862) = 0
                       /\ 0 <= ((-2 * n:71) + mid___cost:864)
                       /\ 0 <= (-1 + mid_i:863) /\ 0 <= (n:71 + -mid_i:863)))
           /\ K:861 = 0 /\ mid_t:862 = t':768 /\ mid_i:863 = i':796
           /\ mid___cost:864 = __cost':767 /\ 0 = K:861
           /\ (K:860 + K:861) = K:859 /\ 0 <= K:859)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
11  13  24  


New-style (IRE) regular expression in IREregExpMap for reID=11: 
Dot(
  Plus(
    Weight(Base relation: 
      {n := 32
       secret := 1234
       __cost := 0
       __retres5 := -1
       argc := param0:23
       argv := param1:26
       argv@pos := param1@pos:25
       argv@width := param1@width:24
       when (param0:23 < 2 \/ 2 < param0:23)}    )
    ,
    Dot(
      Dot(
        Dot(
          Dot(
            Weight(Base relation: 
              {n := 32
               secret := 1234
               __cost := 0
               argc := param0:23
               argv := param1:26
               param0 := tr:764
               argv@pos := param1@pos:25
               param0@pos := type_err:765
               argv@width := param1@width:24
               param0@width := type_err:766
               when (2 <= param0:23 /\ param0:23 <= 2)}            )
            ,
            Var(13)
          )
          ,
          Weight(Base relation: 
            {param0 := havoc:15
             param0@pos := type_err:27
             param0@width := type_err:28}          )
        )
        ,
        Var(24)
      )
      ,
      Weight(Base relation: 
        {__retres5 := 0}      )
    )
  )
  ,
  Weight(Base relation: 
    {return := __retres5:5
     return@pos := type_err:8
     return@width := type_err:9}  )
)


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


New-style (IRE) regular expression in IREregExpMap for reID=24: 
Weight(Base relation: 
  {__cost := phi___cost:876
   i := phi_i:875
   t := phi_t:874
   guess := param0:23
   return := havoc:877
   return@pos := type_err:878
   return@width := type_err:879
   when ((param0:23 <= secret:75 /\ (!(0 <= K:813) \/ mid_i:814 = K:813)
            /\ (!(0 <= K:813)
                  \/ mid___cost:815 = (__cost:73 + (n:71 * K:813)))
            /\ (!((0 <= K:813 /\ K:813 <= 0)) \/ mid_t:816 = t:72)
            /\ (!(1 <= K:813) \/ mid_t:816 = n:71)
            /\ (!(0 <= K:813)
                  \/ -mid___cost:815 <= (-__cost:73 + (-1/2 * K:813)
                                           + (-1/2 * (K:813 * K:813))))
            /\ ((K:813 = 0 /\ t:72 = mid_t:816 /\ 0 = mid_i:814
                   /\ __cost:73 = mid___cost:815)
                  \/ (1 <= K:813 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                        /\ (-n:71 + mid_t:816) = 0
                        /\ 0 <= (-n:71 + mid___cost:815)
                        /\ 0 <= (-1 + mid_i:814) /\ 0 <= (n:71 + -mid_i:814)))
            /\ K:817 = 0 /\ mid_t:816 = t':818 /\ mid_i:814 = i':819
            /\ mid___cost:815 = __cost':820 /\ 0 = K:817
            /\ (K:813 + K:817) = K:821 /\ 0 <= K:821 /\ 0 <= i':819
            /\ n:71 <= i':819 /\ __cost':820 = phi___cost:876
            /\ i':819 = phi_i:875 /\ t':818 = phi_t:874)
           \/ (secret:75 < param0:23 /\ (!(0 <= K:865) \/ mid_i:866 = K:865)
                 /\ (!(0 <= K:865)
                       \/ mid___cost:867 = (__cost:73 + (2 * n:71 * K:865)))
                 /\ (!((0 <= K:865 /\ K:865 <= 0)) \/ mid_t:868 = t:72)
                 /\ (!(1 <= K:865) \/ mid_t:868 = n:71)
                 /\ (!(0 <= K:865)
                       \/ -mid___cost:867 <= (-__cost:73 + -K:865
                                                + -((K:865 * K:865))))
                 /\ ((K:865 = 0 /\ t:72 = mid_t:868 /\ 0 = mid_i:866
                        /\ __cost:73 = mid___cost:867)
                       \/ (1 <= K:865 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                             /\ (-n:71 + mid_t:868) = 0
                             /\ 0 <= ((-2 * n:71) + mid___cost:867)
                             /\ 0 <= (-1 + mid_i:866)
                             /\ 0 <= (n:71 + -mid_i:866))) /\ K:869 = 0
                 /\ mid_t:868 = t':870 /\ mid_i:866 = i':871
                 /\ mid___cost:867 = __cost':872 /\ 0 = K:869
                 /\ (K:865 + K:869) = K:873 /\ 0 <= K:873 /\ 0 <= i':871
                 /\ n:71 <= i':871 /\ __cost':872 = phi___cost:876
                 /\ i':871 = phi_i:875 /\ t':870 = phi_t:874))})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Plus(
      Weight(Base relation: 
        {n := 32
         secret := 1234
         __cost := 0
         __retres5 := -1
         argc := param0:23
         argv := param1:26
         argv@pos := param1@pos:25
         argv@width := param1@width:24
         when (param0:23 < 2 \/ 2 < param0:23)}      )
      ,
      Dot(
        Dot(
          Dot(
            Dot(
              Weight(Base relation: 
                {n := 32
                 secret := 1234
                 __cost := 0
                 argc := param0:23
                 argv := param1:26
                 param0 := tr:764
                 argv@pos := param1@pos:25
                 param0@pos := type_err:765
                 argv@width := param1@width:24
                 param0@width := type_err:766
                 when (2 <= param0:23 /\ param0:23 <= 2)}              )
              ,
              Var(13)
            )
            ,
            Weight(Base relation: 
              {param0 := havoc:15
               param0@pos := type_err:27
               param0@width := type_err:28}            )
          )
          ,
          Var(24)
        )
        ,
        Weight(Base relation: 
          {__retres5 := 0}        )
      )
    )
    ,
    Weight(Base relation: 
      {return := __retres5:5
       return@pos := type_err:8
       return@width := type_err:9}    )
  )
)



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

One()



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

Weight(Base relation: 
  {__cost := phi___cost:876
   return := havoc:877
   return@pos := type_err:878
   return@width := type_err:879
   when ((param0:23 <= secret:75 /\ (!(0 <= K:813) \/ mid_i:814 = K:813)
            /\ (!(0 <= K:813)
                  \/ mid___cost:815 = (__cost:73 + (n:71 * K:813)))
            /\ (!((0 <= K:813 /\ K:813 <= 0)) \/ mid_t:816 = t:908)
            /\ (!(1 <= K:813) \/ mid_t:816 = n:71)
            /\ (!(0 <= K:813)
                  \/ -mid___cost:815 <= (-__cost:73 + (-1/2 * K:813)
                                           + (-1/2 * (K:813 * K:813))))
            /\ ((K:813 = 0 /\ t:908 = mid_t:816 /\ 0 = mid_i:814
                   /\ __cost:73 = mid___cost:815)
                  \/ (1 <= K:813 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                        /\ (-n:71 + mid_t:816) = 0
                        /\ 0 <= (-n:71 + mid___cost:815)
                        /\ 0 <= (-1 + mid_i:814) /\ 0 <= (n:71 + -mid_i:814)))
            /\ K:817 = 0 /\ mid_t:816 = t':818 /\ mid_i:814 = i':819
            /\ mid___cost:815 = __cost':820 /\ 0 = K:817
            /\ (K:813 + K:817) = K:821 /\ 0 <= K:821 /\ 0 <= i':819
            /\ n:71 <= i':819 /\ __cost':820 = phi___cost:876
            /\ i':819 = phi_i:875 /\ t':818 = phi_t:874)
           \/ (secret:75 < param0:23 /\ (!(0 <= K:865) \/ mid_i:866 = K:865)
                 /\ (!(0 <= K:865)
                       \/ mid___cost:867 = (__cost:73 + (2 * n:71 * K:865)))
                 /\ (!((0 <= K:865 /\ K:865 <= 0)) \/ mid_t:868 = t:908)
                 /\ (!(1 <= K:865) \/ mid_t:868 = n:71)
                 /\ (!(0 <= K:865)
                       \/ -mid___cost:867 <= (-__cost:73 + -K:865
                                                + -((K:865 * K:865))))
                 /\ ((K:865 = 0 /\ t:908 = mid_t:868 /\ 0 = mid_i:866
                        /\ __cost:73 = mid___cost:867)
                       \/ (1 <= K:865 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                             /\ (-n:71 + mid_t:868) = 0
                             /\ 0 <= ((-2 * n:71) + mid___cost:867)
                             /\ 0 <= (-1 + mid_i:866)
                             /\ 0 <= (n:71 + -mid_i:866))) /\ K:869 = 0
                 /\ mid_t:868 = t':870 /\ mid_i:866 = i':871
                 /\ mid___cost:867 = __cost':872 /\ 0 = K:869
                 /\ (K:865 + K:869) = K:873 /\ 0 <= K:873 /\ 0 <= i':871
                 /\ n:71 <= i':871 /\ __cost':872 = phi___cost:876
                 /\ i':871 = phi_i:875 /\ t':870 = phi_t:874))})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=11: 
Weight(Base relation: 
  {n := 32
   secret := 1234
   __cost := phi___cost:947
   return := phi___retres5:946
   param0 := phi_param0:943
   return@pos := type_err:948
   param0@pos := phi_param0@pos:940
   return@width := type_err:949
   param0@width := phi_param0@width:937
   when (((param0:23 < 2 \/ 2 < param0:23) /\ 0 = phi___cost:947
            /\ -1 = phi___retres5:946 /\ return:945 = phi_return:944
            /\ param0:23 = phi_param0:943
            /\ return@pos:942 = phi_return@pos:941
            /\ param0@pos:22 = phi_param0@pos:940
            /\ return@width:939 = phi_return@width:938
            /\ param0@width:21 = phi_param0@width:937)
           \/ (2 <= param0:23 /\ param0:23 <= 2
                 /\ ((havoc:909 <= 1234
                        /\ (!(0 <= K:912) \/ mid_i:913 = K:912)
                        /\ (!(0 <= K:912) \/ mid___cost:914 = (32 * K:912))
                        /\ (!((0 <= K:912 /\ K:912 <= 0))
                              \/ mid_t:915 = t:916)
                        /\ (!(1 <= K:912) \/ mid_t:915 = 32)
                        /\ (!(0 <= K:912)
                              \/ -mid___cost:914 <= ((-1/2 * K:912)
                                                       + (-1/2
                                                            * (K:912 * K:912))))
                        /\ ((K:912 = 0 /\ t:916 = mid_t:915 /\ 0 = mid_i:913
                               /\ 0 = mid___cost:914)
                              \/ (1 <= K:912 /\ 0 <= (-1 + 32)
                                    /\ (-32 + mid_t:915) = 0
                                    /\ 0 <= (-32 + mid___cost:914)
                                    /\ 0 <= (-1 + mid_i:913)
                                    /\ 0 <= (32 + -mid_i:913))) /\ K:917 = 0
                        /\ mid_t:915 = t':918 /\ mid_i:913 = i':919
                        /\ mid___cost:914 = __cost':920 /\ 0 = K:917
                        /\ (K:912 + K:917) = K:921 /\ 0 <= K:921
                        /\ 0 <= i':919 /\ 32 <= i':919
                        /\ __cost':920 = phi___cost:922 /\ i':919 = phi_i:923
                        /\ t':918 = phi_t:924)
                       \/ (1234 < havoc:909
                             /\ (!(0 <= K:925) \/ mid_i:926 = K:925)
                             /\ (!(0 <= K:925)
                                   \/ mid___cost:927 = (64 * K:925))
                             /\ (!((0 <= K:925 /\ K:925 <= 0))
                                   \/ mid_t:928 = t:916)
                             /\ (!(1 <= K:925) \/ mid_t:928 = 32)
                             /\ (!(0 <= K:925)
                                   \/ -mid___cost:927 <= (-K:925
                                                            + -((K:925
                                                                   * K:925))))
                             /\ ((K:925 = 0 /\ t:916 = mid_t:928
                                    /\ 0 = mid_i:926 /\ 0 = mid___cost:927)
                                   \/ (1 <= K:925 /\ 0 <= (-1 + 32)
                                         /\ (-32 + mid_t:928) = 0
                                         /\ 0 <= (-64 + mid___cost:927)
                                         /\ 0 <= (-1 + mid_i:926)
                                         /\ 0 <= (32 + -mid_i:926)))
                             /\ K:929 = 0 /\ mid_t:928 = t':930
                             /\ mid_i:926 = i':931
                             /\ mid___cost:927 = __cost':932 /\ 0 = K:929
                             /\ (K:925 + K:929) = K:933 /\ 0 <= K:933
                             /\ 0 <= i':931 /\ 32 <= i':931
                             /\ __cost':932 = phi___cost:922
                             /\ i':931 = phi_i:923 /\ t':930 = phi_t:924))
                 /\ phi___cost:922 = phi___cost:947 /\ 0 = phi___retres5:946
                 /\ havoc:934 = phi_return:944 /\ havoc:909 = phi_param0:943
                 /\ type_err:935 = phi_return@pos:941
                 /\ type_err:910 = phi_param0@pos:940
                 /\ type_err:936 = phi_return@width:938
                 /\ type_err:911 = phi_param0@width:937))})


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


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=24: 
Weight(Base relation: 
  {__cost := phi___cost:876
   return := havoc:877
   return@pos := type_err:878
   return@width := type_err:879
   when ((param0:23 <= secret:75 /\ (!(0 <= K:813) \/ mid_i:814 = K:813)
            /\ (!(0 <= K:813)
                  \/ mid___cost:815 = (__cost:73 + (n:71 * K:813)))
            /\ (!((0 <= K:813 /\ K:813 <= 0)) \/ mid_t:816 = t:908)
            /\ (!(1 <= K:813) \/ mid_t:816 = n:71)
            /\ (!(0 <= K:813)
                  \/ -mid___cost:815 <= (-__cost:73 + (-1/2 * K:813)
                                           + (-1/2 * (K:813 * K:813))))
            /\ ((K:813 = 0 /\ t:908 = mid_t:816 /\ 0 = mid_i:814
                   /\ __cost:73 = mid___cost:815)
                  \/ (1 <= K:813 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                        /\ (-n:71 + mid_t:816) = 0
                        /\ 0 <= (-n:71 + mid___cost:815)
                        /\ 0 <= (-1 + mid_i:814) /\ 0 <= (n:71 + -mid_i:814)))
            /\ K:817 = 0 /\ mid_t:816 = t':818 /\ mid_i:814 = i':819
            /\ mid___cost:815 = __cost':820 /\ 0 = K:817
            /\ (K:813 + K:817) = K:821 /\ 0 <= K:821 /\ 0 <= i':819
            /\ n:71 <= i':819 /\ __cost':820 = phi___cost:876
            /\ i':819 = phi_i:875 /\ t':818 = phi_t:874)
           \/ (secret:75 < param0:23 /\ (!(0 <= K:865) \/ mid_i:866 = K:865)
                 /\ (!(0 <= K:865)
                       \/ mid___cost:867 = (__cost:73 + (2 * n:71 * K:865)))
                 /\ (!((0 <= K:865 /\ K:865 <= 0)) \/ mid_t:868 = t:908)
                 /\ (!(1 <= K:865) \/ mid_t:868 = n:71)
                 /\ (!(0 <= K:865)
                       \/ -mid___cost:867 <= (-__cost:73 + -K:865
                                                + -((K:865 * K:865))))
                 /\ ((K:865 = 0 /\ t:908 = mid_t:868 /\ 0 = mid_i:866
                        /\ __cost:73 = mid___cost:867)
                       \/ (1 <= K:865 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                             /\ (-n:71 + mid_t:868) = 0
                             /\ 0 <= ((-2 * n:71) + mid___cost:867)
                             /\ 0 <= (-1 + mid_i:866)
                             /\ 0 <= (n:71 + -mid_i:866))) /\ K:869 = 0
                 /\ mid_t:868 = t':870 /\ mid_i:866 = i':871
                 /\ mid___cost:867 = __cost':872 /\ 0 = K:869
                 /\ (K:865 + K:869) = K:873 /\ 0 <= K:873 /\ 0 <= i':871
                 /\ n:71 <= i':871 /\ __cost':872 = phi___cost:876
                 /\ i':871 = phi_i:875 /\ t':870 = phi_t:874))})


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

  The IRE-evaluated value on this round is: 

Base relation: 
{n := 32
 secret := 1234
 __cost := phi___cost:947
 return := phi___retres5:946
 param0 := phi_param0:943
 return@pos := type_err:948
 param0@pos := phi_param0@pos:940
 return@width := type_err:949
 param0@width := phi_param0@width:937
 when (((param0:23 < 2 \/ 2 < param0:23) /\ 0 = phi___cost:947
          /\ -1 = phi___retres5:946 /\ return:945 = phi_return:944
          /\ param0:23 = phi_param0:943
          /\ return@pos:942 = phi_return@pos:941
          /\ param0@pos:22 = phi_param0@pos:940
          /\ return@width:939 = phi_return@width:938
          /\ param0@width:21 = phi_param0@width:937)
         \/ (2 <= param0:23 /\ param0:23 <= 2
               /\ ((havoc:909 <= 1234 /\ (!(0 <= K:912) \/ mid_i:913 = K:912)
                      /\ (!(0 <= K:912) \/ mid___cost:914 = (32 * K:912))
                      /\ (!((0 <= K:912 /\ K:912 <= 0)) \/ mid_t:915 = t:916)
                      /\ (!(1 <= K:912) \/ mid_t:915 = 32)
                      /\ (!(0 <= K:912)
                            \/ -mid___cost:914 <= ((-1/2 * K:912)
                                                     + (-1/2
                                                          * (K:912 * K:912))))
                      /\ ((K:912 = 0 /\ t:916 = mid_t:915 /\ 0 = mid_i:913
                             /\ 0 = mid___cost:914)
                            \/ (1 <= K:912 /\ 0 <= (-1 + 32)
                                  /\ (-32 + mid_t:915) = 0
                                  /\ 0 <= (-32 + mid___cost:914)
                                  /\ 0 <= (-1 + mid_i:913)
                                  /\ 0 <= (32 + -mid_i:913))) /\ K:917 = 0
                      /\ mid_t:915 = t':918 /\ mid_i:913 = i':919
                      /\ mid___cost:914 = __cost':920 /\ 0 = K:917
                      /\ (K:912 + K:917) = K:921 /\ 0 <= K:921 /\ 0 <= i':919
                      /\ 32 <= i':919 /\ __cost':920 = phi___cost:922
                      /\ i':919 = phi_i:923 /\ t':918 = phi_t:924)
                     \/ (1234 < havoc:909
                           /\ (!(0 <= K:925) \/ mid_i:926 = K:925)
                           /\ (!(0 <= K:925) \/ mid___cost:927 = (64 * K:925))
                           /\ (!((0 <= K:925 /\ K:925 <= 0))
                                 \/ mid_t:928 = t:916)
                           /\ (!(1 <= K:925) \/ mid_t:928 = 32)
                           /\ (!(0 <= K:925)
                                 \/ -mid___cost:927 <= (-K:925
                                                          + -((K:925 * K:925))))
                           /\ ((K:925 = 0 /\ t:916 = mid_t:928
                                  /\ 0 = mid_i:926 /\ 0 = mid___cost:927)
                                 \/ (1 <= K:925 /\ 0 <= (-1 + 32)
                                       /\ (-32 + mid_t:928) = 0
                                       /\ 0 <= (-64 + mid___cost:927)
                                       /\ 0 <= (-1 + mid_i:926)
                                       /\ 0 <= (32 + -mid_i:926)))
                           /\ K:929 = 0 /\ mid_t:928 = t':930
                           /\ mid_i:926 = i':931
                           /\ mid___cost:927 = __cost':932 /\ 0 = K:929
                           /\ (K:925 + K:929) = K:933 /\ 0 <= K:933
                           /\ 0 <= i':931 /\ 32 <= i':931
                           /\ __cost':932 = phi___cost:922
                           /\ i':931 = phi_i:923 /\ t':930 = phi_t:924))
               /\ phi___cost:922 = phi___cost:947 /\ 0 = phi___retres5:946
               /\ havoc:934 = phi_return:944 /\ havoc:909 = phi_param0:943
               /\ type_err:935 = phi_return@pos:941
               /\ type_err:910 = phi_param0@pos:940
               /\ type_err:936 = phi_return@width:938
               /\ type_err:911 = phi_param0@width:937))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

Evaluating variable number 24 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:876
 return := havoc:877
 return@pos := type_err:878
 return@width := type_err:879
 when ((param0:23 <= secret:75 /\ (!(0 <= K:813) \/ mid_i:814 = K:813)
          /\ (!(0 <= K:813) \/ mid___cost:815 = (__cost:73 + (n:71 * K:813)))
          /\ (!((0 <= K:813 /\ K:813 <= 0)) \/ mid_t:816 = t:908)
          /\ (!(1 <= K:813) \/ mid_t:816 = n:71)
          /\ (!(0 <= K:813)
                \/ -mid___cost:815 <= (-__cost:73 + (-1/2 * K:813)
                                         + (-1/2 * (K:813 * K:813))))
          /\ ((K:813 = 0 /\ t:908 = mid_t:816 /\ 0 = mid_i:814
                 /\ __cost:73 = mid___cost:815)
                \/ (1 <= K:813 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                      /\ (-n:71 + mid_t:816) = 0
                      /\ 0 <= (-n:71 + mid___cost:815)
                      /\ 0 <= (-1 + mid_i:814) /\ 0 <= (n:71 + -mid_i:814)))
          /\ K:817 = 0 /\ mid_t:816 = t':818 /\ mid_i:814 = i':819
          /\ mid___cost:815 = __cost':820 /\ 0 = K:817
          /\ (K:813 + K:817) = K:821 /\ 0 <= K:821 /\ 0 <= i':819
          /\ n:71 <= i':819 /\ __cost':820 = phi___cost:876
          /\ i':819 = phi_i:875 /\ t':818 = phi_t:874)
         \/ (secret:75 < param0:23 /\ (!(0 <= K:865) \/ mid_i:866 = K:865)
               /\ (!(0 <= K:865)
                     \/ mid___cost:867 = (__cost:73 + (2 * n:71 * K:865)))
               /\ (!((0 <= K:865 /\ K:865 <= 0)) \/ mid_t:868 = t:908)
               /\ (!(1 <= K:865) \/ mid_t:868 = n:71)
               /\ (!(0 <= K:865)
                     \/ -mid___cost:867 <= (-__cost:73 + -K:865
                                              + -((K:865 * K:865))))
               /\ ((K:865 = 0 /\ t:908 = mid_t:868 /\ 0 = mid_i:866
                      /\ __cost:73 = mid___cost:867)
                     \/ (1 <= K:865 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                           /\ (-n:71 + mid_t:868) = 0
                           /\ 0 <= ((-2 * n:71) + mid___cost:867)
                           /\ 0 <= (-1 + mid_i:866)
                           /\ 0 <= (n:71 + -mid_i:866))) /\ K:869 = 0
               /\ mid_t:868 = t':870 /\ mid_i:866 = i':871
               /\ mid___cost:867 = __cost':872 /\ 0 = K:869
               /\ (K:865 + K:869) = K:873 /\ 0 <= K:873 /\ 0 <= i':871
               /\ n:71 <= i':871 /\ __cost':872 = phi___cost:876
               /\ i':871 = phi_i:875 /\ t':870 = phi_t:874))}

    (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,86)_g1>	Base relation: 
{n := 32
 secret := 1234
 __cost := 0
 argc := param0:23
 argv := param1:26
 param0 := havoc:950
 argv@pos := param1@pos:25
 param0@pos := type_err:951
 argv@width := param1@width:24
 param0@width := type_err:952
 when (2 <= param0:23 /\ param0:23 <= 2)}	
<__pstate, accept> -> <__pstate, (Unique State Name,98)_g1>	Base relation: 
{n := 32
 secret := 1234
 __cost := 0
 argc := param0:23
 argv := param1:26
 param0 := tr:764
 argv@pos := param1@pos:25
 param0@pos := type_err:765
 argv@width := param1@width:24
 param0@width := type_err:766
 when (2 <= param0:23 /\ param0:23 <= 2)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x15a692f0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x157d9ac0: 
	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,86)_g1 , __done )	Base relation: 
{n := 32
 secret := 1234
 __cost := 0
 argc := param0:23
 argv := param1:26
 param0 := havoc:950
 argv@pos := param1@pos:25
 param0@pos := type_err:951
 argv@width := param1@width:24
 param0@width := type_err:952
 when (2 <= param0:23 /\ param0:23 <= 2)}
    ( __pstate , (Unique State Name,98)_g1 , __done )	Base relation: 
{n := 32
 secret := 1234
 __cost := 0
 argc := param0:23
 argv := param1:26
 param0 := tr:764
 argv@pos := param1@pos:25
 param0@pos := type_err:765
 argv@width := param1@width:24
 param0@width := type_err:766
 when (2 <= param0:23 /\ param0:23 <= 2)}

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

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

Base relation: 
{}

------------------------------------------------
Procedure summary for checkSecret

Base relation: 
{__cost := phi___cost:876
 i := phi_i:875
 t := phi_t:874
 guess := param0:23
 return := havoc:877
 return@pos := type_err:878
 return@width := type_err:879
 when ((param0:23 <= secret:75 /\ (!(0 <= K:813) \/ mid_i:814 = K:813)
          /\ (!(0 <= K:813) \/ mid___cost:815 = (__cost:73 + (n:71 * K:813)))
          /\ (!((0 <= K:813 /\ K:813 <= 0)) \/ mid_t:816 = t:72)
          /\ (!(1 <= K:813) \/ mid_t:816 = n:71)
          /\ (!(0 <= K:813)
                \/ -mid___cost:815 <= (-__cost:73 + (-1/2 * K:813)
                                         + (-1/2 * (K:813 * K:813))))
          /\ ((K:813 = 0 /\ t:72 = mid_t:816 /\ 0 = mid_i:814
                 /\ __cost:73 = mid___cost:815)
                \/ (1 <= K:813 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                      /\ (-n:71 + mid_t:816) = 0
                      /\ 0 <= (-n:71 + mid___cost:815)
                      /\ 0 <= (-1 + mid_i:814) /\ 0 <= (n:71 + -mid_i:814)))
          /\ K:817 = 0 /\ mid_t:816 = t':818 /\ mid_i:814 = i':819
          /\ mid___cost:815 = __cost':820 /\ 0 = K:817
          /\ (K:813 + K:817) = K:821 /\ 0 <= K:821 /\ 0 <= i':819
          /\ n:71 <= i':819 /\ __cost':820 = phi___cost:876
          /\ i':819 = phi_i:875 /\ t':818 = phi_t:874)
         \/ (secret:75 < param0:23 /\ (!(0 <= K:865) \/ mid_i:866 = K:865)
               /\ (!(0 <= K:865)
                     \/ mid___cost:867 = (__cost:73 + (2 * n:71 * K:865)))
               /\ (!((0 <= K:865 /\ K:865 <= 0)) \/ mid_t:868 = t:72)
               /\ (!(1 <= K:865) \/ mid_t:868 = n:71)
               /\ (!(0 <= K:865)
                     \/ -mid___cost:867 <= (-__cost:73 + -K:865
                                              + -((K:865 * K:865))))
               /\ ((K:865 = 0 /\ t:72 = mid_t:868 /\ 0 = mid_i:866
                      /\ __cost:73 = mid___cost:867)
                     \/ (1 <= K:865 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                           /\ (-n:71 + mid_t:868) = 0
                           /\ 0 <= ((-2 * n:71) + mid___cost:867)
                           /\ 0 <= (-1 + mid_i:866)
                           /\ 0 <= (n:71 + -mid_i:866))) /\ K:869 = 0
               /\ mid_t:868 = t':870 /\ mid_i:866 = i':871
               /\ mid___cost:867 = __cost':872 /\ 0 = K:869
               /\ (K:865 + K:869) = K:873 /\ 0 <= K:873 /\ 0 <= i':871
               /\ n:71 <= i':871 /\ __cost':872 = phi___cost:876
               /\ i':871 = phi_i:875 /\ t':870 = phi_t:874))}

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

Base relation: 
{n := 32
 secret := 1234
 __cost := phi___cost:985
 __retres5 := phi___retres5:984
 argc := param0:23
 argv := param1:26
 return := phi___retres5:984
 param0 := phi_param0:982
 argv@pos := param1@pos:25
 return@pos := type_err:986
 param0@pos := phi_param0@pos:980
 argv@width := param1@width:24
 return@width := type_err:987
 param0@width := phi_param0@width:978
 when (((param0:23 < 2 \/ 2 < param0:23) /\ 0 = phi___cost:985
          /\ -1 = phi___retres5:984 /\ return:945 = phi_return:983
          /\ param0:23 = phi_param0:982
          /\ return@pos:942 = phi_return@pos:981
          /\ param0@pos:22 = phi_param0@pos:980
          /\ return@width:939 = phi_return@width:979
          /\ param0@width:21 = phi_param0@width:978)
         \/ (2 <= param0:23 /\ param0:23 <= 2
               /\ ((havoc:950 <= 1234 /\ (!(0 <= K:953) \/ mid_i:954 = K:953)
                      /\ (!(0 <= K:953) \/ mid___cost:955 = (32 * K:953))
                      /\ (!((0 <= K:953 /\ K:953 <= 0)) \/ mid_t:956 = t:957)
                      /\ (!(1 <= K:953) \/ mid_t:956 = 32)
                      /\ (!(0 <= K:953)
                            \/ -mid___cost:955 <= ((-1/2 * K:953)
                                                     + (-1/2
                                                          * (K:953 * K:953))))
                      /\ ((K:953 = 0 /\ t:957 = mid_t:956 /\ 0 = mid_i:954
                             /\ 0 = mid___cost:955)
                            \/ (1 <= K:953 /\ 0 <= (-1 + 32)
                                  /\ (-32 + mid_t:956) = 0
                                  /\ 0 <= (-32 + mid___cost:955)
                                  /\ 0 <= (-1 + mid_i:954)
                                  /\ 0 <= (32 + -mid_i:954))) /\ K:958 = 0
                      /\ mid_t:956 = t':959 /\ mid_i:954 = i':960
                      /\ mid___cost:955 = __cost':961 /\ 0 = K:958
                      /\ (K:953 + K:958) = K:962 /\ 0 <= K:962 /\ 0 <= i':960
                      /\ 32 <= i':960 /\ __cost':961 = phi___cost:963
                      /\ i':960 = phi_i:964 /\ t':959 = phi_t:965)
                     \/ (1234 < havoc:950
                           /\ (!(0 <= K:966) \/ mid_i:967 = K:966)
                           /\ (!(0 <= K:966) \/ mid___cost:968 = (64 * K:966))
                           /\ (!((0 <= K:966 /\ K:966 <= 0))
                                 \/ mid_t:969 = t:957)
                           /\ (!(1 <= K:966) \/ mid_t:969 = 32)
                           /\ (!(0 <= K:966)
                                 \/ -mid___cost:968 <= (-K:966
                                                          + -((K:966 * K:966))))
                           /\ ((K:966 = 0 /\ t:957 = mid_t:969
                                  /\ 0 = mid_i:967 /\ 0 = mid___cost:968)
                                 \/ (1 <= K:966 /\ 0 <= (-1 + 32)
                                       /\ (-32 + mid_t:969) = 0
                                       /\ 0 <= (-64 + mid___cost:968)
                                       /\ 0 <= (-1 + mid_i:967)
                                       /\ 0 <= (32 + -mid_i:967)))
                           /\ K:970 = 0 /\ mid_t:969 = t':971
                           /\ mid_i:967 = i':972
                           /\ mid___cost:968 = __cost':973 /\ 0 = K:970
                           /\ (K:966 + K:970) = K:974 /\ 0 <= K:974
                           /\ 0 <= i':972 /\ 32 <= i':972
                           /\ __cost':973 = phi___cost:963
                           /\ i':972 = phi_i:964 /\ t':971 = phi_t:965))
               /\ phi___cost:963 = phi___cost:985 /\ 0 = phi___retres5:984
               /\ havoc:975 = phi_return:983 /\ havoc:950 = phi_param0:982
               /\ type_err:976 = phi_return@pos:981
               /\ type_err:951 = phi_param0@pos:980
               /\ type_err:977 = phi_return@width:979
               /\ type_err:952 = phi_param0@width:978))}

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

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

Variable bounds at line 21 in checkSecret

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

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