Как это решить с помощью z3?

Учитывая, что прошло некоторое время, я предполагаю, что уместно опубликовать (одно потенциальное) решение на случай, если люди найдут это в будущем:

from z3 import *

def get_decoded(target):
    """
    Helper function to "decode" a target string using Z3
    """

    #
    # We create a Z3 array for the contents of the string (this saves
    # needing have multiple copies of the "s[i]" variables.
    #
    # However, this could be less efficient, but this isn't a concern for this
    # puzzle
    #
    string = Array("string", BitVecSort(32), BitVecSort(32))

    #
    # We save a copy of the string as the "initial" string, as we need to
    # interrogate the string _before_ the updates are made
    #    
    initial_string = string

    #
    # Create a Z3 solver
    #
    s = Solver()

    #
    # We now iterate over the length of the "target" string, and construct the
    # encoding as per the CTF instance
    #
    for idx in range(len(target)):
        #
        # Extract the single character at "idx" from the target string
        #
        single_c = target[idx]

        #
        # Find its ASCII value
        #
        ord_val = ord(single_c)

        #
        # Generate the corresponding Z3 constant
        #
        ord_const = BitVecVal(ord_val, 32)

        #
        # Generate the cell position as a Z3 constant
        #
        cell_pos = BitVecVal(idx, 32)

        #
        # Calculate the non-conditional part of the update
        #
        add_rem = string[cell_pos] + SRem(string[cell_pos], 10)

        #
        # Calculate the conditional part of the update using a Z3 If
        #
        to_store = If(add_rem > 123, -100 - add_rem, add_rem)

        #
        # Update the string with our calculated value
        #
        string = Store(string, idx, to_store)

        #
        # Assert that our calculated position is equal to the input value
        #
        s.add(string[cell_pos] == BitVecVal(ord_val, 32))

    #
    # Check the SMT instance and obtain the model
    #
    assert s.check() == sat
    model = s.model()

    #
    # We now interrogate the model to find out what the "original" string was
    #
    output = []

    #
    # Output string is the same length as the input string
    #
    for idx in range(len(target)):
        #
        # As before, calculate the cell position
        #
        cell_pos = BitVecVal(idx, 32)

        #
        # Extract the value for the index in the string
        #
        model_val = model.eval(initial_string[cell_pos]).as_signed_long()

        #
        # Get the ASCII value (we've stored the ASCII integer value, not the
        # char!)
        #
        model_char = chr(model_val)

        #
        # Append it to our output string
        #
        output.append(model_char)

    #
    # Return the joined string
    #
    return "".join(output)


def get_encoded(value):
    """
    Helper function to "encode" a string using Python
    """

    output = []

    #
    # Iterate over the input string
    #
    for idx in range(len(value)):
        #
        # Value at position (as ASCII int)
        #
        ord_val = ord(value[idx])

        #
        # Value we're going to store
        #  
        to_store = ord_val + ord_val % 10

        #
        # Conditional check
        #
        if to_store > 123:

            #
            # As per the CTF
            #
            to_store = -100 - to_store

        #
        # Add it to the output string
        #
        output.append(chr(to_store))

    #
    # Return it
    #
    return "".join(output)


if __name__ == "__main__":
    """
    Entry point
    """

    #
    # String we're aiming for
    #
    target = "H0Tf00D:<"
    print "Target:                   \"{:s}\"".format(target)

    #
    # Calculate the "reverse" using Z3
    #
    decoded = get_decoded(target)
    print "Decoded (via z3):         \"{:s}\"".format(decoded)

    #
    # We now re-encode
    #
    encoded = get_encoded(decoded)
    print "Encoded (via Python):     \"{:s}\"".format(encoded)

    #
    # Both strings should be equal
    #
    assert encoded == target

# EOF