/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, 125> -> <Unique State Name, 134 124>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 38> -> <Unique State Name, 136>	Base relation: 
{when 0 <= i:101}	
<Unique State Name, 135> -> <Unique State Name, 26>	Base relation: 
{}	
<Unique State Name, 121> -> <Unique State Name, 134 120>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 108> -> <Unique State Name, 132>	Base relation: 
{return := havoc:107
 return@pos := type_err:110
 return@width := type_err:111}	
<Unique State Name, 138> -> <Unique State Name, 85>	Base relation: 
{}	
<Unique State Name, 120> -> <Unique State Name, 129>	Base relation: 
{param0 := guess:23
 param1 := havoc:11
 param0@pos := type_err:45
 param1@pos := type_err:47
 param0@width := type_err:46
 param1@width := type_err:48}	
<Unique State Name, 137> -> <Unique State Name, 69>	Base relation: 
{}	
<Unique State Name, 96> -> <Unique State Name, 65>	Base relation: 
{i := 0
 when !(t:104 = 2)}	
<Unique State Name, 96> -> <Unique State Name, 81>	Base relation: 
{i := 0
 when t:104 = 2}	
<Unique State Name, 130> -> <Unique State Name, 7>	Base relation: 
{n := 10
 secret := 1234
 __cost := 0
 argc := param0:35
 argv := param1:38
 argv@pos := param1@pos:37
 argv@width := param1@width:36}	
<Unique State Name, 104> -> <Unique State Name, 108>	Base relation: 
{}	
<Unique State Name, 107> -> <Unique State Name, 60>	Base relation: 
{when secret:106 < guess:105}	
<Unique State Name, 107> -> <Unique State Name, 103>	Base relation: 
{when guess:105 <= secret:106}	
<Unique State Name, 81> -> <Unique State Name, 138>	Base relation: 
{when 0 <= i:101}	
<Unique State Name, 26> -> <Unique State Name, 22>	Base relation: 
{__cost := (__cost:103 + 1)
 i := (i:101 + 1)
 when (i:101 < ((n:102 * n:102) * n:102) /\ 0 <= __cost:103
         /\ 0 <= (__cost:103 + 1))}	
<Unique State Name, 26> -> <Unique State Name, 54>	Base relation: 
{when ((n:102 * n:102) * n:102) <= i:101}	
<Unique State Name, 136> -> <Unique State Name, 42>	Base relation: 
{}	
<Unique State Name, 61> -> <Unique State Name, 108>	Base relation: 
{}	
<Unique State Name, 65> -> <Unique State Name, 137>	Base relation: 
{when 0 <= i:101}	
<Unique State Name, 69> -> <Unique State Name, 65>	Base relation: 
{__cost := (__cost:103 + 1)
 i := (i:101 + 1)
 when (i:101 < ((n:102 * n:102) * n:102) /\ 0 <= __cost:103
         /\ 0 <= (__cost:103 + 1))}	
<Unique State Name, 69> -> <Unique State Name, 97>	Base relation: 
{when ((n:102 * n:102) * n:102) <= i:101}	
<Unique State Name, 129> -> <Unique State Name, 116 128>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 133> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 85> -> <Unique State Name, 81>	Base relation: 
{__cost := (__cost:103 + 1)
 i := (i:101 + 1)
 when (i:101 < n:102 /\ 0 <= __cost:103 /\ 0 <= (__cost:103 + 1))}	
<Unique State Name, 85> -> <Unique State Name, 97>	Base relation: 
{when n:102 <= i:101}	
<Unique State Name, 53> -> <Unique State Name, 22>	Base relation: 
{i := 0
 when !(t:104 = 2)}	
<Unique State Name, 53> -> <Unique State Name, 38>	Base relation: 
{i := 0
 when t:104 = 2}	
<Unique State Name, 60> -> <Unique State Name, 53>	Base relation: 
{when !(t:104 = 1)}	
<Unique State Name, 60> -> <Unique State Name, 61>	Base relation: 
{__cost := (__cost:103 + 1)
 when (t:104 = 1 /\ 0 <= __cost:103 /\ 0 <= (__cost:103 + 1))}	
<Unique State Name, 103> -> <Unique State Name, 96>	Base relation: 
{when !(t:104 = 1)}	
<Unique State Name, 103> -> <Unique State Name, 104>	Base relation: 
{__cost := (__cost:103 + 1)
 when (t:104 = 1 /\ 0 <= __cost:103 /\ 0 <= (__cost:103 + 1))}	
<Unique State Name, 42> -> <Unique State Name, 38>	Base relation: 
{__cost := (__cost:103 + 1)
 i := (i:101 + 1)
 when (i:101 < (n:102 * n:102) /\ 0 <= __cost:103 /\ 0 <= (__cost:103 + 1))}	
<Unique State Name, 42> -> <Unique State Name, 54>	Base relation: 
{when (n:102 * n:102) <= i:101}	
<Unique State Name, 97> -> <Unique State Name, 104>	Base relation: 
{}	
<Unique State Name, 19> -> <Unique State Name, 133>	Base relation: 
{return := __retres7:6
 return@pos := type_err:9
 return@width := type_err:10}	
<Unique State Name, 54> -> <Unique State Name, 61>	Base relation: 
{}	
<Unique State Name, 124> -> <Unique State Name, 121>	Base relation: 
{guess := havoc:17
 param0 := tr:39
 param0@pos := type_err:40
 param0@width := type_err:41}	
<Unique State Name, 116> -> <Unique State Name, 107>	Base relation: 
{guess := param0:35
 t := param1:38}	
<Unique State Name, 128> -> <Unique State Name, 19>	Base relation: 
{__retres7 := 0}	
<Unique State Name, 22> -> <Unique State Name, 135>	Base relation: 
{when 0 <= i:101}	
<Unique State Name, 134> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 7> -> <Unique State Name, 19>	Base relation: 
{__retres7 := -1
 when (argc:0 < 3 \/ 3 < argc:0)}	
<Unique State Name, 7> -> <Unique State Name, 125>	Base relation: 
{param0 := tr:42
 param0@pos := type_err:43
 param0@width := type_err:44
 when (3 <= argc:0 /\ argc:0 <= 3)}	
<Unique State Name, 132> -> <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:103 + 1)
 i := (i:101 + 1)
 when (0 <= i:101 /\ i:101 < n:102 /\ 0 <= __cost:103
         /\ 0 <= (__cost:103 + 1))}
