Given is the following function: bool check (char * str, uint64_t len) { uint64_t v = 0; for (uint64_t i=0; i < len; i++) { if (str[i] == "-") { 1v -= 1; } else if (str[i] == "*") { v *= 2; } else { return 0; } } return v == 0xffffffffbadc0de0; } Use an SMT solver (z3 python solver) to find the shortest string s, such that check(s, len(s)) returns true. For this, use the provided template control_flow.py. Make sure to print your result. Note: You can use the function check_python to verify your input. Template Code: from z3 import * def check_python(s, l): v = 0 for i in xrange(l): if s[i] == "-": v -= 1 elif s[i] == "*": v *= 2 else: return 0 return v % (2 ** 64) == 0xffffffffbadc0de0 # todo check_sat def check_sat(s, l): pass # todo main solver = Solver() """ 1. Hint: Fixate length manually length = 10 2. Hint: Build byte input string input_str = [BitVec("s" + str(i), 8) for i in range(length)] 3. Hint: ord('+')` returns the ASCII value of "+". 4. Hint: "".join(map(chr, [solver.model()[c].as_long() for c in input_str])) parses the input string from the model """ print(solution) Write the z3 smt solver code. If it is not tested and doesn't output correct value, I'll Downvote directly