/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, 19> -> <Unique State Name, 54>	Base relation: 
{return := havoc:36
 return@pos := type_err:39
 return@width := type_err:40}	
<Unique State Name, 18> -> <Unique State Name, 19>	Base relation: 
{}	
<Unique State Name, 51> -> <Unique State Name, 50>	Base relation: 
{guess := havoc:15}	
<Unique State Name, 43> -> <Unique State Name, 37 42>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 48> -> <Unique State Name, 37 47>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 47> -> <Unique State Name, 43>	Base relation: 
{time0 := return:43
 param0 := secret1:44
 param1 := guess:27
 param0@pos := type_err:64
 param1@pos := type_err:66
 param0@width := type_err:65
 param1@width := type_err:67}	
<Unique State Name, 42> -> <Unique State Name, 18>	Base relation: 
{when time0:34 < return:43}	
<Unique State Name, 49> -> <Unique State Name, 55>	Base relation: 
{return := 0
 return@pos := type_err:12
 return@width := type_err:13}	
<Unique State Name, 37> -> <Unique State Name, 53>	Base relation: 
{return := phi___retres4:107
 return@pos := type_err:108
 return@width := type_err:109
 when (0 <= param0:8 /\ param0:8 <= 1024
         /\ (((ite(0 <= param0:8, floor((param0:8 / 256)),
                   -(floor(-((param0:8 / 256)))))
               mod 4) = (ite(0 <= param1:11, floor((param1:11 / 256)),
                             -(floor(-((param1:11 / 256)))))
                         mod 4) /\ 1 = phi___retres4:107)
               \/ (!((ite(0 <= param0:8, floor((param0:8 / 256)),
                          -(floor(-((param0:8 / 256)))))
                      mod 4) = (ite(0 <= param1:11, floor((param1:11 / 256)),
                                    -(floor(-((param1:11 / 256)))))
                                mod 4)) /\ 0 = phi___retres4:107)))}	
<Unique State Name, 54> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 55> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 50> -> <Unique State Name, 22 49>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 53> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 22> -> <Unique State Name, 48>	Base relation: 
{secret1 := havoc:63
 param0 := havoc:62
 param1 := guess:27
 param0@pos := type_err:68
 param1@pos := type_err:70
 param0@width := type_err:69
 param1@width := type_err:71
 when (0 <= guess:27 /\ guess:27 <= 1024)}	
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  17  20  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {guess := havoc:15}    )
    ,
    Var(17)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:12
     return@width := type_err:13}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=17: 
Dot(
  Dot(
    Dot(
      Dot(
        Weight(Base relation: 
          {secret1 := havoc:63
           param0 := havoc:62
           param1 := guess:27
           param0@pos := type_err:68
           param1@pos := type_err:70
           param0@width := type_err:69
           param1@width := type_err:71
           when (0 <= guess:27 /\ guess:27 <= 1024)}        )
        ,
        Var(20)
      )
      ,
      Weight(Base relation: 
        {time0 := return:43
         param0 := secret1:44
         param1 := guess:27
         param0@pos := type_err:64
         param1@pos := type_err:66
         param0@width := type_err:65
         param1@width := type_err:67}      )
    )
    ,
    Var(20)
  )
  ,
  Weight(Base relation: 
    {return := havoc:115
     return@pos := type_err:116
     return@width := type_err:117
     when time0:34 < return:43}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=20: 
Weight(Base relation: 
  {return := phi___retres4:107
   return@pos := type_err:108
   return@width := type_err:109
   when (0 <= param0:8 /\ param0:8 <= 1024
           /\ (((ite(0 <= param0:8, floor((param0:8 / 256)),
                     -(floor(-((param0:8 / 256)))))
                 mod 4) = (ite(0 <= param1:11, floor((param1:11 / 256)),
                               -(floor(-((param1:11 / 256)))))
                           mod 4) /\ 1 = phi___retres4:107)
                 \/ (!((ite(0 <= param0:8, floor((param0:8 / 256)),
                            -(floor(-((param0:8 / 256)))))
                        mod 4) = (ite(0 <= param1:11,
                                      floor((param1:11 / 256)),
                                      -(floor(-((param1:11 / 256)))))
                                  mod 4)) /\ 0 = phi___retres4:107)))})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {guess := havoc:15}      )
      ,
      Var(17)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:12
       return@width := type_err:13}    )
  )
)



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

