/bat0/stac/Code/icra/WALi-OpenNWA/../icra -cra_newton_basic -cra-split-loops Passing command-line option -cra-split-loops to duet. -> Base relation: {} -> Base relation: {result2 := return:30 password_binval := password_binval3:13} -> Base relation: {} MergeFn[Base relation: {}] -> Base relation: {} MergeFn[Base relation: {}] -> Base relation: {result4 := return:30 when (result1:19 < result2:20 /\ result2:20 < result3:21 /\ result3:21 < return:30)} -> Base relation: {result1 := return:30 password_binval := password_binval2:12} -> Base relation: {} MergeFn[Base relation: {}] -> Base relation: {result3 := return:30 password_binval := password_binval4:14} -> Base relation: {} -> Base relation: {password_binval4 := havoc:34 password_binval3 := havoc:33 password_binval2 := havoc:32 password_binval1 := havoc:31 password_binval := havoc:31 guess_binval := havoc:0 when (0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216)} -> Base relation: {return := phi___retres1:102 return@pos := type_err:105 return@width := type_err:106 when (0 <= guess_binval:2 /\ 0 <= password_binval:88 /\ ((((ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) < (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) \/ (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) < (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256)) /\ 0 = phi___retres1:102) \/ ((ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) <= (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) /\ (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) <= (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) /\ ((((ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) < (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) \/ (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) < (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256)) /\ 1 = phi___retres1:103) \/ ((ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) <= (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) /\ (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) <= (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) /\ ((((password_binval:88 mod 256) < ( guess_binval:2 mod 256) \/ (guess_binval:2 mod 256) < ( password_binval:88 mod 256)) /\ 2 = phi___retres1:104) \/ ((guess_binval:2 mod 256) <= ( password_binval:88 mod 256) /\ (password_binval:88 mod 256) <= ( guess_binval:2 mod 256) /\ 3 = phi___retres1:104)) /\ phi___retres1:104 = phi___retres1:103)) /\ phi___retres1:103 = phi___retres1:102)))} -> Base relation: {return := 0 return@pos := type_err:35 return@width := type_err:36} -> 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: 16 19 New-style (IRE) regular expression in IREregExpMap for reID=16: Dot( Dot( Dot( Dot( Dot( Dot( Dot( Dot( Weight(Base relation: {password_binval4 := havoc:34 password_binval3 := havoc:33 password_binval2 := havoc:32 password_binval1 := havoc:31 password_binval := havoc:31 guess_binval := havoc:0 when (0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216)} ) , Var(19) ) , Weight(Base relation: {result1 := return:30 password_binval := password_binval2:12} ) ) , Var(19) ) , Weight(Base relation: {result2 := return:30 password_binval := password_binval3:13} ) ) , Var(19) ) , Weight(Base relation: {result3 := return:30 password_binval := password_binval4:14} ) ) , Var(19) ) , Weight(Base relation: {result4 := return:30 return := 0 return@pos := type_err:120 return@width := type_err:121 when (result1:19 < result2:20 /\ result2:20 < result3:21 /\ result3:21 < return:30)} ) ) New-style (IRE) regular expression in IREregExpMap for reID=19: Weight(Base relation: {return := phi___retres1:102 return@pos := type_err:105 return@width := type_err:106 when (0 <= guess_binval:2 /\ 0 <= password_binval:88 /\ ((((ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) < (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) \/ (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) < (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256)) /\ 0 = phi___retres1:102) \/ ((ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) <= (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) /\ (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) <= (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) /\ ((((ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) < (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) \/ (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) < (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256)) /\ 1 = phi___retres1:103) \/ ((ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) <= (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) /\ (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) <= (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) /\ ((((password_binval:88 mod 256) < ( guess_binval:2 mod 256) \/ (guess_binval:2 mod 256) < ( password_binval:88 mod 256)) /\ 2 = phi___retres1:104) \/ ((guess_binval:2 mod 256) <= ( password_binval:88 mod 256) /\ (password_binval:88 mod 256) <= ( guess_binval:2 mod 256) /\ 3 = phi___retres1:104)) /\ phi___retres1:104 = phi___retres1:103)) /\ phi___retres1:103 = phi___retres1:102)))}) Performing Gaussian Elimination. ------------------------------ Working on variable 16 New-style (IRE) regular expression for 16 just before isolating it: Project( Dot( Dot( Dot( Dot( Dot( Dot( Dot( Dot( Weight(Base relation: {password_binval4 := havoc:34 password_binval3 := havoc:33 password_binval2 := havoc:32 password_binval1 := havoc:31 password_binval := havoc:31 guess_binval := havoc:0 when (0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216)} ) , Var(19) ) , Weight(Base relation: {result1 := return:30 password_binval := password_binval2:12} ) ) , Var(19) ) , Weight(Base relation: {result2 := return:30 password_binval := password_binval3:13} ) ) , Var(19) ) , Weight(Base relation: {result3 := return:30 password_binval := password_binval4:14} ) ) , Var(19) ) , Weight(Base relation: {result4 := return:30 return := 0 return@pos := type_err:120 return@width := type_err:121 when (result1:19 < result2:20 /\ result2:20 < result3:21 /\ result3:21 < return:30)} ) ) ) ------------------------------ Working on variable 19 New-style (IRE) regular expression for 19 just before isolating it: Weight(Base relation: {return := phi___retres1:102 return@pos := type_err:105 return@width := type_err:106 when (0 <= guess_binval:2 /\ 0 <= password_binval:88 /\ ((((ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) < (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) \/ (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) < (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256)) /\ 0 = phi___retres1:102) \/ ((ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) <= (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) /\ (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) <= (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) /\ ((((ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) < (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) \/ (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) < (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256)) /\ 1 = phi___retres1:103) \/ ((ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) <= (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) /\ (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) <= (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) /\ ((((password_binval:88 mod 256) < ( guess_binval:2 mod 256) \/ (guess_binval:2 mod 256) < ( password_binval:88 mod 256)) /\ 2 = phi___retres1:104) \/ ((guess_binval:2 mod 256) <= ( password_binval:88 mod 256) /\ (password_binval:88 mod 256) <= ( guess_binval:2 mod 256) /\ 3 = phi___retres1:104)) /\ phi___retres1:104 = phi___retres1:103)) /\ phi___retres1:103 = phi___retres1:102)))}) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Finished Gaussian Elimination. New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=16: Weight(Base relation: {result4 := phi___retres1:137 password_binval4 := havoc:34 result3 := phi___retres1:132 password_binval3 := havoc:33 result2 := phi___retres1:127 password_binval2 := havoc:32 result1 := phi___retres1:122 password_binval1 := havoc:31 password_binval := havoc:34 guess_binval := havoc:0 return := 0 return@pos := type_err:142 return@width := type_err:143 when (0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216 /\ 0 <= havoc:0 /\ 0 <= havoc:31 /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256)) /\ 0 = phi___retres1:122) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256)) /\ 1 = phi___retres1:123) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) /\ ((((havoc:31 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < (havoc:31 mod 256)) /\ 2 = phi___retres1:124) \/ ((havoc:0 mod 256) <= (havoc:31 mod 256) /\ (havoc:31 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:124)) /\ phi___retres1:124 = phi___retres1:123)) /\ phi___retres1:123 = phi___retres1:122)) /\ 0 <= havoc:0 /\ 0 <= havoc:32 /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256)) /\ 0 = phi___retres1:127) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256)) /\ 1 = phi___retres1:128) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) /\ ((((havoc:32 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < (havoc:32 mod 256)) /\ 2 = phi___retres1:129) \/ ((havoc:0 mod 256) <= (havoc:32 mod 256) /\ (havoc:32 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:129)) /\ phi___retres1:129 = phi___retres1:128)) /\ phi___retres1:128 = phi___retres1:127)) /\ 0 <= havoc:0 /\ 0 <= havoc:33 /\ ((((ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 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:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256)) /\ 0 = phi___retres1:132) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256) /\ (ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 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:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256)) /\ 1 = phi___retres1:133) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256) /\ (ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) /\ ((((havoc:33 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < (havoc:33 mod 256)) /\ 2 = phi___retres1:134) \/ ((havoc:0 mod 256) <= (havoc:33 mod 256) /\ (havoc:33 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:134)) /\ phi___retres1:134 = phi___retres1:133)) /\ phi___retres1:133 = phi___retres1:132)) /\ 0 <= havoc:0 /\ 0 <= havoc:34 /\ ((((ite(0 <= havoc:34, floor((havoc:34 / 65536)), -(floor(-((havoc:34 / 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:34, floor((havoc:34 / 65536)), -(floor(-((havoc:34 / 65536))))) mod 256)) /\ 0 = phi___retres1:137) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:34, floor((havoc:34 / 65536)), -(floor(-((havoc:34 / 65536))))) mod 256) /\ (ite(0 <= havoc:34, floor((havoc:34 / 65536)), -(floor(-((havoc:34 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:34, floor((havoc:34 / 256)), -(floor(-((havoc:34 / 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:34, floor((havoc:34 / 256)), -(floor(-((havoc:34 / 256))))) mod 256)) /\ 1 = phi___retres1:138) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:34, floor((havoc:34 / 256)), -(floor(-((havoc:34 / 256))))) mod 256) /\ (ite(0 <= havoc:34, floor((havoc:34 / 256)), -(floor(-((havoc:34 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) /\ ((((havoc:34 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < (havoc:34 mod 256)) /\ 2 = phi___retres1:139) \/ ((havoc:0 mod 256) <= (havoc:34 mod 256) /\ (havoc:34 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:139)) /\ phi___retres1:139 = phi___retres1:138)) /\ phi___retres1:138 = phi___retres1:137)) /\ phi___retres1:122 < phi___retres1:127 /\ phi___retres1:127 < phi___retres1:132 /\ phi___retres1:132 < phi___retres1:137)}) New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=19: Weight(Base relation: {return := phi___retres1:102 return@pos := type_err:105 return@width := type_err:106 when (0 <= guess_binval:2 /\ 0 <= password_binval:88 /\ ((((ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) < (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) \/ (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) < (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256)) /\ 0 = phi___retres1:102) \/ ((ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) <= (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) /\ (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) <= (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) /\ ((((ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) < (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) \/ (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) < (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256)) /\ 1 = phi___retres1:103) \/ ((ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) <= (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) /\ (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) <= (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) /\ ((((password_binval:88 mod 256) < ( guess_binval:2 mod 256) \/ (guess_binval:2 mod 256) < ( password_binval:88 mod 256)) /\ 2 = phi___retres1:104) \/ ((guess_binval:2 mod 256) <= ( password_binval:88 mod 256) /\ (password_binval:88 mod 256) <= ( guess_binval:2 mod 256) /\ 3 = phi___retres1:104)) /\ phi___retres1:104 = phi___retres1:103)) /\ phi___retres1:103 = phi___retres1:102)))}) Step 5: ========================================================= [Newton] Running Newton ------------------------------------------------------------------------------- Round 0: Evaluating variable number 16 (using IRE) The IRE-evaluated value on this round is: Base relation: {result4 := phi___retres1:137 password_binval4 := havoc:34 result3 := phi___retres1:132 password_binval3 := havoc:33 result2 := phi___retres1:127 password_binval2 := havoc:32 result1 := phi___retres1:122 password_binval1 := havoc:31 password_binval := havoc:34 guess_binval := havoc:0 return := 0 return@pos := type_err:142 return@width := type_err:143 when (0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216 /\ 0 <= havoc:0 /\ 0 <= havoc:31 /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256)) /\ 0 = phi___retres1:122) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256)) /\ 1 = phi___retres1:123) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) /\ ((((havoc:31 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < (havoc:31 mod 256)) /\ 2 = phi___retres1:124) \/ ((havoc:0 mod 256) <= (havoc:31 mod 256) /\ (havoc:31 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:124)) /\ phi___retres1:124 = phi___retres1:123)) /\ phi___retres1:123 = phi___retres1:122)) /\ 0 <= havoc:0 /\ 0 <= havoc:32 /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256)) /\ 0 = phi___retres1:127) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256)) /\ 1 = phi___retres1:128) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) /\ ((((havoc:32 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < (havoc:32 mod 256)) /\ 2 = phi___retres1:129) \/ ((havoc:0 mod 256) <= (havoc:32 mod 256) /\ (havoc:32 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:129)) /\ phi___retres1:129 = phi___retres1:128)) /\ phi___retres1:128 = phi___retres1:127)) /\ 0 <= havoc:0 /\ 0 <= havoc:33 /\ ((((ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 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:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256)) /\ 0 = phi___retres1:132) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256) /\ (ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 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:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256)) /\ 1 = phi___retres1:133) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256) /\ (ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) /\ ((((havoc:33 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < (havoc:33 mod 256)) /\ 2 = phi___retres1:134) \/ ((havoc:0 mod 256) <= (havoc:33 mod 256) /\ (havoc:33 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:134)) /\ phi___retres1:134 = phi___retres1:133)) /\ phi___retres1:133 = phi___retres1:132)) /\ 0 <= havoc:0 /\ 0 <= havoc:34 /\ ((((ite(0 <= havoc:34, floor((havoc:34 / 65536)), -(floor(-((havoc:34 / 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:34, floor((havoc:34 / 65536)), -(floor(-((havoc:34 / 65536))))) mod 256)) /\ 0 = phi___retres1:137) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:34, floor((havoc:34 / 65536)), -(floor(-((havoc:34 / 65536))))) mod 256) /\ (ite(0 <= havoc:34, floor((havoc:34 / 65536)), -(floor(-((havoc:34 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:34, floor((havoc:34 / 256)), -(floor(-((havoc:34 / 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:34, floor((havoc:34 / 256)), -(floor(-((havoc:34 / 256))))) mod 256)) /\ 1 = phi___retres1:138) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:34, floor((havoc:34 / 256)), -(floor(-((havoc:34 / 256))))) mod 256) /\ (ite(0 <= havoc:34, floor((havoc:34 / 256)), -(floor(-((havoc:34 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) /\ ((((havoc:34 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < (havoc:34 mod 256)) /\ 2 = phi___retres1:139) \/ ((havoc:0 mod 256) <= (havoc:34 mod 256) /\ (havoc:34 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:139)) /\ phi___retres1:139 = phi___retres1:138)) /\ phi___retres1:138 = phi___retres1:137)) /\ phi___retres1:122 < phi___retres1:127 /\ phi___retres1:127 < phi___retres1:132 /\ phi___retres1:132 < phi___retres1:137)} Evaluating variable number 19 (using IRE) The IRE-evaluated value on this round is: Base relation: {return := phi___retres1:102 return@pos := type_err:105 return@width := type_err:106 when (0 <= guess_binval:2 /\ 0 <= password_binval:88 /\ ((((ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) < (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) \/ (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) < (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256)) /\ 0 = phi___retres1:102) \/ ((ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) <= (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) /\ (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) <= (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) /\ ((((ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) < (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) \/ (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) < (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256)) /\ 1 = phi___retres1:103) \/ ((ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) <= (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) /\ (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) <= (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) /\ ((((password_binval:88 mod 256) < ( guess_binval:2 mod 256) \/ (guess_binval:2 mod 256) < ( password_binval:88 mod 256)) /\ 2 = phi___retres1:104) \/ ((guess_binval:2 mod 256) <= ( password_binval:88 mod 256) /\ (password_binval:88 mod 256) <= ( guess_binval:2 mod 256) /\ 3 = phi___retres1:104)) /\ phi___retres1:104 = phi___retres1:103)) /\ phi___retres1:103 = phi___retres1:102)))} (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,69)_g1> Base relation: {password_binval4 := havoc:34 result3 := phi_result3:184 password_binval3 := havoc:33 result2 := phi_result2:183 password_binval2 := havoc:32 result1 := phi_result1:182 password_binval1 := havoc:31 password_binval := phi_password_binval:181 guess_binval := havoc:0 return := phi_return:180 return@pos := phi_return@pos:179 return@width := phi_return@width:178 when ((((((0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216 /\ result1:19 = phi_result1:170 /\ havoc:31 = phi_password_binval:169 /\ return:30 = phi_return:168 /\ return@pos:29 = phi_return@pos:167 /\ return@width:28 = phi_return@width:166) \/ (0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216 /\ 0 <= havoc:0 /\ 0 <= havoc:31 /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256)) /\ 0 = phi___retres1:144) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 256)), -(floor(-( (havoc:31 / 256))))) mod 256)) /\ 1 = phi___retres1:145) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-( (havoc:31 / 256))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor( (havoc:0 / 256)), -(floor( -(( havoc:0 / 256))))) mod 256) /\ ((((havoc:31 mod 256) < ( havoc:0 mod 256) \/ (havoc:0 mod 256) < ( havoc:31 mod 256)) /\ 2 = phi___retres1:146) \/ ((havoc:0 mod 256) <= ( havoc:31 mod 256) /\ (havoc:31 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:146)) /\ phi___retres1:146 = phi___retres1:145)) /\ phi___retres1:145 = phi___retres1:144)) /\ phi___retres1:144 = phi_result1:170 /\ havoc:32 = phi_password_binval:169 /\ phi___retres1:144 = phi_return:168 /\ type_err:147 = phi_return@pos:167 /\ type_err:148 = phi_return@width:166)) /\ result3:21 = phi_result3:177 /\ result2:20 = phi_result2:176 /\ phi_result1:170 = phi_result1:175 /\ phi_password_binval:169 = phi_password_binval:174 /\ phi_return:168 = phi_return:173 /\ phi_return@pos:167 = phi_return@pos:172 /\ phi_return@width:166 = phi_return@width:171) \/ (0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216 /\ 0 <= havoc:0 /\ 0 <= havoc:31 /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256)) /\ 0 = phi___retres1:144) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256)) /\ 1 = phi___retres1:145) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor(( havoc:0 / 256)), -(floor( -((havoc:0 / 256))))) mod 256) /\ ((((havoc:31 mod 256) < ( havoc:0 mod 256) \/ (havoc:0 mod 256) < ( havoc:31 mod 256)) /\ 2 = phi___retres1:146) \/ ((havoc:0 mod 256) <= ( havoc:31 mod 256) /\ (havoc:31 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:146)) /\ phi___retres1:146 = phi___retres1:145)) /\ phi___retres1:145 = phi___retres1:144)) /\ 0 <= havoc:0 /\ 0 <= havoc:32 /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256)) /\ 0 = phi___retres1:149) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256)) /\ 1 = phi___retres1:150) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor(( havoc:0 / 256)), -(floor( -((havoc:0 / 256))))) mod 256) /\ ((((havoc:32 mod 256) < ( havoc:0 mod 256) \/ (havoc:0 mod 256) < ( havoc:32 mod 256)) /\ 2 = phi___retres1:151) \/ ((havoc:0 mod 256) <= ( havoc:32 mod 256) /\ (havoc:32 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:151)) /\ phi___retres1:151 = phi___retres1:150)) /\ phi___retres1:150 = phi___retres1:149)) /\ 0 <= havoc:0 /\ 0 <= havoc:33 /\ ((((ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 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:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256)) /\ 0 = phi___retres1:154) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256) /\ (ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 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:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256)) /\ 1 = phi___retres1:155) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256) /\ (ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor(( havoc:0 / 256)), -(floor( -((havoc:0 / 256))))) mod 256) /\ ((((havoc:33 mod 256) < ( havoc:0 mod 256) \/ (havoc:0 mod 256) < ( havoc:33 mod 256)) /\ 2 = phi___retres1:156) \/ ((havoc:0 mod 256) <= ( havoc:33 mod 256) /\ (havoc:33 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:156)) /\ phi___retres1:156 = phi___retres1:155)) /\ phi___retres1:155 = phi___retres1:154)) /\ phi___retres1:154 = phi_result3:177 /\ phi___retres1:149 = phi_result2:176 /\ phi___retres1:144 = phi_result1:175 /\ havoc:34 = phi_password_binval:174 /\ phi___retres1:154 = phi_return:173 /\ type_err:157 = phi_return@pos:172 /\ type_err:158 = phi_return@width:171)) /\ phi_result3:177 = phi_result3:184 /\ phi_result2:176 = phi_result2:183 /\ phi_result1:175 = phi_result1:182 /\ phi_password_binval:174 = phi_password_binval:181 /\ phi_return:173 = phi_return:180 /\ phi_return@pos:172 = phi_return@pos:179 /\ phi_return@width:171 = phi_return@width:178) \/ (0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216 /\ 0 <= havoc:0 /\ 0 <= havoc:31 /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256)) /\ 0 = phi___retres1:144) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256)) /\ 1 = phi___retres1:145) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-( ( havoc:0 / 256))))) mod 256) /\ ((((havoc:31 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < ( havoc:31 mod 256)) /\ 2 = phi___retres1:146) \/ ((havoc:0 mod 256) <= ( havoc:31 mod 256) /\ (havoc:31 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:146)) /\ phi___retres1:146 = phi___retres1:145)) /\ phi___retres1:145 = phi___retres1:144)) /\ 0 <= havoc:0 /\ 0 <= havoc:32 /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256)) /\ 0 = phi___retres1:149) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256)) /\ 1 = phi___retres1:150) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-( ( havoc:0 / 256))))) mod 256) /\ ((((havoc:32 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < ( havoc:32 mod 256)) /\ 2 = phi___retres1:151) \/ ((havoc:0 mod 256) <= ( havoc:32 mod 256) /\ (havoc:32 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:151)) /\ phi___retres1:151 = phi___retres1:150)) /\ phi___retres1:150 = phi___retres1:149)) /\ result3:21 = phi_result3:184 /\ phi___retres1:149 = phi_result2:183 /\ phi___retres1:144 = phi_result1:182 /\ havoc:33 = phi_password_binval:181 /\ phi___retres1:149 = phi_return:180 /\ type_err:152 = phi_return@pos:179 /\ type_err:153 = phi_return@width:178))} ##### QUERY2 WFA - Initial State : __pstate Q: {__pstate, __done} F: {__done} ( __pstate , accept , __done ) Base relation: {} Weights on states: __pstate 0xc4ee90: Weight: Base relation: {when false} Accept: Base relation: {when false} __done 0xc4bd50: Weight: Base relation: {when false} Accept: Base relation: {} ##### ANS WFA - Initial State : __pstate Q: {__pstate, __done} F: {__done} ( __pstate , accept , __done ) Base relation: {} ( __pstate , (Unique State Name,69)_g1 , __done ) Base relation: {password_binval4 := havoc:34 result3 := phi_result3:184 password_binval3 := havoc:33 result2 := phi_result2:183 password_binval2 := havoc:32 result1 := phi_result1:182 password_binval1 := havoc:31 password_binval := phi_password_binval:181 guess_binval := havoc:0 return := phi_return:180 return@pos := phi_return@pos:179 return@width := phi_return@width:178 when ((((((0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216 /\ result1:19 = phi_result1:170 /\ havoc:31 = phi_password_binval:169 /\ return:30 = phi_return:168 /\ return@pos:29 = phi_return@pos:167 /\ return@width:28 = phi_return@width:166) \/ (0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216 /\ 0 <= havoc:0 /\ 0 <= havoc:31 /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256)) /\ 0 = phi___retres1:144) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 256)), -(floor(-( (havoc:31 / 256))))) mod 256)) /\ 1 = phi___retres1:145) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-( (havoc:31 / 256))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor( (havoc:0 / 256)), -(floor( -(( havoc:0 / 256))))) mod 256) /\ ((((havoc:31 mod 256) < ( havoc:0 mod 256) \/ (havoc:0 mod 256) < ( havoc:31 mod 256)) /\ 2 = phi___retres1:146) \/ ((havoc:0 mod 256) <= ( havoc:31 mod 256) /\ (havoc:31 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:146)) /\ phi___retres1:146 = phi___retres1:145)) /\ phi___retres1:145 = phi___retres1:144)) /\ phi___retres1:144 = phi_result1:170 /\ havoc:32 = phi_password_binval:169 /\ phi___retres1:144 = phi_return:168 /\ type_err:147 = phi_return@pos:167 /\ type_err:148 = phi_return@width:166)) /\ result3:21 = phi_result3:177 /\ result2:20 = phi_result2:176 /\ phi_result1:170 = phi_result1:175 /\ phi_password_binval:169 = phi_password_binval:174 /\ phi_return:168 = phi_return:173 /\ phi_return@pos:167 = phi_return@pos:172 /\ phi_return@width:166 = phi_return@width:171) \/ (0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216 /\ 0 <= havoc:0 /\ 0 <= havoc:31 /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256)) /\ 0 = phi___retres1:144) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256)) /\ 1 = phi___retres1:145) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor(( havoc:0 / 256)), -(floor( -((havoc:0 / 256))))) mod 256) /\ ((((havoc:31 mod 256) < ( havoc:0 mod 256) \/ (havoc:0 mod 256) < ( havoc:31 mod 256)) /\ 2 = phi___retres1:146) \/ ((havoc:0 mod 256) <= ( havoc:31 mod 256) /\ (havoc:31 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:146)) /\ phi___retres1:146 = phi___retres1:145)) /\ phi___retres1:145 = phi___retres1:144)) /\ 0 <= havoc:0 /\ 0 <= havoc:32 /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256)) /\ 0 = phi___retres1:149) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256)) /\ 1 = phi___retres1:150) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor(( havoc:0 / 256)), -(floor( -((havoc:0 / 256))))) mod 256) /\ ((((havoc:32 mod 256) < ( havoc:0 mod 256) \/ (havoc:0 mod 256) < ( havoc:32 mod 256)) /\ 2 = phi___retres1:151) \/ ((havoc:0 mod 256) <= ( havoc:32 mod 256) /\ (havoc:32 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:151)) /\ phi___retres1:151 = phi___retres1:150)) /\ phi___retres1:150 = phi___retres1:149)) /\ 0 <= havoc:0 /\ 0 <= havoc:33 /\ ((((ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 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:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256)) /\ 0 = phi___retres1:154) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256) /\ (ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 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:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256)) /\ 1 = phi___retres1:155) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256) /\ (ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor(( havoc:0 / 256)), -(floor( -((havoc:0 / 256))))) mod 256) /\ ((((havoc:33 mod 256) < ( havoc:0 mod 256) \/ (havoc:0 mod 256) < ( havoc:33 mod 256)) /\ 2 = phi___retres1:156) \/ ((havoc:0 mod 256) <= ( havoc:33 mod 256) /\ (havoc:33 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:156)) /\ phi___retres1:156 = phi___retres1:155)) /\ phi___retres1:155 = phi___retres1:154)) /\ phi___retres1:154 = phi_result3:177 /\ phi___retres1:149 = phi_result2:176 /\ phi___retres1:144 = phi_result1:175 /\ havoc:34 = phi_password_binval:174 /\ phi___retres1:154 = phi_return:173 /\ type_err:157 = phi_return@pos:172 /\ type_err:158 = phi_return@width:171)) /\ phi_result3:177 = phi_result3:184 /\ phi_result2:176 = phi_result2:183 /\ phi_result1:175 = phi_result1:182 /\ phi_password_binval:174 = phi_password_binval:181 /\ phi_return:173 = phi_return:180 /\ phi_return@pos:172 = phi_return@pos:179 /\ phi_return@width:171 = phi_return@width:178) \/ (0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216 /\ 0 <= havoc:0 /\ 0 <= havoc:31 /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256)) /\ 0 = phi___retres1:144) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256)) /\ 1 = phi___retres1:145) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-( ( havoc:0 / 256))))) mod 256) /\ ((((havoc:31 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < ( havoc:31 mod 256)) /\ 2 = phi___retres1:146) \/ ((havoc:0 mod 256) <= ( havoc:31 mod 256) /\ (havoc:31 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:146)) /\ phi___retres1:146 = phi___retres1:145)) /\ phi___retres1:145 = phi___retres1:144)) /\ 0 <= havoc:0 /\ 0 <= havoc:32 /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256)) /\ 0 = phi___retres1:149) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256)) /\ 1 = phi___retres1:150) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-( ( havoc:0 / 256))))) mod 256) /\ ((((havoc:32 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < ( havoc:32 mod 256)) /\ 2 = phi___retres1:151) \/ ((havoc:0 mod 256) <= ( havoc:32 mod 256) /\ (havoc:32 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:151)) /\ phi___retres1:151 = phi___retres1:150)) /\ phi___retres1:150 = phi___retres1:149)) /\ result3:21 = phi_result3:184 /\ phi___retres1:149 = phi_result2:183 /\ phi___retres1:144 = phi_result1:182 /\ havoc:33 = phi_password_binval:181 /\ phi___retres1:149 = phi_return:180 /\ type_err:152 = phi_return@pos:179 /\ type_err:153 = phi_return@width:178))} Weights on states: __pstate 0xc4d1f0: Weight: Base relation: {when false} Accept: Base relation: {when false} __done 0xc4d300: Weight: Base relation: {when false} Accept: Base relation: {} ================================================ Procedure Summaries ------------------------------------------------ Procedure summary for checkSecret Base relation: {return := phi___retres1:102 return@pos := type_err:105 return@width := type_err:106 when (0 <= guess_binval:2 /\ 0 <= password_binval:88 /\ ((((ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) < (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) \/ (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) < (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256)) /\ 0 = phi___retres1:102) \/ ((ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) <= (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) /\ (ite(0 <= password_binval:88, floor((password_binval:88 / 65536)), -(floor(-((password_binval:88 / 65536))))) mod 256) <= (ite(0 <= guess_binval:2, floor((guess_binval:2 / 65536)), -(floor(-((guess_binval:2 / 65536))))) mod 256) /\ ((((ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) < (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) \/ (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) < (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256)) /\ 1 = phi___retres1:103) \/ ((ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) <= (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) /\ (ite(0 <= password_binval:88, floor((password_binval:88 / 256)), -(floor(-((password_binval:88 / 256))))) mod 256) <= (ite(0 <= guess_binval:2, floor((guess_binval:2 / 256)), -(floor(-((guess_binval:2 / 256))))) mod 256) /\ ((((password_binval:88 mod 256) < ( guess_binval:2 mod 256) \/ (guess_binval:2 mod 256) < ( password_binval:88 mod 256)) /\ 2 = phi___retres1:104) \/ ((guess_binval:2 mod 256) <= ( password_binval:88 mod 256) /\ (password_binval:88 mod 256) <= ( guess_binval:2 mod 256) /\ 3 = phi___retres1:104)) /\ phi___retres1:104 = phi___retres1:103)) /\ phi___retres1:103 = phi___retres1:102)))} ------------------------------------------------ Procedure summary for main Base relation: {result4 := phi___retres1:159 password_binval4 := havoc:34 result3 := phi___retres1:154 password_binval3 := havoc:33 result2 := phi___retres1:149 password_binval2 := havoc:32 result1 := phi___retres1:144 password_binval1 := havoc:31 password_binval := havoc:34 guess_binval := havoc:0 return := 0 return@pos := type_err:164 return@width := type_err:165 when (0 <= havoc:0 /\ havoc:0 < 16777216 /\ 0 <= havoc:31 /\ havoc:31 < 16777216 /\ 0 <= havoc:32 /\ havoc:32 < 16777216 /\ 0 <= havoc:33 /\ havoc:33 < 16777216 /\ 0 <= havoc:34 /\ havoc:34 < 16777216 /\ 0 <= havoc:0 /\ 0 <= havoc:31 /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256)) /\ 0 = phi___retres1:144) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 65536)), -(floor(-((havoc:31 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 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:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256)) /\ 1 = phi___retres1:145) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) /\ (ite(0 <= havoc:31, floor((havoc:31 / 256)), -(floor(-((havoc:31 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) /\ ((((havoc:31 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < (havoc:31 mod 256)) /\ 2 = phi___retres1:146) \/ ((havoc:0 mod 256) <= (havoc:31 mod 256) /\ (havoc:31 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:146)) /\ phi___retres1:146 = phi___retres1:145)) /\ phi___retres1:145 = phi___retres1:144)) /\ 0 <= havoc:0 /\ 0 <= havoc:32 /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256)) /\ 0 = phi___retres1:149) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 65536)), -(floor(-((havoc:32 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 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:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256)) /\ 1 = phi___retres1:150) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) /\ (ite(0 <= havoc:32, floor((havoc:32 / 256)), -(floor(-((havoc:32 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) /\ ((((havoc:32 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < (havoc:32 mod 256)) /\ 2 = phi___retres1:151) \/ ((havoc:0 mod 256) <= (havoc:32 mod 256) /\ (havoc:32 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:151)) /\ phi___retres1:151 = phi___retres1:150)) /\ phi___retres1:150 = phi___retres1:149)) /\ 0 <= havoc:0 /\ 0 <= havoc:33 /\ ((((ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 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:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256)) /\ 0 = phi___retres1:154) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256) /\ (ite(0 <= havoc:33, floor((havoc:33 / 65536)), -(floor(-((havoc:33 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 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:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256)) /\ 1 = phi___retres1:155) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256) /\ (ite(0 <= havoc:33, floor((havoc:33 / 256)), -(floor(-((havoc:33 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) /\ ((((havoc:33 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < (havoc:33 mod 256)) /\ 2 = phi___retres1:156) \/ ((havoc:0 mod 256) <= (havoc:33 mod 256) /\ (havoc:33 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:156)) /\ phi___retres1:156 = phi___retres1:155)) /\ phi___retres1:155 = phi___retres1:154)) /\ 0 <= havoc:0 /\ 0 <= havoc:34 /\ ((((ite(0 <= havoc:34, floor((havoc:34 / 65536)), -(floor(-((havoc:34 / 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:34, floor((havoc:34 / 65536)), -(floor(-((havoc:34 / 65536))))) mod 256)) /\ 0 = phi___retres1:159) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) <= (ite(0 <= havoc:34, floor((havoc:34 / 65536)), -(floor(-((havoc:34 / 65536))))) mod 256) /\ (ite(0 <= havoc:34, floor((havoc:34 / 65536)), -(floor(-((havoc:34 / 65536))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 65536)), -(floor(-((havoc:0 / 65536))))) mod 256) /\ ((((ite(0 <= havoc:34, floor((havoc:34 / 256)), -(floor(-((havoc:34 / 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:34, floor((havoc:34 / 256)), -(floor(-((havoc:34 / 256))))) mod 256)) /\ 1 = phi___retres1:160) \/ ((ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) <= (ite(0 <= havoc:34, floor((havoc:34 / 256)), -(floor(-((havoc:34 / 256))))) mod 256) /\ (ite(0 <= havoc:34, floor((havoc:34 / 256)), -(floor(-((havoc:34 / 256))))) mod 256) <= (ite(0 <= havoc:0, floor((havoc:0 / 256)), -(floor(-((havoc:0 / 256))))) mod 256) /\ ((((havoc:34 mod 256) < (havoc:0 mod 256) \/ (havoc:0 mod 256) < (havoc:34 mod 256)) /\ 2 = phi___retres1:161) \/ ((havoc:0 mod 256) <= (havoc:34 mod 256) /\ (havoc:34 mod 256) <= ( havoc:0 mod 256) /\ 3 = phi___retres1:161)) /\ phi___retres1:161 = phi___retres1:160)) /\ phi___retres1:160 = phi___retres1:159)) /\ phi___retres1:144 < phi___retres1:149 /\ phi___retres1:149 < phi___retres1:154 /\ phi___retres1:154 < phi___retres1:159)} ================================================ Assertion Checking at Error Points ================================================ Bounds on Variables Variable bounds at line 58 in main 0 <= guess_binval guess_binval is o(1) guess_binval <= 16777215 guess_binval is O(1) ================================================ Finished!