API tools faq
paste
Advertisement
Guest User

smokemebaby.py

a guest
Apr 26th, 2018
128
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Python 19.01 KB | None | 0 0
raw download clone embed print report
  1. from z3 import *
  2. import string
  3.  
  4. a1 = BitVec('a1', 64)
  5. s = Solver()
  6. flag = ''
  7.  
  8. s.add(8 * (4 * (4 * (8 * (2 * (4 * (9 * (2 * (7 * (a1 - 49) - 29) - 18) - 48) - 27 + 23) + 33) + 33) - 29) + 28) == 58028480)
  9. s.add(a1 > 0)
  10. s.add(a1 < 256)
  11. s.add(a1 != 10)
  12. s.add(a1 !=13)
  13. s.add(a1 != 9)
  14. s.add(a1 != 11)
  15.  
  16. while s.check() == sat:
  17.     if chr(s.model()[a1].as_long()) in string.printable:
  18.         break
  19.  
  20.     s.add(a1 != s.model()[a1])
  21. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  22. flag += chr(s.model()[a1].as_signed_long())
  23. s.reset()
  24.  
  25. s.add(28 * (4 * (2 * ((16 * (2 * (96 * (8 * ((4 * a1 >> 1) + 5) - 28) - 14) - 21) + 28) >> 3) - 7) - 30) == 152397448)
  26. s.add(a1 > 0)
  27. s.add(a1 < 256)
  28. s.add(a1 != 10)
  29. s.add(a1 !=13)
  30. s.add(a1 != 9)
  31. s.add(a1 != 11)
  32.  
  33. while s.check() == sat:
  34.     if chr(s.model()[a1].as_long()) in string.printable:
  35.         break
  36.  
  37.     s.add(a1 != s.model()[a1])
  38. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  39. flag += chr(s.model()[a1].as_signed_long())
  40. s.reset()
  41.  
  42. s.add((96 * (((288 * (((4 * (2 * ((9 * (8 * (4 * a1 - 9) - 6) + 5) >> 1) - 29) >> 1) + 33) >> 1) + 71) >> 2) + 27) + 6) >> 1 == 29395395)
  43. s.add(a1 > 0)
  44. s.add(a1 < 256)
  45. s.add(a1 != 10)
  46. s.add(a1 !=13)
  47. s.add(a1 != 9)
  48. s.add(a1 != 11)
  49.  
  50. while s.check() == sat:
  51.     if chr(s.model()[a1].as_long()) in string.printable:
  52.         break
  53.  
  54.     s.add(a1 != s.model()[a1])
  55. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  56. flag += chr(s.model()[a1].as_signed_long())
  57. s.reset()
  58.  
  59. s.add(4 * (4 * ((4 * (4 * (54 * (4 * (8 * (8 * (a1 >> 1) - 12) - 56) + 17) >> 1) + 55) >> 1) - 32) + 25) == 40426180)
  60. s.add(a1 > 0)
  61. s.add(a1 < 256)
  62. s.add(a1 != 10)
  63. s.add(a1 !=13)
  64. s.add(a1 != 9)
  65. s.add(a1 != 11)
  66.  
  67. while s.check() == sat:
  68.     if chr(s.model()[a1].as_long()) in string.printable:
  69.         break
  70.  
  71.     s.add(a1 != s.model()[a1])
  72. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  73. flag += chr(s.model()[a1].as_signed_long())
  74. s.reset()
  75.  
  76. s.add(9* (32 * (7 * ((8 * ((9 * (4 * (2 * ((4 * (4 * (a1 + 44) + 7) - 7) >> 2) - 30 + 8) - 25) + 17) >> 1) + 17) >> 1) + 16)+ 25) == 176267745)
  77. s.add(a1 > 0)
  78. s.add(a1 < 256)
  79. s.add(a1 != 10)
  80. s.add(a1 !=13)
  81. s.add(a1 != 9)
  82. s.add(a1 != 11)
  83.  
  84. while s.check() == sat:
  85.     if chr(s.model()[a1].as_long()) in string.printable:
  86.         break
  87.  
  88.     s.add(a1 != s.model()[a1])
  89. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  90. flag += chr(s.model()[a1].as_signed_long())
  91. s.reset()
  92.  
  93. s.add(2  * (2 * (4 * (84 * (((2 * ((18 * (5 * ((((a1 >> 1) + 29) >> 1) + 8) - 54) - 23) >> 1) + 31) >> 1) - 35) >> 1) + 6) + 17) == 1163962)
  94. s.add(a1 > 0)
  95. s.add(a1 < 256)
  96. s.add(a1 != 10)
  97. s.add(a1 !=13)
  98. s.add(a1 != 9)
  99. s.add(a1 != 11)
  100.  
  101. while s.check() == sat:
  102.     if chr(s.model()[a1].as_long()) in string.printable:
  103.         break
  104.  
  105.     s.add(a1 != s.model()[a1])
  106. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  107. flag += chr(s.model()[a1].as_signed_long())
  108. s.reset()
  109.  
  110. s.add(4 * (2 * (2 * (2 * (4 * ((4 * (((9 * (8 * (a1 - 49) - 7 + 31) + 25) >> 1) - 57) - 17) >> 1) >> 1) >> 1) >> 1) + 44) >> 1 == 39616)
  111. s.add(a1 > 0)
  112. s.add(a1 < 256)
  113. s.add(a1 != 10)
  114. s.add(a1 !=13)
  115. s.add(a1 != 9)
  116. s.add(a1 != 11)
  117.  
  118. while s.check() == sat:
  119.     if chr(s.model()[a1].as_long()) in string.printable:
  120.         break
  121.  
  122.     s.add(a1 != s.model()[a1])
  123. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  124. flag += chr(s.model()[a1].as_signed_long())
  125. s.reset()
  126.  
  127. s.add(20 * (4 * ((2 * (4 * (4 * (4 * (672 * (8 * (36 * (4 * (4 * a1 + 6) + 19) - 9) + 28) + 15) - 4) % 24) >> 1) >> 1) - 16) - 15) == -300)
  128. s.add(a1 > 0)
  129. s.add(a1 < 256)
  130. s.add(a1 != 10)
  131. s.add(a1 !=13)
  132. s.add(a1 != 9)
  133. s.add(a1 != 11)
  134.  
  135. while s.check() == sat:
  136.     if chr(s.model()[a1].as_long()) in string.printable:
  137.         break
  138.  
  139.     s.add(a1 != s.model()[a1])
  140. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  141. flag += chr(s.model()[a1].as_signed_long())
  142. s.reset()
  143.  
  144. s.add(4 * (8 * ((6 * ((((4 * (4 * (6 * (6 * ((a1 >> 1) - 31 + 22) - 17) >> 1) + 8) >> 1) + 11) >> 1) + 30) >> 1 << 8) + 19) - 3) == 68592212)
  145. s.add(a1 > 0)
  146. s.add(a1 < 256)
  147. s.add(a1 != 10)
  148. s.add(a1 !=13)
  149. s.add(a1 != 9)
  150. s.add(a1 != 11)
  151.  
  152. while s.check() == sat:
  153.     if chr(s.model()[a1].as_long()) in string.printable:
  154.         break
  155.  
  156.     s.add(a1 != s.model()[a1])
  157. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  158. flag += chr(s.model()[a1].as_signed_long())
  159. s.reset()
  160.  
  161. s.add(12096 * (2 * (5 * (3 * (4 * (3 * (24 * a1 + 13) - 19 + 8) + 8) + 8) + 9) - 5) % 8 == 0)
  162. s.add(a1 > 0)
  163. s.add(a1 < 256)
  164. s.add(a1 != 10)
  165. s.add(a1 !=13)
  166. s.add(a1 != 9)
  167. s.add(a1 != 11)
  168.  
  169. while s.check() == sat:
  170.     if chr(s.model()[a1].as_long()) in string.printable:
  171.         break
  172.  
  173.     s.add(a1 != s.model()[a1])
  174. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  175. flag += chr(s.model()[a1].as_signed_long())
  176. s.reset()
  177.  
  178.  
  179. s.add(288 * (4 * (16 * (6 * (((4 * ((5 * (6 * (a1 + 21) - 14) - 7 + 28) >> 1) - 8) >> 1) - 2) + 4) + 4) + 26) >> 1 == 84866976)
  180. s.add(a1 > 0)
  181. s.add(a1 < 256)
  182. s.add(a1 != 10)
  183. s.add(a1 !=13)
  184. s.add(a1 != 9)
  185. s.add(a1 != 11)
  186.  
  187. while s.check() == sat:
  188.     if chr(s.model()[a1].as_long()) in string.printable:
  189.         break
  190.  
  191.     s.add(a1 != s.model()[a1])
  192. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  193. flag += chr(s.model()[a1].as_signed_long())
  194. s.reset()
  195.  
  196. s.add(4 * (6 * (392 * ((8 * (2 * (8 * (2 * (16 * a1 - 28 + 46) - 24) + 19) >> 3) + 20) >> 1) + 15) + 32) == 268485992)
  197. s.add(a1 > 0)
  198. s.add(a1 < 256)
  199. s.add(a1 != 10)
  200. s.add(a1 !=13)
  201. s.add(a1 != 9)
  202. s.add(a1 != 11)
  203.  
  204. while s.check() == sat:
  205.     if chr(s.model()[a1].as_long()) in string.printable:
  206.         break
  207.  
  208.     s.add(a1 != s.model()[a1])
  209. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  210. flag += chr(s.model()[a1].as_signed_long())
  211. s.reset()
  212.  
  213. s.add((2 * (20 * (2 * (4 * ((2 * ((9 * (4 * a1 + 10) >> 1) - 47) - 8) >> 1) - 56) - 5) - 21) - 25 + 4) >> 1 == 313468)
  214. s.add(a1 > 0)
  215. s.add(a1 < 256)
  216. s.add(a1 != 10)
  217. s.add(a1 !=13)
  218. s.add(a1 != 9)
  219. s.add(a1 != 11)
  220.  
  221. while s.check() == sat:
  222.     if chr(s.model()[a1].as_long()) in string.printable:
  223.         break
  224.  
  225.     s.add(a1 != s.model()[a1])
  226. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  227. flag += chr(s.model()[a1].as_signed_long())
  228. s.reset()
  229.  
  230. s.add(8 * (3 * (90 * (6 * (4 * (3 * (10 * (1008 * ((a1 + 9) >> 2) >> 2) + 4) - 6) + 16) - 19) - 14) - 8) % 4 == 0)
  231. s.add(a1 > 0)
  232. s.add(a1 < 256)
  233. s.add(a1 != 10)
  234. s.add(a1 !=13)
  235. s.add(a1 != 9)
  236. s.add(a1 != 11)
  237.  
  238. while s.check() == sat:
  239.     if chr(s.model()[a1].as_long()) in string.printable:
  240.         break
  241.  
  242.     s.add(a1 != s.model()[a1])
  243. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  244. flag += chr(s.model()[a1].as_signed_long())
  245. s.reset()
  246.  
  247. s.add(6 * (7 * (4 * (((2 * (9 * (8 * (4 * a1 - 22 + 31) >> 1) + 7) + 39) >> 1) - 19 + 14) - 24) + 32) == 1581240)
  248. s.add(a1 > 0)
  249. s.add(a1 < 256)
  250. s.add(a1 != 10)
  251. s.add(a1 !=13)
  252. s.add(a1 != 9)
  253. s.add(a1 != 11)
  254.  
  255. while s.check() == sat:
  256.     if chr(s.model()[a1].as_long()) in string.printable:
  257.         break
  258.  
  259.     s.add(a1 != s.model()[a1])
  260. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  261. flag += chr(s.model()[a1].as_signed_long())
  262. s.reset()
  263.  
  264. s.add(40 * ((((6 * (24 * ((7 * (3 * (20 * (2 * (a1 - 47) - 22) - 9) >> 1) + 14) >> 1) + 20) - 10) >> 1) - 52) >> 1) == -7922840)
  265. s.add(a1 > 0)
  266. s.add(a1 < 256)
  267. s.add(a1 != 10)
  268. s.add(a1 !=13)
  269. s.add(a1 != 9)
  270. s.add(a1 != 11)
  271.  
  272. while s.check() == sat:
  273.     if chr(s.model()[a1].as_long()) in string.printable:
  274.         break
  275.  
  276.     s.add(a1 != s.model()[a1])
  277. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  278. flag += chr(s.model()[a1].as_signed_long())
  279. s.reset()
  280.  
  281. s.add(480 * (2 * (3 * (4 * (5 * (4 * (((2 * ((3 * (a1 - 24) - 25) >> 1) - 7) >> 1) + 35) + 18) + 34) - 18) + 25) + 25) == 26065440)
  282. s.add(a1 > 0)
  283. s.add(a1 < 256)
  284. s.add(a1 != 10)
  285. s.add(a1 !=13)
  286. s.add(a1 != 9)
  287. s.add(a1 != 11)
  288.  
  289. while s.check() == sat:
  290.     if chr(s.model()[a1].as_long()) in string.printable:
  291.         break
  292.  
  293.     s.add(a1 != s.model()[a1])
  294. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  295. flag += chr(s.model()[a1].as_signed_long())
  296. s.reset()
  297.  
  298. s.add(4 * (((20 * (2 * (((72 * (2 * (192 * (a1 - 27) - 20) + 1) >> 1) + 48) >> 1) >> 1) + 51) >> 2) - 14) == 11598592)
  299. s.add(a1 > 0)
  300. s.add(a1 < 256)
  301. s.add(a1 != 10)
  302. s.add(a1 !=13)
  303. s.add(a1 != 9)
  304. s.add(a1 != 11)
  305.  
  306. while s.check() == sat:
  307.     if chr(s.model()[a1].as_long()) in string.printable:
  308.         break
  309.  
  310.     s.add(a1 != s.model()[a1])
  311. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  312. flag += chr(s.model()[a1].as_signed_long())
  313. s.reset()
  314.  
  315. s.add(4 * (4 * ((2 * (2 * (1440 * (a1 - 36) - 105) + 31) + 41) >> 1) - 22) == 3361208)
  316. s.add(a1 > 0)
  317. s.add(a1 < 256)
  318. s.add(a1 != 10)
  319. s.add(a1 !=13)
  320. s.add(a1 != 9)
  321. s.add(a1 != 11)
  322.  
  323. while s.check() == sat:
  324.     if chr(s.model()[a1].as_long()) in string.printable:
  325.         break
  326.  
  327.     s.add(a1 != s.model()[a1])
  328. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  329. flag += chr(s.model()[a1].as_signed_long())
  330. s.reset()
  331.  
  332. s.add(18 * ((48 * (2 * (2 * (2 * (2 * (4 * (504 * (a1 - 21) + 30) + 30) >> 1) - 34) + 36) + 10) + 53) >> 1) == 557879220)
  333. s.add(a1 > 0)
  334. s.add(a1 < 256)
  335. s.add(a1 != 10)
  336. s.add(a1 !=13)
  337. s.add(a1 != 9)
  338. s.add(a1 != 11)
  339.  
  340. while s.check() == sat:
  341.     if chr(s.model()[a1].as_long()) in string.printable:
  342.         break
  343.  
  344.     s.add(a1 != s.model()[a1])
  345. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  346. flag += chr(s.model()[a1].as_signed_long())
  347. s.reset()
  348.  
  349. s.add(4 * (14 * (4 * (4 * (1792 * (32 * (144 * (a1 + 15) - 26) - 7 + 17) - 25) + 15) % 13) - 16) == 160)
  350. s.add(a1 > 0)
  351. s.add(a1 < 256)
  352. s.add(a1 != 10)
  353. s.add(a1 !=13)
  354. s.add(a1 != 9)
  355. s.add(a1 != 11)
  356.  
  357. while s.check() == sat:
  358.     if chr(s.model()[a1].as_long()) in string.printable:
  359.         break
  360.  
  361.     s.add(a1 != s.model()[a1])
  362. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  363. flag += chr(s.model()[a1].as_signed_long())
  364. s.reset()
  365.  
  366. s.add(7 * (144 * (6 * (8 * (((4 * (2 * (18 * a1 + 9) + 14) >> 1) - 26) >> 1) + 24) - 9) - 55 + 23) == 192655792)
  367. s.add(a1 > 0)
  368. s.add(a1 < 256)
  369. s.add(a1 != 10)
  370. s.add(a1 !=13)
  371. s.add(a1 != 9)
  372. s.add(a1 != 11)
  373.  
  374. while s.check() == sat:
  375.     if chr(s.model()[a1].as_long()) in string.printable:
  376.         break
  377.  
  378.     s.add(a1 != s.model()[a1])
  379. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  380. flag += chr(s.model()[a1].as_signed_long())
  381. s.reset()
  382.  
  383. s.add(2 * (40 * (((28 * (2 * (4 * ((96 * (((a1 - 33) >> 1) + 11) - 31 + 33) >> 1) + 34) >> 2) >> 2 << 7) - 15) >> 1) - 25) == 155509070)
  384. s.add(a1 > 0)
  385. s.add(a1 < 256)
  386. s.add(a1 != 10)
  387. s.add(a1 !=13)
  388. s.add(a1 != 9)
  389. s.add(a1 != 11)
  390.  
  391. while s.check() == sat:
  392.     if chr(s.model()[a1].as_long()) in string.printable:
  393.         break
  394.  
  395.     s.add(a1 != s.model()[a1])
  396. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  397. flag += chr(s.model()[a1].as_signed_long())
  398. s.reset()
  399.  
  400. s.add(4 * ((9 * (9 * (24 * (96 * (8 * ((a1 << 7) + 5) - 27) - 41) + 19) + 9) % 28 >> 2) - 11) == -36)
  401. s.add(a1 > 0)
  402. s.add(a1 < 256)
  403. s.add(a1 != 10)
  404. s.add(a1 !=13)
  405. s.add(a1 != 9)
  406. s.add(a1 != 11)
  407.  
  408. while s.check() == sat:
  409.     if chr(s.model()[a1].as_long()) in string.printable:
  410.         break
  411.  
  412.     s.add(a1 != s.model()[a1])
  413. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  414. flag += chr(s.model()[a1].as_signed_long())
  415. s.reset()
  416.  
  417.  
  418. s.add(4 * ((32 * (56 * (35 * (14 * (45 * (a1 + 104) - 9 + 18) - 37) + 20) + 59) % 29 >> 1) - 29 + 15) == -24)
  419. s.add(a1 > 0)
  420. s.add(a1 < 256)
  421. s.add(a1 != 10)
  422. s.add(a1 !=13)
  423. s.add(a1 != 9)
  424. s.add(a1 != 11)
  425.  
  426. while s.check() == sat:
  427.     if chr(s.model()[a1].as_long()) in string.printable:
  428.         break
  429.  
  430.     s.add(a1 != s.model()[a1])
  431. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  432. flag += chr(s.model()[a1].as_signed_long())
  433. s.reset()
  434.  
  435.  
  436. s.add(8 * (((8 * (4 * (4 * (28 * (6 * (32256 * a1 >> 1) - 28) + 37) + 24) % 15 + 34) - 21) >> 1) + 37) == 1488)
  437. s.add(a1 > 0)
  438. s.add(a1 < 256)
  439. s.add(a1 != 10)
  440. s.add(a1 !=13)
  441. s.add(a1 != 9)
  442. s.add(a1 != 11)
  443.  
  444. while s.check() == sat:
  445.     if chr(s.model()[a1].as_long()) in string.printable:
  446.         break
  447.  
  448.     s.add(a1 != s.model()[a1])
  449. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  450. flag += chr(s.model()[a1].as_signed_long())
  451. s.reset()
  452.  
  453. s.add(14 * (((4 * (4 * (10 * (1260 * (((32 * (a1 - 20) + 43) >> 1) - 6) - 21) - 29) - 28 + 16) - 6) >> 1) + 8) == 1850056166)
  454. s.add(a1 > 0)
  455. s.add(a1 < 256)
  456. s.add(a1 != 10)
  457. s.add(a1 !=13)
  458. s.add(a1 != 9)
  459. s.add(a1 != 11)
  460.  
  461. while s.check() == sat:
  462.     if chr(s.model()[a1].as_long()) in string.printable:
  463.         break
  464.  
  465.     s.add(a1 != s.model()[a1])
  466. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  467. flag += chr(s.model()[a1].as_signed_long())
  468. s.reset()
  469.  
  470. s.add((2 * (2 * (18 * (32 * (12 * (4 * (((((a1 - 17) >> 1) - 6) >> 1) + 17) - 28) - 11) + 10) - 19) - 32) + 51) << 7 == 379042688)
  471. s.add(a1 > 0)
  472. s.add(a1 < 256)
  473. s.add(a1 != 10)
  474. s.add(a1 !=13)
  475. s.add(a1 != 9)
  476. s.add(a1 != 11)
  477.  
  478. while s.check() == sat:
  479.     if chr(s.model()[a1].as_long()) in string.printable:
  480.         break
  481.  
  482.     s.add(a1 != s.model()[a1])
  483. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  484. flag += chr(s.model()[a1].as_signed_long())
  485. s.reset()
  486.  
  487. s.add(24 * (7 * ((5 * (225 * ((384 * (9 * (8 * (4 * ((4 * a1 >> 1) + 9) + 42) - 18) + 25) >> 1) - 14) - 27) % 13 >> 1) + 26) - 57 + 32) == 4104)
  488. s.add(a1 > 0)
  489. s.add(a1 < 256)
  490. s.add(a1 != 10)
  491. s.add(a1 !=13)
  492. s.add(a1 != 9)
  493. s.add(a1 != 11)
  494.  
  495. while s.check() == sat:
  496.     if chr(s.model()[a1].as_long()) in string.printable:
  497.         break
  498.  
  499.     s.add(a1 != s.model()[a1])
  500. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  501. flag += chr(s.model()[a1].as_signed_long())
  502. s.reset()
  503.  
  504. s.add(4 * ((40 * (4 * (4 * (16 * ((16 * (144 * (6 * (a1 >> 1) - 20 + 45) + 63) >> 1) + 34) >> 1) - 33) >> 1) - 8) >> 1) == 1919677264)
  505. s.add(a1 > 0)
  506. s.add(a1 < 256)
  507. s.add(a1 != 10)
  508. s.add(a1 !=13)
  509. s.add(a1 != 9)
  510. s.add(a1 != 11)
  511.  
  512. while s.check() == sat:
  513.     if chr(s.model()[a1].as_long()) in string.printable:
  514.         break
  515.  
  516.     s.add(a1 != s.model()[a1])
  517. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  518. flag += chr(s.model()[a1].as_signed_long())
  519. s.reset()
  520.  
  521. s.add(12 * (8 * ((2 * (((2 * (4 * a1 + 7) - 14) >> 1 << 6) + 32) - 9) >> 1) + 21) == 789276)
  522. s.add(a1 > 0)
  523. s.add(a1 < 256)
  524. s.add(a1 != 10)
  525. s.add(a1 !=13)
  526. s.add(a1 != 9)
  527. s.add(a1 != 11)
  528.  
  529. while s.check() == sat:
  530.     if chr(s.model()[a1].as_long()) in string.printable:
  531.         break
  532.  
  533.     s.add(a1 != s.model()[a1])
  534. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  535. flag += chr(s.model()[a1].as_signed_long())
  536. s.reset()
  537.  
  538. s.add(32 * (8 * (4 * ((4 * (6 * (8 * (3 * (7 * (4 * ((7 * (a1 + 19) + 17) >> 1) - 33 + 31) - 18) - 21) - 42) + 45) - 10) >> 1) - 7) >> 1) == 1951069824)
  539. s.add(a1 > 0)
  540. s.add(a1 < 256)
  541. s.add(a1 != 10)
  542. s.add(a1 !=13)
  543. s.add(a1 != 9)
  544. s.add(a1 != 11)
  545.  
  546. while s.check() == sat:
  547.     if chr(s.model()[a1].as_long()) in string.printable:
  548.         break
  549.  
  550.     s.add(a1 != s.model()[a1])
  551. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  552. flag += chr(s.model()[a1].as_signed_long())
  553. s.reset()
  554.  
  555. s.add((224 * (((6 * (9 * a1 + 31) + 19) << 6) + 13) - 17 + 28) >> 1 == 44435893)
  556. s.add(a1 > 0)
  557. s.add(a1 < 256)
  558. s.add(a1 != 10)
  559. s.add(a1 !=13)
  560. s.add(a1 != 9)
  561. s.add(a1 != 11)
  562.  
  563. while s.check() == sat:
  564.     if chr(s.model()[a1].as_long()) in string.printable:
  565.         break
  566.  
  567.     s.add(a1 != s.model()[a1])
  568. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  569. flag += chr(s.model()[a1].as_signed_long())
  570. s.reset()
  571.  
  572. s.add(28 * (((48 * (7 * (2 * (4 * (9 * (((8 * (3 * ((a1 - 5) >> 2) - 10) - 32) >> 1) + 17) + 12) + 7) - 28) + 60) + 4) >> 1) + 22) >> 1 == 44412144 )
  573. s.add(a1 > 0)
  574. s.add(a1 < 256)
  575. s.add(a1 != 10)
  576. s.add(a1 !=13)
  577. s.add(a1 != 9)
  578. s.add(a1 != 11)
  579.  
  580. while s.check() == sat:
  581.     if chr(s.model()[a1].as_long()) in string.printable:
  582.         break
  583.  
  584.     s.add(a1 != s.model()[a1])
  585. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  586. flag += chr(s.model()[a1].as_signed_long())
  587. s.reset()
  588.  
  589. s.add(4 * (7 * (8 * (2 * (6 * (5 * (8 * (4 * ((7 * (48 * (8 * (a1 - 34) - 33) + 19) >> 1) - 4) + 38) + 10) - 27) + 11) >> 1) + 7) % 5) == 12)
  590. s.add(a1 > 0)
  591. s.add(a1 < 256)
  592. s.add(a1 != 10)
  593. s.add(a1 !=13)
  594. s.add(a1 != 9)
  595. s.add(a1 != 11)
  596.  
  597. while s.check() == sat:
  598.     if chr(s.model()[a1].as_long()) in string.printable:
  599.         break
  600.  
  601.     s.add(a1 != s.model()[a1])
  602. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  603. flag += chr(s.model()[a1].as_signed_long())
  604. s.reset()
  605.  
  606. s.add(4 * (28 * (3 * (6 * (4 * (14 * (5 * ((9 * ((7 * ((12 * a1 - 25 + 33) >> 1) >> 1) - 8) + 31) >> 1) + 18) - 5 + 33) - 13) + 19) - 16 + 13) + 12) == 1732933488)
  607. s.add(a1 > 0)
  608. s.add(a1 < 256)
  609. s.add(a1 != 10)
  610. s.add(a1 !=13)
  611. s.add(a1 != 9)
  612. s.add(a1 != 11)
  613.  
  614. while s.check() == sat:
  615.     if chr(s.model()[a1].as_long()) in string.printable:
  616.         break
  617.  
  618.     s.add(a1 != s.model()[a1])
  619. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  620. flag += chr(s.model()[a1].as_signed_long())
  621. s.reset()
  622.  
  623. s.add(12 * (5 * (2 * (14 * (27 * (4 * (((9 * (a1 - 23 + 5) + 46) >> 1) + 50) + 9) + 19) + 25) + 49) + 3) == 87900216)
  624. s.add(a1 > 0)
  625. s.add(a1 < 256)
  626. s.add(a1 != 10)
  627. s.add(a1 !=13)
  628. s.add(a1 != 9)
  629. s.add(a1 != 11)
  630.  
  631. while s.check() == sat:
  632.     if chr(s.model()[a1].as_long()) in string.printable:
  633.         break
  634.  
  635.     s.add(a1 != s.model()[a1])
  636. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  637. flag += chr(s.model()[a1].as_signed_long())
  638. s.reset()
  639.  
  640. s.add(8 * (576 * (2 * (4 * ((4 * (2 * ((4 * (7 * (2 * a1 - 30 + 16) + 33) >> 1) - 12) - 32 + 49) >> 1) - 35) + 8) + 14) + 11) == 396168280)
  641. s.add(a1 > 0)
  642. s.add(a1 < 256)
  643. s.add(a1 != 10)
  644. s.add(a1 !=13)
  645. s.add(a1 != 9)
  646. s.add(a1 != 11)
  647.  
  648. while s.check() == sat:
  649.     if chr(s.model()[a1].as_long()) in string.printable:
  650.         break
  651.  
  652.     s.add(a1 != s.model()[a1])
  653. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  654. flag += chr(s.model()[a1].as_signed_long())
  655. s.reset()
  656.  
  657. s.add(7 * (5 * (2 * (4 * (144 * (4 * ((6 * (4 * (40 * (a1 >> 1) >> 1) >> 1) - 30 + 32) >> 1) - 22) + 2) + 17) + 7) + 35) == 308934080)
  658. s.add(a1 > 0)
  659. s.add(a1 < 256)
  660. s.add(a1 != 10)
  661. s.add(a1 !=13)
  662. s.add(a1 != 9)
  663. s.add(a1 != 11)
  664.  
  665. while s.check() == sat:
  666.     if chr(s.model()[a1].as_long()) in string.printable:
  667.         break
  668.  
  669.     s.add(a1 != s.model()[a1])
  670. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  671. flag += chr(s.model()[a1].as_signed_long())
  672. s.reset()
  673.  
  674. s.add(12 * ((16 * (2 * (8 * ((112 * (8 * (28 * (a1 + 32) >> 1) >> 2) >> 1) - 59) >> 1) >> 1) >> 1) + 7) == 77649876)
  675. s.add(a1 > 0)
  676. s.add(a1 < 256)
  677. s.add(a1 != 10)
  678. s.add(a1 !=13)
  679. s.add(a1 != 9)
  680. s.add(a1 != 11)
  681.  
  682. while s.check() == sat:
  683.     if chr(s.model()[a1].as_long()) in string.printable:
  684.         break
  685.  
  686.     s.add(a1 != s.model()[a1])
  687. print chr(s.model()[a1].as_signed_long()) + ' ' + str(s.model()[a1].as_long())
  688. flag += chr(s.model()[a1].as_signed_long())
  689. s.reset()
  690.  
  691. print flag.encode('base64')
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!