Project(
  Dot(
    Dot(
      Dot(
        Dot(
          Weight(Base relation: 
            {secret1 := havoc:63
             param0 := havoc:62
             param1 := guess:27
             param0@pos := type_err:68
             param1@pos := type_err:70
             param0@width := type_err:69
             param1@width := type_err:71
             when (0 <= guess:27 /\ guess:27 <= 1024)}          )
          ,
          Var(20)
        )
        ,
        Weight(Base relation: 
          {time0 := return:43
           param0 := secret1:44
           param1 := guess:27
           param0@pos := type_err:64
           param1@pos := type_err:66
           param0@width := type_err:65
           param1@width := type_err:67}        )
      )
      ,
      Var(20)
    )
    ,
    Weight(Base relation: 
      {return := havoc:115
       return@pos := type_err:116
       return@width := type_err:117
       when time0:34 < return:43}    )
  )
)



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

Weight(Base relation: 
  {return := phi___retres4:107
   return@pos := type_err:108
   return@width := type_err:109
   when (0 <= param0:8 /\ param0:8 <= 1024
           /\ (((ite(0 <= param0:8, floor((param0:8 / 256)),
                     -(floor(-((param0:8 / 256)))))
                 mod 4) = (ite(0 <= param1:11, floor((param1:11 / 256)),
                               -(floor(-((param1:11 / 256)))))
                           mod 4) /\ 1 = phi___retres4:107)
                 \/ (!((ite(0 <= param0:8, floor((param0:8 / 256)),
                            -(floor(-((param0:8 / 256)))))
                        mod 4) = (ite(0 <= param1:11,
                                      floor((param1:11 / 256)),
                                      -(floor(-((param1:11 / 256)))))
                                  mod 4)) /\ 0 = phi___retres4:107)))})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {guess := havoc:15
   return := 0
   param0 := havoc:133
   param1 := havoc:15
   return@pos := type_err:142
   param0@pos := type_err:137
   param1@pos := type_err:138
   return@width := type_err:143
   param0@width := type_err:140
   param1@width := type_err:141
   when (0 <= havoc:15 /\ havoc:15 <= 1024 /\ 0 <= havoc:131
           /\ havoc:131 <= 1024
           /\ (((ite(0 <= havoc:131, floor((havoc:131 / 256)),
                     -(floor(-((havoc:131 / 256)))))
                 mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                               -(floor(-((havoc:15 / 256)))))
                           mod 4) /\ 1 = phi___retres4:132)
                 \/ (!((ite(0 <= havoc:131, floor((havoc:131 / 256)),
                            -(floor(-((havoc:131 / 256)))))
                        mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                                      -(floor(-((havoc:15 / 256)))))
                                  mod 4)) /\ 0 = phi___retres4:132))
           /\ 0 <= havoc:133 /\ havoc:133 <= 1024
           /\ (((ite(0 <= havoc:133, floor((havoc:133 / 256)),
                     -(floor(-((havoc:133 / 256)))))
                 mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                               -(floor(-((havoc:15 / 256)))))
                           mod 4) /\ 1 = phi___retres4:134)
                 \/ (!((ite(0 <= havoc:133, floor((havoc:133 / 256)),
                            -(floor(-((havoc:133 / 256)))))
                        mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                                      -(floor(-((havoc:15 / 256)))))
                                  mod 4)) /\ 0 = phi___retres4:134))
           /\ phi___retres4:132 < phi___retres4:134)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=17: 
