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) Guess the shortest string and Write the z3 smt solver code that provides it. ***If it is not tested and doesn't output correct value, I'll Downvote directly