from z3 import *
# Create a Z3 solver
solver = Solver()
# Create an array of integer variables to represent the elements of a1
a1 = [Int(f'a1[{i}]') for i in range(32)]
print(a1)
# Define the constraints based on the C code
constraints = [
1629056 * a1[0] == 166163712,
6771600 * a1[1] == 731332800,
3682944 * a1[2] == 357245568,
10431000 * a1[3] == 1074393000,
3977328 * a1[4] == 489211344,
5138336 * a1[5] == 518971936,
7532250 * a1[7] == 406741500,
5551632 * a1[8] == 294236496,
3409728 * a1[9] == 177305856,
13013670 * a1[10] == 650683500,
6088797 * a1[11] == 298351053,
7884663 * a1[12] == 386348487,
8944053 * a1[13] == 438258597,
5198490 * a1[14] == 249527520,
4544518 * a1[15] == 445362764,
3645600 * a1[17] == 174988800,
10115280 * a1[16] == 981182160,
9667504 * a1[18] == 493042704,
5364450 * a1[19] == 257493600,
13464540 * a1[20] == 767478780,
5488432 * a1[21] == 312840624,
14479500 * a1[22] == 1404511500,
6451830 * a1[23] == 316139670,
6252576 * a1[24] == 619005024,
7763364 * a1[25] == 372641472,
7327320 * a1[26] == 373693320,
8741520 * a1[27] == 498266640,
8871876 * a1[28] == 452465676,
4086720 * a1[29] == 208422720,
9374400 * a1[30] == 515592000,
5759124 * a1[31] == 719890500
]
# Add the constraints to the solver
solver.add(constraints)
# Check if there is a solution
if solver.check() == sat:
model = solver.model()
# Get the values of a1 that satisfy the constraints
#solution = [model[a1[i]].as_long() for i in range(32)]
print("Solution for a1:", model)
for i in range(32):
print(f"a1[{i}] = {model[a1[i]]}")
else:
print("No solution found.")
a1 = [0]*32
a1[0] = 102
a1[1] = 108
a1[2] = 97
a1[3] = 103
a1[4] = 123
a1[5] = 101
a1[6] = 49 #出题人没给,出题人傻逼来
a1[7] = 54
a1[8] = 53
a1[9] = 52
a1[10] = 50
a1[11] = 49
a1[12] = 49
a1[13] = 49
a1[14] = 48
a1[15] = 98
a1[16] = 97
a1[17] = 48
a1[18] = 51
a1[19] = 48
a1[20] = 57
a1[21] = 57
a1[22] = 97
a1[23] = 49
a1[24] = 99
a1[25] = 48
a1[26] = 51
a1[27] = 57
a1[28] = 51
a1[29] = 51
a1[30] = 55
a1[31] = 125
result = ""
for x in range(32):
#print(type(a1[x]))
result += chr(a1[x])
print(result)
文章来源地址https://www.toymoban.com/news/detail-739068.html
文章来源:https://www.toymoban.com/news/detail-739068.html
到了这里,关于[GUET-CTF2019]re的文章就介绍完了。如果您还想了解更多内容,请在右上角搜索TOY模板网以前的文章或继续浏览下面的相关文章,希望大家以后多多支持TOY模板网!