/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, 15> -> <Unique State Name, 66>	Base relation: 
{password_binval := havoc:15
 guess_binval := havoc:0
 when (0 <= havoc:0 /\ 0 <= havoc:15 /\ havoc:0 < 16777216
         /\ havoc:15 < 16777216)}	
<Unique State Name, 44> -> <Unique State Name, 68>	Base relation: 
{return := phi___retres1:46
 return@pos := type_err:49
 return@width := type_err:50
 when (0 <= guess_binval:4 /\ 0 <= password_binval:5
         /\ ((((ite(0 <= password_binval:5,
                    floor((password_binval:5 / 65536)),
                    -(floor(-((password_binval:5 / 65536)))))
                mod 256) < (ite(0 <= guess_binval:4,
                                floor((guess_binval:4 / 65536)),
                                -(floor(-((guess_binval:4 / 65536)))))
                            mod 256)
                 \/ (ite(0 <= guess_binval:4,
                         floor((guess_binval:4 / 65536)),
                         -(floor(-((guess_binval:4 / 65536)))))
                     mod 256) < (ite(0 <= password_binval:5,
                                     floor((password_binval:5 / 65536)),
                                     -(floor(-((password_binval:5 / 65536)))))
                                 mod 256)) /\ 0 = phi___retres1:46)
               \/ ((ite(0 <= guess_binval:4, floor((guess_binval:4 / 65536)),
                        -(floor(-((guess_binval:4 / 65536)))))
                    mod 256) <= (ite(0 <= password_binval:5,
                                     floor((password_binval:5 / 65536)),
                                     -(floor(-((password_binval:5 / 65536)))))
                                 mod 256)
                     /\ (ite(0 <= password_binval:5,
                             floor((password_binval:5 / 65536)),
                             -(floor(-((password_binval:5 / 65536)))))
                         mod 256) <= (ite(0 <= guess_binval:4,
                                          floor((guess_binval:4 / 65536)),
                                          -(floor(-((guess_binval:4 / 65536)))))
                                      mod 256)
                     /\ ((((ite(0 <= password_binval:5,
                                floor((password_binval:5 / 256)),
                                -(floor(-((password_binval:5 / 256)))))
                            mod 256) < (ite(0 <= guess_binval:4,
                                            floor((guess_binval:4 / 256)),
                                            -(floor(-((guess_binval:4 / 256)))))
                                        mod 256)
                             \/ (ite(0 <= guess_binval:4,
                                     floor((guess_binval:4 / 256)),
                                     -(floor(-((guess_binval:4 / 256)))))
                                 mod 256) < (ite(0 <= password_binval:5,
                                                 floor((password_binval:5
                                                        / 256)),
                                                 -(floor(-((password_binval:5
                                                            / 256)))))
                                             mod 256))
                            /\ 1 = phi___retres1:47)
                           \/ ((ite(0 <= guess_binval:4,
                                    floor((guess_binval:4 / 256)),
                                    -(floor(-((guess_binval:4 / 256)))))
                                mod 256) <= (ite(0 <= password_binval:5,
                                                 floor((password_binval:5
                                                        / 256)),
                                                 -(floor(-((password_binval:5
                                                            / 256)))))
                                             mod 256)
                                 /\ (ite(0 <= password_binval:5,
                                         floor((password_binval:5 / 256)),
                                         -(floor(-((password_binval:5 / 256)))))
                                     mod 256) <= (ite(0 <= guess_binval:4,
                                                      floor((guess_binval:4
                                                             / 256)),
                                                      -(floor(-((guess_binval:4
                                                                 / 256)))))
                                                  mod 256)
                                 /\ ((((password_binval:5 mod 256) < (
                                       guess_binval:4 mod 256)
                                         \/ (guess_binval:4 mod 256) < (
                                            password_binval:5 mod 256))
                                        /\ 2 = phi___retres1:48)
                                       \/ ((guess_binval:4 mod 256) <= (
                                           password_binval:5 mod 256)
                                             /\ (password_binval:5 mod 256) <= (
                                                guess_binval:4 mod 256)
                                             /\ 3 = phi___retres1:48))
                                 /\ phi___retres1:48 = phi___retres1:47))
                     /\ phi___retres1:47 = phi___retres1:46)))}	
<Unique State Name, 50> -> <Unique State Name, 46>	Base relation: 
{i := (i:64 + 1)
 s := ite(0 <= s:66, floor((s:66 / 256)), -(floor(-((s:66 / 256)))))
 when i:64 < k:65}	
<Unique State Name, 50> -> <Unique State Name, 67>	Base relation: 
{return := s:66
 return@pos := type_err:78
 return@width := type_err:79
 when k:65 <= i:64}	
