/bat0/stac/Code/icra/WALi-OpenNWA/../icra -cra_newton_basic -cra-split-loops Passing command-line option -cra-split-loops to duet. -> Base relation: {return := phi___retres3:147 return@pos := type_err:149 return@width := type_err:150 when (0 <= param0:8 /\ param0:8 <= 1024 /\ (((ite(0 <= param0:8, floor((param0:8 / 256)), -(floor(-((param0:8 / 256))))) < ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) \/ ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) < ite(0 <= param0:8, floor(( param0:8 / 256)), -(floor( -((param0:8 / 256)))))) /\ 0 = phi___retres3:147) \/ (ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) <= ite(0 <= param0:8, floor(( param0:8 / 256)), -(floor( -((param0:8 / 256))))) /\ ite(0 <= param0:8, floor((param0:8 / 256)), -(floor(-((param0:8 / 256))))) <= ite(0 <= param1:11, floor( (param1:11 / 256)), -(floor( -( ( param1:11 / 256))))) /\ (((ite(0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) < ite(0 <= param1:11, floor( (param1:11 / 64)), -( floor( -( (param1:11 / 64))))) \/ ite(0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) < ite( 0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64)))))) /\ 1 = phi___retres3:148) \/ (ite(0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) <= ite( 0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) /\ ite(0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) <= ite( 0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) /\ 2 = phi___retres3:148)) /\ phi___retres3:148 = phi___retres3:147)))} -> Base relation: {} -> Base relation: {time1 := return:47 param0 := secret2:57 param1 := guess:27 param0@pos := type_err:82 param1@pos := type_err:84 param0@width := type_err:83 param1@width := type_err:85} -> Base relation: {} -> Base relation: {} MergeFn[Base relation: {}] -> Base relation: {} -> Base relation: {when (time0:37 < time1:38 /\ time1:38 < return:47)} -> Base relation: {} MergeFn[Base relation: {}] -> Base relation: {return := havoc:40 return@pos := type_err:43 return@width := type_err:44} -> Base relation: {time0 := return:47 param0 := secret1:66 param1 := guess:27 param0@pos := type_err:86 param1@pos := type_err:88 param0@width := type_err:87 param1@width := type_err:89} -> Base relation: {} MergeFn[Base relation: {}] -> Base relation: {secret1 := havoc:76 secret2 := havoc:77 param0 := havoc:75 param1 := guess:27 param0@pos := type_err:78 param1@pos := type_err:80 param0@width := type_err:79 param1@width := type_err:81 when (0 <= guess:27 /\ guess:27 <= 1024)} -> Base relation: {} -> Base relation: {} -> Base relation: {} MergeFn[Base relation: {}] -> Base relation: {guess := havoc:15} -> Base relation: {return := 0 return@pos := type_err:12 return@width := type_err:13} ################################################################# 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 21 24 New-style (IRE) regular expression in IREregExpMap for reID=6: Dot( Dot( Weight(Base relation: {guess := havoc:15} ) , Var(21) ) , Weight(Base relation: {return := 0 return@pos := type_err:12 return@width := type_err:13} ) ) New-style (IRE) regular expression in IREregExpMap for reID=21: Dot( Dot( Dot( Dot( Dot( Dot( Weight(Base relation: {secret1 := havoc:76 secret2 := havoc:77 param0 := havoc:75 param1 := guess:27 param0@pos := type_err:78 param1@pos := type_err:80 param0@width := type_err:79 param1@width := type_err:81 when (0 <= guess:27 /\ guess:27 <= 1024)} ) , Var(24) ) , Weight(Base relation: {time0 := return:47 param0 := secret1:66 param1 := guess:27 param0@pos := type_err:86 param1@pos := type_err:88 param0@width := type_err:87 param1@width := type_err:89} ) ) , Var(24) ) , Weight(Base relation: {time1 := return:47 param0 := secret2:57 param1 := guess:27 param0@pos := type_err:82 param1@pos := type_err:84 param0@width := type_err:83 param1@width := type_err:85} ) ) , Var(24) ) , Weight(Base relation: {return := havoc:156 return@pos := type_err:157 return@width := type_err:158 when (time0:37 < time1:38 /\ time1:38 < return:47)} ) ) New-style (IRE) regular expression in IREregExpMap for reID=24: Weight(Base relation: {return := phi___retres3:147 return@pos := type_err:149 return@width := type_err:150 when (0 <= param0:8 /\ param0:8 <= 1024 /\ (((ite(0 <= param0:8, floor((param0:8 / 256)), -(floor(-((param0:8 / 256))))) < ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-(( param1:11 / 256))))) \/ ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) < ite(0 <= param0:8, floor( (param0:8 / 256)), -(floor( -(( param0:8 / 256)))))) /\ 0 = phi___retres3:147) \/ (ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) <= ite(0 <= param0:8, floor( (param0:8 / 256)), -(floor( -(( param0:8 / 256))))) /\ ite(0 <= param0:8, floor((param0:8 / 256)), -(floor(-((param0:8 / 256))))) <= ite(0 <= param1:11, floor( ( param1:11 / 256)), -( floor( -( ( param1:11 / 256))))) /\ (((ite(0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) < ite( 0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) \/ ite(0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) < ite( 0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64)))))) /\ 1 = phi___retres3:148) \/ (ite(0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) <= ite( 0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) /\ ite(0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) <= ite( 0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) /\ 2 = phi___retres3:148)) /\ phi___retres3:148 = phi___retres3:147)))}) Performing Gaussian Elimination. ------------------------------ Working on variable 6 New-style (IRE) regular expression for 6 just before isolating it: Project( Dot( Dot( Weight(Base relation: {guess := havoc:15} ) , Var(21) ) , Weight(Base relation: {return := 0 return@pos := type_err:12 return@width := type_err:13} ) ) ) ------------------------------ Working on variable 21 New-style (IRE) regular expression for 21 just before isolating it: Project( Dot( Dot( Dot( Dot( Dot( Dot( Weight(Base relation: {secret1 := havoc:76 secret2 := havoc:77 param0 := havoc:75 param1 := guess:27 param0@pos := type_err:78 param1@pos := type_err:80 param0@width := type_err:79 param1@width := type_err:81 when (0 <= guess:27 /\ guess:27 <= 1024)} ) , Var(24) ) , Weight(Base relation: {time0 := return:47 param0 := secret1:66 param1 := guess:27 param0@pos := type_err:86 param1@pos := type_err:88 param0@width := type_err:87 param1@width := type_err:89} ) ) , Var(24) ) , Weight(Base relation: {time1 := return:47 param0 := secret2:57 param1 := guess:27 param0@pos := type_err:82 param1@pos := type_err:84 param0@width := type_err:83 param1@width := type_err:85} ) ) , Var(24) ) , Weight(Base relation: {return := havoc:156 return@pos := type_err:157 return@width := type_err:158 when (time0:37 < time1:38 /\ time1:38 < return:47)} ) ) ) ------------------------------ Working on variable 24 New-style (IRE) regular expression for 24 just before isolating it: Weight(Base relation: {return := phi___retres3:147 return@pos := type_err:149 return@width := type_err:150 when (0 <= param0:8 /\ param0:8 <= 1024 /\ (((ite(0 <= param0:8, floor((param0:8 / 256)), -(floor(-((param0:8 / 256))))) < ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-(( param1:11 / 256))))) \/ ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) < ite(0 <= param0:8, floor( (param0:8 / 256)), -(floor( -(( param0:8 / 256)))))) /\ 0 = phi___retres3:147) \/ (ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) <= ite(0 <= param0:8, floor( (param0:8 / 256)), -(floor( -(( param0:8 / 256))))) /\ ite(0 <= param0:8, floor((param0:8 / 256)), -(floor(-((param0:8 / 256))))) <= ite(0 <= param1:11, floor( ( param1:11 / 256)), -( floor( -( ( param1:11 / 256))))) /\ (((ite(0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) < ite( 0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) \/ ite(0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) < ite( 0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64)))))) /\ 1 = phi___retres3:148) \/ (ite(0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) <= ite( 0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) /\ ite(0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) <= ite( 0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) /\ 2 = phi___retres3:148)) /\ phi___retres3:148 = phi___retres3:147)))}) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Finished Gaussian Elimination. New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: Weight(Base relation: {guess := havoc:15 return := 0 param0 := havoc:188 param1 := havoc:15 return@pos := type_err:198 param0@pos := type_err:193 param1@pos := type_err:194 return@width := type_err:199 param0@width := type_err:196 param1@width := type_err:197 when (0 <= havoc:15 /\ havoc:15 <= 1024 /\ 0 <= havoc:182 /\ havoc:182 <= 1024 /\ (((ite(0 <= havoc:182, floor((havoc:182 / 256)), -(floor(-((havoc:182 / 256))))) < ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-( (havoc:15 / 256))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) < ite(0 <= havoc:182, floor( (havoc:182 / 256)), -(floor( -((havoc:182 / 256)))))) /\ 0 = phi___retres3:183) \/ (ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) <= ite(0 <= havoc:182, floor( (havoc:182 / 256)), -(floor( -((havoc:182 / 256))))) /\ ite(0 <= havoc:182, floor((havoc:182 / 256)), -(floor(-((havoc:182 / 256))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) /\ (((ite(0 <= havoc:182, floor((havoc:182 / 64)), -(floor(-((havoc:182 / 64))))) < ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) < ite( 0 <= havoc:182, floor((havoc:182 / 64)), -(floor(-((havoc:182 / 64)))))) /\ 1 = phi___retres3:184) \/ (ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) <= ite( 0 <= havoc:182, floor((havoc:182 / 64)), -(floor(-((havoc:182 / 64))))) /\ ite(0 <= havoc:182, floor((havoc:182 / 64)), -(floor(-((havoc:182 / 64))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) /\ 2 = phi___retres3:184)) /\ phi___retres3:184 = phi___retres3:183)) /\ 0 <= havoc:185 /\ havoc:185 <= 1024 /\ (((ite(0 <= havoc:185, floor((havoc:185 / 256)), -(floor(-((havoc:185 / 256))))) < ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-( (havoc:15 / 256))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) < ite(0 <= havoc:185, floor( (havoc:185 / 256)), -(floor( -((havoc:185 / 256)))))) /\ 0 = phi___retres3:186) \/ (ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) <= ite(0 <= havoc:185, floor( (havoc:185 / 256)), -(floor( -((havoc:185 / 256))))) /\ ite(0 <= havoc:185, floor((havoc:185 / 256)), -(floor(-((havoc:185 / 256))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) /\ (((ite(0 <= havoc:185, floor((havoc:185 / 64)), -(floor(-((havoc:185 / 64))))) < ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) < ite( 0 <= havoc:185, floor((havoc:185 / 64)), -(floor(-((havoc:185 / 64)))))) /\ 1 = phi___retres3:187) \/ (ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) <= ite( 0 <= havoc:185, floor((havoc:185 / 64)), -(floor(-((havoc:185 / 64))))) /\ ite(0 <= havoc:185, floor((havoc:185 / 64)), -(floor(-((havoc:185 / 64))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) /\ 2 = phi___retres3:187)) /\ phi___retres3:187 = phi___retres3:186)) /\ 0 <= havoc:188 /\ havoc:188 <= 1024 /\ (((ite(0 <= havoc:188, floor((havoc:188 / 256)), -(floor(-((havoc:188 / 256))))) < ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-( (havoc:15 / 256))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) < ite(0 <= havoc:188, floor( (havoc:188 / 256)), -(floor( -((havoc:188 / 256)))))) /\ 0 = phi___retres3:189) \/ (ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) <= ite(0 <= havoc:188, floor( (havoc:188 / 256)), -(floor( -((havoc:188 / 256))))) /\ ite(0 <= havoc:188, floor((havoc:188 / 256)), -(floor(-((havoc:188 / 256))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) /\ (((ite(0 <= havoc:188, floor((havoc:188 / 64)), -(floor(-((havoc:188 / 64))))) < ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) < ite( 0 <= havoc:188, floor((havoc:188 / 64)), -(floor(-((havoc:188 / 64)))))) /\ 1 = phi___retres3:190) \/ (ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) <= ite( 0 <= havoc:188, floor((havoc:188 / 64)), -(floor(-((havoc:188 / 64))))) /\ ite(0 <= havoc:188, floor((havoc:188 / 64)), -(floor(-((havoc:188 / 64))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) /\ 2 = phi___retres3:190)) /\ phi___retres3:190 = phi___retres3:189)) /\ phi___retres3:183 < phi___retres3:186 /\ phi___retres3:186 < phi___retres3:189)}) New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=21: Weight(Base relation: {return := havoc:220 param0 := havoc:77 param1 := guess:27 return@pos := type_err:221 param0@pos := type_err:212 param1@pos := type_err:213 return@width := type_err:222 param0@width := type_err:214 param1@width := type_err:215 when (0 <= guess:27 /\ guess:27 <= 1024 /\ 0 <= havoc:75 /\ havoc:75 <= 1024 /\ (((ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor(-((havoc:75 / 256))))) < ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-(( guess:27 / 256))))) \/ ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) < ite(0 <= havoc:75, floor( (havoc:75 / 256)), -(floor( -((havoc:75 / 256)))))) /\ 0 = phi___retres3:200) \/ (ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) <= ite(0 <= havoc:75, floor( (havoc:75 / 256)), -(floor( -((havoc:75 / 256))))) /\ ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor(-((havoc:75 / 256))))) <= ite(0 <= guess:27, floor( ( guess:27 / 256)), -( floor( -( ( guess:27 / 256))))) /\ (((ite(0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) < ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) \/ ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) < ite( 0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64)))))) /\ 1 = phi___retres3:201) \/ (ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) <= ite( 0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) /\ ite(0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) <= ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) /\ 2 = phi___retres3:201)) /\ phi___retres3:201 = phi___retres3:200)) /\ 0 <= havoc:76 /\ havoc:76 <= 1024 /\ (((ite(0 <= havoc:76, floor((havoc:76 / 256)), -(floor(-((havoc:76 / 256))))) < ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-(( guess:27 / 256))))) \/ ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) < ite(0 <= havoc:76, floor( (havoc:76 / 256)), -(floor( -((havoc:76 / 256)))))) /\ 0 = phi___retres3:208) \/ (ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) <= ite(0 <= havoc:76, floor( (havoc:76 / 256)), -(floor( -((havoc:76 / 256))))) /\ ite(0 <= havoc:76, floor((havoc:76 / 256)), -(floor(-((havoc:76 / 256))))) <= ite(0 <= guess:27, floor( ( guess:27 / 256)), -( floor( -( ( guess:27 / 256))))) /\ (((ite(0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64))))) < ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) \/ ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) < ite( 0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64)))))) /\ 1 = phi___retres3:209) \/ (ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) <= ite( 0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64))))) /\ ite(0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64))))) <= ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) /\ 2 = phi___retres3:209)) /\ phi___retres3:209 = phi___retres3:208)) /\ 0 <= havoc:77 /\ havoc:77 <= 1024 /\ (((ite(0 <= havoc:77, floor((havoc:77 / 256)), -(floor(-((havoc:77 / 256))))) < ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-(( guess:27 / 256))))) \/ ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) < ite(0 <= havoc:77, floor( (havoc:77 / 256)), -(floor( -((havoc:77 / 256)))))) /\ 0 = phi___retres3:216) \/ (ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) <= ite(0 <= havoc:77, floor( (havoc:77 / 256)), -(floor( -((havoc:77 / 256))))) /\ ite(0 <= havoc:77, floor((havoc:77 / 256)), -(floor(-((havoc:77 / 256))))) <= ite(0 <= guess:27, floor( ( guess:27 / 256)), -( floor( -( ( guess:27 / 256))))) /\ (((ite(0 <= havoc:77, floor((havoc:77 / 64)), -(floor(-((havoc:77 / 64))))) < ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) \/ ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) < ite( 0 <= havoc:77, floor((havoc:77 / 64)), -(floor(-((havoc:77 / 64)))))) /\ 1 = phi___retres3:217) \/ (ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) <= ite( 0 <= havoc:77, floor((havoc:77 / 64)), -(floor(-((havoc:77 / 64))))) /\ ite(0 <= havoc:77, floor((havoc:77 / 64)), -(floor(-((havoc:77 / 64))))) <= ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) /\ 2 = phi___retres3:217)) /\ phi___retres3:217 = phi___retres3:216)) /\ phi___retres3:200 < phi___retres3:208 /\ phi___retres3:208 < phi___retres3:216)}) New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=24: Weight(Base relation: {return := phi___retres3:147 return@pos := type_err:149 return@width := type_err:150 when (0 <= param0:8 /\ param0:8 <= 1024 /\ (((ite(0 <= param0:8, floor((param0:8 / 256)), -(floor(-((param0:8 / 256))))) < ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-(( param1:11 / 256))))) \/ ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) < ite(0 <= param0:8, floor( (param0:8 / 256)), -(floor( -(( param0:8 / 256)))))) /\ 0 = phi___retres3:147) \/ (ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) <= ite(0 <= param0:8, floor( (param0:8 / 256)), -(floor( -(( param0:8 / 256))))) /\ ite(0 <= param0:8, floor((param0:8 / 256)), -(floor(-((param0:8 / 256))))) <= ite(0 <= param1:11, floor( ( param1:11 / 256)), -( floor( -( ( param1:11 / 256))))) /\ (((ite(0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) < ite( 0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) \/ ite(0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) < ite( 0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64)))))) /\ 1 = phi___retres3:148) \/ (ite(0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) <= ite( 0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) /\ ite(0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) <= ite( 0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) /\ 2 = phi___retres3:148)) /\ phi___retres3:148 = phi___retres3:147)))}) Step 5: ========================================================= [Newton] Running Newton ------------------------------------------------------------------------------- Round 0: Evaluating variable number 6 (using IRE) The IRE-evaluated value on this round is: Base relation: {guess := havoc:15 return := 0 param0 := havoc:188 param1 := havoc:15 return@pos := type_err:198 param0@pos := type_err:193 param1@pos := type_err:194 return@width := type_err:199 param0@width := type_err:196 param1@width := type_err:197 when (0 <= havoc:15 /\ havoc:15 <= 1024 /\ 0 <= havoc:182 /\ havoc:182 <= 1024 /\ (((ite(0 <= havoc:182, floor((havoc:182 / 256)), -(floor(-((havoc:182 / 256))))) < ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) < ite(0 <= havoc:182, floor((havoc:182 / 256)), -(floor( -((havoc:182 / 256)))))) /\ 0 = phi___retres3:183) \/ (ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) <= ite(0 <= havoc:182, floor((havoc:182 / 256)), -(floor( -((havoc:182 / 256))))) /\ ite(0 <= havoc:182, floor((havoc:182 / 256)), -(floor(-((havoc:182 / 256))))) <= ite(0 <= havoc:15, floor( (havoc:15 / 256)), -( floor( -( (havoc:15 / 256))))) /\ (((ite(0 <= havoc:182, floor((havoc:182 / 64)), -(floor(-((havoc:182 / 64))))) < ite(0 <= havoc:15, floor( ( havoc:15 / 64)), -( floor( -( ( havoc:15 / 64))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) < ite( 0 <= havoc:182, floor((havoc:182 / 64)), -(floor(-((havoc:182 / 64)))))) /\ 1 = phi___retres3:184) \/ (ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) <= ite( 0 <= havoc:182, floor((havoc:182 / 64)), -(floor(-((havoc:182 / 64))))) /\ ite(0 <= havoc:182, floor((havoc:182 / 64)), -(floor(-((havoc:182 / 64))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) /\ 2 = phi___retres3:184)) /\ phi___retres3:184 = phi___retres3:183)) /\ 0 <= havoc:185 /\ havoc:185 <= 1024 /\ (((ite(0 <= havoc:185, floor((havoc:185 / 256)), -(floor(-((havoc:185 / 256))))) < ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) < ite(0 <= havoc:185, floor((havoc:185 / 256)), -(floor( -((havoc:185 / 256)))))) /\ 0 = phi___retres3:186) \/ (ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) <= ite(0 <= havoc:185, floor((havoc:185 / 256)), -(floor( -((havoc:185 / 256))))) /\ ite(0 <= havoc:185, floor((havoc:185 / 256)), -(floor(-((havoc:185 / 256))))) <= ite(0 <= havoc:15, floor( (havoc:15 / 256)), -( floor( -( (havoc:15 / 256))))) /\ (((ite(0 <= havoc:185, floor((havoc:185 / 64)), -(floor(-((havoc:185 / 64))))) < ite(0 <= havoc:15, floor( ( havoc:15 / 64)), -( floor( -( ( havoc:15 / 64))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) < ite( 0 <= havoc:185, floor((havoc:185 / 64)), -(floor(-((havoc:185 / 64)))))) /\ 1 = phi___retres3:187) \/ (ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) <= ite( 0 <= havoc:185, floor((havoc:185 / 64)), -(floor(-((havoc:185 / 64))))) /\ ite(0 <= havoc:185, floor((havoc:185 / 64)), -(floor(-((havoc:185 / 64))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) /\ 2 = phi___retres3:187)) /\ phi___retres3:187 = phi___retres3:186)) /\ 0 <= havoc:188 /\ havoc:188 <= 1024 /\ (((ite(0 <= havoc:188, floor((havoc:188 / 256)), -(floor(-((havoc:188 / 256))))) < ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) < ite(0 <= havoc:188, floor((havoc:188 / 256)), -(floor( -((havoc:188 / 256)))))) /\ 0 = phi___retres3:189) \/ (ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) <= ite(0 <= havoc:188, floor((havoc:188 / 256)), -(floor( -((havoc:188 / 256))))) /\ ite(0 <= havoc:188, floor((havoc:188 / 256)), -(floor(-((havoc:188 / 256))))) <= ite(0 <= havoc:15, floor( (havoc:15 / 256)), -( floor( -( (havoc:15 / 256))))) /\ (((ite(0 <= havoc:188, floor((havoc:188 / 64)), -(floor(-((havoc:188 / 64))))) < ite(0 <= havoc:15, floor( ( havoc:15 / 64)), -( floor( -( ( havoc:15 / 64))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) < ite( 0 <= havoc:188, floor((havoc:188 / 64)), -(floor(-((havoc:188 / 64)))))) /\ 1 = phi___retres3:190) \/ (ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) <= ite( 0 <= havoc:188, floor((havoc:188 / 64)), -(floor(-((havoc:188 / 64))))) /\ ite(0 <= havoc:188, floor((havoc:188 / 64)), -(floor(-((havoc:188 / 64))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) /\ 2 = phi___retres3:190)) /\ phi___retres3:190 = phi___retres3:189)) /\ phi___retres3:183 < phi___retres3:186 /\ phi___retres3:186 < phi___retres3:189)} Evaluating variable number 21 (using IRE) The IRE-evaluated value on this round is: Base relation: {return := havoc:220 param0 := havoc:77 param1 := guess:27 return@pos := type_err:221 param0@pos := type_err:212 param1@pos := type_err:213 return@width := type_err:222 param0@width := type_err:214 param1@width := type_err:215 when (0 <= guess:27 /\ guess:27 <= 1024 /\ 0 <= havoc:75 /\ havoc:75 <= 1024 /\ (((ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor(-((havoc:75 / 256))))) < ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) \/ ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) < ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor( -((havoc:75 / 256)))))) /\ 0 = phi___retres3:200) \/ (ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) <= ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor( -((havoc:75 / 256))))) /\ ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor(-((havoc:75 / 256))))) <= ite(0 <= guess:27, floor( (guess:27 / 256)), -(floor( -( ( guess:27 / 256))))) /\ (((ite(0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) < ite(0 <= guess:27, floor( (guess:27 / 64)), -( floor( -( (guess:27 / 64))))) \/ ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) < ite( 0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64)))))) /\ 1 = phi___retres3:201) \/ (ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) <= ite( 0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) /\ ite(0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) <= ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) /\ 2 = phi___retres3:201)) /\ phi___retres3:201 = phi___retres3:200)) /\ 0 <= havoc:76 /\ havoc:76 <= 1024 /\ (((ite(0 <= havoc:76, floor((havoc:76 / 256)), -(floor(-((havoc:76 / 256))))) < ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) \/ ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) < ite(0 <= havoc:76, floor((havoc:76 / 256)), -(floor( -((havoc:76 / 256)))))) /\ 0 = phi___retres3:208) \/ (ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) <= ite(0 <= havoc:76, floor((havoc:76 / 256)), -(floor( -((havoc:76 / 256))))) /\ ite(0 <= havoc:76, floor((havoc:76 / 256)), -(floor(-((havoc:76 / 256))))) <= ite(0 <= guess:27, floor( (guess:27 / 256)), -(floor( -( ( guess:27 / 256))))) /\ (((ite(0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64))))) < ite(0 <= guess:27, floor( (guess:27 / 64)), -( floor( -( (guess:27 / 64))))) \/ ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) < ite( 0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64)))))) /\ 1 = phi___retres3:209) \/ (ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) <= ite( 0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64))))) /\ ite(0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64))))) <= ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) /\ 2 = phi___retres3:209)) /\ phi___retres3:209 = phi___retres3:208)) /\ 0 <= havoc:77 /\ havoc:77 <= 1024 /\ (((ite(0 <= havoc:77, floor((havoc:77 / 256)), -(floor(-((havoc:77 / 256))))) < ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) \/ ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) < ite(0 <= havoc:77, floor((havoc:77 / 256)), -(floor( -((havoc:77 / 256)))))) /\ 0 = phi___retres3:216) \/ (ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) <= ite(0 <= havoc:77, floor((havoc:77 / 256)), -(floor( -((havoc:77 / 256))))) /\ ite(0 <= havoc:77, floor((havoc:77 / 256)), -(floor(-((havoc:77 / 256))))) <= ite(0 <= guess:27, floor( (guess:27 / 256)), -(floor( -( ( guess:27 / 256))))) /\ (((ite(0 <= havoc:77, floor((havoc:77 / 64)), -(floor(-((havoc:77 / 64))))) < ite(0 <= guess:27, floor( (guess:27 / 64)), -( floor( -( (guess:27 / 64))))) \/ ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) < ite( 0 <= havoc:77, floor((havoc:77 / 64)), -(floor(-((havoc:77 / 64)))))) /\ 1 = phi___retres3:217) \/ (ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) <= ite( 0 <= havoc:77, floor((havoc:77 / 64)), -(floor(-((havoc:77 / 64))))) /\ ite(0 <= havoc:77, floor((havoc:77 / 64)), -(floor(-((havoc:77 / 64))))) <= ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) /\ 2 = phi___retres3:217)) /\ phi___retres3:217 = phi___retres3:216)) /\ phi___retres3:200 < phi___retres3:208 /\ phi___retres3:208 < phi___retres3:216)} Evaluating variable number 24 (using IRE) The IRE-evaluated value on this round is: Base relation: {return := phi___retres3:147 return@pos := type_err:149 return@width := type_err:150 when (0 <= param0:8 /\ param0:8 <= 1024 /\ (((ite(0 <= param0:8, floor((param0:8 / 256)), -(floor(-((param0:8 / 256))))) < ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) \/ ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) < ite(0 <= param0:8, floor(( param0:8 / 256)), -(floor( -((param0:8 / 256)))))) /\ 0 = phi___retres3:147) \/ (ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) <= ite(0 <= param0:8, floor(( param0:8 / 256)), -(floor( -((param0:8 / 256))))) /\ ite(0 <= param0:8, floor((param0:8 / 256)), -(floor(-((param0:8 / 256))))) <= ite(0 <= param1:11, floor( (param1:11 / 256)), -(floor( -( ( param1:11 / 256))))) /\ (((ite(0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) < ite(0 <= param1:11, floor( (param1:11 / 64)), -( floor( -( (param1:11 / 64))))) \/ ite(0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) < ite( 0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64)))))) /\ 1 = phi___retres3:148) \/ (ite(0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) <= ite( 0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) /\ ite(0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) <= ite( 0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) /\ 2 = phi___retres3:148)) /\ phi___retres3:148 = phi___retres3:147)))} (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,28)_g1> Base relation: {guess := havoc:15} <__pstate, (Unique State Name,28)_g1> -> <__pstate, (Unique State Name,50)_g1> Base relation: {secret1 := havoc:76 secret2 := havoc:77 time0 := phi_time0:283 time1 := phi_time1:282 return := phi_return:281 param0 := phi_param0:280 param1 := guess:27 return@pos := phi_return@pos:279 param0@pos := phi_param0@pos:278 param1@pos := phi_param1@pos:277 return@width := phi_return@width:276 param0@width := phi_param0@width:275 param1@width := phi_param1@width:274 when ((((0 <= guess:27 /\ guess:27 <= 1024 /\ time0:37 = phi_time0:273 /\ time1:38 = phi_time1:272 /\ return:47 = phi_return:271 /\ havoc:75 = phi_param0:270 /\ return@pos:46 = phi_return@pos:269 /\ type_err:78 = phi_param0@pos:268 /\ type_err:80 = phi_param1@pos:267 /\ return@width:45 = phi_return@width:266 /\ type_err:79 = phi_param0@width:265 /\ type_err:81 = phi_param1@width:264) \/ (0 <= guess:27 /\ guess:27 <= 1024 /\ 0 <= havoc:75 /\ havoc:75 <= 1024 /\ (((ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor(-((havoc:75 / 256))))) < ite(0 <= guess:27, floor( (guess:27 / 256)), -(floor( -(( guess:27 / 256))))) \/ ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) < ite( 0 <= havoc:75, floor((havoc:75 / 256)), -(floor(-((havoc:75 / 256)))))) /\ 0 = phi___retres3:241) \/ (ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) <= ite( 0 <= havoc:75, floor((havoc:75 / 256)), -(floor(-((havoc:75 / 256))))) /\ ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor(-((havoc:75 / 256))))) <= ite( 0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) /\ (((ite(0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) < ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) \/ ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) < ite( 0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64)))))) /\ 1 = phi___retres3:242) \/ (ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) <= ite( 0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) /\ ite(0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) <= ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) /\ 2 = phi___retres3:242)) /\ phi___retres3:242 = phi___retres3:241)) /\ 0 <= havoc:76 /\ havoc:76 <= 1024 /\ (((ite(0 <= havoc:76, floor((havoc:76 / 256)), -(floor(-((havoc:76 / 256))))) < ite(0 <= guess:27, floor( (guess:27 / 256)), -(floor( -(( guess:27 / 256))))) \/ ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) < ite( 0 <= havoc:76, floor((havoc:76 / 256)), -(floor(-((havoc:76 / 256)))))) /\ 0 = phi___retres3:249) \/ (ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) <= ite( 0 <= havoc:76, floor((havoc:76 / 256)), -(floor(-((havoc:76 / 256))))) /\ ite(0 <= havoc:76, floor((havoc:76 / 256)), -(floor(-((havoc:76 / 256))))) <= ite( 0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) /\ (((ite(0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64))))) < ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) \/ ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) < ite( 0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64)))))) /\ 1 = phi___retres3:250) \/ (ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) <= ite( 0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64))))) /\ ite(0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64))))) <= ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) /\ 2 = phi___retres3:250)) /\ phi___retres3:250 = phi___retres3:249)) /\ phi___retres3:241 = phi_time0:273 /\ phi___retres3:249 = phi_time1:272 /\ phi___retres3:249 = phi_return:271 /\ havoc:77 = phi_param0:270 /\ type_err:251 = phi_return@pos:269 /\ type_err:253 = phi_param0@pos:268 /\ type_err:254 = phi_param1@pos:267 /\ type_err:252 = phi_return@width:266 /\ type_err:255 = phi_param0@width:265 /\ type_err:256 = phi_param1@width:264)) /\ phi_time0:273 = phi_time0:283 /\ phi_time1:272 = phi_time1:282 /\ phi_return:271 = phi_return:281 /\ phi_param0:270 = phi_param0:280 /\ phi_return@pos:269 = phi_return@pos:279 /\ phi_param0@pos:268 = phi_param0@pos:278 /\ phi_param1@pos:267 = phi_param1@pos:277 /\ phi_return@width:266 = phi_return@width:276 /\ phi_param0@width:265 = phi_param0@width:275 /\ phi_param1@width:264 = phi_param1@width:274) \/ (0 <= guess:27 /\ guess:27 <= 1024 /\ 0 <= havoc:75 /\ havoc:75 <= 1024 /\ (((ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor(-((havoc:75 / 256))))) < ite(0 <= guess:27, floor(( guess:27 / 256)), -(floor( -((guess:27 / 256))))) \/ ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) < ite(0 <= havoc:75, floor( (havoc:75 / 256)), -( floor( -( (havoc:75 / 256)))))) /\ 0 = phi___retres3:241) \/ (ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) <= ite(0 <= havoc:75, floor( (havoc:75 / 256)), -( floor( -( (havoc:75 / 256))))) /\ ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor(-((havoc:75 / 256))))) <= ite( 0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) /\ (((ite(0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) < ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) \/ ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) < ite( 0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64)))))) /\ 1 = phi___retres3:242) \/ (ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) <= ite( 0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) /\ ite(0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) <= ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) /\ 2 = phi___retres3:242)) /\ phi___retres3:242 = phi___retres3:241)) /\ phi___retres3:241 = phi_time0:283 /\ time1:38 = phi_time1:282 /\ phi___retres3:241 = phi_return:281 /\ havoc:76 = phi_param0:280 /\ type_err:243 = phi_return@pos:279 /\ type_err:245 = phi_param0@pos:278 /\ type_err:246 = phi_param1@pos:277 /\ type_err:244 = phi_return@width:276 /\ type_err:247 = phi_param0@width:275 /\ type_err:248 = phi_param1@width:274))} ##### QUERY2 WFA - Initial State : __pstate Q: {__pstate, __done} F: {__done} ( __pstate , accept , __done ) Base relation: {} Weights on states: __pstate 0x3a06fa0: Weight: Base relation: {when false} Accept: Base relation: {when false} __done 0x3a07050: 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,28)_g1 , __done ) Base relation: {guess := havoc:15} ( __pstate , (Unique State Name,50)_g1 , __done ) Base relation: {guess := havoc:15 secret1 := havoc:301 secret2 := havoc:304 time0 := phi_time0:311 time1 := phi_time1:312 return := phi_return:313 param0 := phi_param0:314 param1 := havoc:15 return@pos := phi_return@pos:315 param0@pos := phi_param0@pos:316 param1@pos := phi_param1@pos:317 return@width := phi_return@width:318 param0@width := phi_param0@width:319 param1@width := phi_param1@width:320 when ((((0 <= havoc:15 /\ havoc:15 <= 1024 /\ time0:37 = phi_time0:284 /\ time1:38 = phi_time1:285 /\ return:47 = phi_return:286 /\ havoc:287 = phi_param0:288 /\ return@pos:46 = phi_return@pos:289 /\ type_err:290 = phi_param0@pos:291 /\ type_err:292 = phi_param1@pos:293 /\ return@width:45 = phi_return@width:294 /\ type_err:295 = phi_param0@width:296 /\ type_err:297 = phi_param1@width:298) \/ (0 <= havoc:15 /\ havoc:15 <= 1024 /\ 0 <= havoc:287 /\ havoc:287 <= 1024 /\ (((ite(0 <= havoc:287, floor((havoc:287 / 256)), -(floor(-((havoc:287 / 256))))) < ite(0 <= havoc:15, floor( (havoc:15 / 256)), -(floor( -( (havoc:15 / 256))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) < ite( 0 <= havoc:287, floor((havoc:287 / 256)), -(floor(-((havoc:287 / 256)))))) /\ 0 = phi___retres3:299) \/ (ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) <= ite( 0 <= havoc:287, floor((havoc:287 / 256)), -(floor(-((havoc:287 / 256))))) /\ ite(0 <= havoc:287, floor((havoc:287 / 256)), -(floor(-((havoc:287 / 256))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) /\ (((ite(0 <= havoc:287, floor((havoc:287 / 64)), -(floor(-((havoc:287 / 64))))) < ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) < ite( 0 <= havoc:287, floor((havoc:287 / 64)), -(floor(-((havoc:287 / 64)))))) /\ 1 = phi___retres3:300) \/ (ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) <= ite( 0 <= havoc:287, floor((havoc:287 / 64)), -(floor(-((havoc:287 / 64))))) /\ ite(0 <= havoc:287, floor((havoc:287 / 64)), -(floor(-((havoc:287 / 64))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) /\ 2 = phi___retres3:300)) /\ phi___retres3:300 = phi___retres3:299)) /\ 0 <= havoc:301 /\ havoc:301 <= 1024 /\ (((ite(0 <= havoc:301, floor((havoc:301 / 256)), -(floor(-((havoc:301 / 256))))) < ite(0 <= havoc:15, floor( (havoc:15 / 256)), -(floor( -( (havoc:15 / 256))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) < ite( 0 <= havoc:301, floor((havoc:301 / 256)), -(floor(-((havoc:301 / 256)))))) /\ 0 = phi___retres3:302) \/ (ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) <= ite( 0 <= havoc:301, floor((havoc:301 / 256)), -(floor(-((havoc:301 / 256))))) /\ ite(0 <= havoc:301, floor((havoc:301 / 256)), -(floor(-((havoc:301 / 256))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) /\ (((ite(0 <= havoc:301, floor((havoc:301 / 64)), -(floor(-((havoc:301 / 64))))) < ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) < ite( 0 <= havoc:301, floor((havoc:301 / 64)), -(floor(-((havoc:301 / 64)))))) /\ 1 = phi___retres3:303) \/ (ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) <= ite( 0 <= havoc:301, floor((havoc:301 / 64)), -(floor(-((havoc:301 / 64))))) /\ ite(0 <= havoc:301, floor((havoc:301 / 64)), -(floor(-((havoc:301 / 64))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) /\ 2 = phi___retres3:303)) /\ phi___retres3:303 = phi___retres3:302)) /\ phi___retres3:299 = phi_time0:284 /\ phi___retres3:302 = phi_time1:285 /\ phi___retres3:302 = phi_return:286 /\ havoc:304 = phi_param0:288 /\ type_err:305 = phi_return@pos:289 /\ type_err:306 = phi_param0@pos:291 /\ type_err:307 = phi_param1@pos:293 /\ type_err:308 = phi_return@width:294 /\ type_err:309 = phi_param0@width:296 /\ type_err:310 = phi_param1@width:298)) /\ phi_time0:284 = phi_time0:311 /\ phi_time1:285 = phi_time1:312 /\ phi_return:286 = phi_return:313 /\ phi_param0:288 = phi_param0:314 /\ phi_return@pos:289 = phi_return@pos:315 /\ phi_param0@pos:291 = phi_param0@pos:316 /\ phi_param1@pos:293 = phi_param1@pos:317 /\ phi_return@width:294 = phi_return@width:318 /\ phi_param0@width:296 = phi_param0@width:319 /\ phi_param1@width:298 = phi_param1@width:320) \/ (0 <= havoc:15 /\ havoc:15 <= 1024 /\ 0 <= havoc:287 /\ havoc:287 <= 1024 /\ (((ite(0 <= havoc:287, floor((havoc:287 / 256)), -(floor(-((havoc:287 / 256))))) < ite(0 <= havoc:15, floor( (havoc:15 / 256)), -(floor( -((havoc:15 / 256))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) < ite(0 <= havoc:287, floor( (havoc:287 / 256)), -( floor( -( (havoc:287 / 256)))))) /\ 0 = phi___retres3:299) \/ (ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) <= ite(0 <= havoc:287, floor( (havoc:287 / 256)), -( floor( -( (havoc:287 / 256))))) /\ ite(0 <= havoc:287, floor((havoc:287 / 256)), -(floor(-((havoc:287 / 256))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) /\ (((ite(0 <= havoc:287, floor((havoc:287 / 64)), -(floor(-((havoc:287 / 64))))) < ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) < ite( 0 <= havoc:287, floor((havoc:287 / 64)), -(floor(-((havoc:287 / 64)))))) /\ 1 = phi___retres3:300) \/ (ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) <= ite( 0 <= havoc:287, floor((havoc:287 / 64)), -(floor(-((havoc:287 / 64))))) /\ ite(0 <= havoc:287, floor((havoc:287 / 64)), -(floor(-((havoc:287 / 64))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) /\ 2 = phi___retres3:300)) /\ phi___retres3:300 = phi___retres3:299)) /\ phi___retres3:299 = phi_time0:311 /\ time1:38 = phi_time1:312 /\ phi___retres3:299 = phi_return:313 /\ havoc:301 = phi_param0:314 /\ type_err:321 = phi_return@pos:315 /\ type_err:322 = phi_param0@pos:316 /\ type_err:323 = phi_param1@pos:317 /\ type_err:324 = phi_return@width:318 /\ type_err:325 = phi_param0@width:319 /\ type_err:326 = phi_param1@width:320))} Weights on states: __pstate 0x3a08cc0: Weight: Base relation: {when false} Accept: Base relation: {when false} __done 0x3a08dd0: Weight: Base relation: {when false} Accept: Base relation: {} ================================================ Procedure Summaries ------------------------------------------------ Procedure summary for checkSecret Base relation: {return := phi___retres3:147 return@pos := type_err:149 return@width := type_err:150 when (0 <= param0:8 /\ param0:8 <= 1024 /\ (((ite(0 <= param0:8, floor((param0:8 / 256)), -(floor(-((param0:8 / 256))))) < ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) \/ ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) < ite(0 <= param0:8, floor(( param0:8 / 256)), -(floor( -((param0:8 / 256)))))) /\ 0 = phi___retres3:147) \/ (ite(0 <= param1:11, floor((param1:11 / 256)), -(floor(-((param1:11 / 256))))) <= ite(0 <= param0:8, floor(( param0:8 / 256)), -(floor( -((param0:8 / 256))))) /\ ite(0 <= param0:8, floor((param0:8 / 256)), -(floor(-((param0:8 / 256))))) <= ite(0 <= param1:11, floor( (param1:11 / 256)), -(floor( -( ( param1:11 / 256))))) /\ (((ite(0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) < ite(0 <= param1:11, floor( (param1:11 / 64)), -( floor( -( (param1:11 / 64))))) \/ ite(0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) < ite( 0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64)))))) /\ 1 = phi___retres3:148) \/ (ite(0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) <= ite( 0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) /\ ite(0 <= param0:8, floor((param0:8 / 64)), -(floor(-((param0:8 / 64))))) <= ite( 0 <= param1:11, floor((param1:11 / 64)), -(floor(-((param1:11 / 64))))) /\ 2 = phi___retres3:148)) /\ phi___retres3:148 = phi___retres3:147)))} ------------------------------------------------ Procedure summary for main Base relation: {guess := havoc:15 return := 0 param0 := havoc:229 param1 := havoc:15 return@pos := type_err:239 param0@pos := type_err:234 param1@pos := type_err:235 return@width := type_err:240 param0@width := type_err:237 param1@width := type_err:238 when (0 <= havoc:15 /\ havoc:15 <= 1024 /\ 0 <= havoc:223 /\ havoc:223 <= 1024 /\ (((ite(0 <= havoc:223, floor((havoc:223 / 256)), -(floor(-((havoc:223 / 256))))) < ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) < ite(0 <= havoc:223, floor((havoc:223 / 256)), -(floor( -((havoc:223 / 256)))))) /\ 0 = phi___retres3:224) \/ (ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) <= ite(0 <= havoc:223, floor((havoc:223 / 256)), -(floor( -((havoc:223 / 256))))) /\ ite(0 <= havoc:223, floor((havoc:223 / 256)), -(floor(-((havoc:223 / 256))))) <= ite(0 <= havoc:15, floor( (havoc:15 / 256)), -( floor( -( (havoc:15 / 256))))) /\ (((ite(0 <= havoc:223, floor((havoc:223 / 64)), -(floor(-((havoc:223 / 64))))) < ite(0 <= havoc:15, floor( ( havoc:15 / 64)), -( floor( -( ( havoc:15 / 64))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) < ite( 0 <= havoc:223, floor((havoc:223 / 64)), -(floor(-((havoc:223 / 64)))))) /\ 1 = phi___retres3:225) \/ (ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) <= ite( 0 <= havoc:223, floor((havoc:223 / 64)), -(floor(-((havoc:223 / 64))))) /\ ite(0 <= havoc:223, floor((havoc:223 / 64)), -(floor(-((havoc:223 / 64))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) /\ 2 = phi___retres3:225)) /\ phi___retres3:225 = phi___retres3:224)) /\ 0 <= havoc:226 /\ havoc:226 <= 1024 /\ (((ite(0 <= havoc:226, floor((havoc:226 / 256)), -(floor(-((havoc:226 / 256))))) < ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) < ite(0 <= havoc:226, floor((havoc:226 / 256)), -(floor( -((havoc:226 / 256)))))) /\ 0 = phi___retres3:227) \/ (ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) <= ite(0 <= havoc:226, floor((havoc:226 / 256)), -(floor( -((havoc:226 / 256))))) /\ ite(0 <= havoc:226, floor((havoc:226 / 256)), -(floor(-((havoc:226 / 256))))) <= ite(0 <= havoc:15, floor( (havoc:15 / 256)), -( floor( -( (havoc:15 / 256))))) /\ (((ite(0 <= havoc:226, floor((havoc:226 / 64)), -(floor(-((havoc:226 / 64))))) < ite(0 <= havoc:15, floor( ( havoc:15 / 64)), -( floor( -( ( havoc:15 / 64))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) < ite( 0 <= havoc:226, floor((havoc:226 / 64)), -(floor(-((havoc:226 / 64)))))) /\ 1 = phi___retres3:228) \/ (ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) <= ite( 0 <= havoc:226, floor((havoc:226 / 64)), -(floor(-((havoc:226 / 64))))) /\ ite(0 <= havoc:226, floor((havoc:226 / 64)), -(floor(-((havoc:226 / 64))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) /\ 2 = phi___retres3:228)) /\ phi___retres3:228 = phi___retres3:227)) /\ 0 <= havoc:229 /\ havoc:229 <= 1024 /\ (((ite(0 <= havoc:229, floor((havoc:229 / 256)), -(floor(-((havoc:229 / 256))))) < ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) < ite(0 <= havoc:229, floor((havoc:229 / 256)), -(floor( -((havoc:229 / 256)))))) /\ 0 = phi___retres3:230) \/ (ite(0 <= havoc:15, floor((havoc:15 / 256)), -(floor(-((havoc:15 / 256))))) <= ite(0 <= havoc:229, floor((havoc:229 / 256)), -(floor( -((havoc:229 / 256))))) /\ ite(0 <= havoc:229, floor((havoc:229 / 256)), -(floor(-((havoc:229 / 256))))) <= ite(0 <= havoc:15, floor( (havoc:15 / 256)), -( floor( -( (havoc:15 / 256))))) /\ (((ite(0 <= havoc:229, floor((havoc:229 / 64)), -(floor(-((havoc:229 / 64))))) < ite(0 <= havoc:15, floor( ( havoc:15 / 64)), -( floor( -( ( havoc:15 / 64))))) \/ ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) < ite( 0 <= havoc:229, floor((havoc:229 / 64)), -(floor(-((havoc:229 / 64)))))) /\ 1 = phi___retres3:231) \/ (ite(0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) <= ite( 0 <= havoc:229, floor((havoc:229 / 64)), -(floor(-((havoc:229 / 64))))) /\ ite(0 <= havoc:229, floor((havoc:229 / 64)), -(floor(-((havoc:229 / 64))))) <= ite( 0 <= havoc:15, floor((havoc:15 / 64)), -(floor(-((havoc:15 / 64))))) /\ 2 = phi___retres3:231)) /\ phi___retres3:231 = phi___retres3:230)) /\ phi___retres3:224 < phi___retres3:227 /\ phi___retres3:227 < phi___retres3:230)} ------------------------------------------------ Procedure summary for start Base relation: {secret1 := havoc:76 secret2 := havoc:77 time0 := phi___retres3:241 time1 := phi___retres3:249 return := havoc:261 param0 := havoc:77 param1 := guess:27 return@pos := type_err:262 param0@pos := type_err:253 param1@pos := type_err:254 return@width := type_err:263 param0@width := type_err:255 param1@width := type_err:256 when (0 <= guess:27 /\ guess:27 <= 1024 /\ 0 <= havoc:75 /\ havoc:75 <= 1024 /\ (((ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor(-((havoc:75 / 256))))) < ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) \/ ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) < ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor( -((havoc:75 / 256)))))) /\ 0 = phi___retres3:241) \/ (ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) <= ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor( -((havoc:75 / 256))))) /\ ite(0 <= havoc:75, floor((havoc:75 / 256)), -(floor(-((havoc:75 / 256))))) <= ite(0 <= guess:27, floor( (guess:27 / 256)), -(floor( -( ( guess:27 / 256))))) /\ (((ite(0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) < ite(0 <= guess:27, floor( (guess:27 / 64)), -( floor( -( (guess:27 / 64))))) \/ ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) < ite( 0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64)))))) /\ 1 = phi___retres3:242) \/ (ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) <= ite( 0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) /\ ite(0 <= havoc:75, floor((havoc:75 / 64)), -(floor(-((havoc:75 / 64))))) <= ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) /\ 2 = phi___retres3:242)) /\ phi___retres3:242 = phi___retres3:241)) /\ 0 <= havoc:76 /\ havoc:76 <= 1024 /\ (((ite(0 <= havoc:76, floor((havoc:76 / 256)), -(floor(-((havoc:76 / 256))))) < ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) \/ ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) < ite(0 <= havoc:76, floor((havoc:76 / 256)), -(floor( -((havoc:76 / 256)))))) /\ 0 = phi___retres3:249) \/ (ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) <= ite(0 <= havoc:76, floor((havoc:76 / 256)), -(floor( -((havoc:76 / 256))))) /\ ite(0 <= havoc:76, floor((havoc:76 / 256)), -(floor(-((havoc:76 / 256))))) <= ite(0 <= guess:27, floor( (guess:27 / 256)), -(floor( -( ( guess:27 / 256))))) /\ (((ite(0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64))))) < ite(0 <= guess:27, floor( (guess:27 / 64)), -( floor( -( (guess:27 / 64))))) \/ ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) < ite( 0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64)))))) /\ 1 = phi___retres3:250) \/ (ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) <= ite( 0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64))))) /\ ite(0 <= havoc:76, floor((havoc:76 / 64)), -(floor(-((havoc:76 / 64))))) <= ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) /\ 2 = phi___retres3:250)) /\ phi___retres3:250 = phi___retres3:249)) /\ 0 <= havoc:77 /\ havoc:77 <= 1024 /\ (((ite(0 <= havoc:77, floor((havoc:77 / 256)), -(floor(-((havoc:77 / 256))))) < ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) \/ ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) < ite(0 <= havoc:77, floor((havoc:77 / 256)), -(floor( -((havoc:77 / 256)))))) /\ 0 = phi___retres3:257) \/ (ite(0 <= guess:27, floor((guess:27 / 256)), -(floor(-((guess:27 / 256))))) <= ite(0 <= havoc:77, floor((havoc:77 / 256)), -(floor( -((havoc:77 / 256))))) /\ ite(0 <= havoc:77, floor((havoc:77 / 256)), -(floor(-((havoc:77 / 256))))) <= ite(0 <= guess:27, floor( (guess:27 / 256)), -(floor( -( ( guess:27 / 256))))) /\ (((ite(0 <= havoc:77, floor((havoc:77 / 64)), -(floor(-((havoc:77 / 64))))) < ite(0 <= guess:27, floor( (guess:27 / 64)), -( floor( -( (guess:27 / 64))))) \/ ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) < ite( 0 <= havoc:77, floor((havoc:77 / 64)), -(floor(-((havoc:77 / 64)))))) /\ 1 = phi___retres3:258) \/ (ite(0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) <= ite( 0 <= havoc:77, floor((havoc:77 / 64)), -(floor(-((havoc:77 / 64))))) /\ ite(0 <= havoc:77, floor((havoc:77 / 64)), -(floor(-((havoc:77 / 64))))) <= ite( 0 <= guess:27, floor((guess:27 / 64)), -(floor(-((guess:27 / 64))))) /\ 2 = phi___retres3:258)) /\ phi___retres3:258 = phi___retres3:257)) /\ phi___retres3:241 < phi___retres3:249 /\ phi___retres3:249 < phi___retres3:257)} ================================================ Assertion Checking at Error Points ================================================ Bounds on Variables Variable bounds at line 19 in start Variable bounds at line 20 in start 0 <= secret1 secret1 is o(1) secret1 <= 1024 secret1 is O(1) Variable bounds at line 21 in start 0 <= secret2 secret2 is o(1) secret2 <= 1024 secret2 is O(1) ================================================ Finished!