/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, 87> -> <Unique State Name, 16>	Base relation: 
{__retres5 := 0}	
<Unique State Name, 97> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 76> -> <Unique State Name, 19>	Base relation: 
{i := 0
 when secret:75 < guess:74}	
<Unique State Name, 76> -> <Unique State Name, 48>	Base relation: 
{i := 0
 when guess:74 <= secret:75}	
<Unique State Name, 101> -> <Unique State Name, 52>	Base relation: 
{}	
<Unique State Name, 85> -> <Unique State Name, 76>	Base relation: 
{guess := param0:23}	
<Unique State Name, 28> -> <Unique State Name, 98>	Base relation: 
{when (0 <= t:72 /\ 1 <= n:71 /\ i:70 < n:71)}	
<Unique State Name, 88> -> <Unique State Name, 85 87>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 19> -> <Unique State Name, 99>	Base relation: 
{when 0 <= i:70}	
<Unique State Name, 100> -> <Unique State Name, 61>	Base relation: 
{}	
<Unique State Name, 23> -> <Unique State Name, 28>	Base relation: 
{t := 0
 when i:70 < n:71}	
<Unique State Name, 23> -> <Unique State Name, 77>	Base relation: 
{when n:71 <= i:70}	
<Unique State Name, 7> -> <Unique State Name, 16>	Base relation: 
{__retres5 := -1
 when (argc:0 < 2 \/ 2 < argc:0)}	
<Unique State Name, 7> -> <Unique State Name, 92>	Base relation: 
{param0 := tr:29
 param0@pos := type_err:30
 param0@width := type_err:31
 when (2 <= argc:0 /\ argc:0 <= 2)}	
<Unique State Name, 16> -> <Unique State Name, 96>	Base relation: 
{return := __retres5:5
 return@pos := type_err:8
 return@width := type_err:9}	
<Unique State Name, 57> -> <Unique State Name, 100>	Base relation: 
{when (0 <= t:72 /\ 1 <= n:71 /\ i:70 < n:71)}	
<Unique State Name, 93> -> <Unique State Name, 7>	Base relation: 
{n := 32
 secret := 1234
 __cost := 0
 argc := param0:23
 argv := param1:26
 argv@pos := param1@pos:25
 argv@width := param1@width:24}	
<Unique State Name, 95> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 32> -> <Unique State Name, 19>	Base relation: 
{i := (i:70 + 1)
 when n:71 <= t:72}	
<Unique State Name, 32> -> <Unique State Name, 28>	Base relation: 
{__cost := (__cost:73 + 1)
 t := (t:72 + 1)
 when (t:72 < n:71 /\ 0 <= __cost:73 /\ 0 <= (__cost:73 + 1))}	
<Unique State Name, 96> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 98> -> <Unique State Name, 32>	Base relation: 
{}	
<Unique State Name, 92> -> <Unique State Name, 97 91>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 52> -> <Unique State Name, 57>	Base relation: 
{t := 0
 when i:70 < n:71}	
<Unique State Name, 52> -> <Unique State Name, 77>	Base relation: 
{when n:71 <= i:70}	
<Unique State Name, 61> -> <Unique State Name, 48>	Base relation: 
{i := (i:70 + 1)
 when n:71 <= t:72}	
<Unique State Name, 61> -> <Unique State Name, 57>	Base relation: 
{__cost := (__cost:73 + 1)
 t := (t:72 + 1)
 when (t:72 < n:71 /\ 0 <= __cost:73 /\ 0 <= (__cost:73 + 1))}	
<Unique State Name, 48> -> <Unique State Name, 101>	Base relation: 
{when 0 <= i:70}	
<Unique State Name, 77> -> <Unique State Name, 95>	Base relation: 
{return := havoc:76
 return@pos := type_err:79
 return@width := type_err:80}	
<Unique State Name, 91> -> <Unique State Name, 88>	Base relation: 
{param0 := havoc:15
 param0@pos := type_err:27
 param0@width := type_err:28}	