<Unique State Name, 70> -> <Unique State Name, 50>	Base relation: 
{}	
<Unique State Name, 68> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 12> -> <Unique State Name, 69>	Base relation: 
{return := havoc:7
 return@pos := type_err:10
 return@width := type_err:11}	
<Unique State Name, 62> -> <Unique State Name, 46>	Base relation: 
{i := 0
 s := param0:74
 k := param1:77}	
<Unique State Name, 69> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 46> -> <Unique State Name, 70>	Base relation: 
{when 0 <= i:64}	
<Unique State Name, 66> -> <Unique State Name, 44 65>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 65> -> <Unique State Name, 12>	Base relation: 
{result := return:14}	
#################################################################
           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: 
7  10  


New-style (IRE) regular expression in IREregExpMap for reID=7: 
Dot(
  Dot(
    Weight(Base relation: 
      {password_binval := havoc:15
       guess_binval := havoc:0
       when (0 <= havoc:0 /\ 0 <= havoc:15 /\ havoc:0 < 16777216
               /\ havoc:15 < 16777216)}    )
    ,
    Var(10)
  )
  ,
  Weight(Base relation: 
    {result := return:14
     return := havoc:132
     return@pos := type_err:133
     return@width := type_err:134}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=10: 
Weight(Base relation: 
  {return := phi___retres1:46
   return@pos := type_err:49
   return@width := type_err:50
   when (0 <= guess_binval:4 /\ 0 <= password_binval:5
           /\ ((((ite(0 <= password_binval:5,
                      floor((password_binval:5 / 65536)),
                      -(floor(-((password_binval:5 / 65536)))))
                  mod 256) < (ite(0 <= guess_binval:4,
                                  floor((guess_binval:4 / 65536)),
                                  -(floor(-((guess_binval:4 / 65536)))))
                              mod 256)
                   \/ (ite(0 <= guess_binval:4,
                           floor((guess_binval:4 / 65536)),
                           -(floor(-((guess_binval:4 / 65536)))))
                       mod 256) < (ite(0 <= password_binval:5,
                                       floor((password_binval:5 / 65536)),
                                       -(floor(-((password_binval:5 / 65536)))))
                                   mod 256)) /\ 0 = phi___retres1:46)
                 \/ ((ite(0 <= guess_binval:4,
                          floor((guess_binval:4 / 65536)),
                          -(floor(-((guess_binval:4 / 65536)))))
                      mod 256) <= (ite(0 <= password_binval:5,
                                       floor((password_binval:5 / 65536)),
                                       -(floor(-((password_binval:5 / 65536)))))
                                   mod 256)
                       /\ (ite(0 <= password_binval:5,
                               floor((password_binval:5 / 65536)),
                               -(floor(-((password_binval:5 / 65536)))))
                           mod 256) <= (ite(0 <= guess_binval:4,
                                            floor((guess_binval:4 / 65536)),
                                            -(floor(-((guess_binval:4 / 65536)))))
                                        mod 256)
                       /\ ((((ite(0 <= password_binval:5,
                                  floor((password_binval:5 / 256)),
                                  -(floor(-((password_binval:5 / 256)))))
                              mod 256) < (ite(0 <= guess_binval:4,
                                              floor((guess_binval:4 / 256)),
                                              -(floor(-((guess_binval:4 / 256)))))
                                          mod 256)
                               \/ (ite(0 <= guess_binval:4,
                                       floor((guess_binval:4 / 256)),
                                       -(floor(-((guess_binval:4 / 256)))))
                                   mod 256) < (ite(0 <= password_binval:5,
                                                   floor((password_binval:5
                                                          / 256)),
                                                   -(floor(-((password_binval:5
                                                              / 256)))))
                                               mod 256))
                              /\ 1 = phi___retres1:47)
                             \/ ((ite(0 <= guess_binval:4,
                                      floor((guess_binval:4 / 256)),
                                      -(floor(-((guess_binval:4 / 256)))))
                                  mod 256) <= (ite(0 <= password_binval:5,
                                                   floor((password_binval:5
                                                          / 256)),
                                                   -(floor(-((password_binval:5
                                                              / 256)))))
                                               mod 256)
                                   /\ (ite(0 <= password_binval:5,
                                           floor((password_binval:5 / 256)),
                                           -(floor(-((password_binval:5 / 256)))))
                                       mod 256) <= (ite(0 <= guess_binval:4,
                                                        floor((guess_binval:4
                                                               / 256)),
                                                        -(floor(-((guess_binval:4
                                                                   / 256)))))
                                                    mod 256)
                                   /\ ((((password_binval:5 mod 256) < (
                                         guess_binval:4 mod 256)
                                           \/ (guess_binval:4 mod 256) < (
                                              password_binval:5 mod 256))
                                          /\ 2 = phi___retres1:48)
                                         \/ ((guess_binval:4 mod 256) <= (
                                             password_binval:5 mod 256)
                                               /\ (password_binval:5 mod 256) <= (
                                                  guess_binval:4 mod 256)
                                               /\ 3 = phi___retres1:48))
                                   /\ phi___retres1:48 = phi___retres1:47))
                       /\ phi___retres1:47 = phi___retres1:46)))})



Performing Gaussian Elimination.


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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {password_binval := havoc:15
         guess_binval := havoc:0
         when (0 <= havoc:0 /\ 0 <= havoc:15 /\ havoc:0 < 16777216
                 /\ havoc:15 < 16777216)}      )
      ,
      Var(10)
    )
    ,
    Weight(Base relation: 
      {result := return:14
       return := havoc:132
       return@pos := type_err:133
       return@width := type_err:134}    )
  )
)



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