Weight(Base relation: 
  {return := havoc:154
   param0 := havoc:63
   param1 := guess:27
   return@pos := type_err:155
   param0@pos := type_err:147
   param1@pos := type_err:148
   return@width := type_err:156
   param0@width := type_err:149
   param1@width := type_err:150
   when (0 <= guess:27 /\ guess:27 <= 1024 /\ 0 <= havoc:62
           /\ havoc:62 <= 1024
           /\ (((ite(0 <= havoc:62, floor((havoc:62 / 256)),
                     -(floor(-((havoc:62 / 256)))))
                 mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                               -(floor(-((guess:27 / 256)))))
                           mod 4) /\ 1 = phi___retres4:144)
                 \/ (!((ite(0 <= havoc:62, floor((havoc:62 / 256)),
                            -(floor(-((havoc:62 / 256)))))
                        mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                                      -(floor(-((guess:27 / 256)))))
                                  mod 4)) /\ 0 = phi___retres4:144))
           /\ 0 <= havoc:63 /\ havoc:63 <= 1024
           /\ (((ite(0 <= havoc:63, floor((havoc:63 / 256)),
                     -(floor(-((havoc:63 / 256)))))
                 mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                               -(floor(-((guess:27 / 256)))))
                           mod 4) /\ 1 = phi___retres4:151)
                 \/ (!((ite(0 <= havoc:63, floor((havoc:63 / 256)),
                            -(floor(-((havoc:63 / 256)))))
                        mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                                      -(floor(-((guess:27 / 256)))))
                                  mod 4)) /\ 0 = phi___retres4:151))
           /\ phi___retres4:144 < phi___retres4:151)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=20: 
Weight(Base relation: 
  {return := phi___retres4:107
   return@pos := type_err:108
   return@width := type_err:109
   when (0 <= param0:8 /\ param0:8 <= 1024
           /\ (((ite(0 <= param0:8, floor((param0:8 / 256)),
                     -(floor(-((param0:8 / 256)))))
                 mod 4) = (ite(0 <= param1:11, floor((param1:11 / 256)),
                               -(floor(-((param1:11 / 256)))))
                           mod 4) /\ 1 = phi___retres4:107)
                 \/ (!((ite(0 <= param0:8, floor((param0:8 / 256)),
                            -(floor(-((param0:8 / 256)))))
                        mod 4) = (ite(0 <= param1:11,
                                      floor((param1:11 / 256)),
                                      -(floor(-((param1:11 / 256)))))
                                  mod 4)) /\ 0 = phi___retres4:107)))})


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

  The IRE-evaluated value on this round is: 

Base relation: 
{guess := havoc:15
 return := 0
 param0 := havoc:133
 param1 := havoc:15
 return@pos := type_err:142
 param0@pos := type_err:137
 param1@pos := type_err:138
 return@width := type_err:143
 param0@width := type_err:140
 param1@width := type_err:141
 when (0 <= havoc:15 /\ havoc:15 <= 1024 /\ 0 <= havoc:131
         /\ havoc:131 <= 1024
         /\ (((ite(0 <= havoc:131, floor((havoc:131 / 256)),
                   -(floor(-((havoc:131 / 256)))))
               mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                             -(floor(-((havoc:15 / 256)))))
                         mod 4) /\ 1 = phi___retres4:132)
               \/ (!((ite(0 <= havoc:131, floor((havoc:131 / 256)),
                          -(floor(-((havoc:131 / 256)))))
                      mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                                    -(floor(-((havoc:15 / 256)))))
                                mod 4)) /\ 0 = phi___retres4:132))
         /\ 0 <= havoc:133 /\ havoc:133 <= 1024
         /\ (((ite(0 <= havoc:133, floor((havoc:133 / 256)),
                   -(floor(-((havoc:133 / 256)))))
               mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                             -(floor(-((havoc:15 / 256)))))
                         mod 4) /\ 1 = phi___retres4:134)
               \/ (!((ite(0 <= havoc:133, floor((havoc:133 / 256)),
                          -(floor(-((havoc:133 / 256)))))
                      mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                                    -(floor(-((havoc:15 / 256)))))
                                mod 4)) /\ 0 = phi___retres4:134))
         /\ phi___retres4:132 < phi___retres4:134)}

