How to use the smt.boolean.Symbol function in smt

while not terminated:
            read_address = self.address + bv.Constant(self.address.size, index)
            byte = self.state.read(read_address, 8)

            if self.state.solver.check(byte.can_be_nonzero()):
                if byte.symbolic:
                    if not constraint.symbolic:
                        constraint = (byte != 0)
                    else:
                        # not sure that I've implemented &= in smt
                        constraint = constraint & (byte != 0)

                    # this might look silly, but it actually makes the
                    # output smt formulae substantially smaller...

                    returned_constraint = bl.Symbol(unique_name('string_length'))
                    self.state.solver.add(returned_constraint == constraint)
                    yield (byte, returned_constraint)
                else:
                    yield (byte, constraint)
            else:
                terminated = True
                yield (bv.Constant(8, 0), constraint)
            index += 1

s_ = s

        count = 0
        null = bv.Constant(ptr.size, 0)
        bytes = []

        not_terminated = None
        not_already_terminated = bl.Constant(True)
        while s_.solver.check(num > count):
            byte = s_.read(ptr + bv.Constant(ptr.size, count), 8)

            not_terminated = not_already_terminated & (byte == value)
            bytes.append((not_already_terminated, byte, count))

            if not_terminated.symbolic:
                not_already_terminated = bl.Symbol(unique_name('tmp'))
                s_.solver.add(not_already_terminated == not_terminated)
            else:
                not_already_terminated = not_terminated

            count += 1

        bytes.reverse()

        result = None
        prev_result = None
        for (not_already_terminated, byte, count) in bytes:
            if result is None:
                result = bv.if_then_else(
                            byte == value,
                            ptr + bv.Constant(ptr.size, count),
                            null)

zero = bv.Constant(ptr1.size, 0)

    bytes = []

    not_terminated = None
    not_already_terminated = bl.Constant(True)
    while s.solver.check(num > count):
        byte1 = s.read(ptr1 + bv.Constant(ptr1.size, count), 8)
        byte2 = s.read(ptr2 + bv.Constant(ptr2.size, count), 8)

        not_terminated = not_already_terminated & (byte1 == byte2)

        bytes.append((not_already_terminated, byte1, byte2))

        if not_terminated.symbolic:
            not_already_terminated = bl.Symbol(unique_name('tmp'))
            s.solver.add(not_already_terminated == not_terminated)
        else:
            not_already_terminated = not_terminated

        count += 1

    bytes.reverse()

    result = None
    prev_result = None
    for (not_already_terminated, byte1, byte2) in bytes:
        if result is None:
            result = bv.if_then_else(
                        byte1 == byte2,
                        zero,
                        bv.if_then_else(