Weight(Base relation: 
  {return := phi___retres1:46
   return@pos := type_err:49
   return@width := type_err:50
   when (0 <= guess_binval:4 /\ 0 <= password_binval:5
           /\ ((((ite(0 <= password_binval:5,
                      floor((password_binval:5 / 65536)),
                      -(floor(-((password_binval:5 / 65536)))))
                  mod 256) < (ite(0 <= guess_binval:4,
                                  floor((guess_binval:4 / 65536)),
                                  -(floor(-((guess_binval:4 / 65536)))))
                              mod 256)
                   \/ (ite(0 <= guess_binval:4,
                           floor((guess_binval:4 / 65536)),
                           -(floor(-((guess_binval:4 / 65536)))))
                       mod 256) < (ite(0 <= password_binval:5,
                                       floor((password_binval:5 / 65536)),
                                       -(floor(-((password_binval:5 / 65536)))))
                                   mod 256)) /\ 0 = phi___retres1:46)
                 \/ ((ite(0 <= guess_binval:4,
                          floor((guess_binval:4 / 65536)),
                          -(floor(-((guess_binval:4 / 65536)))))
                      mod 256) <= (ite(0 <= password_binval:5,
                                       floor((password_binval:5 / 65536)),
                                       -(floor(-((password_binval:5 / 65536)))))
                                   mod 256)
                       /\ (ite(0 <= password_binval:5,
                               floor((password_binval:5 / 65536)),
                               -(floor(-((password_binval:5 / 65536)))))
                           mod 256) <= (ite(0 <= guess_binval:4,
                                            floor((guess_binval:4 / 65536)),
                                            -(floor(-((guess_binval:4 / 65536)))))
                                        mod 256)
                       /\ ((((ite(0 <= password_binval:5,
                                  floor((password_binval:5 / 256)),
                                  -(floor(-((password_binval:5 / 256)))))
                              mod 256) < (ite(0 <= guess_binval:4,
                                              floor((guess_binval:4 / 256)),
                                              -(floor(-((guess_binval:4 / 256)))))
                                          mod 256)
                               \/ (ite(0 <= guess_binval:4,
                                       floor((guess_binval:4 / 256)),
                                       -(floor(-((guess_binval:4 / 256)))))
                                   mod 256) < (ite(0 <= password_binval:5,
                                                   floor((password_binval:5
                                                          / 256)),
                                                   -(floor(-((password_binval:5
                                                              / 256)))))
                                               mod 256))
                              /\ 1 = phi___retres1:47)
                             \/ ((ite(0 <= guess_binval:4,
                                      floor((guess_binval:4 / 256)),
                                      -(floor(-((guess_binval:4 / 256)))))
                                  mod 256) <= (ite(0 <= password_binval:5,
                                                   floor((password_binval:5
                                                          / 256)),
                                                   -(floor(-((password_binval:5
                                                              / 256)))))
                                               mod 256)
                                   /\ (ite(0 <= password_binval:5,
                                           floor((password_binval:5 / 256)),
                                           -(floor(-((password_binval:5 / 256)))))
                                       mod 256) <= (ite(0 <= guess_binval:4,
                                                        floor((guess_binval:4
                                                               / 256)),
                                                        -(floor(-((guess_binval:4
                                                                   / 256)))))
                                                    mod 256)
                                   /\ ((((password_binval:5 mod 256) < (
                                         guess_binval:4 mod 256)
                                           \/ (guess_binval:4 mod 256) < (
                                              password_binval:5 mod 256))
                                          /\ 2 = phi___retres1:48)
                                         \/ ((guess_binval:4 mod 256) <= (
                                             password_binval:5 mod 256)
                                               /\ (password_binval:5 mod 256) <= (
                                                  guess_binval:4 mod 256)
                                               /\ 3 = phi___retres1:48))
                                   /\ phi___retres1:48 = phi___retres1:47))
                       /\ phi___retres1:47 = phi___retres1:46)))})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=7: 