Evaluating variable number 17 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{return := havoc:154
 param0 := havoc:63
 param1 := guess:27
 return@pos := type_err:155
 param0@pos := type_err:147
 param1@pos := type_err:148
 return@width := type_err:156
 param0@width := type_err:149
 param1@width := type_err:150
 when (0 <= guess:27 /\ guess:27 <= 1024 /\ 0 <= havoc:62 /\ havoc:62 <= 1024
         /\ (((ite(0 <= havoc:62, floor((havoc:62 / 256)),
                   -(floor(-((havoc:62 / 256)))))
               mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                             -(floor(-((guess:27 / 256)))))
                         mod 4) /\ 1 = phi___retres4:144)
               \/ (!((ite(0 <= havoc:62, floor((havoc:62 / 256)),
                          -(floor(-((havoc:62 / 256)))))
                      mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                                    -(floor(-((guess:27 / 256)))))
                                mod 4)) /\ 0 = phi___retres4:144))
         /\ 0 <= havoc:63 /\ havoc:63 <= 1024
         /\ (((ite(0 <= havoc:63, floor((havoc:63 / 256)),
                   -(floor(-((havoc:63 / 256)))))
               mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                             -(floor(-((guess:27 / 256)))))
                         mod 4) /\ 1 = phi___retres4:151)
               \/ (!((ite(0 <= havoc:63, floor((havoc:63 / 256)),
                          -(floor(-((havoc:63 / 256)))))
                      mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                                    -(floor(-((guess:27 / 256)))))
                                mod 4)) /\ 0 = phi___retres4:151))
         /\ phi___retres4:144 < phi___retres4:151)}

Evaluating variable number 20 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{return := phi___retres4:107
 return@pos := type_err:108
 return@width := type_err:109
 when (0 <= param0:8 /\ param0:8 <= 1024
         /\ (((ite(0 <= param0:8, floor((param0:8 / 256)),
                   -(floor(-((param0:8 / 256)))))
               mod 4) = (ite(0 <= param1:11, floor((param1:11 / 256)),
                             -(floor(-((param1:11 / 256)))))
                         mod 4) /\ 1 = phi___retres4:107)
               \/ (!((ite(0 <= param0:8, floor((param0:8 / 256)),
                          -(floor(-((param0:8 / 256)))))
                      mod 4) = (ite(0 <= param1:11, floor((param1:11 / 256)),
                                    -(floor(-((param1:11 / 256)))))
                                mod 4)) /\ 0 = phi___retres4:107)))}

    (IRE-tc) Checking termination condition.
    (IRE-tc)     >> All star bodies equivalent.

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,22)_g1> -> <__pstate, (Unique State Name,37)_g1>	Base relation: 
{secret1 := havoc:63
 time0 := phi_time0:191
 return := phi_return:190
 param0 := phi_param0:189
 param1 := guess:27
 return@pos := phi_return@pos:188
 param0@pos := phi_param0@pos:187
 param1@pos := phi_param1@pos:186
 return@width := phi_return@width:185
 param0@width := phi_param0@width:184
 param1@width := phi_param1@width:183
 when ((0 <= guess:27 /\ guess:27 <= 1024 /\ 0 <= havoc:62
          /\ havoc:62 <= 1024
          /\ (((ite(0 <= havoc:62, floor((havoc:62 / 256)),
                    -(floor(-((havoc:62 / 256)))))
                mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                              -(floor(-((guess:27 / 256)))))
                          mod 4) /\ 1 = phi___retres4:170)
                \/ (!((ite(0 <= havoc:62, floor((havoc:62 / 256)),
                           -(floor(-((havoc:62 / 256)))))
                       mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                                     -(floor(-((guess:27 / 256)))))
                                 mod 4)) /\ 0 = phi___retres4:170))
          /\ phi___retres4:170 = phi_time0:191
          /\ phi___retres4:170 = phi_return:190 /\ havoc:63 = phi_param0:189
          /\ type_err:171 = phi_return@pos:188
          /\ type_err:173 = phi_param0@pos:187
          /\ type_err:174 = phi_param1@pos:186
          /\ type_err:172 = phi_return@width:185
          /\ type_err:175 = phi_param0@width:184
          /\ type_err:176 = phi_param1@width:183)
         \/ (0 <= guess:27 /\ guess:27 <= 1024 /\ time0:34 = phi_time0:191
               /\ return:43 = phi_return:190 /\ havoc:62 = phi_param0:189
               /\ return@pos:42 = phi_return@pos:188
               /\ type_err:68 = phi_param0@pos:187
               /\ type_err:70 = phi_param1@pos:186
               /\ return@width:41 = phi_return@width:185
               /\ type_err:69 = phi_param0@width:184
               /\ type_err:71 = phi_param1@width:183))}	
