How to use the mythril.analysis.solver.get_transaction_sequence function in mythril

for annotation in state_annotation.overflowing_state_annotations:

            log.debug(
                "Checking overflow in {} at transaction end address {}, ostate address {}".format(
                    state.get_current_instruction()["opcode"],
                    state.get_current_instruction()["address"],
                    annotation.address,
                )
            )

            try:

                constraints = state.mstate.constraints + annotation.constraint

                transaction_sequence = solver.get_transaction_sequence(
                    state, constraints
                )
            except UnsatError:
                continue

            _type = "Underflow" if annotation.operator == "subtraction" else "Overflow"
            issue = Issue(
                contract=state.environment.active_account.contract_name,
                function_name=annotation.function_name,
                address=annotation.address,
                swc_id=INTEGER_OVERFLOW_AND_UNDERFLOW,
                bytecode=state.environment.code.bytecode,
                title=self._get_title(_type),
                severity="High",
                description_head=self._get_description_head(annotation, _type),
                description_tail=self._get_description_tail(annotation, _type),

[a for a in state.get_annotations(UncheckedRetvalAnnotation)],
        )
        if len(annotations) == 0:
            state.annotate(UncheckedRetvalAnnotation())
            annotations = cast(
                List[UncheckedRetvalAnnotation],
                [a for a in state.get_annotations(UncheckedRetvalAnnotation)],
            )

        retvals = annotations[0].retvals

        if instruction["opcode"] in ("STOP", "RETURN"):
            issues = []
            for retval in retvals:
                try:
                    transaction_sequence = solver.get_transaction_sequence(
                        state, state.world_state.constraints + [retval["retval"] == 0]
                    )
                except UnsatError:
                    continue

                description_tail = (
                    "External calls return a boolean value. If the callee contract halts with an exception, 'false' is "
                    "returned and execution continues in the caller. It is usually recommended to wrap external calls "
                    "into a require statement to prevent unexpected states."
                )

                issue = Issue(
                    contract=state.environment.active_account.contract_name,
                    function_name=state.environment.active_function_name,
                    address=retval["address"],
                    bytecode=state.environment.code.bytecode,

swc_id = DEPRECATED_FUNCTIONS_USAGE

        elif instruction["opcode"] == "CALLCODE":
            log.debug("CALLCODE in function " + state.environment.active_function_name)
            title = "Use of callcode"
            description_head = "Use of callcode is deprecated."
            description_tail = (
                "The callcode method executes code of another contract in the context of the caller account. "
                "Due to a bug in the implementation it does not persist sender and value over the call. It was "
                "therefore deprecated and may be removed in the future. Use the delegatecall method instead."
            )
            swc_id = DEPRECATED_FUNCTIONS_USAGE
        else:
            return []
        try:
            transaction_sequence = get_transaction_sequence(
                state, state.mstate.constraints
            )
        except UnsatError:
            return []
        issue = Issue(
            contract=state.environment.active_account.contract_name,
            function_name=state.environment.active_function_name,
            address=instruction["address"],
            title=title,
            bytecode=state.environment.code.bytecode,
            swc_id=swc_id,
            severity="Medium",
            description_head=description_head,
            description_tail=description_tail,
            gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
            transaction_sequence=transaction_sequence,

state.annotate(MultipleSendsAnnotation())
            annotations = cast(
                List[MultipleSendsAnnotation],
                list(state.get_annotations(MultipleSendsAnnotation)),
            )

        call_offsets = annotations[0].call_offsets

        if instruction["opcode"] in ["CALL", "DELEGATECALL", "STATICCALL", "CALLCODE"]:
            call_offsets.append(state.get_current_instruction()["address"])

        else:  # RETURN or STOP

            for offset in call_offsets[1:]:
                try:
                    transaction_sequence = get_transaction_sequence(
                        state, state.world_state.constraints
                    )
                except UnsatError:
                    continue
                description_tail = (
                    "This call is executed after a previous call in the same transaction. "
                    "Try to isolate each call, transfer or send into its own transaction."
                )

                issue = Issue(
                    contract=state.environment.active_account.contract_name,
                    function_name=state.environment.active_function_name,
                    address=offset,
                    swc_id=MULTIPLE_SENDS,
                    bytecode=state.environment.code.bytecode,
                    title="Multiple Calls in a Single Transaction",

for tx in state.world_state.transaction_sequence:
            if not isinstance(tx, ContractCreationTransaction):
                constraints.append(tx.caller == ATTACKER_ADDRESS)

        try:
            try:
                transaction_sequence = solver.get_transaction_sequence(
                    state,
                    state.mstate.constraints + constraints + [to == ATTACKER_ADDRESS],
                )
                description_tail = (
                    "Anyone can kill this contract and withdraw its balance to an arbitrary "
                    "address."
                )
            except UnsatError:
                transaction_sequence = solver.get_transaction_sequence(
                    state, state.mstate.constraints + constraints
                )
                description_tail = "Arbitrary senders can kill this contract."

            issue = Issue(
                contract=state.environment.active_account.contract_name,
                function_name=state.environment.active_function_name,
                address=instruction["address"],
                swc_id=UNPROTECTED_SELFDESTRUCT,
                bytecode=state.environment.code.bytecode,
                title="Unprotected Selfdestruct",
                severity="High",
                description_head=description_head,
                description_tail=description_tail,
                transaction_sequence=transaction_sequence,
                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),

def check_potential_issues(state: GlobalState) -> None:
    """
    Called at the end of a transaction, checks potential issues, and
    adds valid issues to the detector.

    :param state: The final global state of a transaction
    :return:
    """
    annotation = get_potential_issues_annotation(state)
    for potential_issue in annotation.potential_issues:
        try:
            transaction_sequence = get_transaction_sequence(
                state, state.world_state.constraints + potential_issue.constraints
            )
        except UnsatError:
            continue

        annotation.potential_issues.remove(potential_issue)
        potential_issue.detector.cache.add(potential_issue.address)
        potential_issue.detector.issues.append(
            Issue(
                contract=potential_issue.contract,
                function_name=potential_issue.function_name,
                address=potential_issue.address,
                title=potential_issue.title,
                bytecode=potential_issue.bytecode,
                swc_id=potential_issue.swc_id,
                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),

def _analyze_state(state):
        """

        :param state:
        :return:
        """

        jump_dest = state.mstate.stack[-1]
        if jump_dest.symbolic is False:
            return []
        # Most probably the jump destination can have multiple locations in these circumstances
        try:
            transaction_sequence = get_transaction_sequence(
                state, state.world_state.constraints
            )
        except UnsatError:
            return []
        issue = Issue(
            contract=state.environment.active_account.contract_name,
            function_name=state.environment.active_function_name,
            address=state.get_current_instruction()["address"],
            swc_id=ARBITRARY_JUMP,
            title="Jump to an arbitrary instruction",
            severity="Medium",
            bytecode=state.environment.code.bytecode,
            description_head="The caller can jump to any point in the code.",
            description_tail="This can lead to unintended consequences."
            "Please avoid using low level code as much as possible",
            gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),

return None
        constraints = Constraints()
        gas = self.call_state.mstate.stack[-1]
        to = self.call_state.mstate.stack[-2]
        constraints += [
            UGT(gas, symbol_factory.BitVecVal(2300, 256)),
            Or(
                to > symbol_factory.BitVecVal(16, 256),
                to == symbol_factory.BitVecVal(0, 256),
            ),
        ]
        if self.user_defined_address:
            constraints += [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF]

        try:
            solver.get_transaction_sequence(
                global_state, constraints + global_state.mstate.constraints
            )
        except UnsatError:
            return None

        severity = "Medium" if self.user_defined_address else "Low"
        address = global_state.get_current_instruction()["address"]
        logging.debug(
            "[EXTERNAL_CALLS] Detected state changes at addresses: {}".format(address)
        )
        description_head = (
            "The contract account state is changed after an external call. "
        )
        description_tail = (
            "Consider that the called contract could re-enter the function before this "
            "state change takes place. This can lead to business logic vulnerabilities."

:return:
        """
        log.debug("ASSERT_FAIL in function " + state.environment.active_function_name)

        try:
            address = state.get_current_instruction()["address"]

            description_tail = (
                "It is possible to trigger an exception (opcode 0xfe). "
                "Exceptions can be caused by type errors, division by zero, "
                "out-of-bounds array access, or assert violations. "
                "Note that explicit `assert()` should only be used to check invariants. "
                "Use `require()` for regular input checking."
            )

            transaction_sequence = solver.get_transaction_sequence(
                state, state.mstate.constraints
            )

            issue = Issue(
                contract=state.environment.active_account.contract_name,
                function_name=state.environment.active_function_name,
                address=address,
                swc_id=ASSERT_VIOLATION,
                title="Exception State",
                severity="Low",
                description_head="A reachable exception has been detected.",
                description_tail=description_tail,
                bytecode=state.environment.code.bytecode,
                transaction_sequence=transaction_sequence,
                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
            )