/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 * n:102) /\ 0 <= __cost:103 /\ 0 <= (__cost:103 + 1))}	
<Unique State Name, 85> -> <Unique State Name, 97>	Base relation: 
{when (n:102 * 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 * n:102) /\ 0 <= __cost:103
         /\ 0 <= (__cost:103 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':704) = (1)*(__cost:103) + 1
           (i':705) = (1)*(i:101) + 1
           }
          pre:
            [|-i:101+(n:102 * n:102)-1>=0; __cost:103>=0; i:101>=0|]
          post:
            [|i':705-1>=0; __cost':704-1>=0; (n:102 * n:102)-i':705>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':704
   i := i':705
   when ((!(0 <= K:716) \/ mid___cost:719 = (__cost:103 + K:716))
           /\ (!(0 <= K:716) \/ mid_i:718 = (i:101 + K:716))
           /\ ((K:716 = 0 /\ i:101 = mid_i:718 /\ __cost:103 = mid___cost:719)
                 \/ (1 <= K:716 /\ 0 <= (-1 + -i:101 + (n:102 * n:102))
                       /\ 0 <= __cost:103 /\ 0 <= i:101
                       /\ 0 <= (-1 + mid_i:718) /\ 0 <= (-1 + mid___cost:719)
                       /\ 0 <= ((n:102 * n:102) + -mid_i:718))) /\ K:717 = 0
           /\ mid_i:718 = i':705 /\ mid___cost:719 = __cost':704 /\ 0 = K:717
           /\ (K:716 + K:717) = K:715 /\ 0 <= K:715)}
}
(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':705) = (1)*(i:101) + 1
           (__cost':704) = (1)*(__cost:103) + 1
           }
          pre:
            [|-i:101+((n:102 * n:102) * n:102)-1>=0; __cost:103>=0; i:101>=0|]
          post:
            [|i':705-1>=0; __cost':704-1>=0;
              ((n:102 * n:102) * n:102)-i':705>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':704
   i := i':705
   when ((!(0 <= K:739) \/ mid_i:741 = (i:101 + K:739))
           /\ (!(0 <= K:739) \/ mid___cost:742 = (__cost:103 + K:739))
           /\ ((K:739 = 0 /\ i:101 = mid_i:741 /\ __cost:103 = mid___cost:742)
                 \/ (1 <= K:739
                       /\ 0 <= (-1 + -i:101 + ((n:102 * n:102) * n:102))
                       /\ 0 <= __cost:103 /\ 0 <= i:101
                       /\ 0 <= (-1 + mid_i:741) /\ 0 <= (-1 + mid___cost:742)
                       /\ 0 <= (((n:102 * n:102) * n:102) + -mid_i:741)))
           /\ K:740 = 0 /\ mid_i:741 = i':705 /\ mid___cost:742 = __cost':704
           /\ 0 = K:740 /\ (K:739 + K:740) = K:738 /\ 0 <= K:738)}
}
(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':704) = (1)*(__cost:103) + 1
           (i':705) = (1)*(i:101) + 1
           }
          pre:
            [|-i:101+(n:102 * n:102)-1>=0; __cost:103>=0; i:101>=0|]
          post:
            [|i':705-1>=0; __cost':704-1>=0; (n:102 * n:102)-i':705>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':704
   i := i':705
   when ((!(0 <= K:764) \/ mid___cost:767 = (__cost:103 + K:764))
           /\ (!(0 <= K:764) \/ mid_i:766 = (i:101 + K:764))
           /\ ((K:764 = 0 /\ i:101 = mid_i:766 /\ __cost:103 = mid___cost:767)
                 \/ (1 <= K:764 /\ 0 <= (-1 + -i:101 + (n:102 * n:102))
                       /\ 0 <= __cost:103 /\ 0 <= i:101
                       /\ 0 <= (-1 + mid_i:766) /\ 0 <= (-1 + mid___cost:767)
                       /\ 0 <= ((n:102 * n:102) + -mid_i:766))) /\ K:765 = 0
           /\ mid_i:766 = i':705 /\ mid___cost:767 = __cost':704 /\ 0 = K:765
           /\ (K:764 + K:765) = K:763 /\ 0 <= K:763)}
}
(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':705) = (1)*(i:101) + 1
           (__cost':704) = (1)*(__cost:103) + 1
           }
          pre:
            [|-i:101+((n:102 * n:102) * n:102)-1>=0; __cost:103>=0; i:101>=0|]
          post:
            [|i':705-1>=0; __cost':704-1>=0;
              ((n:102 * n:102) * n:102)-i':705>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':704
   i := i':705
   when ((!(0 <= K:787) \/ mid_i:789 = (i:101 + K:787))
           /\ (!(0 <= K:787) \/ mid___cost:790 = (__cost:103 + K:787))
           /\ ((K:787 = 0 /\ i:101 = mid_i:789 /\ __cost:103 = mid___cost:790)
                 \/ (1 <= K:787
                       /\ 0 <= (-1 + -i:101 + ((n:102 * n:102) * n:102))
                       /\ 0 <= __cost:103 /\ 0 <= i:101
                       /\ 0 <= (-1 + mid_i:789) /\ 0 <= (-1 + mid___cost:790)
                       /\ 0 <= (((n:102 * n:102) * n:102) + -mid_i:789)))
           /\ K:788 = 0 /\ mid_i:789 = i':705 /\ mid___cost:790 = __cost':704
           /\ 0 = K:788 /\ (K:787 + K:788) = K:786 /\ 0 <= K:786)}
}
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:701
                   argv@pos := param1@pos:37
                   param0@pos := type_err:702
                   argv@width := param1@width:36
                   param0@width := type_err:703
                   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:803
   i := phi_i:802
   guess := param0:35
   t := param1:38
   return := havoc:804
   return@pos := type_err:805
   return@width := type_err:806
   when ((((param0:35 <= secret:106 /\ param1:38 = 1 /\ 0 <= __cost:103
              /\ 0 <= (__cost:103 + 1) /\ (__cost:103 + 1) = phi___cost:753
              /\ i:101 = phi_i:752)
             \/ (((param0:35 <= secret:106 /\ !(param1:38 = 1)
                     /\ param1:38 = 2
                     /\ (!(0 <= K:720)
                           \/ mid___cost:721 = (__cost:103 + K:720))
                     /\ (!(0 <= K:720) \/ mid_i:722 = K:720)
                     /\ ((K:720 = 0 /\ 0 = mid_i:722
                            /\ __cost:103 = mid___cost:721)
                           \/ (1 <= K:720 /\ 0 <= (-1 + (n:102 * n:102))
                                 /\ 0 <= __cost:103 /\ 0 <= (-1 + mid_i:722)
                                 /\ 0 <= (-1 + mid___cost:721)
                                 /\ 0 <= ((n:102 * n:102) + -mid_i:722)))
                     /\ K:723 = 0 /\ mid_i:722 = i':724
                     /\ mid___cost:721 = __cost':725 /\ 0 = K:723
                     /\ (K:720 + K:723) = K:726 /\ 0 <= K:726 /\ 0 <= i':724
                     /\ (n:102 * n:102) <= i':724
                     /\ __cost':725 = phi___cost:751 /\ i':724 = phi_i:750)
                    \/ (param0:35 <= secret:106 /\ !(param1:38 = 1)
                          /\ !(param1:38 = 2)
                          /\ (!(0 <= K:743) \/ mid_i:744 = K:743)
                          /\ (!(0 <= K:743)
                                \/ mid___cost:745 = (__cost:103 + K:743))
                          /\ ((K:743 = 0 /\ 0 = mid_i:744
                                 /\ __cost:103 = mid___cost:745)
                                \/ (1 <= K:743
                                      /\ 0 <= (-1 + ((n:102 * n:102) * n:102))
                                      /\ 0 <= __cost:103
                                      /\ 0 <= (-1 + mid_i:744)
                                      /\ 0 <= (-1 + mid___cost:745)
                                      /\ 0 <= (((n:102 * n:102) * n:102)
                                                 + -mid_i:744))) /\ K:746 = 0
                          /\ mid_i:744 = i':747
                          /\ mid___cost:745 = __cost':748 /\ 0 = K:746
                          /\ (K:743 + K:746) = K:749 /\ 0 <= K:749
                          /\ 0 <= i':747
                          /\ ((n:102 * n:102) * n:102) <= i':747
                          /\ __cost':748 = phi___cost:751
                          /\ i':747 = phi_i:750))
                   /\ phi___cost:751 = phi___cost:753
                   /\ phi_i:750 = phi_i:752))
            /\ phi___cost:753 = phi___cost:803 /\ phi_i:752 = phi_i:802)
           \/ (((secret:106 < param0:35 /\ param1:38 = 1 /\ 0 <= __cost:103
                   /\ 0 <= (__cost:103 + 1)
                   /\ (__cost:103 + 1) = phi___cost:801 /\ i:101 = phi_i:800)
                  \/ (((secret:106 < param0:35 /\ !(param1:38 = 1)
                          /\ param1:38 = 2
                          /\ (!(0 <= K:768)
                                \/ mid___cost:769 = (__cost:103 + K:768))
                          /\ (!(0 <= K:768) \/ mid_i:770 = K:768)
                          /\ ((K:768 = 0 /\ 0 = mid_i:770
                                 /\ __cost:103 = mid___cost:769)
                                \/ (1 <= K:768 /\ 0 <= (-1 + (n:102 * n:102))
                                      /\ 0 <= __cost:103
                                      /\ 0 <= (-1 + mid_i:770)
                                      /\ 0 <= (-1 + mid___cost:769)
                                      /\ 0 <= ((n:102 * n:102) + -mid_i:770)))
                          /\ K:771 = 0 /\ mid_i:770 = i':772
                          /\ mid___cost:769 = __cost':773 /\ 0 = K:771
                          /\ (K:768 + K:771) = K:774 /\ 0 <= K:774
                          /\ 0 <= i':772 /\ (n:102 * n:102) <= i':772
                          /\ __cost':773 = phi___cost:799
                          /\ i':772 = phi_i:798)
                         \/ (secret:106 < param0:35 /\ !(param1:38 = 1)
                               /\ !(param1:38 = 2)
                               /\ (!(0 <= K:791) \/ mid_i:792 = K:791)
                               /\ (!(0 <= K:791)
                                     \/ mid___cost:793 = (__cost:103 + K:791))
                               /\ ((K:791 = 0 /\ 0 = mid_i:792
                                      /\ __cost:103 = mid___cost:793)
                                     \/ (1 <= K:791
                                           /\ 0 <= (-1
                                                      + ((n:102 * n:102)
                                                           * n:102))
                                           /\ 0 <= __cost:103
                                           /\ 0 <= (-1 + mid_i:792)
                                           /\ 0 <= (-1 + mid___cost:793)
                                           /\ 0 <= (((n:102 * n:102) * n:102)
                                                      + -mid_i:792)))
                               /\ K:794 = 0 /\ mid_i:792 = i':795
                               /\ mid___cost:793 = __cost':796 /\ 0 = K:794
                               /\ (K:791 + K:794) = K:797 /\ 0 <= K:797
                               /\ 0 <= i':795
                               /\ ((n:102 * n:102) * n:102) <= i':795
                               /\ __cost':796 = phi___cost:799
                               /\ i':795 = phi_i:798))
                        /\ phi___cost:799 = phi___cost:801
                        /\ phi_i:798 = phi_i:800))
                 /\ phi___cost:801 = phi___cost:803 /\ phi_i:800 = phi_i:802))})



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:701
                     argv@pos := param1@pos:37
                     param0@pos := type_err:702
                     argv@width := param1@width:36
                     param0@width := type_err:703
                     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:803
   return := havoc:804
   return@pos := type_err:805
   return@width := type_err:806
   when ((((param0:35 <= secret:106 /\ param1:38 = 1 /\ 0 <= __cost:103
              /\ 0 <= (__cost:103 + 1) /\ (__cost:103 + 1) = phi___cost:753
              /\ i:807 = phi_i:752)
             \/ (((param0:35 <= secret:106 /\ !(param1:38 = 1)
                     /\ param1:38 = 2
                     /\ (!(0 <= K:720)
                           \/ mid___cost:721 = (__cost:103 + K:720))
                     /\ (!(0 <= K:720) \/ mid_i:722 = K:720)
                     /\ ((K:720 = 0 /\ 0 = mid_i:722
                            /\ __cost:103 = mid___cost:721)
                           \/ (1 <= K:720 /\ 0 <= (-1 + (n:102 * n:102))
                                 /\ 0 <= __cost:103 /\ 0 <= (-1 + mid_i:722)
                                 /\ 0 <= (-1 + mid___cost:721)
                                 /\ 0 <= ((n:102 * n:102) + -mid_i:722)))
                     /\ K:723 = 0 /\ mid_i:722 = i':724
                     /\ mid___cost:721 = __cost':725 /\ 0 = K:723
                     /\ (K:720 + K:723) = K:726 /\ 0 <= K:726 /\ 0 <= i':724
                     /\ (n:102 * n:102) <= i':724
                     /\ __cost':725 = phi___cost:751 /\ i':724 = phi_i:750)
                    \/ (param0:35 <= secret:106 /\ !(param1:38 = 1)
                          /\ !(param1:38 = 2)
                          /\ (!(0 <= K:743) \/ mid_i:744 = K:743)
                          /\ (!(0 <= K:743)
                                \/ mid___cost:745 = (__cost:103 + K:743))
                          /\ ((K:743 = 0 /\ 0 = mid_i:744
                                 /\ __cost:103 = mid___cost:745)
                                \/ (1 <= K:743
                                      /\ 0 <= (-1 + ((n:102 * n:102) * n:102))
                                      /\ 0 <= __cost:103
                                      /\ 0 <= (-1 + mid_i:744)
                                      /\ 0 <= (-1 + mid___cost:745)
                                      /\ 0 <= (((n:102 * n:102) * n:102)
                                                 + -mid_i:744))) /\ K:746 = 0
                          /\ mid_i:744 = i':747
                          /\ mid___cost:745 = __cost':748 /\ 0 = K:746
                          /\ (K:743 + K:746) = K:749 /\ 0 <= K:749
                          /\ 0 <= i':747
                          /\ ((n:102 * n:102) * n:102) <= i':747
                          /\ __cost':748 = phi___cost:751
                          /\ i':747 = phi_i:750))
                   /\ phi___cost:751 = phi___cost:753
                   /\ phi_i:750 = phi_i:752))
            /\ phi___cost:753 = phi___cost:803 /\ phi_i:752 = phi_i:802)
           \/ (((secret:106 < param0:35 /\ param1:38 = 1 /\ 0 <= __cost:103
                   /\ 0 <= (__cost:103 + 1)
                   /\ (__cost:103 + 1) = phi___cost:801 /\ i:807 = phi_i:800)
                  \/ (((secret:106 < param0:35 /\ !(param1:38 = 1)
                          /\ param1:38 = 2
                          /\ (!(0 <= K:768)
                                \/ mid___cost:769 = (__cost:103 + K:768))
                          /\ (!(0 <= K:768) \/ mid_i:770 = K:768)
                          /\ ((K:768 = 0 /\ 0 = mid_i:770
                                 /\ __cost:103 = mid___cost:769)
                                \/ (1 <= K:768 /\ 0 <= (-1 + (n:102 * n:102))
                                      /\ 0 <= __cost:103
                                      /\ 0 <= (-1 + mid_i:770)
                                      /\ 0 <= (-1 + mid___cost:769)
                                      /\ 0 <= ((n:102 * n:102) + -mid_i:770)))
                          /\ K:771 = 0 /\ mid_i:770 = i':772
                          /\ mid___cost:769 = __cost':773 /\ 0 = K:771
                          /\ (K:768 + K:771) = K:774 /\ 0 <= K:774
                          /\ 0 <= i':772 /\ (n:102 * n:102) <= i':772
                          /\ __cost':773 = phi___cost:799
                          /\ i':772 = phi_i:798)
                         \/ (secret:106 < param0:35 /\ !(param1:38 = 1)
                               /\ !(param1:38 = 2)
                               /\ (!(0 <= K:791) \/ mid_i:792 = K:791)
                               /\ (!(0 <= K:791)
                                     \/ mid___cost:793 = (__cost:103 + K:791))
                               /\ ((K:791 = 0 /\ 0 = mid_i:792
                                      /\ __cost:103 = mid___cost:793)
                                     \/ (1 <= K:791
                                           /\ 0 <= (-1
                                                      + ((n:102 * n:102)
                                                           * n:102))
                                           /\ 0 <= __cost:103
                                           /\ 0 <= (-1 + mid_i:792)
                                           /\ 0 <= (-1 + mid___cost:793)
                                           /\ 0 <= (((n:102 * n:102) * n:102)
                                                      + -mid_i:792)))
                               /\ K:794 = 0 /\ mid_i:792 = i':795
                               /\ mid___cost:793 = __cost':796 /\ 0 = K:794
                               /\ (K:791 + K:794) = K:797 /\ 0 <= K:797
                               /\ 0 <= i':795
                               /\ ((n:102 * n:102) * n:102) <= i':795
                               /\ __cost':796 = phi___cost:799
                               /\ i':795 = phi_i:798))
                        /\ phi___cost:799 = phi___cost:801
                        /\ phi_i:798 = phi_i:800))
                 /\ phi___cost:801 = phi___cost:803 /\ phi_i:800 = phi_i:802))})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=14: 
Weight(Base relation: 
  {n := 10
   secret := 1234
   __cost := phi___cost:873
   return := phi___retres7:871
   param0 := phi_param0:868
   param1 := phi_param1:867
   return@pos := type_err:874
   param0@pos := phi_param0@pos:864
   param1@pos := phi_param1@pos:863
   return@width := type_err:875
   param0@width := phi_param0@width:860
   param1@width := phi_param1@width:859
   when (((param0:35 < 3 \/ 3 < param0:35) /\ 0 = phi___cost:873
            /\ guess:876 = phi_guess:872 /\ -1 = phi___retres7:871
            /\ return:870 = phi_return:869 /\ param0:35 = phi_param0:868
            /\ param1:38 = phi_param1:867
            /\ return@pos:866 = phi_return@pos:865
            /\ param0@pos:34 = phi_param0@pos:864
            /\ param1@pos:37 = phi_param1@pos:863
            /\ return@width:862 = phi_return@width:861
            /\ param0@width:33 = phi_param0@width:860
            /\ param1@width:36 = phi_param1@width:859)
           \/ (3 <= param0:35 /\ param0:35 <= 3
                 /\ ((((havoc:808 <= 1234 /\ havoc:812 = 1
                          /\ 1 = phi___cost:817 /\ i:818 = phi_i:819)
                         \/ (((havoc:808 <= 1234 /\ !(havoc:812 = 1)
                                 /\ havoc:812 = 2
                                 /\ (!(0 <= K:820) \/ mid___cost:821 = K:820)
                                 /\ (!(0 <= K:820) \/ mid_i:822 = K:820)
                                 /\ ((K:820 = 0 /\ 0 = mid_i:822
                                        /\ 0 = mid___cost:821)
                                       \/ (1 <= K:820 /\ 0 <= (-1 + 100)
                                             /\ 0 <= (-1 + mid_i:822)
                                             /\ 0 <= (-1 + mid___cost:821)
                                             /\ 0 <= (100 + -mid_i:822)))
                                 /\ K:823 = 0 /\ mid_i:822 = i':824
                                 /\ mid___cost:821 = __cost':825 /\ 0 = K:823
                                 /\ (K:820 + K:823) = K:826 /\ 0 <= K:826
                                 /\ 0 <= i':824 /\ 100 <= i':824
                                 /\ __cost':825 = phi___cost:827
                                 /\ i':824 = phi_i:828)
                                \/ (havoc:808 <= 1234 /\ !(havoc:812 = 1)
                                      /\ !(havoc:812 = 2)
                                      /\ (!(0 <= K:829) \/ mid_i:830 = K:829)
                                      /\ (!(0 <= K:829)
                                            \/ mid___cost:831 = K:829)
                                      /\ ((K:829 = 0 /\ 0 = mid_i:830
                                             /\ 0 = mid___cost:831)
                                            \/ (1 <= K:829
                                                  /\ 0 <= (-1 + 1000)
                                                  /\ 0 <= (-1 + mid_i:830)
                                                  /\ 0 <= (-1
                                                             + mid___cost:831)
                                                  /\ 0 <= (1000 + -mid_i:830)))
                                      /\ K:832 = 0 /\ mid_i:830 = i':833
                                      /\ mid___cost:831 = __cost':834
                                      /\ 0 = K:832 /\ (K:829 + K:832) = K:835
                                      /\ 0 <= K:835 /\ 0 <= i':833
                                      /\ 1000 <= i':833
                                      /\ __cost':834 = phi___cost:827
                                      /\ i':833 = phi_i:828))
                               /\ phi___cost:827 = phi___cost:817
                               /\ phi_i:828 = phi_i:819))
                        /\ phi___cost:817 = phi___cost:836
                        /\ phi_i:819 = phi_i:837)
                       \/ (((1234 < havoc:808 /\ havoc:812 = 1
                               /\ 1 = phi___cost:838 /\ i:818 = phi_i:839)
                              \/ (((1234 < havoc:808 /\ !(havoc:812 = 1)
                                      /\ havoc:812 = 2
                                      /\ (!(0 <= K:840)
                                            \/ mid___cost:841 = K:840)
                                      /\ (!(0 <= K:840) \/ mid_i:842 = K:840)
                                      /\ ((K:840 = 0 /\ 0 = mid_i:842
                                             /\ 0 = mid___cost:841)
                                            \/ (1 <= K:840 /\ 0 <= (-1 + 100)
                                                  /\ 0 <= (-1 + mid_i:842)
                                                  /\ 0 <= (-1
                                                             + mid___cost:841)
                                                  /\ 0 <= (100 + -mid_i:842)))
                                      /\ K:843 = 0 /\ mid_i:842 = i':844
                                      /\ mid___cost:841 = __cost':845
                                      /\ 0 = K:843 /\ (K:840 + K:843) = K:846
                                      /\ 0 <= K:846 /\ 0 <= i':844
                                      /\ 100 <= i':844
                                      /\ __cost':845 = phi___cost:847
                                      /\ i':844 = phi_i:848)
                                     \/ (1234 < havoc:808 /\ !(havoc:812 = 1)
                                           /\ !(havoc:812 = 2)
                                           /\ (!(0 <= K:849)
                                                 \/ mid_i:850 = K:849)
                                           /\ (!(0 <= K:849)
                                                 \/ mid___cost:851 = K:849)
                                           /\ ((K:849 = 0 /\ 0 = mid_i:850
                                                  /\ 0 = mid___cost:851)
                                                 \/ (1 <= K:849
                                                       /\ 0 <= (-1 + 1000)
                                                       /\ 0 <= (-1
                                                                  + mid_i:850)
                                                       /\ 0 <= (-1
                                                                  + mid___cost:851)
                                                       /\ 0 <= (1000
                                                                  + -mid_i:850)))
                                           /\ K:852 = 0 /\ mid_i:850 = i':853
                                           /\ mid___cost:851 = __cost':854
                                           /\ 0 = K:852
                                           /\ (K:849 + K:852) = K:855
                                           /\ 0 <= K:855 /\ 0 <= i':853
                                           /\ 1000 <= i':853
                                           /\ __cost':854 = phi___cost:847
                                           /\ i':853 = phi_i:848))
                                    /\ phi___cost:847 = phi___cost:838
                                    /\ phi_i:848 = phi_i:839))
                             /\ phi___cost:838 = phi___cost:836
                             /\ phi_i:839 = phi_i:837))
                 /\ phi___cost:836 = phi___cost:873
                 /\ havoc:808 = phi_guess:872 /\ 0 = phi___retres7:871
                 /\ havoc:856 = phi_return:869 /\ havoc:808 = phi_param0:868
                 /\ havoc:812 = phi_param1:867
                 /\ type_err:857 = phi_return@pos:865
                 /\ type_err:813 = phi_param0@pos:864
                 /\ type_err:814 = phi_param1@pos:863
                 /\ type_err:858 = phi_return@width:861
                 /\ type_err:815 = phi_param0@width:860
                 /\ type_err:816 = phi_param1@width:859))})


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:803
   return := havoc:804
   return@pos := type_err:805
   return@width := type_err:806
   when ((((param0:35 <= secret:106 /\ param1:38 = 1 /\ 0 <= __cost:103
              /\ 0 <= (__cost:103 + 1) /\ (__cost:103 + 1) = phi___cost:753
              /\ i:807 = phi_i:752)
             \/ (((param0:35 <= secret:106 /\ !(param1:38 = 1)
                     /\ param1:38 = 2
                     /\ (!(0 <= K:720)
                           \/ mid___cost:721 = (__cost:103 + K:720))
                     /\ (!(0 <= K:720) \/ mid_i:722 = K:720)
                     /\ ((K:720 = 0 /\ 0 = mid_i:722
                            /\ __cost:103 = mid___cost:721)
                           \/ (1 <= K:720 /\ 0 <= (-1 + (n:102 * n:102))
                                 /\ 0 <= __cost:103 /\ 0 <= (-1 + mid_i:722)
                                 /\ 0 <= (-1 + mid___cost:721)
                                 /\ 0 <= ((n:102 * n:102) + -mid_i:722)))
                     /\ K:723 = 0 /\ mid_i:722 = i':724
                     /\ mid___cost:721 = __cost':725 /\ 0 = K:723
                     /\ (K:720 + K:723) = K:726 /\ 0 <= K:726 /\ 0 <= i':724
                     /\ (n:102 * n:102) <= i':724
                     /\ __cost':725 = phi___cost:751 /\ i':724 = phi_i:750)
                    \/ (param0:35 <= secret:106 /\ !(param1:38 = 1)
                          /\ !(param1:38 = 2)
                          /\ (!(0 <= K:743) \/ mid_i:744 = K:743)
                          /\ (!(0 <= K:743)
                                \/ mid___cost:745 = (__cost:103 + K:743))
                          /\ ((K:743 = 0 /\ 0 = mid_i:744
                                 /\ __cost:103 = mid___cost:745)
                                \/ (1 <= K:743
                                      /\ 0 <= (-1 + ((n:102 * n:102) * n:102))
                                      /\ 0 <= __cost:103
                                      /\ 0 <= (-1 + mid_i:744)
                                      /\ 0 <= (-1 + mid___cost:745)
                                      /\ 0 <= (((n:102 * n:102) * n:102)
                                                 + -mid_i:744))) /\ K:746 = 0
                          /\ mid_i:744 = i':747
                          /\ mid___cost:745 = __cost':748 /\ 0 = K:746
                          /\ (K:743 + K:746) = K:749 /\ 0 <= K:749
                          /\ 0 <= i':747
                          /\ ((n:102 * n:102) * n:102) <= i':747
                          /\ __cost':748 = phi___cost:751
                          /\ i':747 = phi_i:750))
                   /\ phi___cost:751 = phi___cost:753
                   /\ phi_i:750 = phi_i:752))
            /\ phi___cost:753 = phi___cost:803 /\ phi_i:752 = phi_i:802)
           \/ (((secret:106 < param0:35 /\ param1:38 = 1 /\ 0 <= __cost:103
                   /\ 0 <= (__cost:103 + 1)
                   /\ (__cost:103 + 1) = phi___cost:801 /\ i:807 = phi_i:800)
                  \/ (((secret:106 < param0:35 /\ !(param1:38 = 1)
                          /\ param1:38 = 2
                          /\ (!(0 <= K:768)
                                \/ mid___cost:769 = (__cost:103 + K:768))
                          /\ (!(0 <= K:768) \/ mid_i:770 = K:768)
                          /\ ((K:768 = 0 /\ 0 = mid_i:770
                                 /\ __cost:103 = mid___cost:769)
                                \/ (1 <= K:768 /\ 0 <= (-1 + (n:102 * n:102))
                                      /\ 0 <= __cost:103
                                      /\ 0 <= (-1 + mid_i:770)
                                      /\ 0 <= (-1 + mid___cost:769)
                                      /\ 0 <= ((n:102 * n:102) + -mid_i:770)))
                          /\ K:771 = 0 /\ mid_i:770 = i':772
                          /\ mid___cost:769 = __cost':773 /\ 0 = K:771
                          /\ (K:768 + K:771) = K:774 /\ 0 <= K:774
                          /\ 0 <= i':772 /\ (n:102 * n:102) <= i':772
                          /\ __cost':773 = phi___cost:799
                          /\ i':772 = phi_i:798)
                         \/ (secret:106 < param0:35 /\ !(param1:38 = 1)
                               /\ !(param1:38 = 2)
                               /\ (!(0 <= K:791) \/ mid_i:792 = K:791)
                               /\ (!(0 <= K:791)
                                     \/ mid___cost:793 = (__cost:103 + K:791))
                               /\ ((K:791 = 0 /\ 0 = mid_i:792
                                      /\ __cost:103 = mid___cost:793)
                                     \/ (1 <= K:791
                                           /\ 0 <= (-1
                                                      + ((n:102 * n:102)
                                                           * n:102))
                                           /\ 0 <= __cost:103
                                           /\ 0 <= (-1 + mid_i:792)
                                           /\ 0 <= (-1 + mid___cost:793)
                                           /\ 0 <= (((n:102 * n:102) * n:102)
                                                      + -mid_i:792)))
                               /\ K:794 = 0 /\ mid_i:792 = i':795
                               /\ mid___cost:793 = __cost':796 /\ 0 = K:794
                               /\ (K:791 + K:794) = K:797 /\ 0 <= K:797
                               /\ 0 <= i':795
                               /\ ((n:102 * n:102) * n:102) <= i':795
                               /\ __cost':796 = phi___cost:799
                               /\ i':795 = phi_i:798))
                        /\ phi___cost:799 = phi___cost:801
                        /\ phi_i:798 = phi_i:800))
                 /\ phi___cost:801 = phi___cost:803 /\ phi_i:800 = phi_i:802))})


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:873
 return := phi___retres7:871
 param0 := phi_param0:868
 param1 := phi_param1:867
 return@pos := type_err:874
 param0@pos := phi_param0@pos:864
 param1@pos := phi_param1@pos:863
 return@width := type_err:875
 param0@width := phi_param0@width:860
 param1@width := phi_param1@width:859
 when (((param0:35 < 3 \/ 3 < param0:35) /\ 0 = phi___cost:873
          /\ guess:876 = phi_guess:872 /\ -1 = phi___retres7:871
          /\ return:870 = phi_return:869 /\ param0:35 = phi_param0:868
          /\ param1:38 = phi_param1:867
          /\ return@pos:866 = phi_return@pos:865
          /\ param0@pos:34 = phi_param0@pos:864
          /\ param1@pos:37 = phi_param1@pos:863
          /\ return@width:862 = phi_return@width:861
          /\ param0@width:33 = phi_param0@width:860
          /\ param1@width:36 = phi_param1@width:859)
         \/ (3 <= param0:35 /\ param0:35 <= 3
               /\ ((((havoc:808 <= 1234 /\ havoc:812 = 1
                        /\ 1 = phi___cost:817 /\ i:818 = phi_i:819)
                       \/ (((havoc:808 <= 1234 /\ !(havoc:812 = 1)
                               /\ havoc:812 = 2
                               /\ (!(0 <= K:820) \/ mid___cost:821 = K:820)
                               /\ (!(0 <= K:820) \/ mid_i:822 = K:820)
                               /\ ((K:820 = 0 /\ 0 = mid_i:822
                                      /\ 0 = mid___cost:821)
                                     \/ (1 <= K:820 /\ 0 <= (-1 + 100)
                                           /\ 0 <= (-1 + mid_i:822)
                                           /\ 0 <= (-1 + mid___cost:821)
                                           /\ 0 <= (100 + -mid_i:822)))
                               /\ K:823 = 0 /\ mid_i:822 = i':824
                               /\ mid___cost:821 = __cost':825 /\ 0 = K:823
                               /\ (K:820 + K:823) = K:826 /\ 0 <= K:826
                               /\ 0 <= i':824 /\ 100 <= i':824
                               /\ __cost':825 = phi___cost:827
                               /\ i':824 = phi_i:828)
                              \/ (havoc:808 <= 1234 /\ !(havoc:812 = 1)
                                    /\ !(havoc:812 = 2)
                                    /\ (!(0 <= K:829) \/ mid_i:830 = K:829)
                                    /\ (!(0 <= K:829)
                                          \/ mid___cost:831 = K:829)
                                    /\ ((K:829 = 0 /\ 0 = mid_i:830
                                           /\ 0 = mid___cost:831)
                                          \/ (1 <= K:829 /\ 0 <= (-1 + 1000)
                                                /\ 0 <= (-1 + mid_i:830)
                                                /\ 0 <= (-1 + mid___cost:831)
                                                /\ 0 <= (1000 + -mid_i:830)))
                                    /\ K:832 = 0 /\ mid_i:830 = i':833
                                    /\ mid___cost:831 = __cost':834
                                    /\ 0 = K:832 /\ (K:829 + K:832) = K:835
                                    /\ 0 <= K:835 /\ 0 <= i':833
                                    /\ 1000 <= i':833
                                    /\ __cost':834 = phi___cost:827
                                    /\ i':833 = phi_i:828))
                             /\ phi___cost:827 = phi___cost:817
                             /\ phi_i:828 = phi_i:819))
                      /\ phi___cost:817 = phi___cost:836
                      /\ phi_i:819 = phi_i:837)
                     \/ (((1234 < havoc:808 /\ havoc:812 = 1
                             /\ 1 = phi___cost:838 /\ i:818 = phi_i:839)
                            \/ (((1234 < havoc:808 /\ !(havoc:812 = 1)
                                    /\ havoc:812 = 2
                                    /\ (!(0 <= K:840)
                                          \/ mid___cost:841 = K:840)
                                    /\ (!(0 <= K:840) \/ mid_i:842 = K:840)
                                    /\ ((K:840 = 0 /\ 0 = mid_i:842
                                           /\ 0 = mid___cost:841)
                                          \/ (1 <= K:840 /\ 0 <= (-1 + 100)
                                                /\ 0 <= (-1 + mid_i:842)
                                                /\ 0 <= (-1 + mid___cost:841)
                                                /\ 0 <= (100 + -mid_i:842)))
                                    /\ K:843 = 0 /\ mid_i:842 = i':844
                                    /\ mid___cost:841 = __cost':845
                                    /\ 0 = K:843 /\ (K:840 + K:843) = K:846
                                    /\ 0 <= K:846 /\ 0 <= i':844
                                    /\ 100 <= i':844
                                    /\ __cost':845 = phi___cost:847
                                    /\ i':844 = phi_i:848)
                                   \/ (1234 < havoc:808 /\ !(havoc:812 = 1)
                                         /\ !(havoc:812 = 2)
                                         /\ (!(0 <= K:849)
                                               \/ mid_i:850 = K:849)
                                         /\ (!(0 <= K:849)
                                               \/ mid___cost:851 = K:849)
                                         /\ ((K:849 = 0 /\ 0 = mid_i:850
                                                /\ 0 = mid___cost:851)
                                               \/ (1 <= K:849
                                                     /\ 0 <= (-1 + 1000)
                                                     /\ 0 <= (-1 + mid_i:850)
                                                     /\ 0 <= (-1
                                                                + mid___cost:851)
                                                     /\ 0 <= (1000
                                                                + -mid_i:850)))
                                         /\ K:852 = 0 /\ mid_i:850 = i':853
                                         /\ mid___cost:851 = __cost':854
                                         /\ 0 = K:852
                                         /\ (K:849 + K:852) = K:855
                                         /\ 0 <= K:855 /\ 0 <= i':853
                                         /\ 1000 <= i':853
                                         /\ __cost':854 = phi___cost:847
                                         /\ i':853 = phi_i:848))
                                  /\ phi___cost:847 = phi___cost:838
                                  /\ phi_i:848 = phi_i:839))
                           /\ phi___cost:838 = phi___cost:836
                           /\ phi_i:839 = phi_i:837))
               /\ phi___cost:836 = phi___cost:873
               /\ havoc:808 = phi_guess:872 /\ 0 = phi___retres7:871
               /\ havoc:856 = phi_return:869 /\ havoc:808 = phi_param0:868
               /\ havoc:812 = phi_param1:867
               /\ type_err:857 = phi_return@pos:865
               /\ type_err:813 = phi_param0@pos:864
               /\ type_err:814 = phi_param1@pos:863
               /\ type_err:858 = phi_return@width:861
               /\ type_err:815 = phi_param0@width:860
               /\ type_err:816 = phi_param1@width:859))}

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:803
 return := havoc:804
 return@pos := type_err:805
 return@width := type_err:806
 when ((((param0:35 <= secret:106 /\ param1:38 = 1 /\ 0 <= __cost:103
            /\ 0 <= (__cost:103 + 1) /\ (__cost:103 + 1) = phi___cost:753
            /\ i:807 = phi_i:752)
           \/ (((param0:35 <= secret:106 /\ !(param1:38 = 1) /\ param1:38 = 2
                   /\ (!(0 <= K:720) \/ mid___cost:721 = (__cost:103 + K:720))
                   /\ (!(0 <= K:720) \/ mid_i:722 = K:720)
                   /\ ((K:720 = 0 /\ 0 = mid_i:722
                          /\ __cost:103 = mid___cost:721)
                         \/ (1 <= K:720 /\ 0 <= (-1 + (n:102 * n:102))
                               /\ 0 <= __cost:103 /\ 0 <= (-1 + mid_i:722)
                               /\ 0 <= (-1 + mid___cost:721)
                               /\ 0 <= ((n:102 * n:102) + -mid_i:722)))
                   /\ K:723 = 0 /\ mid_i:722 = i':724
                   /\ mid___cost:721 = __cost':725 /\ 0 = K:723
                   /\ (K:720 + K:723) = K:726 /\ 0 <= K:726 /\ 0 <= i':724
                   /\ (n:102 * n:102) <= i':724
                   /\ __cost':725 = phi___cost:751 /\ i':724 = phi_i:750)
                  \/ (param0:35 <= secret:106 /\ !(param1:38 = 1)
                        /\ !(param1:38 = 2)
                        /\ (!(0 <= K:743) \/ mid_i:744 = K:743)
                        /\ (!(0 <= K:743)
                              \/ mid___cost:745 = (__cost:103 + K:743))
                        /\ ((K:743 = 0 /\ 0 = mid_i:744
                               /\ __cost:103 = mid___cost:745)
                              \/ (1 <= K:743
                                    /\ 0 <= (-1 + ((n:102 * n:102) * n:102))
                                    /\ 0 <= __cost:103
                                    /\ 0 <= (-1 + mid_i:744)
                                    /\ 0 <= (-1 + mid___cost:745)
                                    /\ 0 <= (((n:102 * n:102) * n:102)
                                               + -mid_i:744))) /\ K:746 = 0
                        /\ mid_i:744 = i':747 /\ mid___cost:745 = __cost':748
                        /\ 0 = K:746 /\ (K:743 + K:746) = K:749 /\ 0 <= K:749
                        /\ 0 <= i':747 /\ ((n:102 * n:102) * n:102) <= i':747
                        /\ __cost':748 = phi___cost:751 /\ i':747 = phi_i:750))
                 /\ phi___cost:751 = phi___cost:753 /\ phi_i:750 = phi_i:752))
          /\ phi___cost:753 = phi___cost:803 /\ phi_i:752 = phi_i:802)
         \/ (((secret:106 < param0:35 /\ param1:38 = 1 /\ 0 <= __cost:103
                 /\ 0 <= (__cost:103 + 1)
                 /\ (__cost:103 + 1) = phi___cost:801 /\ i:807 = phi_i:800)
                \/ (((secret:106 < param0:35 /\ !(param1:38 = 1)
                        /\ param1:38 = 2
                        /\ (!(0 <= K:768)
                              \/ mid___cost:769 = (__cost:103 + K:768))
                        /\ (!(0 <= K:768) \/ mid_i:770 = K:768)
                        /\ ((K:768 = 0 /\ 0 = mid_i:770
                               /\ __cost:103 = mid___cost:769)
                              \/ (1 <= K:768 /\ 0 <= (-1 + (n:102 * n:102))
                                    /\ 0 <= __cost:103
                                    /\ 0 <= (-1 + mid_i:770)
                                    /\ 0 <= (-1 + mid___cost:769)
                                    /\ 0 <= ((n:102 * n:102) + -mid_i:770)))
                        /\ K:771 = 0 /\ mid_i:770 = i':772
                        /\ mid___cost:769 = __cost':773 /\ 0 = K:771
                        /\ (K:768 + K:771) = K:774 /\ 0 <= K:774
                        /\ 0 <= i':772 /\ (n:102 * n:102) <= i':772
                        /\ __cost':773 = phi___cost:799 /\ i':772 = phi_i:798)
                       \/ (secret:106 < param0:35 /\ !(param1:38 = 1)
                             /\ !(param1:38 = 2)
                             /\ (!(0 <= K:791) \/ mid_i:792 = K:791)
                             /\ (!(0 <= K:791)
                                   \/ mid___cost:793 = (__cost:103 + K:791))
                             /\ ((K:791 = 0 /\ 0 = mid_i:792
                                    /\ __cost:103 = mid___cost:793)
                                   \/ (1 <= K:791
                                         /\ 0 <= (-1
                                                    + ((n:102 * n:102)
                                                         * n:102))
                                         /\ 0 <= __cost:103
                                         /\ 0 <= (-1 + mid_i:792)
                                         /\ 0 <= (-1 + mid___cost:793)
                                         /\ 0 <= (((n:102 * n:102) * n:102)
                                                    + -mid_i:792)))
                             /\ K:794 = 0 /\ mid_i:792 = i':795
                             /\ mid___cost:793 = __cost':796 /\ 0 = K:794
                             /\ (K:791 + K:794) = K:797 /\ 0 <= K:797
                             /\ 0 <= i':795
                             /\ ((n:102 * n:102) * n:102) <= i':795
                             /\ __cost':796 = phi___cost:799
                             /\ i':795 = phi_i:798))
                      /\ phi___cost:799 = phi___cost:801
                      /\ phi_i:798 = phi_i:800))
               /\ phi___cost:801 = phi___cost:803 /\ phi_i:800 = phi_i:802))}

    (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:945
 argc := param0:35
 argv := param1:38
 param0 := phi_param0:944
 argv@pos := param1@pos:37
 param0@pos := phi_param0@pos:943
 argv@width := param1@width:36
 param0@width := phi_param0@width:942
 when ((3 <= param0:35 /\ param0:35 <= 3 /\ havoc:877 = phi_guess:945
          /\ tr:878 = phi_param0:944 /\ type_err:879 = phi_param0@pos:943
          /\ type_err:880 = phi_param0@width:942)
         \/ (3 <= param0:35 /\ param0:35 <= 3 /\ guess:23 = phi_guess:945
               /\ tr:701 = phi_param0:944
               /\ type_err:702 = phi_param0@pos:943
               /\ type_err:703 = phi_param0@width:942))}	
<__pstate, accept> -> <__pstate, (Unique State Name,116)_g1>	Base relation: 
{n := 10
 secret := 1234
 __cost := 0
 guess := havoc:877
 argc := param0:35
 argv := param1:38
 param0 := havoc:877
 param1 := havoc:881
 argv@pos := param1@pos:37
 param0@pos := type_err:882
 param1@pos := type_err:883
 argv@width := param1@width:36
 param0@width := type_err:884
 param1@width := type_err:885
 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 0x11f5be90: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0xf17ad50: 
	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:945
 argc := param0:35
 argv := param1:38
 param0 := phi_param0:944
 argv@pos := param1@pos:37
 param0@pos := phi_param0@pos:943
 argv@width := param1@width:36
 param0@width := phi_param0@width:942
 when ((3 <= param0:35 /\ param0:35 <= 3 /\ havoc:877 = phi_guess:945
          /\ tr:878 = phi_param0:944 /\ type_err:879 = phi_param0@pos:943
          /\ type_err:880 = phi_param0@width:942)
         \/ (3 <= param0:35 /\ param0:35 <= 3 /\ guess:23 = phi_guess:945
               /\ tr:701 = phi_param0:944
               /\ type_err:702 = phi_param0@pos:943
               /\ type_err:703 = phi_param0@width:942))}
    ( __pstate , (Unique State Name,116)_g1 , __done )	Base relation: 
{n := 10
 secret := 1234
 __cost := 0
 guess := havoc:877
 argc := param0:35
 argv := param1:38
 param0 := havoc:877
 param1 := havoc:881
 argv@pos := param1@pos:37
 param0@pos := type_err:882
 param1@pos := type_err:883
 argv@width := param1@width:36
 param0@width := type_err:884
 param1@width := type_err:885
 when (3 <= param0:35 /\ param0:35 <= 3)}

Weights on states: 
__done 0x11f5c7c0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x11f5bca0: 
	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:803
 i := phi_i:802
 guess := param0:35
 t := param1:38
 return := havoc:804
 return@pos := type_err:805
 return@width := type_err:806
 when ((((param0:35 <= secret:106 /\ param1:38 = 1 /\ 0 <= __cost:103
            /\ 0 <= (__cost:103 + 1) /\ (__cost:103 + 1) = phi___cost:753
            /\ i:101 = phi_i:752)
           \/ (((param0:35 <= secret:106 /\ !(param1:38 = 1) /\ param1:38 = 2
                   /\ (!(0 <= K:720) \/ mid___cost:721 = (__cost:103 + K:720))
                   /\ (!(0 <= K:720) \/ mid_i:722 = K:720)
                   /\ ((K:720 = 0 /\ 0 = mid_i:722
                          /\ __cost:103 = mid___cost:721)
                         \/ (1 <= K:720 /\ 0 <= (-1 + (n:102 * n:102))
                               /\ 0 <= __cost:103 /\ 0 <= (-1 + mid_i:722)
                               /\ 0 <= (-1 + mid___cost:721)
                               /\ 0 <= ((n:102 * n:102) + -mid_i:722)))
                   /\ K:723 = 0 /\ mid_i:722 = i':724
                   /\ mid___cost:721 = __cost':725 /\ 0 = K:723
                   /\ (K:720 + K:723) = K:726 /\ 0 <= K:726 /\ 0 <= i':724
                   /\ (n:102 * n:102) <= i':724
                   /\ __cost':725 = phi___cost:751 /\ i':724 = phi_i:750)
                  \/ (param0:35 <= secret:106 /\ !(param1:38 = 1)
                        /\ !(param1:38 = 2)
                        /\ (!(0 <= K:743) \/ mid_i:744 = K:743)
                        /\ (!(0 <= K:743)
                              \/ mid___cost:745 = (__cost:103 + K:743))
                        /\ ((K:743 = 0 /\ 0 = mid_i:744
                               /\ __cost:103 = mid___cost:745)
                              \/ (1 <= K:743
                                    /\ 0 <= (-1 + ((n:102 * n:102) * n:102))
                                    /\ 0 <= __cost:103
                                    /\ 0 <= (-1 + mid_i:744)
                                    /\ 0 <= (-1 + mid___cost:745)
                                    /\ 0 <= (((n:102 * n:102) * n:102)
                                               + -mid_i:744))) /\ K:746 = 0
                        /\ mid_i:744 = i':747 /\ mid___cost:745 = __cost':748
                        /\ 0 = K:746 /\ (K:743 + K:746) = K:749 /\ 0 <= K:749
                        /\ 0 <= i':747 /\ ((n:102 * n:102) * n:102) <= i':747
                        /\ __cost':748 = phi___cost:751 /\ i':747 = phi_i:750))
                 /\ phi___cost:751 = phi___cost:753 /\ phi_i:750 = phi_i:752))
          /\ phi___cost:753 = phi___cost:803 /\ phi_i:752 = phi_i:802)
         \/ (((secret:106 < param0:35 /\ param1:38 = 1 /\ 0 <= __cost:103
                 /\ 0 <= (__cost:103 + 1)
                 /\ (__cost:103 + 1) = phi___cost:801 /\ i:101 = phi_i:800)
                \/ (((secret:106 < param0:35 /\ !(param1:38 = 1)
                        /\ param1:38 = 2
                        /\ (!(0 <= K:768)
                              \/ mid___cost:769 = (__cost:103 + K:768))
                        /\ (!(0 <= K:768) \/ mid_i:770 = K:768)
                        /\ ((K:768 = 0 /\ 0 = mid_i:770
                               /\ __cost:103 = mid___cost:769)
                              \/ (1 <= K:768 /\ 0 <= (-1 + (n:102 * n:102))
                                    /\ 0 <= __cost:103
                                    /\ 0 <= (-1 + mid_i:770)
                                    /\ 0 <= (-1 + mid___cost:769)
                                    /\ 0 <= ((n:102 * n:102) + -mid_i:770)))
                        /\ K:771 = 0 /\ mid_i:770 = i':772
                        /\ mid___cost:769 = __cost':773 /\ 0 = K:771
                        /\ (K:768 + K:771) = K:774 /\ 0 <= K:774
                        /\ 0 <= i':772 /\ (n:102 * n:102) <= i':772
                        /\ __cost':773 = phi___cost:799 /\ i':772 = phi_i:798)
                       \/ (secret:106 < param0:35 /\ !(param1:38 = 1)
                             /\ !(param1:38 = 2)
                             /\ (!(0 <= K:791) \/ mid_i:792 = K:791)
                             /\ (!(0 <= K:791)
                                   \/ mid___cost:793 = (__cost:103 + K:791))
                             /\ ((K:791 = 0 /\ 0 = mid_i:792
                                    /\ __cost:103 = mid___cost:793)
                                   \/ (1 <= K:791
                                         /\ 0 <= (-1
                                                    + ((n:102 * n:102)
                                                         * n:102))
                                         /\ 0 <= __cost:103
                                         /\ 0 <= (-1 + mid_i:792)
                                         /\ 0 <= (-1 + mid___cost:793)
                                         /\ 0 <= (((n:102 * n:102) * n:102)
                                                    + -mid_i:792)))
                             /\ K:794 = 0 /\ mid_i:792 = i':795
                             /\ mid___cost:793 = __cost':796 /\ 0 = K:794
                             /\ (K:791 + K:794) = K:797 /\ 0 <= K:797
                             /\ 0 <= i':795
                             /\ ((n:102 * n:102) * n:102) <= i':795
                             /\ __cost':796 = phi___cost:799
                             /\ i':795 = phi_i:798))
                      /\ phi___cost:799 = phi___cost:801
                      /\ phi_i:798 = phi_i:800))
               /\ phi___cost:801 = phi___cost:803 /\ phi_i:800 = phi_i:802))}

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

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

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

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

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