Weight(Base relation: 
  {result := phi___retres1:135
   password_binval := havoc:15
   guess_binval := havoc:0
   return := havoc:140
   return@pos := type_err:141
   return@width := type_err:142
   when (0 <= havoc:0 /\ 0 <= havoc:15 /\ havoc:0 < 16777216
           /\ havoc:15 < 16777216 /\ 0 <= havoc:0 /\ 0 <= havoc:15
           /\ ((((ite(0 <= havoc:15, floor((havoc:15 / 65536)),
                      -(floor(-((havoc:15 / 65536)))))
                  mod 256) < (ite(0 <= havoc:0, floor((havoc:0 / 65536)),
                                  -(floor(-((havoc:0 / 65536)))))
                              mod 256)
                   \/ (ite(0 <= havoc:0, floor((havoc:0 / 65536)),
                           -(floor(-((havoc:0 / 65536)))))
                       mod 256) < (ite(0 <= havoc:15,
                                       floor((havoc:15 / 65536)),
                                       -(floor(-((havoc:15 / 65536)))))
                                   mod 256)) /\ 0 = phi___retres1:135)
                 \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)),
                          -(floor(-((havoc:0 / 65536)))))
                      mod 256) <= (ite(0 <= havoc:15,
                                       floor((havoc:15 / 65536)),
                                       -(floor(-((havoc:15 / 65536)))))
                                   mod 256)
                       /\ (ite(0 <= havoc:15, floor((havoc:15 / 65536)),
                               -(floor(-((havoc:15 / 65536)))))
                           mod 256) <= (ite(0 <= havoc:0,
                                            floor((havoc:0 / 65536)),
                                            -(floor(-((havoc:0 / 65536)))))
                                        mod 256)
                       /\ ((((ite(0 <= havoc:15, floor((havoc:15 / 256)),
                                  -(floor(-((havoc:15 / 256)))))
                              mod 256) < (ite(0 <= havoc:0,
                                              floor((havoc:0 / 256)),
                                              -(floor(-((havoc:0 / 256)))))
                                          mod 256)
                               \/ (ite(0 <= havoc:0, floor((havoc:0 / 256)),
                                       -(floor(-((havoc:0 / 256)))))
                                   mod 256) < (ite(0 <= havoc:15,
                                                   floor((havoc:15 / 256)),
                                                   -(floor(-((havoc:15 / 256)))))
                                               mod 256))
                              /\ 1 = phi___retres1:136)
                             \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)),
                                      -(floor(-((havoc:0 / 256)))))
                                  mod 256) <= (ite(0 <= havoc:15,
                                                   floor((havoc:15 / 256)),
                                                   -(floor(-((havoc:15 / 256)))))
                                               mod 256)
                                   /\ (ite(0 <= havoc:15,
                                           floor((havoc:15 / 256)),
                                           -(floor(-((havoc:15 / 256)))))
                                       mod 256) <= (ite(0 <= havoc:0,
                                                        floor((havoc:0 / 256)),
                                                        -(floor(-((havoc:0
                                                                   / 256)))))
                                                    mod 256)
                                   /\ ((((havoc:15 mod 256) < (havoc:0
                                                               mod 256)
                                           \/ (havoc:0 mod 256) < (havoc:15
                                                                   mod 256))
                                          /\ 2 = phi___retres1:137)
                                         \/ ((havoc:0 mod 256) <= (havoc:15
                                                                   mod 256)
                                               /\ (havoc:15 mod 256) <= (
                                                  havoc:0 mod 256)
                                               /\ 3 = phi___retres1:137))
                                   /\ phi___retres1:137 = phi___retres1:136))
                       /\ phi___retres1:136 = phi___retres1:135)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=10: 
