/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, 48> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 42> -> <Unique State Name, 48>	Base relation: 
{return := phi___retres1:47
 return@pos := type_err:48
 return@width := type_err:49
 when ((((ite(0 <= password_binval:32,
              floor((password_binval:32 / 16777216)),
              -(floor(-((password_binval:32 / 16777216)))))
          mod 256) < (ite(0 <= guess_binval:31,
                          floor((guess_binval:31 / 16777216)),
                          -(floor(-((guess_binval:31 / 16777216)))))
                      mod 256)
           \/ (ite(0 <= guess_binval:31, floor((guess_binval:31 / 16777216)),
                   -(floor(-((guess_binval:31 / 16777216)))))
               mod 256) < (ite(0 <= password_binval:32,
                               floor((password_binval:32 / 16777216)),
                               -(floor(-((password_binval:32 / 16777216)))))
                           mod 256)) /\ 0 = phi___retres1:47)
         \/ ((ite(0 <= guess_binval:31, floor((guess_binval:31 / 16777216)),
                  -(floor(-((guess_binval:31 / 16777216)))))
              mod 256) <= (ite(0 <= password_binval:32,
                               floor((password_binval:32 / 16777216)),
                               -(floor(-((password_binval:32 / 16777216)))))
                           mod 256)
               /\ (ite(0 <= password_binval:32,
                       floor((password_binval:32 / 16777216)),
                       -(floor(-((password_binval:32 / 16777216)))))
                   mod 256) <= (ite(0 <= guess_binval:31,
                                    floor((guess_binval:31 / 16777216)),
                                    -(floor(-((guess_binval:31 / 16777216)))))
                                mod 256)
               /\ ((((ite(0 <= password_binval:32,
                          floor((password_binval:32 / 65536)),
                          -(floor(-((password_binval:32 / 65536)))))
                      mod 256) < (ite(0 <= guess_binval:31,
                                      floor((guess_binval:31 / 65536)),
                                      -(floor(-((guess_binval:31 / 65536)))))
                                  mod 256)
                       \/ (ite(0 <= guess_binval:31,
                               floor((guess_binval:31 / 65536)),
                               -(floor(-((guess_binval:31 / 65536)))))
                           mod 256) < (ite(0 <= password_binval:32,
                                           floor((password_binval:32 / 65536)),
                                           -(floor(-((password_binval:32
                                                      / 65536)))))
                                       mod 256)) /\ 1 = phi___retres1:44)
                     \/ ((ite(0 <= guess_binval:31,
                              floor((guess_binval:31 / 65536)),
                              -(floor(-((guess_binval:31 / 65536)))))
                          mod 256) <= (ite(0 <= password_binval:32,
                                           floor((password_binval:32 / 65536)),
                                           -(floor(-((password_binval:32
                                                      / 65536)))))
                                       mod 256)
                           /\ (ite(0 <= password_binval:32,
                                   floor((password_binval:32 / 65536)),
                                   -(floor(-((password_binval:32 / 65536)))))
                               mod 256) <= (ite(0 <= guess_binval:31,
                                                floor((guess_binval:31
                                                       / 65536)),
                                                -(floor(-((guess_binval:31
                                                           / 65536)))))
                                            mod 256)
                           /\ ((((ite(0 <= password_binval:32,
                                      floor((password_binval:32 / 256)),
                                      -(floor(-((password_binval:32 / 256)))))
                                  mod 256) < (ite(0 <= guess_binval:31,
                                                  floor((guess_binval:31
                                                         / 256)),
                                                  -(floor(-((guess_binval:31
                                                             / 256)))))
                                              mod 256)
                                   \/ (ite(0 <= guess_binval:31,
                                           floor((guess_binval:31 / 256)),
                                           -(floor(-((guess_binval:31 / 256)))))
                                       mod 256) < (ite(0 <= password_binval:32,
                                                       floor((password_binval:32
                                                              / 256)),
                                                       -(floor(-((password_binval:32
                                                                  / 256)))))
                                                   mod 256))
                                  /\ 2 = phi___retres1:45)
                                 \/ ((ite(0 <= guess_binval:31,
                                          floor((guess_binval:31 / 256)),
                                          -(floor(-((guess_binval:31 / 256)))))
                                      mod 256) <= (ite(0 <= password_binval:32,
                                                       floor((password_binval:32
                                                              / 256)),
                                                       -(floor(-((password_binval:32
                                                                  / 256)))))
                                                   mod 256)
                                       /\ (ite(0 <= password_binval:32,
                                               floor((password_binval:32
                                                      / 256)),
                                               -(floor(-((password_binval:32
                                                          / 256)))))
                                           mod 256) <= (ite(0 <= guess_binval:31,
                                                            floor((guess_binval:31
                                                                   / 256)),
                                                            -(floor(-(
                                                                    (
                                                                    guess_binval:31
                                                                    / 256)))))
                                                        mod 256)
                                       /\ ((((password_binval:32 mod 256) < (
                                             guess_binval:31 mod 256)
                                               \/ (guess_binval:31 mod 256) < (
                                                  password_binval:32 mod 256))
                                              /\ 3 = phi___retres1:46)
                                             \/ ((guess_binval:31 mod 256) <= (
                                                 password_binval:32 mod 256)
                                                   /\ (password_binval:32
                                                       mod 256) <= (guess_binval:31
                                                                    mod 256)
                                                   /\ 4 = phi___retres1:46))
                                       /\ phi___retres1:46 = phi___retres1:45))
                           /\ phi___retres1:45 = phi___retres1:44))
               /\ phi___retres1:44 = phi___retres1:47))}	
