How to use the mythril.laser.smt.If function in mythril

try:
            # Attempt to concretize value
            if isinstance(value, bool):
                _bytes = (
                    int(1).to_bytes(32, byteorder="big")
                    if value
                    else int(0).to_bytes(32, byteorder="big")
                )
            else:
                _bytes = util.concrete_int_to_bytes(value)
            assert len(_bytes) == 32
            self[index : index + 32] = list(bytearray(_bytes))
        except (Z3Exception, AttributeError):  # BitVector or BoolRef
            value = cast(Union[BitVec, Bool], value)
            if isinstance(value, Bool):
                value_to_write = If(
                    value,
                    symbol_factory.BitVecVal(1, 256),
                    symbol_factory.BitVecVal(0, 256),
                )
            else:
                value_to_write = value
            assert value_to_write.size() == 256

            for i in range(0, value_to_write.size(), 8):
                self[index + 31 - (i // 8)] = Extract(i + 7, i, value_to_write)

"""
        Merge storage
        :param storage1: To storage to merge into
        :param storage2: To storage to merge with
        :param path_condition: The constraint for this storage to be executed
        :return:
        """
        storage1._standard_storage = If(
            path_condition, storage1._standard_storage, storage2._standard_storage
        )
        storage1.storage_keys_loaded = storage1.storage_keys_loaded.union(
            storage2.storage_keys_loaded
        )
        for key, value in storage2.printable_storage.items():
            if key in storage1.printable_storage:
                storage1.printable_storage[key] = If(
                    path_condition, storage1.printable_storage[key], value
                )
            else:
                storage1.printable_storage[key] = value

expr_item = (
            symbol_factory.BitVecVal(item, 256) if isinstance(item, int) else item
        )  # type: BitVec

        symbolic_base_value = If(
            expr_item >= self._size,
            symbol_factory.BitVecVal(0, 8),
            BitVec(
                symbol_factory.BitVecSym(
                    "{}_calldata_{}".format(self.tx_id, str(item)), 8
                )
            ),
        )
        return_value = symbolic_base_value
        for r_index, r_value in self._reads:
            return_value = If(r_index == expr_item, r_value, return_value)
        if not clean:
            self._reads.append((expr_item, symbolic_base_value))
        return simplify(return_value)

def merge_storage(storage1: Storage, storage2: Storage, path_condition: Bool):
        """
        Merge storage
        :param storage1: To storage to merge into
        :param storage2: To storage to merge with
        :param path_condition: The constraint for this storage to be executed
        :return:
        """
        storage1._standard_storage = If(
            path_condition, storage1._standard_storage, storage2._standard_storage
        )
        storage1.storage_keys_loaded = storage1.storage_keys_loaded.union(
            storage2.storage_keys_loaded
        )
        for key, value in storage2.printable_storage.items():
            if key in storage1.printable_storage:
                storage1.printable_storage[key] = If(
                    path_condition, storage1.printable_storage[key], value
                )
            else:
                storage1.printable_storage[key] = value

def merge_states(self, state1: WorldState, state2: WorldState):
        """
        Merge state2 into state1
        :param state1: The state to be merged into
        :param state2: The state which is merged into state1
        :return:
        """

        # Merge constraints
        state1.constraints, condition1, _ = self._merge_constraints(
            state1.constraints, state2.constraints
        )

        # Merge balances
        state1.balances = cast(Array, If(condition1, state1.balances, state2.balances))
        state1.starting_balances = cast(
            Array, If(condition1, state1.starting_balances, state2.starting_balances)
        )

        # Merge accounts
        for address, account in state2.accounts.items():
            if address not in state1._accounts:
                state1.put_account(account)
            else:
                self.merge_accounts(
                    state1._accounts[address], account, condition1, state1.balances
                )

        # Merge annotations
        self._merge_annotations(state1, state2)

def and_(self, global_state: GlobalState) -> List[GlobalState]:
        """

        :param global_state:
        :return:
        """
        stack = global_state.mstate.stack
        op1, op2 = stack.pop(), stack.pop()
        if isinstance(op1, Bool):
            op1 = If(
                op1, symbol_factory.BitVecVal(1, 256), symbol_factory.BitVecVal(0, 256)
            )
        if isinstance(op2, Bool):
            op2 = If(
                op2, symbol_factory.BitVecVal(1, 256), symbol_factory.BitVecVal(0, 256)
            )
        if not isinstance(op1, Expression):
            op1 = symbol_factory.BitVecVal(op1, 256)
        if not isinstance(op2, Expression):
            op2 = symbol_factory.BitVecVal(op2, 256)
        stack.append(op1 & op2)

        return [global_state]

:param global_state:
        :return:
        """
        state = global_state.mstate

        op1 = state.stack.pop()
        op2 = state.stack.pop()

        if isinstance(op1, Bool):
            op1 = If(
                op1, symbol_factory.BitVecVal(1, 256), symbol_factory.BitVecVal(0, 256)
            )

        if isinstance(op2, Bool):
            op2 = If(
                op2, symbol_factory.BitVecVal(1, 256), symbol_factory.BitVecVal(0, 256)
            )

        exp = op1 == op2

        state.stack.append(exp)
        return [global_state]