Weight(Base relation: 
  {return := phi___retres1:46
   return@pos := type_err:49
   return@width := type_err:50
   when (0 <= guess_binval:4 /\ 0 <= password_binval:5
           /\ ((((ite(0 <= password_binval:5,
                      floor((password_binval:5 / 65536)),
                      -(floor(-((password_binval:5 / 65536)))))
                  mod 256) < (ite(0 <= guess_binval:4,
                                  floor((guess_binval:4 / 65536)),
                                  -(floor(-((guess_binval:4 / 65536)))))
                              mod 256)
                   \/ (ite(0 <= guess_binval:4,
                           floor((guess_binval:4 / 65536)),
                           -(floor(-((guess_binval:4 / 65536)))))
                       mod 256) < (ite(0 <= password_binval:5,
                                       floor((password_binval:5 / 65536)),
                                       -(floor(-((password_binval:5 / 65536)))))
                                   mod 256)) /\ 0 = phi___retres1:46)
                 \/ ((ite(0 <= guess_binval:4,
                          floor((guess_binval:4 / 65536)),
                          -(floor(-((guess_binval:4 / 65536)))))
                      mod 256) <= (ite(0 <= password_binval:5,
                                       floor((password_binval:5 / 65536)),
                                       -(floor(-((password_binval:5 / 65536)))))
                                   mod 256)
                       /\ (ite(0 <= password_binval:5,
                               floor((password_binval:5 / 65536)),
                               -(floor(-((password_binval:5 / 65536)))))
                           mod 256) <= (ite(0 <= guess_binval:4,
                                            floor((guess_binval:4 / 65536)),
                                            -(floor(-((guess_binval:4 / 65536)))))
                                        mod 256)
                       /\ ((((ite(0 <= password_binval:5,
                                  floor((password_binval:5 / 256)),
                                  -(floor(-((password_binval:5 / 256)))))
                              mod 256) < (ite(0 <= guess_binval:4,
                                              floor((guess_binval:4 / 256)),
                                              -(floor(-((guess_binval:4 / 256)))))
                                          mod 256)
                               \/ (ite(0 <= guess_binval:4,
                                       floor((guess_binval:4 / 256)),
                                       -(floor(-((guess_binval:4 / 256)))))
                                   mod 256) < (ite(0 <= password_binval:5,
                                                   floor((password_binval:5
                                                          / 256)),
                                                   -(floor(-((password_binval:5
                                                              / 256)))))
                                               mod 256))
                              /\ 1 = phi___retres1:47)
                             \/ ((ite(0 <= guess_binval:4,
                                      floor((guess_binval:4 / 256)),
                                      -(floor(-((guess_binval:4 / 256)))))
                                  mod 256) <= (ite(0 <= password_binval:5,
                                                   floor((password_binval:5
                                                          / 256)),
                                                   -(floor(-((password_binval:5
                                                              / 256)))))
                                               mod 256)
                                   /\ (ite(0 <= password_binval:5,
                                           floor((password_binval:5 / 256)),
                                           -(floor(-((password_binval:5 / 256)))))
                                       mod 256) <= (ite(0 <= guess_binval:4,
                                                        floor((guess_binval:4
                                                               / 256)),
                                                        -(floor(-((guess_binval:4
                                                                   / 256)))))
                                                    mod 256)
                                   /\ ((((password_binval:5 mod 256) < (
                                         guess_binval:4 mod 256)
                                           \/ (guess_binval:4 mod 256) < (
                                              password_binval:5 mod 256))
                                          /\ 2 = phi___retres1:48)
                                         \/ ((guess_binval:4 mod 256) <= (
                                             password_binval:5 mod 256)
                                               /\ (password_binval:5 mod 256) <= (
                                                  guess_binval:4 mod 256)
                                               /\ 3 = phi___retres1:48))
                                   /\ phi___retres1:48 = phi___retres1:47))
                       /\ phi___retres1:47 = phi___retres1:46)))})


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

  The IRE-evaluated value on this round is: 