<Unique State Name, 46> -> <Unique State Name, 45>	Base relation: 
{password_binval := param1:15
 guess_binval := param0:12}	
<Unique State Name, 49> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 44> -> <Unique State Name, 49>	Base relation: 
{result := return:9
 return := 0
 return@pos := type_err:16
 return@width := type_err:17}	
<Unique State Name, 45> -> <Unique State Name, 42 44>	Base relation: 
{}	MergeFn[Base relation: 
{}]
#################################################################
           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  9  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {password_binval := param1:15
       guess_binval := param0:12}    )
    ,
    Var(9)
  )
  ,
  Weight(Base relation: 
    {result := return:9
     return := 0
     return@pos := type_err:16
     return@width := type_err:17}  )
)


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



Performing Gaussian Elimination.


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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {password_binval := param1:15
         guess_binval := param0:12}      )
      ,
      Var(9)
    )
    ,
    Weight(Base relation: 
      {result := return:9
       return := 0
       return@pos := type_err:16
       return@width := type_err:17}    )
  )
)



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

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



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {result := phi___retres1:63
   password_binval := param1:15
   guess_binval := param0:12
   return := 0
   return@pos := type_err:69
   return@width := type_err:70
   when ((((ite(0 <= param1:15, floor((param1:15 / 16777216)),
                -(floor(-((param1:15 / 16777216)))))
            mod 256) < (ite(0 <= param0:12, floor((param0:12 / 16777216)),
                            -(floor(-((param0:12 / 16777216)))))
                        mod 256)
             \/ (ite(0 <= param0:12, floor((param0:12 / 16777216)),
                     -(floor(-((param0:12 / 16777216)))))
                 mod 256) < (ite(0 <= param1:15,
                                 floor((param1:15 / 16777216)),
                                 -(floor(-((param1:15 / 16777216)))))
                             mod 256)) /\ 0 = phi___retres1:63)
           \/ ((ite(0 <= param0:12, floor((param0:12 / 16777216)),
                    -(floor(-((param0:12 / 16777216)))))
                mod 256) <= (ite(0 <= param1:15,
                                 floor((param1:15 / 16777216)),
                                 -(floor(-((param1:15 / 16777216)))))
                             mod 256)
                 /\ (ite(0 <= param1:15, floor((param1:15 / 16777216)),
                         -(floor(-((param1:15 / 16777216)))))
                     mod 256) <= (ite(0 <= param0:12,
                                      floor((param0:12 / 16777216)),
                                      -(floor(-((param0:12 / 16777216)))))
                                  mod 256)
                 /\ ((((ite(0 <= param1:15, floor((param1:15 / 65536)),
                            -(floor(-((param1:15 / 65536)))))
                        mod 256) < (ite(0 <= param0:12,
                                        floor((param0:12 / 65536)),
                                        -(floor(-((param0:12 / 65536)))))
                                    mod 256)
                         \/ (ite(0 <= param0:12, floor((param0:12 / 65536)),
                                 -(floor(-((param0:12 / 65536)))))
                             mod 256) < (ite(0 <= param1:15,
                                             floor((param1:15 / 65536)),
                                             -(floor(-((param1:15 / 65536)))))
                                         mod 256)) /\ 1 = phi___retres1:64)
                       \/ ((ite(0 <= param0:12, floor((param0:12 / 65536)),
                                -(floor(-((param0:12 / 65536)))))
                            mod 256) <= (ite(0 <= param1:15,
                                             floor((param1:15 / 65536)),
                                             -(floor(-((param1:15 / 65536)))))
                                         mod 256)
                             /\ (ite(0 <= param1:15,
                                     floor((param1:15 / 65536)),
                                     -(floor(-((param1:15 / 65536)))))
                                 mod 256) <= (ite(0 <= param0:12,
                                                  floor((param0:12 / 65536)),
                                                  -(floor(-((param0:12
                                                             / 65536)))))
                                              mod 256)
                             /\ ((((ite(0 <= param1:15,
                                        floor((param1:15 / 256)),
                                        -(floor(-((param1:15 / 256)))))
                                    mod 256) < (ite(0 <= param0:12,
                                                    floor((param0:12 / 256)),
                                                    -(floor(-((param0:12
                                                               / 256)))))
                                                mod 256)
                                     \/ (ite(0 <= param0:12,
                                             floor((param0:12 / 256)),
                                             -(floor(-((param0:12 / 256)))))
                                         mod 256) < (ite(0 <= param1:15,
                                                         floor((param1:15
                                                                / 256)),
                                                         -(floor(-((param1:15
                                                                    / 256)))))
                                                     mod 256))
                                    /\ 2 = phi___retres1:65)
                                   \/ ((ite(0 <= param0:12,
                                            floor((param0:12 / 256)),
                                            -(floor(-((param0:12 / 256)))))
                                        mod 256) <= (ite(0 <= param1:15,
                                                         floor((param1:15
                                                                / 256)),
                                                         -(floor(-((param1:15
                                                                    / 256)))))
                                                     mod 256)
                                         /\ (ite(0 <= param1:15,
                                                 floor((param1:15 / 256)),
                                                 -(floor(-((param1:15 / 256)))))
                                             mod 256) <= (ite(0 <= param0:12,
                                                              floor((
                                                                    param0:12
                                                                    / 256)),
                                                              -(floor(
                                                                -((param0:12
                                                                   / 256)))))
                                                          mod 256)
                                         /\ ((((param1:15 mod 256) < (
                                               param0:12 mod 256)
                                                 \/ (param0:12 mod 256) < (
                                                    param1:15 mod 256))
                                                /\ 3 = phi___retres1:66)
                                               \/ ((param0:12 mod 256) <= (
                                                   param1:15 mod 256)
                                                     /\ (param1:15 mod 256) <= (
                                                        param0:12 mod 256)
                                                     /\ 4 = phi___retres1:66))
                                         /\ phi___retres1:66 = phi___retres1:65))
                             /\ phi___retres1:65 = phi___retres1:64))
                 /\ phi___retres1:64 = phi___retres1:63))})


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


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

  The IRE-evaluated value on this round is: 