<Unique State Name, 99> -> <Unique State Name, 23>	Base relation: 
{}	
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:73 + 1)
 t := (t:72 + 1)
 when (0 <= t:72 /\ 1 <= n:71 /\ i:70 < n:71 /\ t:72 < n:71 /\ 0 <= __cost:73
         /\ 0 <= (__cost:73 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':745) = (1)*(__cost:73) + 1
           (t':746) = (1)*(t:72) + 1
           }
          pre:
            [|__cost:73>=0; t:72>=0; n:71-i:70-1>=0; n:71-t:72-1>=0|]
          post:
            [|t':746-1>=0; __cost':745-1>=0; n:71-i:70-1>=0; n:71-t':746>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':745
   t := t':746
   when ((!(0 <= K:756) \/ mid___cost:759 = (__cost:73 + K:756))
           /\ (!(0 <= K:756) \/ mid_t:758 = (t:72 + K:756))
           /\ ((K:756 = 0 /\ t:72 = mid_t:758 /\ __cost:73 = mid___cost:759)
                 \/ (1 <= K:756 /\ 0 <= __cost:73 /\ 0 <= t:72
                       /\ 0 <= (-1 + n:71 + -i:70)
                       /\ 0 <= (-1 + n:71 + -t:72) /\ 0 <= (-1 + mid_t:758)
                       /\ 0 <= (-1 + mid___cost:759)
                       /\ 0 <= (-1 + n:71 + -i:70)
                       /\ 0 <= (n:71 + -mid_t:758))) /\ K:757 = 0
           /\ mid_t:758 = t':746 /\ mid___cost:759 = __cost':745 /\ 0 = K:757
           /\ (K:756 + K:757) = K:755 /\ 0 <= K:755)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':772
 i := (i:70 + 1)
 t := t':771
 when (0 <= i:70 /\ i:70 < n:71
         /\ (!(0 <= K:767) \/ mid___cost:768 = (__cost:73 + K:767))
         /\ (!(0 <= K:767) \/ mid_t:769 = K:767)
         /\ ((K:767 = 0 /\ 0 = mid_t:769 /\ __cost:73 = mid___cost:768)
               \/ (1 <= K:767 /\ 0 <= __cost:73 /\ 0 <= (-1 + n:71 + -i:70)
                     /\ 0 <= (-1 + n:71) /\ 0 <= (-1 + mid_t:769)
                     /\ 0 <= (-1 + mid___cost:768)
                     /\ 0 <= (-1 + n:71 + -i:70) /\ 0 <= (n:71 + -mid_t:769)))
         /\ K:770 = 0 /\ mid_t:769 = t':771 /\ mid___cost:768 = __cost':772
         /\ 0 = K:770 /\ (K:767 + K:770) = K:773 /\ 0 <= K:773 /\ 0 <= t':771
         /\ 1 <= n:71 /\ i:70 < n:71 /\ n:71 <= t':771)}
**** alpha hat: 
  {<Split [true
            (i':774) = (1)*(i:70) + 1
           (__cost':745) = (1)*(__cost:73) + n:71
           (t':746) = n:71
           (-__cost':745) <= (1)*(-__cost:73) + (-1)*1 + (-1)*i:70
           }
          pre:
            [|-i:70+n:71-1>=0; __cost:73>=0; i:70>=0|]
          post:
            [|-n:71+t':746=0; -n:71+__cost':745>=0; i':774-1>=0;
              n:71-i':774>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':745
   i := i':774
   t := t':746
   when ((!(0 <= K:786) \/ mid_i:789 = (i:70 + K:786))
           /\ (!(0 <= K:786) \/ mid___cost:790 = (__cost:73 + (n:71 * K:786)))
           /\ (!((0 <= K:786 /\ K:786 <= 0)) \/ mid_t:788 = t:72)
           /\ (!(1 <= K:786) \/ mid_t:788 = n:71)
           /\ (!(0 <= K:786)
                 \/ -mid___cost:790 <= (-__cost:73 + (-1/2 * K:786)
                                          + -((i:70 * K:786))
                                          + (-1/2 * (K:786 * K:786))))
           /\ ((K:786 = 0 /\ t:72 = mid_t:788 /\ i:70 = mid_i:789
                  /\ __cost:73 = mid___cost:790)
                 \/ (1 <= K:786 /\ 0 <= (-1 + -i:70 + n:71) /\ 0 <= __cost:73
                       /\ 0 <= i:70 /\ (-n:71 + mid_t:788) = 0
                       /\ 0 <= (-n:71 + mid___cost:790)
                       /\ 0 <= (-1 + mid_i:789) /\ 0 <= (n:71 + -mid_i:789)))
           /\ K:787 = 0 /\ mid_t:788 = t':746 /\ mid_i:789 = i':774
           /\ mid___cost:790 = __cost':745 /\ 0 = K:787
           /\ (K:786 + K:787) = K:785 /\ 0 <= K:785)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:73 + 1)
 t := (t:72 + 1)
 when (0 <= t:72 /\ 1 <= n:71 /\ i:70 < n:71 /\ t:72 < n:71 /\ 0 <= __cost:73
         /\ 0 <= (__cost:73 + 1))}
**** alpha hat: 
  {<Split [true
            (__cost':745) = (1)*(__cost:73) + 1
           (t':746) = (1)*(t:72) + 1
           }
          pre:
            [|__cost:73>=0; t:72>=0; n:71-i:70-1>=0; n:71-t:72-1>=0|]
          post:
            [|t':746-1>=0; __cost':745-1>=0; n:71-i:70-1>=0; n:71-t':746>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':745
   t := t':746
   when ((!(0 <= K:809) \/ mid___cost:812 = (__cost:73 + K:809))
           /\ (!(0 <= K:809) \/ mid_t:811 = (t:72 + K:809))
           /\ ((K:809 = 0 /\ t:72 = mid_t:811 /\ __cost:73 = mid___cost:812)
                 \/ (1 <= K:809 /\ 0 <= __cost:73 /\ 0 <= t:72
                       /\ 0 <= (-1 + n:71 + -i:70)
                       /\ 0 <= (-1 + n:71 + -t:72) /\ 0 <= (-1 + mid_t:811)
                       /\ 0 <= (-1 + mid___cost:812)
                       /\ 0 <= (-1 + n:71 + -i:70)
                       /\ 0 <= (n:71 + -mid_t:811))) /\ K:810 = 0
           /\ mid_t:811 = t':746 /\ mid___cost:812 = __cost':745 /\ 0 = K:810
           /\ (K:809 + K:810) = K:808 /\ 0 <= K:808)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := __cost':825
 i := (i:70 + 1)
 t := t':824
 when (0 <= i:70 /\ i:70 < n:71
         /\ (!(0 <= K:820) \/ mid___cost:821 = (__cost:73 + K:820))
         /\ (!(0 <= K:820) \/ mid_t:822 = K:820)
         /\ ((K:820 = 0 /\ 0 = mid_t:822 /\ __cost:73 = mid___cost:821)
               \/ (1 <= K:820 /\ 0 <= __cost:73 /\ 0 <= (-1 + n:71 + -i:70)
                     /\ 0 <= (-1 + n:71) /\ 0 <= (-1 + mid_t:822)
                     /\ 0 <= (-1 + mid___cost:821)
                     /\ 0 <= (-1 + n:71 + -i:70) /\ 0 <= (n:71 + -mid_t:822)))
         /\ K:823 = 0 /\ mid_t:822 = t':824 /\ mid___cost:821 = __cost':825
         /\ 0 = K:823 /\ (K:820 + K:823) = K:826 /\ 0 <= K:826 /\ 0 <= t':824
         /\ 1 <= n:71 /\ i:70 < n:71 /\ n:71 <= t':824)}
**** alpha hat: 
  {<Split [true
            (i':774) = (1)*(i:70) + 1
           (__cost':745) = (1)*(__cost:73) + n:71
           (t':746) = n:71
           (-__cost':745) <= (1)*(-__cost:73) + (-1)*1 + (-1)*i:70
           }
          pre:
            [|-i:70+n:71-1>=0; __cost:73>=0; i:70>=0|]
          post:
            [|-n:71+t':746=0; -n:71+__cost':745>=0; i':774-1>=0;
              n:71-i':774>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':745
   i := i':774
   t := t':746
   when ((!(0 <= K:838) \/ mid_i:841 = (i:70 + K:838))
           /\ (!(0 <= K:838) \/ mid___cost:842 = (__cost:73 + (n:71 * K:838)))
           /\ (!((0 <= K:838 /\ K:838 <= 0)) \/ mid_t:840 = t:72)
           /\ (!(1 <= K:838) \/ mid_t:840 = n:71)
           /\ (!(0 <= K:838)
                 \/ -mid___cost:842 <= (-__cost:73 + (-1/2 * K:838)
                                          + -((i:70 * K:838))
                                          + (-1/2 * (K:838 * K:838))))
           /\ ((K:838 = 0 /\ t:72 = mid_t:840 /\ i:70 = mid_i:841
                  /\ __cost:73 = mid___cost:842)
                 \/ (1 <= K:838 /\ 0 <= (-1 + -i:70 + n:71) /\ 0 <= __cost:73
                       /\ 0 <= i:70 /\ (-n:71 + mid_t:840) = 0
                       /\ 0 <= (-n:71 + mid___cost:842)
                       /\ 0 <= (-1 + mid_i:841) /\ 0 <= (n:71 + -mid_i:841)))
           /\ K:839 = 0 /\ mid_t:840 = t':746 /\ mid_i:841 = i':774
           /\ mid___cost:842 = __cost':745 /\ 0 = K:839
           /\ (K:838 + K:839) = K:837 /\ 0 <= K:837)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
11  13  23  


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


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


New-style (IRE) regular expression in IREregExpMap for reID=23: 
Weight(Base relation: 
  {__cost := phi___cost:854
   i := phi_i:853
   t := phi_t:852
   guess := param0:23
   return := havoc:855
   return@pos := type_err:856
   return@width := type_err:857
   when ((param0:23 <= secret:75 /\ (!(0 <= K:791) \/ mid_i:792 = K:791)
            /\ (!(0 <= K:791)
                  \/ mid___cost:793 = (__cost:73 + (n:71 * K:791)))
            /\ (!((0 <= K:791 /\ K:791 <= 0)) \/ mid_t:794 = t:72)
            /\ (!(1 <= K:791) \/ mid_t:794 = n:71)
            /\ (!(0 <= K:791)
                  \/ -mid___cost:793 <= (-__cost:73 + (-1/2 * K:791)
                                           + (-1/2 * (K:791 * K:791))))
            /\ ((K:791 = 0 /\ t:72 = mid_t:794 /\ 0 = mid_i:792
                   /\ __cost:73 = mid___cost:793)
                  \/ (1 <= K:791 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                        /\ (-n:71 + mid_t:794) = 0
                        /\ 0 <= (-n:71 + mid___cost:793)
                        /\ 0 <= (-1 + mid_i:792) /\ 0 <= (n:71 + -mid_i:792)))
            /\ K:795 = 0 /\ mid_t:794 = t':796 /\ mid_i:792 = i':797
            /\ mid___cost:793 = __cost':798 /\ 0 = K:795
            /\ (K:791 + K:795) = K:799 /\ 0 <= K:799 /\ 0 <= i':797
            /\ n:71 <= i':797 /\ __cost':798 = phi___cost:854
            /\ i':797 = phi_i:853 /\ t':796 = phi_t:852)
           \/ (secret:75 < param0:23 /\ (!(0 <= K:843) \/ mid_i:844 = K:843)
                 /\ (!(0 <= K:843)
                       \/ mid___cost:845 = (__cost:73 + (n:71 * K:843)))
                 /\ (!((0 <= K:843 /\ K:843 <= 0)) \/ mid_t:846 = t:72)
                 /\ (!(1 <= K:843) \/ mid_t:846 = n:71)
                 /\ (!(0 <= K:843)
                       \/ -mid___cost:845 <= (-__cost:73 + (-1/2 * K:843)
                                                + (-1/2 * (K:843 * K:843))))
                 /\ ((K:843 = 0 /\ t:72 = mid_t:846 /\ 0 = mid_i:844
                        /\ __cost:73 = mid___cost:845)
                       \/ (1 <= K:843 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                             /\ (-n:71 + mid_t:846) = 0
                             /\ 0 <= (-n:71 + mid___cost:845)
                             /\ 0 <= (-1 + mid_i:844)
                             /\ 0 <= (n:71 + -mid_i:844))) /\ K:847 = 0
                 /\ mid_t:846 = t':848 /\ mid_i:844 = i':849
                 /\ mid___cost:845 = __cost':850 /\ 0 = K:847
                 /\ (K:843 + K:847) = K:851 /\ 0 <= K:851 /\ 0 <= i':849
                 /\ n:71 <= i':849 /\ __cost':850 = phi___cost:854
                 /\ i':849 = phi_i:853 /\ t':848 = phi_t:852))})



Performing Gaussian Elimination.


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

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



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

One()



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

Weight(Base relation: 
  {__cost := phi___cost:854
   return := havoc:855
   return@pos := type_err:856
   return@width := type_err:857
   when ((param0:23 <= secret:75 /\ (!(0 <= K:791) \/ mid_i:792 = K:791)
            /\ (!(0 <= K:791)
                  \/ mid___cost:793 = (__cost:73 + (n:71 * K:791)))
            /\ (!((0 <= K:791 /\ K:791 <= 0)) \/ mid_t:794 = t:886)
            /\ (!(1 <= K:791) \/ mid_t:794 = n:71)
            /\ (!(0 <= K:791)
                  \/ -mid___cost:793 <= (-__cost:73 + (-1/2 * K:791)
                                           + (-1/2 * (K:791 * K:791))))
            /\ ((K:791 = 0 /\ t:886 = mid_t:794 /\ 0 = mid_i:792
                   /\ __cost:73 = mid___cost:793)
                  \/ (1 <= K:791 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                        /\ (-n:71 + mid_t:794) = 0
                        /\ 0 <= (-n:71 + mid___cost:793)
                        /\ 0 <= (-1 + mid_i:792) /\ 0 <= (n:71 + -mid_i:792)))
            /\ K:795 = 0 /\ mid_t:794 = t':796 /\ mid_i:792 = i':797
            /\ mid___cost:793 = __cost':798 /\ 0 = K:795
            /\ (K:791 + K:795) = K:799 /\ 0 <= K:799 /\ 0 <= i':797
            /\ n:71 <= i':797 /\ __cost':798 = phi___cost:854
            /\ i':797 = phi_i:853 /\ t':796 = phi_t:852)
           \/ (secret:75 < param0:23 /\ (!(0 <= K:843) \/ mid_i:844 = K:843)
                 /\ (!(0 <= K:843)
                       \/ mid___cost:845 = (__cost:73 + (n:71 * K:843)))
                 /\ (!((0 <= K:843 /\ K:843 <= 0)) \/ mid_t:846 = t:886)
                 /\ (!(1 <= K:843) \/ mid_t:846 = n:71)
                 /\ (!(0 <= K:843)
                       \/ -mid___cost:845 <= (-__cost:73 + (-1/2 * K:843)
                                                + (-1/2 * (K:843 * K:843))))
                 /\ ((K:843 = 0 /\ t:886 = mid_t:846 /\ 0 = mid_i:844
                        /\ __cost:73 = mid___cost:845)
                       \/ (1 <= K:843 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                             /\ (-n:71 + mid_t:846) = 0
                             /\ 0 <= (-n:71 + mid___cost:845)
                             /\ 0 <= (-1 + mid_i:844)
                             /\ 0 <= (n:71 + -mid_i:844))) /\ K:847 = 0
                 /\ mid_t:846 = t':848 /\ mid_i:844 = i':849
                 /\ mid___cost:845 = __cost':850 /\ 0 = K:847
                 /\ (K:843 + K:847) = K:851 /\ 0 <= K:851 /\ 0 <= i':849
                 /\ n:71 <= i':849 /\ __cost':850 = phi___cost:854
                 /\ i':849 = phi_i:853 /\ t':848 = phi_t:852))})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=11: 
Weight(Base relation: 
  {n := 32
   secret := 1234
   __cost := phi___cost:925
   return := phi___retres5:924
   param0 := phi_param0:921
   return@pos := type_err:926
   param0@pos := phi_param0@pos:918
   return@width := type_err:927
   param0@width := phi_param0@width:915
   when (((param0:23 < 2 \/ 2 < param0:23) /\ 0 = phi___cost:925
            /\ -1 = phi___retres5:924 /\ return:923 = phi_return:922
            /\ param0:23 = phi_param0:921
            /\ return@pos:920 = phi_return@pos:919
            /\ param0@pos:22 = phi_param0@pos:918
            /\ return@width:917 = phi_return@width:916
            /\ param0@width:21 = phi_param0@width:915)
           \/ (2 <= param0:23 /\ param0:23 <= 2
                 /\ ((havoc:887 <= 1234
                        /\ (!(0 <= K:890) \/ mid_i:891 = K:890)
                        /\ (!(0 <= K:890) \/ mid___cost:892 = (32 * K:890))
                        /\ (!((0 <= K:890 /\ K:890 <= 0))
                              \/ mid_t:893 = t:894)
                        /\ (!(1 <= K:890) \/ mid_t:893 = 32)
                        /\ (!(0 <= K:890)
                              \/ -mid___cost:892 <= ((-1/2 * K:890)
                                                       + (-1/2
                                                            * (K:890 * K:890))))
                        /\ ((K:890 = 0 /\ t:894 = mid_t:893 /\ 0 = mid_i:891
                               /\ 0 = mid___cost:892)
                              \/ (1 <= K:890 /\ 0 <= (-1 + 32)
                                    /\ (-32 + mid_t:893) = 0
                                    /\ 0 <= (-32 + mid___cost:892)
                                    /\ 0 <= (-1 + mid_i:891)
                                    /\ 0 <= (32 + -mid_i:891))) /\ K:895 = 0
                        /\ mid_t:893 = t':896 /\ mid_i:891 = i':897
                        /\ mid___cost:892 = __cost':898 /\ 0 = K:895
                        /\ (K:890 + K:895) = K:899 /\ 0 <= K:899
                        /\ 0 <= i':897 /\ 32 <= i':897
                        /\ __cost':898 = phi___cost:900 /\ i':897 = phi_i:901
                        /\ t':896 = phi_t:902)
                       \/ (1234 < havoc:887
                             /\ (!(0 <= K:903) \/ mid_i:904 = K:903)
                             /\ (!(0 <= K:903)
                                   \/ mid___cost:905 = (32 * K:903))
                             /\ (!((0 <= K:903 /\ K:903 <= 0))
                                   \/ mid_t:906 = t:894)
                             /\ (!(1 <= K:903) \/ mid_t:906 = 32)
                             /\ (!(0 <= K:903)
                                   \/ -mid___cost:905 <= ((-1/2 * K:903)
                                                            + (-1/2
                                                                 * (K:903
                                                                    * K:903))))
                             /\ ((K:903 = 0 /\ t:894 = mid_t:906
                                    /\ 0 = mid_i:904 /\ 0 = mid___cost:905)
                                   \/ (1 <= K:903 /\ 0 <= (-1 + 32)
                                         /\ (-32 + mid_t:906) = 0
                                         /\ 0 <= (-32 + mid___cost:905)
                                         /\ 0 <= (-1 + mid_i:904)
                                         /\ 0 <= (32 + -mid_i:904)))
                             /\ K:907 = 0 /\ mid_t:906 = t':908
                             /\ mid_i:904 = i':909
                             /\ mid___cost:905 = __cost':910 /\ 0 = K:907
                             /\ (K:903 + K:907) = K:911 /\ 0 <= K:911
                             /\ 0 <= i':909 /\ 32 <= i':909
                             /\ __cost':910 = phi___cost:900
                             /\ i':909 = phi_i:901 /\ t':908 = phi_t:902))
                 /\ phi___cost:900 = phi___cost:925 /\ 0 = phi___retres5:924
                 /\ havoc:912 = phi_return:922 /\ havoc:887 = phi_param0:921
                 /\ type_err:913 = phi_return@pos:919
                 /\ type_err:888 = phi_param0@pos:918
                 /\ type_err:914 = phi_return@width:916
                 /\ type_err:889 = phi_param0@width:915))})


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


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=23: 
Weight(Base relation: 
  {__cost := phi___cost:854
   return := havoc:855
   return@pos := type_err:856
   return@width := type_err:857
   when ((param0:23 <= secret:75 /\ (!(0 <= K:791) \/ mid_i:792 = K:791)
            /\ (!(0 <= K:791)
                  \/ mid___cost:793 = (__cost:73 + (n:71 * K:791)))
            /\ (!((0 <= K:791 /\ K:791 <= 0)) \/ mid_t:794 = t:886)
            /\ (!(1 <= K:791) \/ mid_t:794 = n:71)
            /\ (!(0 <= K:791)
                  \/ -mid___cost:793 <= (-__cost:73 + (-1/2 * K:791)
                                           + (-1/2 * (K:791 * K:791))))
            /\ ((K:791 = 0 /\ t:886 = mid_t:794 /\ 0 = mid_i:792
                   /\ __cost:73 = mid___cost:793)
                  \/ (1 <= K:791 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                        /\ (-n:71 + mid_t:794) = 0
                        /\ 0 <= (-n:71 + mid___cost:793)
                        /\ 0 <= (-1 + mid_i:792) /\ 0 <= (n:71 + -mid_i:792)))
            /\ K:795 = 0 /\ mid_t:794 = t':796 /\ mid_i:792 = i':797
            /\ mid___cost:793 = __cost':798 /\ 0 = K:795
            /\ (K:791 + K:795) = K:799 /\ 0 <= K:799 /\ 0 <= i':797
            /\ n:71 <= i':797 /\ __cost':798 = phi___cost:854
            /\ i':797 = phi_i:853 /\ t':796 = phi_t:852)
           \/ (secret:75 < param0:23 /\ (!(0 <= K:843) \/ mid_i:844 = K:843)
                 /\ (!(0 <= K:843)
                       \/ mid___cost:845 = (__cost:73 + (n:71 * K:843)))
                 /\ (!((0 <= K:843 /\ K:843 <= 0)) \/ mid_t:846 = t:886)
                 /\ (!(1 <= K:843) \/ mid_t:846 = n:71)
                 /\ (!(0 <= K:843)
                       \/ -mid___cost:845 <= (-__cost:73 + (-1/2 * K:843)
                                                + (-1/2 * (K:843 * K:843))))
                 /\ ((K:843 = 0 /\ t:886 = mid_t:846 /\ 0 = mid_i:844
                        /\ __cost:73 = mid___cost:845)
                       \/ (1 <= K:843 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                             /\ (-n:71 + mid_t:846) = 0
                             /\ 0 <= (-n:71 + mid___cost:845)
                             /\ 0 <= (-1 + mid_i:844)
                             /\ 0 <= (n:71 + -mid_i:844))) /\ K:847 = 0
                 /\ mid_t:846 = t':848 /\ mid_i:844 = i':849
                 /\ mid___cost:845 = __cost':850 /\ 0 = K:847
                 /\ (K:843 + K:847) = K:851 /\ 0 <= K:851 /\ 0 <= i':849
                 /\ n:71 <= i':849 /\ __cost':850 = phi___cost:854
                 /\ i':849 = phi_i:853 /\ t':848 = phi_t:852))})


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

  The IRE-evaluated value on this round is: 

Base relation: 
{n := 32
 secret := 1234
 __cost := phi___cost:925
 return := phi___retres5:924
 param0 := phi_param0:921
 return@pos := type_err:926
 param0@pos := phi_param0@pos:918
 return@width := type_err:927
 param0@width := phi_param0@width:915
 when (((param0:23 < 2 \/ 2 < param0:23) /\ 0 = phi___cost:925
          /\ -1 = phi___retres5:924 /\ return:923 = phi_return:922
          /\ param0:23 = phi_param0:921
          /\ return@pos:920 = phi_return@pos:919
          /\ param0@pos:22 = phi_param0@pos:918
          /\ return@width:917 = phi_return@width:916
          /\ param0@width:21 = phi_param0@width:915)
         \/ (2 <= param0:23 /\ param0:23 <= 2
               /\ ((havoc:887 <= 1234 /\ (!(0 <= K:890) \/ mid_i:891 = K:890)
                      /\ (!(0 <= K:890) \/ mid___cost:892 = (32 * K:890))
                      /\ (!((0 <= K:890 /\ K:890 <= 0)) \/ mid_t:893 = t:894)
                      /\ (!(1 <= K:890) \/ mid_t:893 = 32)
                      /\ (!(0 <= K:890)
                            \/ -mid___cost:892 <= ((-1/2 * K:890)
                                                     + (-1/2
                                                          * (K:890 * K:890))))
                      /\ ((K:890 = 0 /\ t:894 = mid_t:893 /\ 0 = mid_i:891
                             /\ 0 = mid___cost:892)
                            \/ (1 <= K:890 /\ 0 <= (-1 + 32)
                                  /\ (-32 + mid_t:893) = 0
                                  /\ 0 <= (-32 + mid___cost:892)
                                  /\ 0 <= (-1 + mid_i:891)
                                  /\ 0 <= (32 + -mid_i:891))) /\ K:895 = 0
                      /\ mid_t:893 = t':896 /\ mid_i:891 = i':897
                      /\ mid___cost:892 = __cost':898 /\ 0 = K:895
                      /\ (K:890 + K:895) = K:899 /\ 0 <= K:899 /\ 0 <= i':897
                      /\ 32 <= i':897 /\ __cost':898 = phi___cost:900
                      /\ i':897 = phi_i:901 /\ t':896 = phi_t:902)
                     \/ (1234 < havoc:887
                           /\ (!(0 <= K:903) \/ mid_i:904 = K:903)
                           /\ (!(0 <= K:903) \/ mid___cost:905 = (32 * K:903))
                           /\ (!((0 <= K:903 /\ K:903 <= 0))
                                 \/ mid_t:906 = t:894)
                           /\ (!(1 <= K:903) \/ mid_t:906 = 32)
                           /\ (!(0 <= K:903)
                                 \/ -mid___cost:905 <= ((-1/2 * K:903)
                                                          + (-1/2
                                                               * (K:903
                                                                    * K:903))))
                           /\ ((K:903 = 0 /\ t:894 = mid_t:906
                                  /\ 0 = mid_i:904 /\ 0 = mid___cost:905)
                                 \/ (1 <= K:903 /\ 0 <= (-1 + 32)
                                       /\ (-32 + mid_t:906) = 0
                                       /\ 0 <= (-32 + mid___cost:905)
                                       /\ 0 <= (-1 + mid_i:904)
                                       /\ 0 <= (32 + -mid_i:904)))
                           /\ K:907 = 0 /\ mid_t:906 = t':908
                           /\ mid_i:904 = i':909
                           /\ mid___cost:905 = __cost':910 /\ 0 = K:907
                           /\ (K:903 + K:907) = K:911 /\ 0 <= K:911
                           /\ 0 <= i':909 /\ 32 <= i':909
                           /\ __cost':910 = phi___cost:900
                           /\ i':909 = phi_i:901 /\ t':908 = phi_t:902))
               /\ phi___cost:900 = phi___cost:925 /\ 0 = phi___retres5:924
               /\ havoc:912 = phi_return:922 /\ havoc:887 = phi_param0:921
               /\ type_err:913 = phi_return@pos:919
               /\ type_err:888 = phi_param0@pos:918
               /\ type_err:914 = phi_return@width:916
               /\ type_err:889 = phi_param0@width:915))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

Evaluating variable number 23 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:854
 return := havoc:855
 return@pos := type_err:856
 return@width := type_err:857
 when ((param0:23 <= secret:75 /\ (!(0 <= K:791) \/ mid_i:792 = K:791)
          /\ (!(0 <= K:791) \/ mid___cost:793 = (__cost:73 + (n:71 * K:791)))
          /\ (!((0 <= K:791 /\ K:791 <= 0)) \/ mid_t:794 = t:886)
          /\ (!(1 <= K:791) \/ mid_t:794 = n:71)
          /\ (!(0 <= K:791)
                \/ -mid___cost:793 <= (-__cost:73 + (-1/2 * K:791)
                                         + (-1/2 * (K:791 * K:791))))
          /\ ((K:791 = 0 /\ t:886 = mid_t:794 /\ 0 = mid_i:792
                 /\ __cost:73 = mid___cost:793)
                \/ (1 <= K:791 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                      /\ (-n:71 + mid_t:794) = 0
                      /\ 0 <= (-n:71 + mid___cost:793)
                      /\ 0 <= (-1 + mid_i:792) /\ 0 <= (n:71 + -mid_i:792)))
          /\ K:795 = 0 /\ mid_t:794 = t':796 /\ mid_i:792 = i':797
          /\ mid___cost:793 = __cost':798 /\ 0 = K:795
          /\ (K:791 + K:795) = K:799 /\ 0 <= K:799 /\ 0 <= i':797
          /\ n:71 <= i':797 /\ __cost':798 = phi___cost:854
          /\ i':797 = phi_i:853 /\ t':796 = phi_t:852)
         \/ (secret:75 < param0:23 /\ (!(0 <= K:843) \/ mid_i:844 = K:843)
               /\ (!(0 <= K:843)
                     \/ mid___cost:845 = (__cost:73 + (n:71 * K:843)))
               /\ (!((0 <= K:843 /\ K:843 <= 0)) \/ mid_t:846 = t:886)
               /\ (!(1 <= K:843) \/ mid_t:846 = n:71)
               /\ (!(0 <= K:843)
                     \/ -mid___cost:845 <= (-__cost:73 + (-1/2 * K:843)
                                              + (-1/2 * (K:843 * K:843))))
               /\ ((K:843 = 0 /\ t:886 = mid_t:846 /\ 0 = mid_i:844
                      /\ __cost:73 = mid___cost:845)
                     \/ (1 <= K:843 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                           /\ (-n:71 + mid_t:846) = 0
                           /\ 0 <= (-n:71 + mid___cost:845)
                           /\ 0 <= (-1 + mid_i:844)
                           /\ 0 <= (n:71 + -mid_i:844))) /\ K:847 = 0
               /\ mid_t:846 = t':848 /\ mid_i:844 = i':849
               /\ mid___cost:845 = __cost':850 /\ 0 = K:847
               /\ (K:843 + K:847) = K:851 /\ 0 <= K:851 /\ 0 <= i':849
               /\ n:71 <= i':849 /\ __cost':850 = phi___cost:854
               /\ i':849 = phi_i:853 /\ t':848 = phi_t:852))}

    (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,85)_g1>	Base relation: 
{n := 32
 secret := 1234
 __cost := 0
 argc := param0:23
 argv := param1:26
 param0 := havoc:928
 argv@pos := param1@pos:25
 param0@pos := type_err:929
 argv@width := param1@width:24
 param0@width := type_err:930
 when (2 <= param0:23 /\ param0:23 <= 2)}	
<__pstate, accept> -> <__pstate, (Unique State Name,97)_g1>	Base relation: 
{n := 32
 secret := 1234
 __cost := 0
 argc := param0:23
 argv := param1:26
 param0 := tr:742
 argv@pos := param1@pos:25
 param0@pos := type_err:743
 argv@width := param1@width:24
 param0@width := type_err:744
 when (2 <= param0:23 /\ param0:23 <= 2)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x160992f0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x16077e50: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
##### ANS
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}
    ( __pstate , (Unique State Name,97)_g1 , __done )	Base relation: 
{n := 32
 secret := 1234
 __cost := 0
 argc := param0:23
 argv := param1:26
 param0 := tr:742
 argv@pos := param1@pos:25
 param0@pos := type_err:743
 argv@width := param1@width:24
 param0@width := type_err:744
 when (2 <= param0:23 /\ param0:23 <= 2)}
    ( __pstate , (Unique State Name,85)_g1 , __done )	Base relation: 
{n := 32
 secret := 1234
 __cost := 0
 argc := param0:23
 argv := param1:26
 param0 := havoc:928
 argv@pos := param1@pos:25
 param0@pos := type_err:929
 argv@width := param1@width:24
 param0@width := type_err:930
 when (2 <= param0:23 /\ param0:23 <= 2)}

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

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

Base relation: 
{}

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

Base relation: 
{__cost := phi___cost:854
 i := phi_i:853
 t := phi_t:852
 guess := param0:23
 return := havoc:855
 return@pos := type_err:856
 return@width := type_err:857
 when ((param0:23 <= secret:75 /\ (!(0 <= K:791) \/ mid_i:792 = K:791)
          /\ (!(0 <= K:791) \/ mid___cost:793 = (__cost:73 + (n:71 * K:791)))
          /\ (!((0 <= K:791 /\ K:791 <= 0)) \/ mid_t:794 = t:72)
          /\ (!(1 <= K:791) \/ mid_t:794 = n:71)
          /\ (!(0 <= K:791)
                \/ -mid___cost:793 <= (-__cost:73 + (-1/2 * K:791)
                                         + (-1/2 * (K:791 * K:791))))
          /\ ((K:791 = 0 /\ t:72 = mid_t:794 /\ 0 = mid_i:792
                 /\ __cost:73 = mid___cost:793)
                \/ (1 <= K:791 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                      /\ (-n:71 + mid_t:794) = 0
                      /\ 0 <= (-n:71 + mid___cost:793)
                      /\ 0 <= (-1 + mid_i:792) /\ 0 <= (n:71 + -mid_i:792)))
          /\ K:795 = 0 /\ mid_t:794 = t':796 /\ mid_i:792 = i':797
          /\ mid___cost:793 = __cost':798 /\ 0 = K:795
          /\ (K:791 + K:795) = K:799 /\ 0 <= K:799 /\ 0 <= i':797
          /\ n:71 <= i':797 /\ __cost':798 = phi___cost:854
          /\ i':797 = phi_i:853 /\ t':796 = phi_t:852)
         \/ (secret:75 < param0:23 /\ (!(0 <= K:843) \/ mid_i:844 = K:843)
               /\ (!(0 <= K:843)
                     \/ mid___cost:845 = (__cost:73 + (n:71 * K:843)))
               /\ (!((0 <= K:843 /\ K:843 <= 0)) \/ mid_t:846 = t:72)
               /\ (!(1 <= K:843) \/ mid_t:846 = n:71)
               /\ (!(0 <= K:843)
                     \/ -mid___cost:845 <= (-__cost:73 + (-1/2 * K:843)
                                              + (-1/2 * (K:843 * K:843))))
               /\ ((K:843 = 0 /\ t:72 = mid_t:846 /\ 0 = mid_i:844
                      /\ __cost:73 = mid___cost:845)
                     \/ (1 <= K:843 /\ 0 <= (-1 + n:71) /\ 0 <= __cost:73
                           /\ (-n:71 + mid_t:846) = 0
                           /\ 0 <= (-n:71 + mid___cost:845)
                           /\ 0 <= (-1 + mid_i:844)
                           /\ 0 <= (n:71 + -mid_i:844))) /\ K:847 = 0
               /\ mid_t:846 = t':848 /\ mid_i:844 = i':849
               /\ mid___cost:845 = __cost':850 /\ 0 = K:847
               /\ (K:843 + K:847) = K:851 /\ 0 <= K:851 /\ 0 <= i':849
               /\ n:71 <= i':849 /\ __cost':850 = phi___cost:854
               /\ i':849 = phi_i:853 /\ t':848 = phi_t:852))}

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

Base relation: 
{n := 32
 secret := 1234
 __cost := phi___cost:963
 __retres5 := phi___retres5:962
 argc := param0:23
 argv := param1:26
 return := phi___retres5:962
 param0 := phi_param0:960
 argv@pos := param1@pos:25
 return@pos := type_err:964
 param0@pos := phi_param0@pos:958
 argv@width := param1@width:24
 return@width := type_err:965
 param0@width := phi_param0@width:956
 when (((param0:23 < 2 \/ 2 < param0:23) /\ 0 = phi___cost:963
          /\ -1 = phi___retres5:962 /\ return:923 = phi_return:961
          /\ param0:23 = phi_param0:960
          /\ return@pos:920 = phi_return@pos:959
          /\ param0@pos:22 = phi_param0@pos:958
          /\ return@width:917 = phi_return@width:957
          /\ param0@width:21 = phi_param0@width:956)
         \/ (2 <= param0:23 /\ param0:23 <= 2
               /\ ((havoc:928 <= 1234 /\ (!(0 <= K:931) \/ mid_i:932 = K:931)
                      /\ (!(0 <= K:931) \/ mid___cost:933 = (32 * K:931))
                      /\ (!((0 <= K:931 /\ K:931 <= 0)) \/ mid_t:934 = t:935)
                      /\ (!(1 <= K:931) \/ mid_t:934 = 32)
                      /\ (!(0 <= K:931)
                            \/ -mid___cost:933 <= ((-1/2 * K:931)
                                                     + (-1/2
                                                          * (K:931 * K:931))))
                      /\ ((K:931 = 0 /\ t:935 = mid_t:934 /\ 0 = mid_i:932
                             /\ 0 = mid___cost:933)
                            \/ (1 <= K:931 /\ 0 <= (-1 + 32)
                                  /\ (-32 + mid_t:934) = 0
                                  /\ 0 <= (-32 + mid___cost:933)
                                  /\ 0 <= (-1 + mid_i:932)
                                  /\ 0 <= (32 + -mid_i:932))) /\ K:936 = 0
                      /\ mid_t:934 = t':937 /\ mid_i:932 = i':938
                      /\ mid___cost:933 = __cost':939 /\ 0 = K:936
                      /\ (K:931 + K:936) = K:940 /\ 0 <= K:940 /\ 0 <= i':938
                      /\ 32 <= i':938 /\ __cost':939 = phi___cost:941
                      /\ i':938 = phi_i:942 /\ t':937 = phi_t:943)
                     \/ (1234 < havoc:928
                           /\ (!(0 <= K:944) \/ mid_i:945 = K:944)
                           /\ (!(0 <= K:944) \/ mid___cost:946 = (32 * K:944))
                           /\ (!((0 <= K:944 /\ K:944 <= 0))
                                 \/ mid_t:947 = t:935)
                           /\ (!(1 <= K:944) \/ mid_t:947 = 32)
                           /\ (!(0 <= K:944)
                                 \/ -mid___cost:946 <= ((-1/2 * K:944)
                                                          + (-1/2
                                                               * (K:944
                                                                    * K:944))))
                           /\ ((K:944 = 0 /\ t:935 = mid_t:947
                                  /\ 0 = mid_i:945 /\ 0 = mid___cost:946)
                                 \/ (1 <= K:944 /\ 0 <= (-1 + 32)
                                       /\ (-32 + mid_t:947) = 0
                                       /\ 0 <= (-32 + mid___cost:946)
                                       /\ 0 <= (-1 + mid_i:945)
                                       /\ 0 <= (32 + -mid_i:945)))
                           /\ K:948 = 0 /\ mid_t:947 = t':949
                           /\ mid_i:945 = i':950
                           /\ mid___cost:946 = __cost':951 /\ 0 = K:948
                           /\ (K:944 + K:948) = K:952 /\ 0 <= K:952
                           /\ 0 <= i':950 /\ 32 <= i':950
                           /\ __cost':951 = phi___cost:941
                           /\ i':950 = phi_i:942 /\ t':949 = phi_t:943))
               /\ phi___cost:941 = phi___cost:963 /\ 0 = phi___retres5:962
               /\ havoc:953 = phi_return:961 /\ havoc:928 = phi_param0:960
               /\ type_err:954 = phi_return@pos:959
               /\ type_err:929 = phi_param0@pos:958
               /\ type_err:955 = phi_return@width:957
               /\ type_err:930 = phi_param0@width:956))}

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

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

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