Base relation: 
{result := phi___retres1:135
 password_binval := havoc:15
 guess_binval := havoc:0
 return := havoc:140
 return@pos := type_err:141
 return@width := type_err:142
 when (0 <= havoc:0 /\ 0 <= havoc:15 /\ havoc:0 < 16777216
         /\ havoc:15 < 16777216 /\ 0 <= havoc:0 /\ 0 <= havoc:15
         /\ ((((ite(0 <= havoc:15, floor((havoc:15 / 65536)),
                    -(floor(-((havoc:15 / 65536)))))
                mod 256) < (ite(0 <= havoc:0, floor((havoc:0 / 65536)),
                                -(floor(-((havoc:0 / 65536)))))
                            mod 256)
                 \/ (ite(0 <= havoc:0, floor((havoc:0 / 65536)),
                         -(floor(-((havoc:0 / 65536)))))
                     mod 256) < (ite(0 <= havoc:15,
                                     floor((havoc:15 / 65536)),
                                     -(floor(-((havoc:15 / 65536)))))
                                 mod 256)) /\ 0 = phi___retres1:135)
               \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)),
                        -(floor(-((havoc:0 / 65536)))))
                    mod 256) <= (ite(0 <= havoc:15,
                                     floor((havoc:15 / 65536)),
                                     -(floor(-((havoc:15 / 65536)))))
                                 mod 256)
                     /\ (ite(0 <= havoc:15, floor((havoc:15 / 65536)),
                             -(floor(-((havoc:15 / 65536)))))
                         mod 256) <= (ite(0 <= havoc:0,
                                          floor((havoc:0 / 65536)),
                                          -(floor(-((havoc:0 / 65536)))))
                                      mod 256)
                     /\ ((((ite(0 <= havoc:15, floor((havoc:15 / 256)),
                                -(floor(-((havoc:15 / 256)))))
                            mod 256) < (ite(0 <= havoc:0,
                                            floor((havoc:0 / 256)),
                                            -(floor(-((havoc:0 / 256)))))
                                        mod 256)
                             \/ (ite(0 <= havoc:0, floor((havoc:0 / 256)),
                                     -(floor(-((havoc:0 / 256)))))
                                 mod 256) < (ite(0 <= havoc:15,
                                                 floor((havoc:15 / 256)),
                                                 -(floor(-((havoc:15 / 256)))))
                                             mod 256))
                            /\ 1 = phi___retres1:136)
                           \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)),
                                    -(floor(-((havoc:0 / 256)))))
                                mod 256) <= (ite(0 <= havoc:15,
                                                 floor((havoc:15 / 256)),
                                                 -(floor(-((havoc:15 / 256)))))
                                             mod 256)
                                 /\ (ite(0 <= havoc:15,
                                         floor((havoc:15 / 256)),
                                         -(floor(-((havoc:15 / 256)))))
                                     mod 256) <= (ite(0 <= havoc:0,
                                                      floor((havoc:0 / 256)),
                                                      -(floor(-((havoc:0
                                                                 / 256)))))
                                                  mod 256)
                                 /\ ((((havoc:15 mod 256) < (havoc:0 mod 256)
                                         \/ (havoc:0 mod 256) < (havoc:15
                                                                 mod 256))
                                        /\ 2 = phi___retres1:137)
                                       \/ ((havoc:0 mod 256) <= (havoc:15
                                                                 mod 256)
                                             /\ (havoc:15 mod 256) <= (
                                                havoc:0 mod 256)
                                             /\ 3 = phi___retres1:137))
                                 /\ phi___retres1:137 = phi___retres1:136))
                     /\ phi___retres1:136 = phi___retres1:135)))}

Evaluating variable number 10 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{return := phi___retres1:46
 return@pos := type_err:49
 return@width := type_err:50
 when (0 <= guess_binval:4 /\ 0 <= password_binval:5
         /\ ((((ite(0 <= password_binval:5,
                    floor((password_binval:5 / 65536)),
                    -(floor(-((password_binval:5 / 65536)))))
                mod 256) < (ite(0 <= guess_binval:4,
                                floor((guess_binval:4 / 65536)),
                                -(floor(-((guess_binval:4 / 65536)))))
                            mod 256)
                 \/ (ite(0 <= guess_binval:4,
                         floor((guess_binval:4 / 65536)),
                         -(floor(-((guess_binval:4 / 65536)))))
                     mod 256) < (ite(0 <= password_binval:5,
                                     floor((password_binval:5 / 65536)),
                                     -(floor(-((password_binval:5 / 65536)))))
                                 mod 256)) /\ 0 = phi___retres1:46)
               \/ ((ite(0 <= guess_binval:4, floor((guess_binval:4 / 65536)),
                        -(floor(-((guess_binval:4 / 65536)))))
                    mod 256) <= (ite(0 <= password_binval:5,
                                     floor((password_binval:5 / 65536)),
                                     -(floor(-((password_binval:5 / 65536)))))
                                 mod 256)
                     /\ (ite(0 <= password_binval:5,
                             floor((password_binval:5 / 65536)),
                             -(floor(-((password_binval:5 / 65536)))))
                         mod 256) <= (ite(0 <= guess_binval:4,
                                          floor((guess_binval:4 / 65536)),
                                          -(floor(-((guess_binval:4 / 65536)))))
                                      mod 256)
                     /\ ((((ite(0 <= password_binval:5,
                                floor((password_binval:5 / 256)),
                                -(floor(-((password_binval:5 / 256)))))
                            mod 256) < (ite(0 <= guess_binval:4,
                                            floor((guess_binval:4 / 256)),
                                            -(floor(-((guess_binval:4 / 256)))))
                                        mod 256)
                             \/ (ite(0 <= guess_binval:4,
                                     floor((guess_binval:4 / 256)),
                                     -(floor(-((guess_binval:4 / 256)))))
                                 mod 256) < (ite(0 <= password_binval:5,
                                                 floor((password_binval:5
                                                        / 256)),
                                                 -(floor(-((password_binval:5
                                                            / 256)))))
                                             mod 256))
                            /\ 1 = phi___retres1:47)
                           \/ ((ite(0 <= guess_binval:4,
                                    floor((guess_binval:4 / 256)),
                                    -(floor(-((guess_binval:4 / 256)))))
                                mod 256) <= (ite(0 <= password_binval:5,
                                                 floor((password_binval:5
                                                        / 256)),
                                                 -(floor(-((password_binval:5
                                                            / 256)))))
                                             mod 256)
                                 /\ (ite(0 <= password_binval:5,
                                         floor((password_binval:5 / 256)),
                                         -(floor(-((password_binval:5 / 256)))))
                                     mod 256) <= (ite(0 <= guess_binval:4,
                                                      floor((guess_binval:4
                                                             / 256)),
                                                      -(floor(-((guess_binval:4
                                                                 / 256)))))
                                                  mod 256)
                                 /\ ((((password_binval:5 mod 256) < (
                                       guess_binval:4 mod 256)
                                         \/ (guess_binval:4 mod 256) < (
                                            password_binval:5 mod 256))
                                        /\ 2 = phi___retres1:48)
                                       \/ ((guess_binval:4 mod 256) <= (
                                           password_binval:5 mod 256)
                                             /\ (password_binval:5 mod 256) <= (
                                                guess_binval:4 mod 256)
                                             /\ 3 = phi___retres1:48))
                                 /\ phi___retres1:48 = phi___retres1:47))
                     /\ phi___retres1:47 = phi___retres1:46)))}

    (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,44)_g1>	Base relation: 
{password_binval := havoc:15
 guess_binval := havoc:0
 when (0 <= havoc:0 /\ 0 <= havoc:15 /\ havoc:0 < 16777216
         /\ havoc:15 < 16777216)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x4df9e70: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x51cd3f0: 
	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,44)_g1 , __done )	Base relation: 
{password_binval := havoc:15
 guess_binval := havoc:0
 when (0 <= havoc:0 /\ 0 <= havoc:15 /\ havoc:0 < 16777216
         /\ havoc:15 < 16777216)}

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

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