Base relation: 
{result := phi___retres1:63
 password_binval := param1:15
 guess_binval := param0:12
 return := 0
 return@pos := type_err:69
 return@width := type_err:70
 when ((((ite(0 <= param1:15, floor((param1:15 / 16777216)),
              -(floor(-((param1:15 / 16777216)))))
          mod 256) < (ite(0 <= param0:12, floor((param0:12 / 16777216)),
                          -(floor(-((param0:12 / 16777216)))))
                      mod 256)
           \/ (ite(0 <= param0:12, floor((param0:12 / 16777216)),
                   -(floor(-((param0:12 / 16777216)))))
               mod 256) < (ite(0 <= param1:15, floor((param1:15 / 16777216)),
                               -(floor(-((param1:15 / 16777216)))))
                           mod 256)) /\ 0 = phi___retres1:63)
         \/ ((ite(0 <= param0:12, floor((param0:12 / 16777216)),
                  -(floor(-((param0:12 / 16777216)))))
              mod 256) <= (ite(0 <= param1:15, floor((param1:15 / 16777216)),
                               -(floor(-((param1:15 / 16777216)))))
                           mod 256)
               /\ (ite(0 <= param1:15, floor((param1:15 / 16777216)),
                       -(floor(-((param1:15 / 16777216)))))
                   mod 256) <= (ite(0 <= param0:12,
                                    floor((param0:12 / 16777216)),
                                    -(floor(-((param0:12 / 16777216)))))
                                mod 256)
               /\ ((((ite(0 <= param1:15, floor((param1:15 / 65536)),
                          -(floor(-((param1:15 / 65536)))))
                      mod 256) < (ite(0 <= param0:12,
                                      floor((param0:12 / 65536)),
                                      -(floor(-((param0:12 / 65536)))))
                                  mod 256)
                       \/ (ite(0 <= param0:12, floor((param0:12 / 65536)),
                               -(floor(-((param0:12 / 65536)))))
                           mod 256) < (ite(0 <= param1:15,
                                           floor((param1:15 / 65536)),
                                           -(floor(-((param1:15 / 65536)))))
                                       mod 256)) /\ 1 = phi___retres1:64)
                     \/ ((ite(0 <= param0:12, floor((param0:12 / 65536)),
                              -(floor(-((param0:12 / 65536)))))
                          mod 256) <= (ite(0 <= param1:15,
                                           floor((param1:15 / 65536)),
                                           -(floor(-((param1:15 / 65536)))))
                                       mod 256)
                           /\ (ite(0 <= param1:15,
                                   floor((param1:15 / 65536)),
                                   -(floor(-((param1:15 / 65536)))))
                               mod 256) <= (ite(0 <= param0:12,
                                                floor((param0:12 / 65536)),
                                                -(floor(-((param0:12 / 65536)))))
                                            mod 256)
                           /\ ((((ite(0 <= param1:15,
                                      floor((param1:15 / 256)),
                                      -(floor(-((param1:15 / 256)))))
                                  mod 256) < (ite(0 <= param0:12,
                                                  floor((param0:12 / 256)),
                                                  -(floor(-((param0:12 / 256)))))
                                              mod 256)
                                   \/ (ite(0 <= param0:12,
                                           floor((param0:12 / 256)),
                                           -(floor(-((param0:12 / 256)))))
                                       mod 256) < (ite(0 <= param1:15,
                                                       floor((param1:15 / 256)),
                                                       -(floor(-((param1:15
                                                                  / 256)))))
                                                   mod 256))
                                  /\ 2 = phi___retres1:65)
                                 \/ ((ite(0 <= param0:12,
                                          floor((param0:12 / 256)),
                                          -(floor(-((param0:12 / 256)))))
                                      mod 256) <= (ite(0 <= param1:15,
                                                       floor((param1:15 / 256)),
                                                       -(floor(-((param1:15
                                                                  / 256)))))
                                                   mod 256)
                                       /\ (ite(0 <= param1:15,
                                               floor((param1:15 / 256)),
                                               -(floor(-((param1:15 / 256)))))
                                           mod 256) <= (ite(0 <= param0:12,
                                                            floor((param0:12
                                                                   / 256)),
                                                            -(floor(-(
                                                                    (
                                                                    param0:12
                                                                    / 256)))))
                                                        mod 256)
                                       /\ ((((param1:15 mod 256) < (param0:12
                                                                    mod 256)
                                               \/ (param0:12 mod 256) < (
                                                  param1:15 mod 256))
                                              /\ 3 = phi___retres1:66)
                                             \/ ((param0:12 mod 256) <= (
                                                 param1:15 mod 256)
                                                   /\ (param1:15 mod 256) <= (
                                                      param0:12 mod 256)
                                                   /\ 4 = phi___retres1:66))
                                       /\ phi___retres1:66 = phi___retres1:65))
                           /\ phi___retres1:65 = phi___retres1:64))
               /\ phi___retres1:64 = phi___retres1:63))}