<__pstate, accept> -> <__pstate, (Unique State Name,22)_g1>	Base relation: 
{guess := havoc:15}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x150d770: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x1175460: 
	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,37)_g1 , __done )	Base relation: 
{guess := havoc:15
 secret1 := havoc:196
 time0 := phi_time0:194
 return := phi_return:195
 param0 := phi_param0:197
 param1 := havoc:15
 return@pos := phi_return@pos:199
 param0@pos := phi_param0@pos:201
 param1@pos := phi_param1@pos:203
 return@width := phi_return@width:205
 param0@width := phi_param0@width:207
 param1@width := phi_param1@width:209
 when ((0 <= havoc:15 /\ havoc:15 <= 1024 /\ 0 <= havoc:192
          /\ havoc:192 <= 1024
          /\ (((ite(0 <= havoc:192, floor((havoc:192 / 256)),
                    -(floor(-((havoc:192 / 256)))))
                mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                              -(floor(-((havoc:15 / 256)))))
                          mod 4) /\ 1 = phi___retres4:193)
                \/ (!((ite(0 <= havoc:192, floor((havoc:192 / 256)),
                           -(floor(-((havoc:192 / 256)))))
                       mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                                     -(floor(-((havoc:15 / 256)))))
                                 mod 4)) /\ 0 = phi___retres4:193))
          /\ phi___retres4:193 = phi_time0:194
          /\ phi___retres4:193 = phi_return:195 /\ havoc:196 = phi_param0:197
          /\ type_err:198 = phi_return@pos:199
          /\ type_err:200 = phi_param0@pos:201
          /\ type_err:202 = phi_param1@pos:203
          /\ type_err:204 = phi_return@width:205
          /\ type_err:206 = phi_param0@width:207
          /\ type_err:208 = phi_param1@width:209)
         \/ (0 <= havoc:15 /\ havoc:15 <= 1024 /\ time0:34 = phi_time0:194
               /\ return:43 = phi_return:195 /\ havoc:192 = phi_param0:197
               /\ return@pos:42 = phi_return@pos:199
               /\ type_err:210 = phi_param0@pos:201
               /\ type_err:211 = phi_param1@pos:203
               /\ return@width:41 = phi_return@width:205
               /\ type_err:212 = phi_param0@width:207
               /\ type_err:213 = phi_param1@width:209))}
    ( __pstate , (Unique State Name,22)_g1 , __done )	Base relation: 
{guess := havoc:15}

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

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

Base relation: 
{return := phi___retres4:107
 return@pos := type_err:108
 return@width := type_err:109
 when (0 <= param0:8 /\ param0:8 <= 1024
         /\ (((ite(0 <= param0:8, floor((param0:8 / 256)),
                   -(floor(-((param0:8 / 256)))))
               mod 4) = (ite(0 <= param1:11, floor((param1:11 / 256)),
                             -(floor(-((param1:11 / 256)))))
                         mod 4) /\ 1 = phi___retres4:107)
               \/ (!((ite(0 <= param0:8, floor((param0:8 / 256)),
                          -(floor(-((param0:8 / 256)))))
                      mod 4) = (ite(0 <= param1:11, floor((param1:11 / 256)),
                                    -(floor(-((param1:11 / 256)))))
                                mod 4)) /\ 0 = phi___retres4:107)))}

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