Base relation: 
{return := phi___retres1:46
 return@pos := type_err:49
 return@width := type_err:50
 when (0 <= guess_binval:4 /\ 0 <= password_binval:5
         /\ ((((ite(0 <= password_binval:5,
                    floor((password_binval:5 / 65536)),
                    -(floor(-((password_binval:5 / 65536)))))
                mod 256) < (ite(0 <= guess_binval:4,
                                floor((guess_binval:4 / 65536)),
                                -(floor(-((guess_binval:4 / 65536)))))
                            mod 256)
                 \/ (ite(0 <= guess_binval:4,
                         floor((guess_binval:4 / 65536)),
                         -(floor(-((guess_binval:4 / 65536)))))
                     mod 256) < (ite(0 <= password_binval:5,
                                     floor((password_binval:5 / 65536)),
                                     -(floor(-((password_binval:5 / 65536)))))
                                 mod 256)) /\ 0 = phi___retres1:46)
               \/ ((ite(0 <= guess_binval:4, floor((guess_binval:4 / 65536)),
                        -(floor(-((guess_binval:4 / 65536)))))
                    mod 256) <= (ite(0 <= password_binval:5,
                                     floor((password_binval:5 / 65536)),
                                     -(floor(-((password_binval:5 / 65536)))))
                                 mod 256)
                     /\ (ite(0 <= password_binval:5,
                             floor((password_binval:5 / 65536)),
                             -(floor(-((password_binval:5 / 65536)))))
                         mod 256) <= (ite(0 <= guess_binval:4,
                                          floor((guess_binval:4 / 65536)),
                                          -(floor(-((guess_binval:4 / 65536)))))
                                      mod 256)
                     /\ ((((ite(0 <= password_binval:5,
                                floor((password_binval:5 / 256)),
                                -(floor(-((password_binval:5 / 256)))))
                            mod 256) < (ite(0 <= guess_binval:4,
                                            floor((guess_binval:4 / 256)),
                                            -(floor(-((guess_binval:4 / 256)))))
                                        mod 256)
                             \/ (ite(0 <= guess_binval:4,
                                     floor((guess_binval:4 / 256)),
                                     -(floor(-((guess_binval:4 / 256)))))
                                 mod 256) < (ite(0 <= password_binval:5,
                                                 floor((password_binval:5
                                                        / 256)),
                                                 -(floor(-((password_binval:5
                                                            / 256)))))
                                             mod 256))
                            /\ 1 = phi___retres1:47)
                           \/ ((ite(0 <= guess_binval:4,
                                    floor((guess_binval:4 / 256)),
                                    -(floor(-((guess_binval:4 / 256)))))
                                mod 256) <= (ite(0 <= password_binval:5,
                                                 floor((password_binval:5
                                                        / 256)),
                                                 -(floor(-((password_binval:5
                                                            / 256)))))
                                             mod 256)
                                 /\ (ite(0 <= password_binval:5,
                                         floor((password_binval:5 / 256)),
                                         -(floor(-((password_binval:5 / 256)))))
                                     mod 256) <= (ite(0 <= guess_binval:4,
                                                      floor((guess_binval:4
                                                             / 256)),
                                                      -(floor(-((guess_binval:4
                                                                 / 256)))))
                                                  mod 256)
                                 /\ ((((password_binval:5 mod 256) < (
                                       guess_binval:4 mod 256)
                                         \/ (guess_binval:4 mod 256) < (
                                            password_binval:5 mod 256))
                                        /\ 2 = phi___retres1:48)
                                       \/ ((guess_binval:4 mod 256) <= (
                                           password_binval:5 mod 256)
                                             /\ (password_binval:5 mod 256) <= (
                                                guess_binval:4 mod 256)
                                             /\ 3 = phi___retres1:48))
                                 /\ phi___retres1:48 = phi___retres1:47))
                     /\ phi___retres1:47 = phi___retres1:46)))}

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