Evaluating variable number 9 (using IRE) 

  The IRE-evaluated value on this round is: 

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

    (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,42)_g1>	Base relation: 
{password_binval := param1:15
 guess_binval := param0:12}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x2164e90: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x2164820: 
	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,42)_g1 , __done )	Base relation: 
{password_binval := param1:15
 guess_binval := param0:12}

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

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

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

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

Base relation: 
{result := phi___retres1:71
 password_binval := param1:15
 guess_binval := param0:12
 return := 0
 return@pos := type_err:77
 return@width := type_err:78
 when ((((ite(0 <= param1:15, floor((param1:15 / 16777216)),
              -(floor(-((param1:15 / 16777216)))))
          mod 256) < (ite(0 <= param0:12, floor((param0:12 / 16777216)),
                          -(floor(-((param0:12 / 16777216)))))
                      mod 256)
           \/ (ite(0 <= param0:12, floor((param0:12 / 16777216)),
                   -(floor(-((param0:12 / 16777216)))))
               mod 256) < (ite(0 <= param1:15, floor((param1:15 / 16777216)),
                               -(floor(-((param1:15 / 16777216)))))
                           mod 256)) /\ 0 = phi___retres1:71)
         \/ ((ite(0 <= param0:12, floor((param0:12 / 16777216)),
                  -(floor(-((param0:12 / 16777216)))))
              mod 256) <= (ite(0 <= param1:15, floor((param1:15 / 16777216)),
                               -(floor(-((param1:15 / 16777216)))))
                           mod 256)
               /\ (ite(0 <= param1:15, floor((param1:15 / 16777216)),
                       -(floor(-((param1:15 / 16777216)))))
                   mod 256) <= (ite(0 <= param0:12,
                                    floor((param0:12 / 16777216)),
                                    -(floor(-((param0:12 / 16777216)))))
                                mod 256)
               /\ ((((ite(0 <= param1:15, floor((param1:15 / 65536)),
                          -(floor(-((param1:15 / 65536)))))
                      mod 256) < (ite(0 <= param0:12,
                                      floor((param0:12 / 65536)),
                                      -(floor(-((param0:12 / 65536)))))
                                  mod 256)
                       \/ (ite(0 <= param0:12, floor((param0:12 / 65536)),
                               -(floor(-((param0:12 / 65536)))))
                           mod 256) < (ite(0 <= param1:15,
                                           floor((param1:15 / 65536)),
                                           -(floor(-((param1:15 / 65536)))))
                                       mod 256)) /\ 1 = phi___retres1:72)
                     \/ ((ite(0 <= param0:12, floor((param0:12 / 65536)),
                              -(floor(-((param0:12 / 65536)))))
                          mod 256) <= (ite(0 <= param1:15,
                                           floor((param1:15 / 65536)),
                                           -(floor(-((param1:15 / 65536)))))
                                       mod 256)
                           /\ (ite(0 <= param1:15,
                                   floor((param1:15 / 65536)),
                                   -(floor(-((param1:15 / 65536)))))
                               mod 256) <= (ite(0 <= param0:12,
                                                floor((param0:12 / 65536)),
                                                -(floor(-((param0:12 / 65536)))))
                                            mod 256)
                           /\ ((((ite(0 <= param1:15,
                                      floor((param1:15 / 256)),
                                      -(floor(-((param1:15 / 256)))))
                                  mod 256) < (ite(0 <= param0:12,
                                                  floor((param0:12 / 256)),
                                                  -(floor(-((param0:12 / 256)))))
                                              mod 256)
                                   \/ (ite(0 <= param0:12,
                                           floor((param0:12 / 256)),
                                           -(floor(-((param0:12 / 256)))))
                                       mod 256) < (ite(0 <= param1:15,
                                                       floor((param1:15 / 256)),
                                                       -(floor(-((param1:15
                                                                  / 256)))))
                                                   mod 256))
                                  /\ 2 = phi___retres1:73)
                                 \/ ((ite(0 <= param0:12,
                                          floor((param0:12 / 256)),
                                          -(floor(-((param0:12 / 256)))))
                                      mod 256) <= (ite(0 <= param1:15,
                                                       floor((param1:15 / 256)),
                                                       -(floor(-((param1:15
                                                                  / 256)))))
                                                   mod 256)
                                       /\ (ite(0 <= param1:15,
                                               floor((param1:15 / 256)),
                                               -(floor(-((param1:15 / 256)))))
                                           mod 256) <= (ite(0 <= param0:12,
                                                            floor((param0:12
                                                                   / 256)),
                                                            -(floor(-(
                                                                    (
                                                                    param0:12
                                                                    / 256)))))
                                                        mod 256)
                                       /\ ((((param1:15 mod 256) < (param0:12
                                                                    mod 256)
                                               \/ (param0:12 mod 256) < (
                                                  param1:15 mod 256))
                                              /\ 3 = phi___retres1:74)
                                             \/ ((param0:12 mod 256) <= (
                                                 param1:15 mod 256)
                                                   /\ (param1:15 mod 256) <= (
                                                      param0:12 mod 256)
                                                   /\ 4 = phi___retres1:74))
                                       /\ phi___retres1:74 = phi___retres1:73))
                           /\ phi___retres1:73 = phi___retres1:72))
               /\ phi___retres1:72 = phi___retres1:71))}

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

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

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