**** alpha hat: 
  {<Split [true
            (i':780) = (1)*(i:101) + 1
           (__cost':779) = (1)*(__cost:103) + 1
           }
          pre:
            [|-i:101+n:102-1>=0; __cost:103>=0; i:101>=0|]
          post:
            [|i':780-1>=0; __cost':779-1>=0; n:102-i':780>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':779
   i := i':780
   when ((!(0 <= K:789) \/ mid_i:791 = (i:101 + K:789))
           /\ (!(0 <= K:789) \/ mid___cost:792 = (__cost:103 + K:789))
           /\ ((K:789 = 0 /\ i:101 = mid_i:791 /\ __cost:103 = mid___cost:792)
                 \/ (1 <= K:789 /\ 0 <= (-1 + -i:101 + n:102)
                       /\ 0 <= __cost:103 /\ 0 <= i:101
                       /\ 0 <= (-1 + mid_i:791) /\ 0 <= (-1 + mid___cost:792)
                       /\ 0 <= (n:102 + -mid_i:791))) /\ K:790 = 0
           /\ mid_i:791 = i':780 /\ mid___cost:792 = __cost':779 /\ 0 = K:790
           /\ (K:789 + K:790) = K:788 /\ 0 <= K:788)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:103 + 1)
 i := (i:101 + 1)
 when (0 <= i:101 /\ i:101 < ((n:102 * n:102) * n:102) /\ 0 <= __cost:103
         /\ 0 <= (__cost:103 + 1))}
**** alpha hat: 
  {<Split [true
            (i':780) = (1)*(i:101) + 1
           (__cost':779) = (1)*(__cost:103) + 1
           }
          pre:
            [|-i:101+((n:102 * n:102) * n:102)-1>=0; __cost:103>=0; i:101>=0|]
          post:
            [|i':780-1>=0; __cost':779-1>=0;
              ((n:102 * n:102) * n:102)-i':780>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':779
   i := i':780
   when ((!(0 <= K:812) \/ mid_i:814 = (i:101 + K:812))
           /\ (!(0 <= K:812) \/ mid___cost:815 = (__cost:103 + K:812))
           /\ ((K:812 = 0 /\ i:101 = mid_i:814 /\ __cost:103 = mid___cost:815)
                 \/ (1 <= K:812
                       /\ 0 <= (-1 + -i:101 + ((n:102 * n:102) * n:102))
                       /\ 0 <= __cost:103 /\ 0 <= i:101
                       /\ 0 <= (-1 + mid_i:814) /\ 0 <= (-1 + mid___cost:815)
                       /\ 0 <= (((n:102 * n:102) * n:102) + -mid_i:814)))
           /\ K:813 = 0 /\ mid_i:814 = i':780 /\ mid___cost:815 = __cost':779
           /\ 0 = K:813 /\ (K:812 + K:813) = K:811 /\ 0 <= K:811)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:103 + 1)
 i := (i:101 + 1)
 when (0 <= i:101 /\ i:101 < (n:102 * n:102) /\ 0 <= __cost:103
         /\ 0 <= (__cost:103 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':779) = (1)*(__cost:103) + 1
           (i':780) = (1)*(i:101) + 1
           }
          pre:
            [|-i:101+(n:102 * n:102)-1>=0; __cost:103>=0; i:101>=0|]
          post:
            [|i':780-1>=0; __cost':779-1>=0; (n:102 * n:102)-i':780>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':779
   i := i':780
   when ((!(0 <= K:837) \/ mid___cost:840 = (__cost:103 + K:837))
           /\ (!(0 <= K:837) \/ mid_i:839 = (i:101 + K:837))
           /\ ((K:837 = 0 /\ i:101 = mid_i:839 /\ __cost:103 = mid___cost:840)
                 \/ (1 <= K:837 /\ 0 <= (-1 + -i:101 + (n:102 * n:102))
                       /\ 0 <= __cost:103 /\ 0 <= i:101
                       /\ 0 <= (-1 + mid_i:839) /\ 0 <= (-1 + mid___cost:840)
                       /\ 0 <= ((n:102 * n:102) + -mid_i:839))) /\ K:838 = 0
           /\ mid_i:839 = i':780 /\ mid___cost:840 = __cost':779 /\ 0 = K:838
           /\ (K:837 + K:838) = K:836 /\ 0 <= K:836)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:103 + 1)
 i := (i:101 + 1)
 when (0 <= i:101 /\ i:101 < ((n:102 * n:102) * n:102) /\ 0 <= __cost:103
         /\ 0 <= (__cost:103 + 1))}
**** alpha hat: 
  {<Split [true
            (i':780) = (1)*(i:101) + 1
           (__cost':779) = (1)*(__cost:103) + 1
           }
          pre:
            [|-i:101+((n:102 * n:102) * n:102)-1>=0; __cost:103>=0; i:101>=0|]
          post:
            [|i':780-1>=0; __cost':779-1>=0;
              ((n:102 * n:102) * n:102)-i':780>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':779
   i := i':780
   when ((!(0 <= K:860) \/ mid_i:862 = (i:101 + K:860))
           /\ (!(0 <= K:860) \/ mid___cost:863 = (__cost:103 + K:860))
           /\ ((K:860 = 0 /\ i:101 = mid_i:862 /\ __cost:103 = mid___cost:863)
                 \/ (1 <= K:860
                       /\ 0 <= (-1 + -i:101 + ((n:102 * n:102) * n:102))
                       /\ 0 <= __cost:103 /\ 0 <= i:101
                       /\ 0 <= (-1 + mid_i:862) /\ 0 <= (-1 + mid___cost:863)
                       /\ 0 <= (((n:102 * n:102) * n:102) + -mid_i:862)))
           /\ K:861 = 0 /\ mid_i:862 = i':780 /\ mid___cost:863 = __cost':779
           /\ 0 = K:861 /\ (K:860 + K:861) = K:859 /\ 0 <= K:859)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
14  16  25  


New-style (IRE) regular expression in IREregExpMap for reID=14: 
Dot(
  Plus(
    Weight(Base relation: 
      {n := 10
       secret := 1234
       __cost := 0
       __retres7 := -1
       argc := param0:35
       argv := param1:38
       argv@pos := param1@pos:37
       argv@width := param1@width:36
       when (param0:35 < 3 \/ 3 < param0:35)}    )
    ,
    Dot(
      Dot(
        Dot(
          Dot(
            Dot(
              Dot(
                Weight(Base relation: 
                  {n := 10
                   secret := 1234
                   __cost := 0
                   argc := param0:35
                   argv := param1:38
                   param0 := tr:776
                   argv@pos := param1@pos:37
                   param0@pos := type_err:777
                   argv@width := param1@width:36
                   param0@width := type_err:778
                   when (3 <= param0:35 /\ param0:35 <= 3)}                )
                ,
                Var(16)
              )
              ,
              Weight(Base relation: 
                {guess := havoc:17
                 param0 := tr:39
                 param0@pos := type_err:40
                 param0@width := type_err:41}              )
            )
            ,
            Var(16)
          )
          ,
          Weight(Base relation: 
            {param0 := guess:23
             param1 := havoc:11
             param0@pos := type_err:45
             param1@pos := type_err:47
             param0@width := type_err:46
             param1@width := type_err:48}          )
        )
        ,
        Var(25)
      )
      ,
      Weight(Base relation: 
        {__retres7 := 0}      )
    )
  )
  ,
  Weight(Base relation: 
    {return := __retres7:6
     return@pos := type_err:9
     return@width := type_err:10}  )
)


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


New-style (IRE) regular expression in IREregExpMap for reID=25: 
Weight(Base relation: 
  {__cost := phi___cost:876
   i := phi_i:875
   guess := param0:35
   t := param1:38
   return := havoc:877
   return@pos := type_err:878
   return@width := type_err:879
   when ((((param0:35 <= secret:106 /\ param1:38 = 1 /\ 0 <= __cost:103
              /\ 0 <= (__cost:103 + 1) /\ (__cost:103 + 1) = phi___cost:826
              /\ i:101 = phi_i:825)
             \/ (((param0:35 <= secret:106 /\ !(param1:38 = 1)
                     /\ param1:38 = 2 /\ (!(0 <= K:793) \/ mid_i:794 = K:793)
                     /\ (!(0 <= K:793)
                           \/ mid___cost:795 = (__cost:103 + K:793))
                     /\ ((K:793 = 0 /\ 0 = mid_i:794
                            /\ __cost:103 = mid___cost:795)
                           \/ (1 <= K:793 /\ 0 <= (-1 + n:102)
                                 /\ 0 <= __cost:103 /\ 0 <= (-1 + mid_i:794)
                                 /\ 0 <= (-1 + mid___cost:795)
                                 /\ 0 <= (n:102 + -mid_i:794))) /\ K:796 = 0
                     /\ mid_i:794 = i':797 /\ mid___cost:795 = __cost':798
                     /\ 0 = K:796 /\ (K:793 + K:796) = K:799 /\ 0 <= K:799
                     /\ 0 <= i':797 /\ n:102 <= i':797
                     /\ __cost':798 = phi___cost:824 /\ i':797 = phi_i:823)
                    \/ (param0:35 <= secret:106 /\ !(param1:38 = 1)
                          /\ !(param1:38 = 2)
                          /\ (!(0 <= K:816) \/ mid_i:817 = K:816)
                          /\ (!(0 <= K:816)
                                \/ mid___cost:818 = (__cost:103 + K:816))
                          /\ ((K:816 = 0 /\ 0 = mid_i:817
                                 /\ __cost:103 = mid___cost:818)
                                \/ (1 <= K:816
                                      /\ 0 <= (-1 + ((n:102 * n:102) * n:102))
                                      /\ 0 <= __cost:103
                                      /\ 0 <= (-1 + mid_i:817)
                                      /\ 0 <= (-1 + mid___cost:818)
                                      /\ 0 <= (((n:102 * n:102) * n:102)
                                                 + -mid_i:817))) /\ K:819 = 0
                          /\ mid_i:817 = i':820
                          /\ mid___cost:818 = __cost':821 /\ 0 = K:819
                          /\ (K:816 + K:819) = K:822 /\ 0 <= K:822
                          /\ 0 <= i':820
                          /\ ((n:102 * n:102) * n:102) <= i':820
                          /\ __cost':821 = phi___cost:824
                          /\ i':820 = phi_i:823))
                   /\ phi___cost:824 = phi___cost:826
                   /\ phi_i:823 = phi_i:825))
            /\ phi___cost:826 = phi___cost:876 /\ phi_i:825 = phi_i:875)
           \/ (((secret:106 < param0:35 /\ param1:38 = 1 /\ 0 <= __cost:103
                   /\ 0 <= (__cost:103 + 1)
                   /\ (__cost:103 + 1) = phi___cost:874 /\ i:101 = phi_i:873)
                  \/ (((secret:106 < param0:35 /\ !(param1:38 = 1)
                          /\ param1:38 = 2
                          /\ (!(0 <= K:841)
                                \/ mid___cost:842 = (__cost:103 + K:841))
                          /\ (!(0 <= K:841) \/ mid_i:843 = K:841)
                          /\ ((K:841 = 0 /\ 0 = mid_i:843
                                 /\ __cost:103 = mid___cost:842)
                                \/ (1 <= K:841 /\ 0 <= (-1 + (n:102 * n:102))
                                      /\ 0 <= __cost:103
                                      /\ 0 <= (-1 + mid_i:843)
                                      /\ 0 <= (-1 + mid___cost:842)
                                      /\ 0 <= ((n:102 * n:102) + -mid_i:843)))
                          /\ K:844 = 0 /\ mid_i:843 = i':845
                          /\ mid___cost:842 = __cost':846 /\ 0 = K:844
                          /\ (K:841 + K:844) = K:847 /\ 0 <= K:847
                          /\ 0 <= i':845 /\ (n:102 * n:102) <= i':845
                          /\ __cost':846 = phi___cost:872
                          /\ i':845 = phi_i:871)
                         \/ (secret:106 < param0:35 /\ !(param1:38 = 1)
                               /\ !(param1:38 = 2)
                               /\ (!(0 <= K:864) \/ mid_i:865 = K:864)
                               /\ (!(0 <= K:864)
                                     \/ mid___cost:866 = (__cost:103 + K:864))
                               /\ ((K:864 = 0 /\ 0 = mid_i:865
                                      /\ __cost:103 = mid___cost:866)
                                     \/ (1 <= K:864
                                           /\ 0 <= (-1
                                                      + ((n:102 * n:102)
                                                           * n:102))
                                           /\ 0 <= __cost:103
                                           /\ 0 <= (-1 + mid_i:865)
                                           /\ 0 <= (-1 + mid___cost:866)
                                           /\ 0 <= (((n:102 * n:102) * n:102)
                                                      + -mid_i:865)))
                               /\ K:867 = 0 /\ mid_i:865 = i':868
                               /\ mid___cost:866 = __cost':869 /\ 0 = K:867
                               /\ (K:864 + K:867) = K:870 /\ 0 <= K:870
                               /\ 0 <= i':868
                               /\ ((n:102 * n:102) * n:102) <= i':868
                               /\ __cost':869 = phi___cost:872
                               /\ i':868 = phi_i:871))
                        /\ phi___cost:872 = phi___cost:874
                        /\ phi_i:871 = phi_i:873))
                 /\ phi___cost:874 = phi___cost:876 /\ phi_i:873 = phi_i:875))})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Plus(
      Weight(Base relation: 
        {n := 10
         secret := 1234
         __cost := 0
         __retres7 := -1
         argc := param0:35
         argv := param1:38
         argv@pos := param1@pos:37
         argv@width := param1@width:36
         when (param0:35 < 3 \/ 3 < param0:35)}      )
      ,
      Dot(
        Dot(
          Dot(
            Dot(
              Dot(
                Dot(
                  Weight(Base relation: 
                    {n := 10
                     secret := 1234
                     __cost := 0
                     argc := param0:35
                     argv := param1:38
                     param0 := tr:776
                     argv@pos := param1@pos:37
                     param0@pos := type_err:777
                     argv@width := param1@width:36
                     param0@width := type_err:778
                     when (3 <= param0:35 /\ param0:35 <= 3)}                  )
                  ,
                  Var(16)
                )
                ,
                Weight(Base relation: 
                  {guess := havoc:17
                   param0 := tr:39
                   param0@pos := type_err:40
                   param0@width := type_err:41}                )
              )
              ,
              Var(16)
            )
            ,
            Weight(Base relation: 
              {param0 := guess:23
               param1 := havoc:11
               param0@pos := type_err:45
               param1@pos := type_err:47
               param0@width := type_err:46
               param1@width := type_err:48}            )
          )
          ,
          Var(25)
        )
        ,
        Weight(Base relation: 
          {__retres7 := 0}        )
      )
    )
    ,
    Weight(Base relation: 
      {return := __retres7:6
       return@pos := type_err:9
       return@width := type_err:10}    )
  )
)



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

One()



  ------------------------------ 
Working on variable 25
  New-style (IRE) regular expression for 25 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:35 <= secret:106 /\ param1:38 = 1 /\ 0 <= __cost:103
              /\ 0 <= (__cost:103 + 1) /\ (__cost:103 + 1) = phi___cost:826
              /\ i:880 = phi_i:825)
             \/ (((param0:35 <= secret:106 /\ !(param1:38 = 1)
                     /\ param1:38 = 2 /\ (!(0 <= K:793) \/ mid_i:794 = K:793)
                     /\ (!(0 <= K:793)
                           \/ mid___cost:795 = (__cost:103 + K:793))
                     /\ ((K:793 = 0 /\ 0 = mid_i:794
                            /\ __cost:103 = mid___cost:795)
                           \/ (1 <= K:793 /\ 0 <= (-1 + n:102)
                                 /\ 0 <= __cost:103 /\ 0 <= (-1 + mid_i:794)
                                 /\ 0 <= (-1 + mid___cost:795)
                                 /\ 0 <= (n:102 + -mid_i:794))) /\ K:796 = 0
                     /\ mid_i:794 = i':797 /\ mid___cost:795 = __cost':798
                     /\ 0 = K:796 /\ (K:793 + K:796) = K:799 /\ 0 <= K:799
                     /\ 0 <= i':797 /\ n:102 <= i':797
                     /\ __cost':798 = phi___cost:824 /\ i':797 = phi_i:823)
                    \/ (param0:35 <= secret:106 /\ !(param1:38 = 1)
                          /\ !(param1:38 = 2)
                          /\ (!(0 <= K:816) \/ mid_i:817 = K:816)
                          /\ (!(0 <= K:816)
                                \/ mid___cost:818 = (__cost:103 + K:816))
                          /\ ((K:816 = 0 /\ 0 = mid_i:817
                                 /\ __cost:103 = mid___cost:818)
                                \/ (1 <= K:816
                                      /\ 0 <= (-1 + ((n:102 * n:102) * n:102))
                                      /\ 0 <= __cost:103
                                      /\ 0 <= (-1 + mid_i:817)
                                      /\ 0 <= (-1 + mid___cost:818)
                                      /\ 0 <= (((n:102 * n:102) * n:102)
                                                 + -mid_i:817))) /\ K:819 = 0
                          /\ mid_i:817 = i':820
                          /\ mid___cost:818 = __cost':821 /\ 0 = K:819
                          /\ (K:816 + K:819) = K:822 /\ 0 <= K:822
                          /\ 0 <= i':820
                          /\ ((n:102 * n:102) * n:102) <= i':820
                          /\ __cost':821 = phi___cost:824
                          /\ i':820 = phi_i:823))
                   /\ phi___cost:824 = phi___cost:826
                   /\ phi_i:823 = phi_i:825))
            /\ phi___cost:826 = phi___cost:876 /\ phi_i:825 = phi_i:875)
           \/ (((secret:106 < param0:35 /\ param1:38 = 1 /\ 0 <= __cost:103
                   /\ 0 <= (__cost:103 + 1)
                   /\ (__cost:103 + 1) = phi___cost:874 /\ i:880 = phi_i:873)
                  \/ (((secret:106 < param0:35 /\ !(param1:38 = 1)
                          /\ param1:38 = 2
                          /\ (!(0 <= K:841)
                                \/ mid___cost:842 = (__cost:103 + K:841))
                          /\ (!(0 <= K:841) \/ mid_i:843 = K:841)
                          /\ ((K:841 = 0 /\ 0 = mid_i:843
                                 /\ __cost:103 = mid___cost:842)
                                \/ (1 <= K:841 /\ 0 <= (-1 + (n:102 * n:102))
                                      /\ 0 <= __cost:103
                                      /\ 0 <= (-1 + mid_i:843)
                                      /\ 0 <= (-1 + mid___cost:842)
                                      /\ 0 <= ((n:102 * n:102) + -mid_i:843)))
                          /\ K:844 = 0 /\ mid_i:843 = i':845
                          /\ mid___cost:842 = __cost':846 /\ 0 = K:844
                          /\ (K:841 + K:844) = K:847 /\ 0 <= K:847
                          /\ 0 <= i':845 /\ (n:102 * n:102) <= i':845
                          /\ __cost':846 = phi___cost:872
                          /\ i':845 = phi_i:871)
                         \/ (secret:106 < param0:35 /\ !(param1:38 = 1)
                               /\ !(param1:38 = 2)
                               /\ (!(0 <= K:864) \/ mid_i:865 = K:864)
                               /\ (!(0 <= K:864)
                                     \/ mid___cost:866 = (__cost:103 + K:864))
                               /\ ((K:864 = 0 /\ 0 = mid_i:865
                                      /\ __cost:103 = mid___cost:866)
                                     \/ (1 <= K:864
                                           /\ 0 <= (-1
                                                      + ((n:102 * n:102)
                                                           * n:102))
                                           /\ 0 <= __cost:103
                                           /\ 0 <= (-1 + mid_i:865)
                                           /\ 0 <= (-1 + mid___cost:866)
                                           /\ 0 <= (((n:102 * n:102) * n:102)
                                                      + -mid_i:865)))
                               /\ K:867 = 0 /\ mid_i:865 = i':868
                               /\ mid___cost:866 = __cost':869 /\ 0 = K:867
                               /\ (K:864 + K:867) = K:870 /\ 0 <= K:870
                               /\ 0 <= i':868
                               /\ ((n:102 * n:102) * n:102) <= i':868
                               /\ __cost':869 = phi___cost:872
                               /\ i':868 = phi_i:871))
                        /\ phi___cost:872 = phi___cost:874
                        /\ phi_i:871 = phi_i:873))
                 /\ phi___cost:874 = phi___cost:876 /\ phi_i:873 = phi_i:875))})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=14: 
Weight(Base relation: 
  {n := 10
   secret := 1234
   __cost := phi___cost:946
   return := phi___retres7:944
   param0 := phi_param0:941
   param1 := phi_param1:940
   return@pos := type_err:947
   param0@pos := phi_param0@pos:937
   param1@pos := phi_param1@pos:936
   return@width := type_err:948
   param0@width := phi_param0@width:933
   param1@width := phi_param1@width:932
   when (((param0:35 < 3 \/ 3 < param0:35) /\ 0 = phi___cost:946
            /\ guess:949 = phi_guess:945 /\ -1 = phi___retres7:944
            /\ return:943 = phi_return:942 /\ param0:35 = phi_param0:941
            /\ param1:38 = phi_param1:940
            /\ return@pos:939 = phi_return@pos:938
            /\ param0@pos:34 = phi_param0@pos:937
            /\ param1@pos:37 = phi_param1@pos:936
            /\ return@width:935 = phi_return@width:934
            /\ param0@width:33 = phi_param0@width:933
            /\ param1@width:36 = phi_param1@width:932)
           \/ (3 <= param0:35 /\ param0:35 <= 3
                 /\ ((((havoc:881 <= 1234 /\ havoc:885 = 1
                          /\ 1 = phi___cost:890 /\ i:891 = phi_i:892)
                         \/ (((havoc:881 <= 1234 /\ !(havoc:885 = 1)
                                 /\ havoc:885 = 2
                                 /\ (!(0 <= K:893) \/ mid_i:894 = K:893)
                                 /\ (!(0 <= K:893) \/ mid___cost:895 = K:893)
                                 /\ ((K:893 = 0 /\ 0 = mid_i:894
                                        /\ 0 = mid___cost:895)
                                       \/ (1 <= K:893 /\ 0 <= (-1 + 10)
                                             /\ 0 <= (-1 + mid_i:894)
                                             /\ 0 <= (-1 + mid___cost:895)
                                             /\ 0 <= (10 + -mid_i:894)))
                                 /\ K:896 = 0 /\ mid_i:894 = i':897
                                 /\ mid___cost:895 = __cost':898 /\ 0 = K:896
                                 /\ (K:893 + K:896) = K:899 /\ 0 <= K:899
                                 /\ 0 <= i':897 /\ 10 <= i':897
                                 /\ __cost':898 = phi___cost:900
                                 /\ i':897 = phi_i:901)
                                \/ (havoc:881 <= 1234 /\ !(havoc:885 = 1)
                                      /\ !(havoc:885 = 2)
                                      /\ (!(0 <= K:902) \/ mid_i:903 = K:902)
                                      /\ (!(0 <= K:902)
                                            \/ mid___cost:904 = K:902)
                                      /\ ((K:902 = 0 /\ 0 = mid_i:903
                                             /\ 0 = mid___cost:904)
                                            \/ (1 <= K:902
                                                  /\ 0 <= (-1 + 1000)
                                                  /\ 0 <= (-1 + mid_i:903)
                                                  /\ 0 <= (-1
                                                             + mid___cost:904)
                                                  /\ 0 <= (1000 + -mid_i:903)))
                                      /\ K:905 = 0 /\ mid_i:903 = i':906
                                      /\ mid___cost:904 = __cost':907
                                      /\ 0 = K:905 /\ (K:902 + K:905) = K:908
                                      /\ 0 <= K:908 /\ 0 <= i':906
                                      /\ 1000 <= i':906
                                      /\ __cost':907 = phi___cost:900
                                      /\ i':906 = phi_i:901))
                               /\ phi___cost:900 = phi___cost:890
                               /\ phi_i:901 = phi_i:892))
                        /\ phi___cost:890 = phi___cost:909
                        /\ phi_i:892 = phi_i:910)
                       \/ (((1234 < havoc:881 /\ havoc:885 = 1
                               /\ 1 = phi___cost:911 /\ i:891 = phi_i:912)
                              \/ (((1234 < havoc:881 /\ !(havoc:885 = 1)
                                      /\ havoc:885 = 2
                                      /\ (!(0 <= K:913)
                                            \/ mid___cost:914 = K:913)
                                      /\ (!(0 <= K:913) \/ mid_i:915 = K:913)
                                      /\ ((K:913 = 0 /\ 0 = mid_i:915
                                             /\ 0 = mid___cost:914)
                                            \/ (1 <= K:913 /\ 0 <= (-1 + 100)
                                                  /\ 0 <= (-1 + mid_i:915)
                                                  /\ 0 <= (-1
                                                             + mid___cost:914)
                                                  /\ 0 <= (100 + -mid_i:915)))
                                      /\ K:916 = 0 /\ mid_i:915 = i':917
                                      /\ mid___cost:914 = __cost':918
                                      /\ 0 = K:916 /\ (K:913 + K:916) = K:919
                                      /\ 0 <= K:919 /\ 0 <= i':917
                                      /\ 100 <= i':917
                                      /\ __cost':918 = phi___cost:920
                                      /\ i':917 = phi_i:921)
                                     \/ (1234 < havoc:881 /\ !(havoc:885 = 1)
                                           /\ !(havoc:885 = 2)
                                           /\ (!(0 <= K:922)
                                                 \/ mid_i:923 = K:922)
                                           /\ (!(0 <= K:922)
                                                 \/ mid___cost:924 = K:922)
                                           /\ ((K:922 = 0 /\ 0 = mid_i:923
                                                  /\ 0 = mid___cost:924)
                                                 \/ (1 <= K:922
                                                       /\ 0 <= (-1 + 1000)
                                                       /\ 0 <= (-1
                                                                  + mid_i:923)
                                                       /\ 0 <= (-1
                                                                  + mid___cost:924)
                                                       /\ 0 <= (1000
                                                                  + -mid_i:923)))
                                           /\ K:925 = 0 /\ mid_i:923 = i':926
                                           /\ mid___cost:924 = __cost':927
                                           /\ 0 = K:925
                                           /\ (K:922 + K:925) = K:928
                                           /\ 0 <= K:928 /\ 0 <= i':926
                                           /\ 1000 <= i':926
                                           /\ __cost':927 = phi___cost:920
                                           /\ i':926 = phi_i:921))
                                    /\ phi___cost:920 = phi___cost:911
                                    /\ phi_i:921 = phi_i:912))
                             /\ phi___cost:911 = phi___cost:909
                             /\ phi_i:912 = phi_i:910))
                 /\ phi___cost:909 = phi___cost:946
                 /\ havoc:881 = phi_guess:945 /\ 0 = phi___retres7:944
                 /\ havoc:929 = phi_return:942 /\ havoc:881 = phi_param0:941
                 /\ havoc:885 = phi_param1:940
                 /\ type_err:930 = phi_return@pos:938
                 /\ type_err:886 = phi_param0@pos:937
                 /\ type_err:887 = phi_param1@pos:936
                 /\ type_err:931 = phi_return@width:934
                 /\ type_err:888 = phi_param0@width:933
                 /\ type_err:889 = phi_param1@width:932))})


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


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=25: 
Weight(Base relation: 
  {__cost := phi___cost:876
   return := havoc:877
   return@pos := type_err:878
   return@width := type_err:879
   when ((((param0:35 <= secret:106 /\ param1:38 = 1 /\ 0 <= __cost:103
              /\ 0 <= (__cost:103 + 1) /\ (__cost:103 + 1) = phi___cost:826
              /\ i:880 = phi_i:825)
             \/ (((param0:35 <= secret:106 /\ !(param1:38 = 1)
                     /\ param1:38 = 2 /\ (!(0 <= K:793) \/ mid_i:794 = K:793)
                     /\ (!(0 <= K:793)
                           \/ mid___cost:795 = (__cost:103 + K:793))
                     /\ ((K:793 = 0 /\ 0 = mid_i:794
                            /\ __cost:103 = mid___cost:795)
                           \/ (1 <= K:793 /\ 0 <= (-1 + n:102)
                                 /\ 0 <= __cost:103 /\ 0 <= (-1 + mid_i:794)
                                 /\ 0 <= (-1 + mid___cost:795)
                                 /\ 0 <= (n:102 + -mid_i:794))) /\ K:796 = 0
                     /\ mid_i:794 = i':797 /\ mid___cost:795 = __cost':798
                     /\ 0 = K:796 /\ (K:793 + K:796) = K:799 /\ 0 <= K:799
                     /\ 0 <= i':797 /\ n:102 <= i':797
                     /\ __cost':798 = phi___cost:824 /\ i':797 = phi_i:823)
                    \/ (param0:35 <= secret:106 /\ !(param1:38 = 1)
                          /\ !(param1:38 = 2)
                          /\ (!(0 <= K:816) \/ mid_i:817 = K:816)
                          /\ (!(0 <= K:816)
                                \/ mid___cost:818 = (__cost:103 + K:816))
                          /\ ((K:816 = 0 /\ 0 = mid_i:817
                                 /\ __cost:103 = mid___cost:818)
                                \/ (1 <= K:816
                                      /\ 0 <= (-1 + ((n:102 * n:102) * n:102))
                                      /\ 0 <= __cost:103
                                      /\ 0 <= (-1 + mid_i:817)
                                      /\ 0 <= (-1 + mid___cost:818)
                                      /\ 0 <= (((n:102 * n:102) * n:102)
                                                 + -mid_i:817))) /\ K:819 = 0
                          /\ mid_i:817 = i':820
                          /\ mid___cost:818 = __cost':821 /\ 0 = K:819
                          /\ (K:816 + K:819) = K:822 /\ 0 <= K:822
                          /\ 0 <= i':820
                          /\ ((n:102 * n:102) * n:102) <= i':820
                          /\ __cost':821 = phi___cost:824
                          /\ i':820 = phi_i:823))
                   /\ phi___cost:824 = phi___cost:826
                   /\ phi_i:823 = phi_i:825))
            /\ phi___cost:826 = phi___cost:876 /\ phi_i:825 = phi_i:875)
           \/ (((secret:106 < param0:35 /\ param1:38 = 1 /\ 0 <= __cost:103
                   /\ 0 <= (__cost:103 + 1)
                   /\ (__cost:103 + 1) = phi___cost:874 /\ i:880 = phi_i:873)
                  \/ (((secret:106 < param0:35 /\ !(param1:38 = 1)
                          /\ param1:38 = 2
                          /\ (!(0 <= K:841)
                                \/ mid___cost:842 = (__cost:103 + K:841))
                          /\ (!(0 <= K:841) \/ mid_i:843 = K:841)
                          /\ ((K:841 = 0 /\ 0 = mid_i:843
                                 /\ __cost:103 = mid___cost:842)
                                \/ (1 <= K:841 /\ 0 <= (-1 + (n:102 * n:102))
                                      /\ 0 <= __cost:103
                                      /\ 0 <= (-1 + mid_i:843)
                                      /\ 0 <= (-1 + mid___cost:842)
                                      /\ 0 <= ((n:102 * n:102) + -mid_i:843)))
                          /\ K:844 = 0 /\ mid_i:843 = i':845
                          /\ mid___cost:842 = __cost':846 /\ 0 = K:844
                          /\ (K:841 + K:844) = K:847 /\ 0 <= K:847
                          /\ 0 <= i':845 /\ (n:102 * n:102) <= i':845
                          /\ __cost':846 = phi___cost:872
                          /\ i':845 = phi_i:871)
                         \/ (secret:106 < param0:35 /\ !(param1:38 = 1)
                               /\ !(param1:38 = 2)
                               /\ (!(0 <= K:864) \/ mid_i:865 = K:864)
                               /\ (!(0 <= K:864)
                                     \/ mid___cost:866 = (__cost:103 + K:864))
                               /\ ((K:864 = 0 /\ 0 = mid_i:865
                                      /\ __cost:103 = mid___cost:866)
                                     \/ (1 <= K:864
                                           /\ 0 <= (-1
                                                      + ((n:102 * n:102)
                                                           * n:102))
                                           /\ 0 <= __cost:103
                                           /\ 0 <= (-1 + mid_i:865)
                                           /\ 0 <= (-1 + mid___cost:866)
                                           /\ 0 <= (((n:102 * n:102) * n:102)
                                                      + -mid_i:865)))
                               /\ K:867 = 0 /\ mid_i:865 = i':868
                               /\ mid___cost:866 = __cost':869 /\ 0 = K:867
                               /\ (K:864 + K:867) = K:870 /\ 0 <= K:870
                               /\ 0 <= i':868
                               /\ ((n:102 * n:102) * n:102) <= i':868
                               /\ __cost':869 = phi___cost:872
                               /\ i':868 = phi_i:871))
                        /\ phi___cost:872 = phi___cost:874
                        /\ phi_i:871 = phi_i:873))
                 /\ phi___cost:874 = phi___cost:876 /\ phi_i:873 = phi_i:875))})


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

  The IRE-evaluated value on this round is: 

Base relation: 
{n := 10
 secret := 1234
 __cost := phi___cost:946
 return := phi___retres7:944
 param0 := phi_param0:941
 param1 := phi_param1:940
 return@pos := type_err:947
 param0@pos := phi_param0@pos:937
 param1@pos := phi_param1@pos:936
 return@width := type_err:948
 param0@width := phi_param0@width:933
 param1@width := phi_param1@width:932
 when (((param0:35 < 3 \/ 3 < param0:35) /\ 0 = phi___cost:946
          /\ guess:949 = phi_guess:945 /\ -1 = phi___retres7:944
          /\ return:943 = phi_return:942 /\ param0:35 = phi_param0:941
          /\ param1:38 = phi_param1:940
          /\ return@pos:939 = phi_return@pos:938
          /\ param0@pos:34 = phi_param0@pos:937
          /\ param1@pos:37 = phi_param1@pos:936
          /\ return@width:935 = phi_return@width:934
          /\ param0@width:33 = phi_param0@width:933
          /\ param1@width:36 = phi_param1@width:932)
         \/ (3 <= param0:35 /\ param0:35 <= 3
               /\ ((((havoc:881 <= 1234 /\ havoc:885 = 1
                        /\ 1 = phi___cost:890 /\ i:891 = phi_i:892)
                       \/ (((havoc:881 <= 1234 /\ !(havoc:885 = 1)
                               /\ havoc:885 = 2
                               /\ (!(0 <= K:893) \/ mid_i:894 = K:893)
                               /\ (!(0 <= K:893) \/ mid___cost:895 = K:893)
                               /\ ((K:893 = 0 /\ 0 = mid_i:894
                                      /\ 0 = mid___cost:895)
                                     \/ (1 <= K:893 /\ 0 <= (-1 + 10)
                                           /\ 0 <= (-1 + mid_i:894)
                                           /\ 0 <= (-1 + mid___cost:895)
                                           /\ 0 <= (10 + -mid_i:894)))
                               /\ K:896 = 0 /\ mid_i:894 = i':897
                               /\ mid___cost:895 = __cost':898 /\ 0 = K:896
                               /\ (K:893 + K:896) = K:899 /\ 0 <= K:899
                               /\ 0 <= i':897 /\ 10 <= i':897
                               /\ __cost':898 = phi___cost:900
                               /\ i':897 = phi_i:901)
                              \/ (havoc:881 <= 1234 /\ !(havoc:885 = 1)
                                    /\ !(havoc:885 = 2)
                                    /\ (!(0 <= K:902) \/ mid_i:903 = K:902)
                                    /\ (!(0 <= K:902)
                                          \/ mid___cost:904 = K:902)
                                    /\ ((K:902 = 0 /\ 0 = mid_i:903
                                           /\ 0 = mid___cost:904)
                                          \/ (1 <= K:902 /\ 0 <= (-1 + 1000)
                                                /\ 0 <= (-1 + mid_i:903)
                                                /\ 0 <= (-1 + mid___cost:904)
                                                /\ 0 <= (1000 + -mid_i:903)))
                                    /\ K:905 = 0 /\ mid_i:903 = i':906
                                    /\ mid___cost:904 = __cost':907
                                    /\ 0 = K:905 /\ (K:902 + K:905) = K:908
                                    /\ 0 <= K:908 /\ 0 <= i':906
                                    /\ 1000 <= i':906
                                    /\ __cost':907 = phi___cost:900
                                    /\ i':906 = phi_i:901))
                             /\ phi___cost:900 = phi___cost:890
                             /\ phi_i:901 = phi_i:892))
                      /\ phi___cost:890 = phi___cost:909
                      /\ phi_i:892 = phi_i:910)
                     \/ (((1234 < havoc:881 /\ havoc:885 = 1
                             /\ 1 = phi___cost:911 /\ i:891 = phi_i:912)
                            \/ (((1234 < havoc:881 /\ !(havoc:885 = 1)
                                    /\ havoc:885 = 2
                                    /\ (!(0 <= K:913)
                                          \/ mid___cost:914 = K:913)
                                    /\ (!(0 <= K:913) \/ mid_i:915 = K:913)
                                    /\ ((K:913 = 0 /\ 0 = mid_i:915
                                           /\ 0 = mid___cost:914)
                                          \/ (1 <= K:913 /\ 0 <= (-1 + 100)
                                                /\ 0 <= (-1 + mid_i:915)
                                                /\ 0 <= (-1 + mid___cost:914)
                                                /\ 0 <= (100 + -mid_i:915)))
                                    /\ K:916 = 0 /\ mid_i:915 = i':917
                                    /\ mid___cost:914 = __cost':918
                                    /\ 0 = K:916 /\ (K:913 + K:916) = K:919
                                    /\ 0 <= K:919 /\ 0 <= i':917
                                    /\ 100 <= i':917
                                    /\ __cost':918 = phi___cost:920
                                    /\ i':917 = phi_i:921)
                                   \/ (1234 < havoc:881 /\ !(havoc:885 = 1)
                                         /\ !(havoc:885 = 2)
                                         /\ (!(0 <= K:922)
                                               \/ mid_i:923 = K:922)
                                         /\ (!(0 <= K:922)
                                               \/ mid___cost:924 = K:922)
                                         /\ ((K:922 = 0 /\ 0 = mid_i:923
                                                /\ 0 = mid___cost:924)
                                               \/ (1 <= K:922
                                                     /\ 0 <= (-1 + 1000)
                                                     /\ 0 <= (-1 + mid_i:923)
                                                     /\ 0 <= (-1
                                                                + mid___cost:924)
                                                     /\ 0 <= (1000
                                                                + -mid_i:923)))
                                         /\ K:925 = 0 /\ mid_i:923 = i':926
                                         /\ mid___cost:924 = __cost':927
                                         /\ 0 = K:925
                                         /\ (K:922 + K:925) = K:928
                                         /\ 0 <= K:928 /\ 0 <= i':926
                                         /\ 1000 <= i':926
                                         /\ __cost':927 = phi___cost:920
                                         /\ i':926 = phi_i:921))
                                  /\ phi___cost:920 = phi___cost:911
                                  /\ phi_i:921 = phi_i:912))
                           /\ phi___cost:911 = phi___cost:909
                           /\ phi_i:912 = phi_i:910))
               /\ phi___cost:909 = phi___cost:946
               /\ havoc:881 = phi_guess:945 /\ 0 = phi___retres7:944
               /\ havoc:929 = phi_return:942 /\ havoc:881 = phi_param0:941
               /\ havoc:885 = phi_param1:940
               /\ type_err:930 = phi_return@pos:938
               /\ type_err:886 = phi_param0@pos:937
               /\ type_err:887 = phi_param1@pos:936
               /\ type_err:931 = phi_return@width:934
               /\ type_err:888 = phi_param0@width:933
               /\ type_err:889 = phi_param1@width:932))}

Evaluating variable number 16 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

Evaluating variable number 25 (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:35 <= secret:106 /\ param1:38 = 1 /\ 0 <= __cost:103
            /\ 0 <= (__cost:103 + 1) /\ (__cost:103 + 1) = phi___cost:826
            /\ i:880 = phi_i:825)
           \/ (((param0:35 <= secret:106 /\ !(param1:38 = 1) /\ param1:38 = 2
                   /\ (!(0 <= K:793) \/ mid_i:794 = K:793)
                   /\ (!(0 <= K:793) \/ mid___cost:795 = (__cost:103 + K:793))
                   /\ ((K:793 = 0 /\ 0 = mid_i:794
                          /\ __cost:103 = mid___cost:795)
                         \/ (1 <= K:793 /\ 0 <= (-1 + n:102)
                               /\ 0 <= __cost:103 /\ 0 <= (-1 + mid_i:794)
                               /\ 0 <= (-1 + mid___cost:795)
                               /\ 0 <= (n:102 + -mid_i:794))) /\ K:796 = 0
                   /\ mid_i:794 = i':797 /\ mid___cost:795 = __cost':798
                   /\ 0 = K:796 /\ (K:793 + K:796) = K:799 /\ 0 <= K:799
                   /\ 0 <= i':797 /\ n:102 <= i':797
                   /\ __cost':798 = phi___cost:824 /\ i':797 = phi_i:823)
                  \/ (param0:35 <= secret:106 /\ !(param1:38 = 1)
                        /\ !(param1:38 = 2)
                        /\ (!(0 <= K:816) \/ mid_i:817 = K:816)
                        /\ (!(0 <= K:816)
                              \/ mid___cost:818 = (__cost:103 + K:816))
                        /\ ((K:816 = 0 /\ 0 = mid_i:817
                               /\ __cost:103 = mid___cost:818)
                              \/ (1 <= K:816
                                    /\ 0 <= (-1 + ((n:102 * n:102) * n:102))
                                    /\ 0 <= __cost:103
                                    /\ 0 <= (-1 + mid_i:817)
                                    /\ 0 <= (-1 + mid___cost:818)
                                    /\ 0 <= (((n:102 * n:102) * n:102)
                                               + -mid_i:817))) /\ K:819 = 0
                        /\ mid_i:817 = i':820 /\ mid___cost:818 = __cost':821
                        /\ 0 = K:819 /\ (K:816 + K:819) = K:822 /\ 0 <= K:822
                        /\ 0 <= i':820 /\ ((n:102 * n:102) * n:102) <= i':820
                        /\ __cost':821 = phi___cost:824 /\ i':820 = phi_i:823))
                 /\ phi___cost:824 = phi___cost:826 /\ phi_i:823 = phi_i:825))
          /\ phi___cost:826 = phi___cost:876 /\ phi_i:825 = phi_i:875)
         \/ (((secret:106 < param0:35 /\ param1:38 = 1 /\ 0 <= __cost:103
                 /\ 0 <= (__cost:103 + 1)
                 /\ (__cost:103 + 1) = phi___cost:874 /\ i:880 = phi_i:873)
                \/ (((secret:106 < param0:35 /\ !(param1:38 = 1)
                        /\ param1:38 = 2
                        /\ (!(0 <= K:841)
                              \/ mid___cost:842 = (__cost:103 + K:841))
                        /\ (!(0 <= K:841) \/ mid_i:843 = K:841)
                        /\ ((K:841 = 0 /\ 0 = mid_i:843
                               /\ __cost:103 = mid___cost:842)
                              \/ (1 <= K:841 /\ 0 <= (-1 + (n:102 * n:102))
                                    /\ 0 <= __cost:103
                                    /\ 0 <= (-1 + mid_i:843)
                                    /\ 0 <= (-1 + mid___cost:842)
                                    /\ 0 <= ((n:102 * n:102) + -mid_i:843)))
                        /\ K:844 = 0 /\ mid_i:843 = i':845
                        /\ mid___cost:842 = __cost':846 /\ 0 = K:844
                        /\ (K:841 + K:844) = K:847 /\ 0 <= K:847
                        /\ 0 <= i':845 /\ (n:102 * n:102) <= i':845
                        /\ __cost':846 = phi___cost:872 /\ i':845 = phi_i:871)
                       \/ (secret:106 < param0:35 /\ !(param1:38 = 1)
                             /\ !(param1:38 = 2)
                             /\ (!(0 <= K:864) \/ mid_i:865 = K:864)
                             /\ (!(0 <= K:864)
                                   \/ mid___cost:866 = (__cost:103 + K:864))
                             /\ ((K:864 = 0 /\ 0 = mid_i:865
                                    /\ __cost:103 = mid___cost:866)
                                   \/ (1 <= K:864
                                         /\ 0 <= (-1
                                                    + ((n:102 * n:102)
                                                         * n:102))
                                         /\ 0 <= __cost:103
                                         /\ 0 <= (-1 + mid_i:865)
                                         /\ 0 <= (-1 + mid___cost:866)
                                         /\ 0 <= (((n:102 * n:102) * n:102)
                                                    + -mid_i:865)))
                             /\ K:867 = 0 /\ mid_i:865 = i':868
                             /\ mid___cost:866 = __cost':869 /\ 0 = K:867
                             /\ (K:864 + K:867) = K:870 /\ 0 <= K:870
                             /\ 0 <= i':868
                             /\ ((n:102 * n:102) * n:102) <= i':868
                             /\ __cost':869 = phi___cost:872
                             /\ i':868 = phi_i:871))
                      /\ phi___cost:872 = phi___cost:874
                      /\ phi_i:871 = phi_i:873))
               /\ phi___cost:874 = phi___cost:876 /\ phi_i:873 = phi_i:875))}

    (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,134)_g1>	Base relation: 
{n := 10
 secret := 1234
 __cost := 0
 guess := phi_guess:1018
 argc := param0:35
 argv := param1:38
 param0 := phi_param0:1017
 argv@pos := param1@pos:37
 param0@pos := phi_param0@pos:1016
 argv@width := param1@width:36
 param0@width := phi_param0@width:1015
 when ((3 <= param0:35 /\ param0:35 <= 3 /\ havoc:950 = phi_guess:1018
          /\ tr:951 = phi_param0:1017 /\ type_err:952 = phi_param0@pos:1016
          /\ type_err:953 = phi_param0@width:1015)
         \/ (3 <= param0:35 /\ param0:35 <= 3 /\ guess:23 = phi_guess:1018
               /\ tr:776 = phi_param0:1017
               /\ type_err:777 = phi_param0@pos:1016
               /\ type_err:778 = phi_param0@width:1015))}	
<__pstate, accept> -> <__pstate, (Unique State Name,116)_g1>	Base relation: 
{n := 10
 secret := 1234
 __cost := 0
 guess := havoc:950
 argc := param0:35
 argv := param1:38
 param0 := havoc:950
 param1 := havoc:954
 argv@pos := param1@pos:37
 param0@pos := type_err:955
 param1@pos := type_err:956
 argv@width := param1@width:36
 param0@width := type_err:957
 param1@width := type_err:958
 when (3 <= param0:35 /\ param0:35 <= 3)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x117951b0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x119fec90: 
	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,134)_g1 , __done )	Base relation: 
{n := 10
 secret := 1234
 __cost := 0
 guess := phi_guess:1018
 argc := param0:35
 argv := param1:38
 param0 := phi_param0:1017
 argv@pos := param1@pos:37
 param0@pos := phi_param0@pos:1016
 argv@width := param1@width:36
 param0@width := phi_param0@width:1015
 when ((3 <= param0:35 /\ param0:35 <= 3 /\ havoc:950 = phi_guess:1018
          /\ tr:951 = phi_param0:1017 /\ type_err:952 = phi_param0@pos:1016
          /\ type_err:953 = phi_param0@width:1015)
         \/ (3 <= param0:35 /\ param0:35 <= 3 /\ guess:23 = phi_guess:1018
               /\ tr:776 = phi_param0:1017
               /\ type_err:777 = phi_param0@pos:1016
               /\ type_err:778 = phi_param0@width:1015))}
    ( __pstate , (Unique State Name,116)_g1 , __done )	Base relation: 
{n := 10
 secret := 1234
 __cost := 0
 guess := havoc:950
 argc := param0:35
 argv := param1:38
 param0 := havoc:950
 param1 := havoc:954
 argv@pos := param1@pos:37
 param0@pos := type_err:955
 param1@pos := type_err:956
 argv@width := param1@width:36
 param0@width := type_err:957
 param1@width := type_err:958
 when (3 <= param0:35 /\ param0:35 <= 3)}

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

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

Base relation: 
{}

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

Base relation: 
{__cost := phi___cost:876
 i := phi_i:875
 guess := param0:35
 t := param1:38
 return := havoc:877
 return@pos := type_err:878
 return@width := type_err:879
 when ((((param0:35 <= secret:106 /\ param1:38 = 1 /\ 0 <= __cost:103
            /\ 0 <= (__cost:103 + 1) /\ (__cost:103 + 1) = phi___cost:826
            /\ i:101 = phi_i:825)
           \/ (((param0:35 <= secret:106 /\ !(param1:38 = 1) /\ param1:38 = 2
                   /\ (!(0 <= K:793) \/ mid_i:794 = K:793)
                   /\ (!(0 <= K:793) \/ mid___cost:795 = (__cost:103 + K:793))
                   /\ ((K:793 = 0 /\ 0 = mid_i:794
                          /\ __cost:103 = mid___cost:795)
                         \/ (1 <= K:793 /\ 0 <= (-1 + n:102)
                               /\ 0 <= __cost:103 /\ 0 <= (-1 + mid_i:794)
                               /\ 0 <= (-1 + mid___cost:795)
                               /\ 0 <= (n:102 + -mid_i:794))) /\ K:796 = 0
                   /\ mid_i:794 = i':797 /\ mid___cost:795 = __cost':798
                   /\ 0 = K:796 /\ (K:793 + K:796) = K:799 /\ 0 <= K:799
                   /\ 0 <= i':797 /\ n:102 <= i':797
                   /\ __cost':798 = phi___cost:824 /\ i':797 = phi_i:823)
                  \/ (param0:35 <= secret:106 /\ !(param1:38 = 1)
                        /\ !(param1:38 = 2)
                        /\ (!(0 <= K:816) \/ mid_i:817 = K:816)
                        /\ (!(0 <= K:816)
                              \/ mid___cost:818 = (__cost:103 + K:816))
                        /\ ((K:816 = 0 /\ 0 = mid_i:817
                               /\ __cost:103 = mid___cost:818)
                              \/ (1 <= K:816
                                    /\ 0 <= (-1 + ((n:102 * n:102) * n:102))
                                    /\ 0 <= __cost:103
                                    /\ 0 <= (-1 + mid_i:817)
                                    /\ 0 <= (-1 + mid___cost:818)
                                    /\ 0 <= (((n:102 * n:102) * n:102)
                                               + -mid_i:817))) /\ K:819 = 0
                        /\ mid_i:817 = i':820 /\ mid___cost:818 = __cost':821
                        /\ 0 = K:819 /\ (K:816 + K:819) = K:822 /\ 0 <= K:822
                        /\ 0 <= i':820 /\ ((n:102 * n:102) * n:102) <= i':820
                        /\ __cost':821 = phi___cost:824 /\ i':820 = phi_i:823))
                 /\ phi___cost:824 = phi___cost:826 /\ phi_i:823 = phi_i:825))
          /\ phi___cost:826 = phi___cost:876 /\ phi_i:825 = phi_i:875)
         \/ (((secret:106 < param0:35 /\ param1:38 = 1 /\ 0 <= __cost:103
                 /\ 0 <= (__cost:103 + 1)
                 /\ (__cost:103 + 1) = phi___cost:874 /\ i:101 = phi_i:873)
                \/ (((secret:106 < param0:35 /\ !(param1:38 = 1)
                        /\ param1:38 = 2
                        /\ (!(0 <= K:841)
                              \/ mid___cost:842 = (__cost:103 + K:841))
                        /\ (!(0 <= K:841) \/ mid_i:843 = K:841)
                        /\ ((K:841 = 0 /\ 0 = mid_i:843
                               /\ __cost:103 = mid___cost:842)
                              \/ (1 <= K:841 /\ 0 <= (-1 + (n:102 * n:102))
                                    /\ 0 <= __cost:103
                                    /\ 0 <= (-1 + mid_i:843)
                                    /\ 0 <= (-1 + mid___cost:842)
                                    /\ 0 <= ((n:102 * n:102) + -mid_i:843)))
                        /\ K:844 = 0 /\ mid_i:843 = i':845
                        /\ mid___cost:842 = __cost':846 /\ 0 = K:844
                        /\ (K:841 + K:844) = K:847 /\ 0 <= K:847
                        /\ 0 <= i':845 /\ (n:102 * n:102) <= i':845
                        /\ __cost':846 = phi___cost:872 /\ i':845 = phi_i:871)
                       \/ (secret:106 < param0:35 /\ !(param1:38 = 1)
                             /\ !(param1:38 = 2)
                             /\ (!(0 <= K:864) \/ mid_i:865 = K:864)
                             /\ (!(0 <= K:864)
                                   \/ mid___cost:866 = (__cost:103 + K:864))
                             /\ ((K:864 = 0 /\ 0 = mid_i:865
                                    /\ __cost:103 = mid___cost:866)
                                   \/ (1 <= K:864
                                         /\ 0 <= (-1
                                                    + ((n:102 * n:102)
                                                         * n:102))
                                         /\ 0 <= __cost:103
                                         /\ 0 <= (-1 + mid_i:865)
                                         /\ 0 <= (-1 + mid___cost:866)
                                         /\ 0 <= (((n:102 * n:102) * n:102)
                                                    + -mid_i:865)))
                             /\ K:867 = 0 /\ mid_i:865 = i':868
                             /\ mid___cost:866 = __cost':869 /\ 0 = K:867
                             /\ (K:864 + K:867) = K:870 /\ 0 <= K:870
                             /\ 0 <= i':868
                             /\ ((n:102 * n:102) * n:102) <= i':868
                             /\ __cost':869 = phi___cost:872
                             /\ i':868 = phi_i:871))
                      /\ phi___cost:872 = phi___cost:874
                      /\ phi_i:871 = phi_i:873))
               /\ phi___cost:874 = phi___cost:876 /\ phi_i:873 = phi_i:875))}

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

Base relation: 
{n := 10
 secret := 1234
 __cost := phi___cost:1012
 guess := phi_guess:1011
 __retres7 := phi___retres7:1010
 argc := param0:35
 argv := param1:38
 return := phi___retres7:1010
 param0 := phi_param0:1008
 param1 := phi_param1:1007
 argv@pos := param1@pos:37
 return@pos := type_err:1013
 param0@pos := phi_param0@pos:1005
 param1@pos := phi_param1@pos:1004
 argv@width := param1@width:36
 return@width := type_err:1014
 param0@width := phi_param0@width:1002
 param1@width := phi_param1@width:1001
 when (((param0:35 < 3 \/ 3 < param0:35) /\ 0 = phi___cost:1012
          /\ guess:23 = phi_guess:1011 /\ -1 = phi___retres7:1010
          /\ return:943 = phi_return:1009 /\ param0:35 = phi_param0:1008
          /\ param1:38 = phi_param1:1007
          /\ return@pos:939 = phi_return@pos:1006
          /\ param0@pos:34 = phi_param0@pos:1005
          /\ param1@pos:37 = phi_param1@pos:1004
          /\ return@width:935 = phi_return@width:1003
          /\ param0@width:33 = phi_param0@width:1002
          /\ param1@width:36 = phi_param1@width:1001)
         \/ (3 <= param0:35 /\ param0:35 <= 3
               /\ ((((havoc:950 <= 1234 /\ havoc:954 = 1
                        /\ 1 = phi___cost:959 /\ i:960 = phi_i:961)
                       \/ (((havoc:950 <= 1234 /\ !(havoc:954 = 1)
                               /\ havoc:954 = 2
                               /\ (!(0 <= K:962) \/ mid_i:963 = K:962)
                               /\ (!(0 <= K:962) \/ mid___cost:964 = K:962)
                               /\ ((K:962 = 0 /\ 0 = mid_i:963
                                      /\ 0 = mid___cost:964)
                                     \/ (1 <= K:962 /\ 0 <= (-1 + 10)
                                           /\ 0 <= (-1 + mid_i:963)
                                           /\ 0 <= (-1 + mid___cost:964)
                                           /\ 0 <= (10 + -mid_i:963)))
                               /\ K:965 = 0 /\ mid_i:963 = i':966
                               /\ mid___cost:964 = __cost':967 /\ 0 = K:965
                               /\ (K:962 + K:965) = K:968 /\ 0 <= K:968
                               /\ 0 <= i':966 /\ 10 <= i':966
                               /\ __cost':967 = phi___cost:969
                               /\ i':966 = phi_i:970)
                              \/ (havoc:950 <= 1234 /\ !(havoc:954 = 1)
                                    /\ !(havoc:954 = 2)
                                    /\ (!(0 <= K:971) \/ mid_i:972 = K:971)
                                    /\ (!(0 <= K:971)
                                          \/ mid___cost:973 = K:971)
                                    /\ ((K:971 = 0 /\ 0 = mid_i:972
                                           /\ 0 = mid___cost:973)
                                          \/ (1 <= K:971 /\ 0 <= (-1 + 1000)
                                                /\ 0 <= (-1 + mid_i:972)
                                                /\ 0 <= (-1 + mid___cost:973)
                                                /\ 0 <= (1000 + -mid_i:972)))
                                    /\ K:974 = 0 /\ mid_i:972 = i':975
                                    /\ mid___cost:973 = __cost':976
                                    /\ 0 = K:974 /\ (K:971 + K:974) = K:977
                                    /\ 0 <= K:977 /\ 0 <= i':975
                                    /\ 1000 <= i':975
                                    /\ __cost':976 = phi___cost:969
                                    /\ i':975 = phi_i:970))
                             /\ phi___cost:969 = phi___cost:959
                             /\ phi_i:970 = phi_i:961))
                      /\ phi___cost:959 = phi___cost:978
                      /\ phi_i:961 = phi_i:979)
                     \/ (((1234 < havoc:950 /\ havoc:954 = 1
                             /\ 1 = phi___cost:980 /\ i:960 = phi_i:981)
                            \/ (((1234 < havoc:950 /\ !(havoc:954 = 1)
                                    /\ havoc:954 = 2
                                    /\ (!(0 <= K:982)
                                          \/ mid___cost:983 = K:982)
                                    /\ (!(0 <= K:982) \/ mid_i:984 = K:982)
                                    /\ ((K:982 = 0 /\ 0 = mid_i:984
                                           /\ 0 = mid___cost:983)
                                          \/ (1 <= K:982 /\ 0 <= (-1 + 100)
                                                /\ 0 <= (-1 + mid_i:984)
                                                /\ 0 <= (-1 + mid___cost:983)
                                                /\ 0 <= (100 + -mid_i:984)))
                                    /\ K:985 = 0 /\ mid_i:984 = i':986
                                    /\ mid___cost:983 = __cost':987
                                    /\ 0 = K:985 /\ (K:982 + K:985) = K:988
                                    /\ 0 <= K:988 /\ 0 <= i':986
                                    /\ 100 <= i':986
                                    /\ __cost':987 = phi___cost:989
                                    /\ i':986 = phi_i:990)
                                   \/ (1234 < havoc:950 /\ !(havoc:954 = 1)
                                         /\ !(havoc:954 = 2)
                                         /\ (!(0 <= K:991)
                                               \/ mid_i:992 = K:991)
                                         /\ (!(0 <= K:991)
                                               \/ mid___cost:993 = K:991)
                                         /\ ((K:991 = 0 /\ 0 = mid_i:992
                                                /\ 0 = mid___cost:993)
                                               \/ (1 <= K:991
                                                     /\ 0 <= (-1 + 1000)
                                                     /\ 0 <= (-1 + mid_i:992)
                                                     /\ 0 <= (-1
                                                                + mid___cost:993)
                                                     /\ 0 <= (1000
                                                                + -mid_i:992)))
                                         /\ K:994 = 0 /\ mid_i:992 = i':995
                                         /\ mid___cost:993 = __cost':996
                                         /\ 0 = K:994
                                         /\ (K:991 + K:994) = K:997
                                         /\ 0 <= K:997 /\ 0 <= i':995
                                         /\ 1000 <= i':995
                                         /\ __cost':996 = phi___cost:989
                                         /\ i':995 = phi_i:990))
                                  /\ phi___cost:989 = phi___cost:980
                                  /\ phi_i:990 = phi_i:981))
                           /\ phi___cost:980 = phi___cost:978
                           /\ phi_i:981 = phi_i:979))
               /\ phi___cost:978 = phi___cost:1012
               /\ havoc:950 = phi_guess:1011 /\ 0 = phi___retres7:1010
               /\ havoc:998 = phi_return:1009 /\ havoc:950 = phi_param0:1008
               /\ havoc:954 = phi_param1:1007
               /\ type_err:999 = phi_return@pos:1006
               /\ type_err:955 = phi_param0@pos:1005
               /\ type_err:956 = phi_param1@pos:1004
               /\ type_err:1000 = phi_return@width:1003
               /\ type_err:957 = phi_param0@width:1002
               /\ type_err:958 = phi_param1@width:1001))}

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

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

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