Base relation: 
{result := phi___retres1:143
 password_binval := havoc:15
 guess_binval := havoc:0
 return := havoc:148
 return@pos := type_err:149
 return@width := type_err:150
 when (0 <= havoc:0 /\ 0 <= havoc:15 /\ havoc:0 < 16777216
         /\ havoc:15 < 16777216 /\ 0 <= havoc:0 /\ 0 <= havoc:15
         /\ ((((ite(0 <= havoc:15, floor((havoc:15 / 65536)),
                    -(floor(-((havoc:15 / 65536)))))
                mod 256) < (ite(0 <= havoc:0, floor((havoc:0 / 65536)),
                                -(floor(-((havoc:0 / 65536)))))
                            mod 256)
                 \/ (ite(0 <= havoc:0, floor((havoc:0 / 65536)),
                         -(floor(-((havoc:0 / 65536)))))
                     mod 256) < (ite(0 <= havoc:15,
                                     floor((havoc:15 / 65536)),
                                     -(floor(-((havoc:15 / 65536)))))
                                 mod 256)) /\ 0 = phi___retres1:143)
               \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)),
                        -(floor(-((havoc:0 / 65536)))))
                    mod 256) <= (ite(0 <= havoc:15,
                                     floor((havoc:15 / 65536)),
                                     -(floor(-((havoc:15 / 65536)))))
                                 mod 256)
                     /\ (ite(0 <= havoc:15, floor((havoc:15 / 65536)),
                             -(floor(-((havoc:15 / 65536)))))
                         mod 256) <= (ite(0 <= havoc:0,
                                          floor((havoc:0 / 65536)),
                                          -(floor(-((havoc:0 / 65536)))))
                                      mod 256)
                     /\ ((((ite(0 <= havoc:15, floor((havoc:15 / 256)),
                                -(floor(-((havoc:15 / 256)))))
                            mod 256) < (ite(0 <= havoc:0,
                                            floor((havoc:0 / 256)),
                                            -(floor(-((havoc:0 / 256)))))
                                        mod 256)
                             \/ (ite(0 <= havoc:0, floor((havoc:0 / 256)),
                                     -(floor(-((havoc:0 / 256)))))
                                 mod 256) < (ite(0 <= havoc:15,
                                                 floor((havoc:15 / 256)),
                                                 -(floor(-((havoc:15 / 256)))))
                                             mod 256))
                            /\ 1 = phi___retres1:144)
                           \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)),
                                    -(floor(-((havoc:0 / 256)))))
                                mod 256) <= (ite(0 <= havoc:15,
                                                 floor((havoc:15 / 256)),
                                                 -(floor(-((havoc:15 / 256)))))
                                             mod 256)
                                 /\ (ite(0 <= havoc:15,
                                         floor((havoc:15 / 256)),
                                         -(floor(-((havoc:15 / 256)))))
                                     mod 256) <= (ite(0 <= havoc:0,
                                                      floor((havoc:0 / 256)),
                                                      -(floor(-((havoc:0
                                                                 / 256)))))
                                                  mod 256)
                                 /\ ((((havoc:15 mod 256) < (havoc:0 mod 256)
                                         \/ (havoc:0 mod 256) < (havoc:15
                                                                 mod 256))
                                        /\ 2 = phi___retres1:145)
                                       \/ ((havoc:0 mod 256) <= (havoc:15
                                                                 mod 256)
                                             /\ (havoc:15 mod 256) <= (
                                                havoc:0 mod 256)
                                             /\ 3 = phi___retres1:145))
                                 /\ phi___retres1:145 = phi___retres1:144))
                     /\ phi___retres1:144 = phi___retres1:143)))}

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

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

Variable bounds at line 35 in main

0 <= result
result is o(1)
result <= 3
result is O(1)

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