Base relation: 
{guess := havoc:15
 return := 0
 param0 := havoc:159
 param1 := havoc:15
 return@pos := type_err:168
 param0@pos := type_err:163
 param1@pos := type_err:164
 return@width := type_err:169
 param0@width := type_err:166
 param1@width := type_err:167
 when (0 <= havoc:15 /\ havoc:15 <= 1024 /\ 0 <= havoc:157
         /\ havoc:157 <= 1024
         /\ (((ite(0 <= havoc:157, floor((havoc:157 / 256)),
                   -(floor(-((havoc:157 / 256)))))
               mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                             -(floor(-((havoc:15 / 256)))))
                         mod 4) /\ 1 = phi___retres4:158)
               \/ (!((ite(0 <= havoc:157, floor((havoc:157 / 256)),
                          -(floor(-((havoc:157 / 256)))))
                      mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                                    -(floor(-((havoc:15 / 256)))))
                                mod 4)) /\ 0 = phi___retres4:158))
         /\ 0 <= havoc:159 /\ havoc:159 <= 1024
         /\ (((ite(0 <= havoc:159, floor((havoc:159 / 256)),
                   -(floor(-((havoc:159 / 256)))))
               mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                             -(floor(-((havoc:15 / 256)))))
                         mod 4) /\ 1 = phi___retres4:160)
               \/ (!((ite(0 <= havoc:159, floor((havoc:159 / 256)),
                          -(floor(-((havoc:159 / 256)))))
                      mod 4) = (ite(0 <= havoc:15, floor((havoc:15 / 256)),
                                    -(floor(-((havoc:15 / 256)))))
                                mod 4)) /\ 0 = phi___retres4:160))
         /\ phi___retres4:158 < phi___retres4:160)}

------------------------------------------------
Procedure summary for start

Base relation: 
{secret1 := havoc:63
 time0 := phi___retres4:170
 return := havoc:180
 param0 := havoc:63
 param1 := guess:27
 return@pos := type_err:181
 param0@pos := type_err:173
 param1@pos := type_err:174
 return@width := type_err:182
 param0@width := type_err:175
 param1@width := type_err:176
 when (0 <= guess:27 /\ guess:27 <= 1024 /\ 0 <= havoc:62 /\ havoc:62 <= 1024
         /\ (((ite(0 <= havoc:62, floor((havoc:62 / 256)),
                   -(floor(-((havoc:62 / 256)))))
               mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                             -(floor(-((guess:27 / 256)))))
                         mod 4) /\ 1 = phi___retres4:170)
               \/ (!((ite(0 <= havoc:62, floor((havoc:62 / 256)),
                          -(floor(-((havoc:62 / 256)))))
                      mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                                    -(floor(-((guess:27 / 256)))))
                                mod 4)) /\ 0 = phi___retres4:170))
         /\ 0 <= havoc:63 /\ havoc:63 <= 1024
         /\ (((ite(0 <= havoc:63, floor((havoc:63 / 256)),
                   -(floor(-((havoc:63 / 256)))))
               mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                             -(floor(-((guess:27 / 256)))))
                         mod 4) /\ 1 = phi___retres4:177)
               \/ (!((ite(0 <= havoc:63, floor((havoc:63 / 256)),
                          -(floor(-((havoc:63 / 256)))))
                      mod 4) = (ite(0 <= guess:27, floor((guess:27 / 256)),
                                    -(floor(-((guess:27 / 256)))))
                                mod 4)) /\ 0 = phi___retres4:177))
         /\ phi___retres4:170 < phi___retres4:177)}

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

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

Variable bounds at line 15 in start


Variable bounds at line 16 in start

0 <= secret1
secret1 is o(1)
secret1 <= 1024
secret1 is O(1)

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