diff --git a/package/version b/package/version
index 74799d81f..f31857478 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.127
+0.1.128
diff --git a/poetry.lock b/poetry.lock
index b5aff083e..0f9911c92 100644
--- a/poetry.lock
+++ b/poetry.lock
@@ -1,4 +1,4 @@
-# This file is automatically @generated by Poetry 1.7.1 and should not be changed by hand.
+# This file is automatically @generated by Poetry 1.6.1 and should not be changed by hand.
 
 [[package]]
 name = "attrs"
@@ -447,8 +447,8 @@ tomlkit = "^0.11.6"
 [package.source]
 type = "git"
 url = "https://github.com/runtimeverification/evm-semantics.git"
-reference = "v1.0.427"
-resolved_reference = "47876048fd96126b87919963fad1d8cdca2943c6"
+reference = "symbolic-calldata-gen"
+resolved_reference = "72299152e8c54219e9baa33ed16b8306d22c8dcc"
 subdirectory = "kevm-pyk"
 
 [[package]]
diff --git a/pyproject.toml b/pyproject.toml
index c0e9ddc51..ac365f23d 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.127"
+version = "0.1.128"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
@@ -12,7 +12,7 @@ authors = [
 
 [tool.poetry.dependencies]
 python = "^3.10"
-kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.427", subdirectory = "kevm-pyk" }
+kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", branch = "dynamic-tuple", subdirectory = "kevm-pyk" }
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index aa3eeed83..9b57bcc06 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.127'
+VERSION: Final = '0.1.128'
diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index b730acc9c..fc3f03716 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -245,7 +245,7 @@ def custom_view(self, contract_name: str, element: KCFGElem) -> Iterable[str]:
 
     def build(self) -> None:
         try:
-            run_process(['forge', 'build', '--root', str(self._root)], logger=_LOGGER)
+            run_process(['forge', 'build', '--root', str(self._root), '--extra-output', 'devdoc'], logger=_LOGGER)
         except FileNotFoundError:
             print("Error: 'forge' command not found. Please ensure that 'forge' is installed and added to your PATH.")
             sys.exit(1)
diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md
index ec3e4cb1f..c44ab1f6a 100644
--- a/src/kontrol/kdist/cheatcodes.md
+++ b/src/kontrol/kdist/cheatcodes.md
@@ -345,6 +345,7 @@ The `<output>` cell will be updated with the value of the address generated from
          <k> #call_foundry SELECTOR ARGS => . ... </k>
          <output> _ => #bufStrict(32, #addrFromPrivateKey(#unparseDataBytes(ARGS))) </output>
       requires SELECTOR ==Int selector ( "addr(uint256)" )
+      [preserves-definedness]
 ```
 
 #### `load` - Loads a storage slot from an address.
@@ -896,6 +897,7 @@ The `ECDSASign` function returns the signed data in [r,s,v] form, which we conve
          <k> #call_foundry SELECTOR ARGS => . ... </k>
          <output> _ => #sign(#range(ARGS, 32, 32),#range(ARGS,0,32)) </output>
       requires SELECTOR ==Int selector ( "sign(uint256,bytes32)" )
+      [preserves-definedness]
 ```
 
 Otherwise, throw an error for any other call to the Foundry contract.
@@ -943,6 +945,7 @@ Utils
            <code> _ => #if #asWord(CODE) ==Int 0 #then .Bytes #else CODE #fi </code>
            ...
          </account>
+    [preserves-definedness]
 ```
 
 - `#returnNonce ACCTID` takes the nonce of a given account and places it on the `<output>` cell.
@@ -997,6 +1000,7 @@ Utils
            <storage> STORAGE => STORAGE [ LOC <- VALUE ] </storage>
              ...
          </account>
+    [preserves-definedness]
 ```
 
 `#setSymbolicStorage ACCTID` takes a given account and makes its storage fully symbolic.
diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index 61b87d0c3..9124a9699 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -478,6 +478,10 @@ def _update_cterm_from_node(cterm: CTerm, node: KCFG.Node, contract_name: str) -
     new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'GAS_CELL', gas_cell), [])
     new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'CALLGAS_CELL', callgas_cell), [])
 
+    # adding constraints from the initial cterm
+    for constraint in cterm.constraints:
+        new_init_cterm = new_init_cterm.add_constraint(constraint)
+
     return new_init_cterm
 
 
diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py
index f9d96cf14..6a012bd0e 100644
--- a/src/kontrol/solc_to_k.py
+++ b/src/kontrol/solc_to_k.py
@@ -15,7 +15,7 @@
 from pyk.kast.outer import KDefinition, KFlatModule, KImport, KNonTerminal, KProduction, KRequire, KRule, KTerminal
 from pyk.kdist import kdist
 from pyk.prelude.kbool import TRUE, andBool
-from pyk.prelude.kint import intToken
+from pyk.prelude.kint import eqInt, intToken
 from pyk.prelude.string import stringToken
 from pyk.utils import FrozenDict, hash_str, run_process, single
 
@@ -71,36 +71,79 @@ class Input:
     type: str
     components: tuple[Input, ...] = ()
     idx: int = 0
+    array_lengths: list[int] | None = None
+    dynamic_type_length: int | None = None
+
+    @cached_property
+    def arg_name(self) -> str:
+        return f'V{self.idx}_{self.name.replace("-", "_")}'
 
     @staticmethod
-    def from_dict(input: dict, idx: int = 0) -> Input:
+    def from_dict(input: dict, idx: int = 0, natspec_lengths: dict | None = None) -> Input:
         name = input['name']
         type = input['type']
-        if input.get('components') is not None and input['type'] != 'tuple[]':
-            return Input(name, type, tuple(Input._unwrap_components(input['components'], idx)), idx)
+        array_lengths, dynamic_type_length = (
+            get_input_length(input, natspec_lengths) if natspec_lengths is not None else (None, None)
+        )
+        if input.get('components') is not None:
+            _v = Input(
+                name,
+                type,
+                tuple(Input._unwrap_components(input['components'], idx, natspec_lengths)),
+                idx,
+                array_lengths,
+                dynamic_type_length,
+            )
         else:
-            return Input(name, type, idx=idx)
-
-    @staticmethod
-    def arg_name(input: Input) -> str:
-        return f'V{input.idx}_{input.name.replace("-", "_")}'
+            _v = Input(name, type, idx=idx, array_lengths=array_lengths, dynamic_type_length=dynamic_type_length)
+        return _v
 
     @staticmethod
     def _make_single_type(input: Input) -> KApply:
-        input_name = Input.arg_name(input)
-        input_type = input.type
-        return KEVM.abi_type(input_type, KVariable(input_name))
+        if input.type.endswith('[]'):
+            base_type = input.type.split('[')[0]
+            # TODO: support nested array processing
+            if input.array_lengths is None:
+                raise ValueError(f'Array length bounds missing for {input.name}')
+            array_length = input.array_lengths[0]
+            args: list[KInner] = []
+            if base_type == 'tuple':
+                args = [Input._make_tuple_type(input.components, _index) for _index in range(0, array_length)]
+            else:
+                array_elements = [Input(f'{input.name}_{n}', base_type, idx=input.idx) for n in range(array_length)]
+                args = Input._make_array_elements(array_elements)
+
+            return KEVM.abi_array(
+                args[0],
+                intToken(array_length),
+                args,
+            )
+
+        else:
+            input_name = input.arg_name
+            input_type = input.type
+            return KEVM.abi_type(input_type, KVariable(input_name))
 
     @staticmethod
-    def _make_complex_type(components: Iterable[Input]) -> KApply:
+    def _make_tuple_type(components: Iterable[Input], inner_index: int | None = None) -> KApply:
         """
-        recursively unwrap components in arguments of complex types and convert them to KEVM types
+        recursively unwrap components of a tuple and convert them to KEVM types
+        inner_index is used for array of tuples
         """
         abi_types: list[KInner] = []
         for comp in components:
+            if inner_index is not None:
+                comp = Input(
+                    f'{comp.name}_{inner_index}',
+                    comp.type,
+                    comp.components,
+                    idx=comp.idx,
+                    array_lengths=comp.array_lengths,
+                    dynamic_type_length=comp.dynamic_type_length,
+                )
             # nested tuple, unwrap its components
             if comp.type == 'tuple':
-                tuple = Input._make_complex_type(comp.components)
+                tuple = Input._make_tuple_type(comp.components, inner_index)
                 abi_type = tuple
             else:
                 abi_type = Input._make_single_type(comp)
@@ -108,7 +151,19 @@ def _make_complex_type(components: Iterable[Input]) -> KApply:
         return KEVM.abi_tuple(abi_types)
 
     @staticmethod
-    def _unwrap_components(components: dict, i: int = 0) -> list[Input]:
+    def _make_array_elements(elements: Iterable[Input]) -> list[KInner]:
+        """
+        recursively unwrap components in arguments of complex types and convert them to KEVM types
+        """
+        abi_types: list[KInner] = []
+        for el in elements:
+            # TODO(palina): support nested arrays
+            abi_type = Input._make_single_type(el)
+            abi_types.append(abi_type)
+        return abi_types
+
+    @staticmethod
+    def _unwrap_components(components: dict, i: int = 0, natspec_lengths: dict | None = None) -> list[Input]:
         """
         recursively unwrap components in arguments of complex types
         """
@@ -116,17 +171,20 @@ def _unwrap_components(components: dict, i: int = 0) -> list[Input]:
         for comp in components:
             _name = comp['name']
             _type = comp['type']
-            if comp.get('components') is not None and type != 'tuple[]':
-                new_comps = Input._unwrap_components(comp['components'], i)
+            arrays_length, dynamic_type_length = (
+                get_input_length(comp, natspec_lengths) if natspec_lengths is not None else (None, None)
+            )
+            if comp.get('components') is not None:  # and type != 'tuple[]':
+                new_comps = Input._unwrap_components(comp['components'], i, natspec_lengths)
             else:
                 new_comps = []
-            comps.append(Input(_name, _type, tuple(new_comps), i))
+            comps.append(Input(_name, _type, tuple(new_comps), i, arrays_length, dynamic_type_length))
             i += 1
         return comps
 
     def to_abi(self) -> KApply:
         if self.type == 'tuple':
-            return Input._make_complex_type(self.components)
+            return Input._make_tuple_type(self.components)
         else:
             return Input._make_single_type(self)
 
@@ -138,16 +196,77 @@ def flattened(self) -> list[Input]:
             return [self]
 
 
-def inputs_from_abi(abi_inputs: Iterable[dict]) -> list[Input]:
+def inputs_from_abi(abi_inputs: Iterable[dict], natspec_lengths: dict | None) -> list[Input]:
     inputs = []
-    i = 0
+    index = 0
     for input in abi_inputs:
-        cur_input = Input.from_dict(input, i)
+        cur_input = Input.from_dict(input, index, natspec_lengths)
         inputs.append(cur_input)
-        i += len(cur_input.flattened())
+        index += len(cur_input.flattened())
     return inputs
 
 
+def get_input_length(input_dict: dict, lengths: dict) -> tuple[list[int] | None, int | None]:
+    """
+    Reads from NatSpec comments the maximum length bound of an array, dynamic type, array of dynamic type, or nested arrays.
+    In case of arrays and nested arrays, the bound values are stored in a list.
+    In case of dynamic types such as `string` and `bytes` the length bound is stored in its own variable.
+    As a convention, the length of a nested array or of a dynamic type array is accessed by appending `[]` to the name of the variable.
+    i.e. for `bytes[][] _b`, the lengths are registered as:
+        _b: length of the upper most array
+        _b[]: length of the inner array
+        _b[][]: length of the `bytes` elements in the inner array.
+    If an array length is missing, the default value will be `2` to avoid generating symbolic variables.
+    The dynamic type length is optional, it's lack off will cause branchings in symbolic execution.
+    """
+    _name: str = input_dict['name']
+    _type: str = input_dict['type']
+    dynamic_type_length: int | None
+    input_array_lengths: list[int] | None
+    array_lengths: list[int] = []
+    while _type.endswith('[]'):
+        array_lengths.append(lengths.get(_name, 2))
+        _type = _type[:-2]
+        _name += '[]'
+    input_array_lengths = array_lengths if array_lengths else None
+    dynamic_type_length = lengths.get(_name) if _type in ['bytes', 'string'] else None
+    return (input_array_lengths, dynamic_type_length)
+
+
+def parse_devdoc(tag: str, devdoc: dict | None) -> dict:
+    """
+    Parses developer documentation (devdoc) to extract specific information based on a given tag.
+    Example:
+        If devdoc contains { 'custom:length': '_withdrawalProof 10,_withdrawalProof[] 600,_l2OutputIndex 4,'},
+        and the function is called with tag='custom:length', it would return:
+        { '_withdrawalProof': 10, '_withdrawalProof[]': 600, '_l2OutputIndex': 4 }
+    """
+
+    if devdoc is None or tag not in devdoc:
+        return {}
+
+    natspecs = {}
+    natspec_values = devdoc[tag]
+
+    # Split the string by comma and iterate over each part
+    for part in natspec_values.split(','):
+        # Trim whitespace and skip if empty
+        part = part.strip()
+        if not part:
+            continue
+
+        # Split each part into variable and length
+        try:
+            key, value_str = part.split(':')
+            # Trim whitespace from variable and length, and convert length to int
+            key = key.strip()
+            natspecs[key] = int(value_str.strip())
+        except ValueError:
+            # Handle cases where the split does not give exactly 2 items
+            _LOGGER.warning(f'Skipping invalid fomat {part} in {tag}')
+    return natspecs
+
+
 @dataclass
 class Contract:
     @dataclass
@@ -226,6 +345,7 @@ class Method:
         payable: bool
         signature: str
         ast: dict | None
+        natspec_values: dict | None
 
         def __init__(
             self,
@@ -237,11 +357,11 @@ def __init__(
             contract_digest: str,
             contract_storage_digest: str,
             sort: KSort,
+            devdoc: dict | None,
         ) -> None:
             self.signature = msig
             self.name = abi['name']
             self.id = id
-            self.inputs = tuple(inputs_from_abi(abi['inputs']))
             self.contract_name = contract_name
             self.contract_digest = contract_digest
             self.contract_storage_digest = contract_storage_digest
@@ -249,6 +369,8 @@ def __init__(
             # TODO: Check that we're handling all state mutability cases
             self.payable = abi['stateMutability'] == 'payable'
             self.ast = ast
+            self.natspec_values = parse_devdoc('custom:length', devdoc)
+            self.inputs = tuple(inputs_from_abi(abi['inputs'], self.natspec_values))
 
         @property
         def klabel(self) -> KLabel:
@@ -282,11 +404,38 @@ def flat_inputs(self) -> tuple[Input, ...]:
 
         @cached_property
         def arg_names(self) -> Iterable[str]:
-            return tuple(Input.arg_name(input) for input in self.flat_inputs)
+            arg_names: list[str] = []
+            for input in self.inputs:
+                if input.type.endswith('[]'):
+                    if input.array_lengths is None:
+                        raise ValueError(f'Array length bounds missing for {input.name}')
+                    _length = input.array_lengths[0]
+                    arg_names.extend(
+                        f'{sub_input.arg_name}_{i}' for i in range(_length) for sub_input in input.flattened()
+                    )
+                else:
+                    arg_names.extend([f'{sub_input.arg_name}' for sub_input in input.flattened()])
+            return tuple(arg_names)
 
         @cached_property
         def arg_types(self) -> Iterable[str]:
-            return tuple(input.type for input in self.flat_inputs)
+            arg_types: list[str] = []
+            for input in self.inputs:
+                if input.type.endswith('[]'):
+                    if input.array_lengths is None:
+                        raise ValueError(f'Array length bounds missing for {input.name}')
+                    _length = input.array_lengths[0]
+                    base_type = input.type.split('[')[0]
+                    if base_type == 'tuple':
+                        arg_types.extend(
+                            f'{sub_input.type}' for _i in range(_length) for sub_input in input.flattened()
+                        )
+                    else:
+                        arg_types.extend([base_type] * _length)
+
+                else:
+                    arg_types.extend([f'{sub_input.type}' for sub_input in input.flattened()])
+            return tuple(arg_types)
 
         def up_to_date(self, digest_file: Path) -> bool:
             if not digest_file.exists():
@@ -347,13 +496,20 @@ def production(self) -> KProduction:
 
         def rule(self, contract: KInner, application_label: KLabel, contract_name: str) -> KRule | None:
             prod_klabel = self.unique_klabel
+            arg_vars = []
             arg_vars = [KVariable(name) for name in self.arg_names]
             args: list[KInner] = []
             conjuncts: list[KInner] = []
             for input in self.inputs:
                 abi_type = input.to_abi()
                 args.append(abi_type)
-                rps = _range_predicates(abi_type)
+                rps = []
+                if input.type == 'tuple':
+                    for sub_input in input.components:
+                        _abi_type = sub_input.to_abi()
+                        rps.extend(_range_predicates(_abi_type, sub_input.dynamic_type_length))
+                else:
+                    rps = _range_predicates(abi_type, input.dynamic_type_length)
                 for rp in rps:
                     if rp is None:
                         _LOGGER.info(
@@ -375,6 +531,12 @@ def callvalue_cell(self) -> KInner:
             )
 
         def calldata_cell(self, contract: Contract) -> KInner:
+            args: list[KInner] = []
+
+            for input in self.inputs:
+                abi_type = input.to_abi()
+                args.append(abi_type)
+
             return KApply(contract.klabel_method, [KApply(contract.klabel), self.application])
 
         @cached_property
@@ -429,14 +591,32 @@ def __init__(self, contract_name: str, contract_json: dict, foundry: bool = Fals
         }
 
         _methods = []
+
+        # getting NatSpec comments
+        if 'metadata' in self.contract_json:
+            metadata = self.contract_json['metadata']
+            devdoc = metadata['output']['devdoc']['methods']
+
         for method in contract_json['abi']:
             if method['type'] == 'function':
                 msig = method_sig_from_abi(method)
                 method_selector: str = str(evm['methodIdentifiers'][msig])
                 mid = int(method_selector, 16)
                 method_ast = function_asts[method_selector] if method_selector in function_asts else None
+
+                # using relevant NatSpec comments in Method initialization
+                method_devdoc = devdoc[msig] if msig in devdoc else None
+
                 _m = Contract.Method(
-                    msig, mid, method, method_ast, self._name, self.digest, self.storage_digest, self.sort_method
+                    msig,
+                    mid,
+                    method,
+                    method_ast,
+                    self._name,
+                    self.digest,
+                    self.storage_digest,
+                    self.sort_method,
+                    method_devdoc,
                 )
                 _methods.append(_m)
             if method['type'] == 'constructor':
@@ -822,24 +1002,30 @@ def _evm_base_sort_int(type_label: str) -> bool:
     return success
 
 
-def _range_predicates(abi: KApply) -> list[KInner | None]:
+def _range_predicates(abi: KApply, dynamic_type_length: int | None = None) -> list[KInner | None]:
     rp: list[KInner | None] = []
     if abi.label.name == 'abi_type_tuple':
         if type(abi.args[0]) is KApply:
-            rp += _range_collection_predicates(abi.args[0])
+            rp += _range_collection_predicates(abi.args[0], dynamic_type_length)
+    elif abi.label.name == 'abi_type_array':
+        # array elements:
+        if type(abi.args[2]) is KApply:
+            rp += _range_collection_predicates(abi.args[2], dynamic_type_length)
     else:
         type_label = abi.label.name.removeprefix('abi_type_')
+        if type_label in ['bytes', 'string'] and dynamic_type_length is not None:
+            rp.append(eqInt(KEVM.size_bytes(single(abi.args)), intToken(dynamic_type_length)))
         rp.append(_range_predicate(single(abi.args), type_label))
     return rp
 
 
-def _range_collection_predicates(abi: KApply) -> list[KInner | None]:
+def _range_collection_predicates(abi: KApply, dynamic_type_length: int | None = None) -> list[KInner | None]:
     rp: list[KInner | None] = []
     if abi.label.name == '_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs':
         if type(abi.args[0]) is KApply:
-            rp += _range_predicates(abi.args[0])
+            rp += _range_predicates(abi.args[0], dynamic_type_length)
         if type(abi.args[1]) is KApply:
-            rp += _range_collection_predicates(abi.args[1])
+            rp += _range_collection_predicates(abi.args[1], dynamic_type_length)
     elif abi.label.name == '.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs':
         return rp
     else:
@@ -854,7 +1040,8 @@ def _range_predicate(term: KInner, type_label: str) -> KInner | None:
         case 'bool':
             return KEVM.range_bool(term)
         case 'bytes':
-            return KEVM.range_uint(128, KEVM.size_bytes(term))
+            #  the compiler-inserted check asserts that lengthBytes(B) <= maxUint64
+            return KEVM.range_uint(64, KEVM.size_bytes(term))
         case 'string':
             return TRUE
 
diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected
index 659607f98..08117724b 100644
--- a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected
+++ b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected
@@ -191,7 +191,7 @@ Node 18:
               0
             </refund>
             <accessedAccounts>
-              ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+              .Set
             </accessedAccounts>
             <accessedStorage>
               .Map
@@ -1252,7 +1252,7 @@ Node 18:
                      0
                    </refund>
                    <accessedAccounts>
-                     ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1447,7 +1447,7 @@ Node 18:
                      0
                    </refund>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1648,7 +1648,7 @@ Node 18:
                      0
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) => ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1853,7 +1853,7 @@ Node 18:
                      0
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -2156,7 +2156,7 @@ Node 18:
                      0
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     ( .Set => SetItem ( 728815563385977040452943777879061427756277306518 ) )
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -2437,7 +2437,7 @@ Node 18:
                      0
                    </memoryUsed>
                    <callGas>
-                     0
+                     CALLGAS_CELL:Gas
                    </callGas>
                    <static>
                      true
@@ -2457,7 +2457,7 @@ Node 18:
                      0
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     SetItem ( 728815563385977040452943777879061427756277306518 )
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -2738,7 +2738,7 @@ Node 18:
                      0
                    </memoryUsed>
                    <callGas>
-                     0
+                     CALLGAS_CELL:Gas
                    </callGas>
                    <static>
                      true
@@ -2758,7 +2758,7 @@ Node 18:
                      0
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     SetItem ( 728815563385977040452943777879061427756277306518 )
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -3042,7 +3042,7 @@ Node 18:
                      0
                    </memoryUsed>
                    <callGas>
-                     0
+                     CALLGAS_CELL:Gas
                    </callGas>
                    <static>
                      true
@@ -3062,7 +3062,7 @@ Node 18:
                      0
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     SetItem ( 728815563385977040452943777879061427756277306518 )
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -3368,7 +3368,7 @@ Node 18:
                      0
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     ( SetItem ( 728815563385977040452943777879061427756277306518 ) => .Set )
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -3573,7 +3573,7 @@ Node 18:
                      0
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -3779,7 +3779,7 @@ Node 18:
                      0
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected
index 36671d04a..22073d993 100644
--- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected
@@ -121,7 +121,7 @@ Node 7:
               0
             </refund>
             <accessedAccounts>
-              SetItem ( 645326474426547203313410069153905908525362434349 )
+              .Set
             </accessedAccounts>
             <accessedStorage>
               .Map
@@ -329,6 +329,7 @@ Node 7:
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -338,7 +339,7 @@ Node 7:
                      0
                    </refund>
                    <accessedAccounts>
-                     ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -546,6 +547,7 @@ Node 7:
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -555,7 +557,7 @@ Node 7:
                      0
                    </refund>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -767,6 +769,7 @@ Node 7:
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -776,7 +779,7 @@ Node 7:
                      0
                    </refund>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -988,6 +991,7 @@ Node 7:
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -997,7 +1001,7 @@ Node 7:
                      0
                    </refund>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1207,6 +1211,7 @@ Node 7:
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -1216,7 +1221,7 @@ Node 7:
                      0
                    </refund>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
diff --git a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
index 3c03327a2..fe1e47dd9 100644
--- a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
@@ -145,7 +145,7 @@ Node 10:
               SetItem ( 645326474426547203313410069153905908525362434349 )
             </accessedAccounts>
             <accessedStorage>
-              ( 728815563385977040452943777879061427756277306518 |-> SetItem ( 7 ) )
+              .Map
             </accessedStorage>
             ...
           </substate>
@@ -352,6 +352,7 @@ Node 10:
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -361,7 +362,7 @@ Node 10:
                      0
                    </refund>
                    <accessedAccounts>
-                     ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -569,6 +570,7 @@ Node 10:
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -578,7 +580,7 @@ Node 10:
                      0
                    </refund>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -791,6 +793,7 @@ Node 10:
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -800,7 +803,7 @@ Node 10:
                      0
                    </refund>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1011,6 +1014,7 @@ Node 10:
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -1020,7 +1024,7 @@ Node 10:
                      0
                    </refund>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1454,6 +1458,7 @@ Node 10:
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -1463,10 +1468,10 @@ Node 10:
                      0
                    </refund>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
                    </accessedAccounts>
                    <accessedStorage>
-                     ( .Map => ( 728815563385977040452943777879061427756277306518 |-> SetItem ( 7 ) ) )
+                     .Map
                    </accessedStorage>
                    ...
                  </substate>
@@ -1675,6 +1680,7 @@ Node 10:
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -1687,7 +1693,224 @@ Node 10:
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
                    <accessedStorage>
-                     ( 728815563385977040452943777879061427756277306518 |-> SetItem ( 7 ) )
+                     .Map
+                   </accessedStorage>
+                   ...
+                 </substate>
+                 <origin>
+                   ORIGIN_ID:Int
+                 </origin>
+                 <block>
+                   <number>
+                     NUMBER_CELL:Int
+                   </number>
+                   ...
+                 </block>
+                 ...
+               </evm>
+               <network>
+                 <accounts>
+                   ( <account>
+                     <acctID>
+                       645326474426547203313410069153905908525362434349
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     ...
+                     <storage>
+                       ( 46308022326495007027972728677917914892729792999299745830475596687180801507328 |-> 1 )
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       0
+                     </nonce>
+                   </account>
+                   <account>
+                     <acctID>
+                       728815563385977040452943777879061427756277306518
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     ...
+                     <storage>
+                       ( 7 |-> 256 )
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       1
+                     </nonce>
+                   </account> )
+                 </accounts>
+                 ...
+               </network>
+             </ethereum>
+             ...
+           </kevm>
+           <cheatcodes>
+             <prank>
+               <prevCaller>
+                 .Account
+               </prevCaller>
+               <prevOrigin>
+                 .Account
+               </prevOrigin>
+               <newCaller>
+                 .Account
+               </newCaller>
+               <newOrigin>
+                 .Account
+               </newOrigin>
+               <active>
+                 false
+               </active>
+               <singleCall>
+                 false
+               </singleCall>
+               ...
+             </prank>
+             <expectedRevert>
+               <isRevertExpected>
+                 false
+               </isRevertExpected>
+               ...
+             </expectedRevert>
+             <expectedOpcode>
+               <isOpcodeExpected>
+                 false
+               </isOpcodeExpected>
+               <expectedAddress>
+                 .Account
+               </expectedAddress>
+               <expectedValue>
+                 0
+               </expectedValue>
+               <expectedData>
+                 b""
+               </expectedData>
+               <opcodeType>
+                 .OpcodeType
+               </opcodeType>
+             </expectedOpcode>
+             <expectEmit>
+               <recordEvent>
+                 false
+               </recordEvent>
+               <isEventExpected>
+                 false
+               </isEventExpected>
+               ...
+             </expectEmit>
+             <whitelist>
+               <isCallWhitelistActive>
+                 false
+               </isCallWhitelistActive>
+               <isStorageWhitelistActive>
+                 false
+               </isStorageWhitelistActive>
+               <addressSet>
+                 .Set
+               </addressSet>
+               <storageSlotSet>
+                 .Set
+               </storageSlotSet>
+             </whitelist>
+           </cheatcodes>
+         </foundry>
+      requires ( 0 <=Int CALLER_ID:Int
+       andBool ( 0 <=Int ORIGIN_ID:Int
+       andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
+       andBool ( 0 <=Int NUMBER_CELL:Int
+       andBool ( 0 <=Int VV0_a_114b9705:Int
+       andBool ( 0 <=Int VV1_b_114b9705:Int
+       andBool ( CALLER_ID:Int <Int pow160
+       andBool ( ORIGIN_ID:Int <Int pow160
+       andBool ( NUMBER_CELL:Int <=Int maxSInt256
+       andBool ( VV0_a_114b9705:Int <Int pow256
+       andBool ( VV1_b_114b9705:Int <Int pow256
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+               ))))))))))))
+      [label(BASIC-BLOCK-8-TO-9)]
+    
+    rule [BASIC-BLOCK-9-TO-10]: <foundry>
+           <kevm>
+             <k>
+               #halt
+               ~> ( #pc [ STOP ]
+               ~> #execute => .K )
+               ~> _CONTINUATION
+             </k>
+             <mode>
+               NORMAL
+             </mode>
+             <schedule>
+               SHANGHAI
+             </schedule>
+             <useGas>
+               false
+             </useGas>
+             <ethereum>
+               <evm>
+                 <output>
+                   b""
+                 </output>
+                 <statusCode>
+                   EVMC_SUCCESS
+                 </statusCode>
+                 <callStack>
+                   .List
+                 </callStack>
+                 <interimStates>
+                   .List
+                 </interimStates>
+                 <callState>
+                   ...
+                   ...
+                   <id>
+                     728815563385977040452943777879061427756277306518
+                   </id>
+                   <caller>
+                     CALLER_ID:Int
+                   </caller>
+                   <callData>
+                     b"\xe4\x1b\xef\xb4" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes #buf ( 32 , VV1_b_114b9705:Int )
+                   </callData>
+                   <callValue>
+                     0
+                   </callValue>
+                   <wordStack>
+                     ( selector ( "test_assume_false(uint256,uint256)" ) : .WordStack )
+                   </wordStack>
+                   <localMem>
+                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
+                   </localMem>
+                   ...
+                   ...
+                   <memoryUsed>
+                     0
+                   </memoryUsed>
+                   <static>
+                     false
+                   </static>
+                   <callDepth>
+                     0
+                   </callDepth>
+                   ...
+                 </callState>
+                 <substate>
+                   <log>
+                     ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n      Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n     Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } )
+                   </log>
+                   <accessedAccounts>
+                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                   </accessedAccounts>
+                   <accessedStorage>
+                     .Map
                    </accessedStorage>
                    ...
                  </substate>
diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py
index 9184f5338..214003aff 100644
--- a/src/tests/integration/test_foundry_prove.py
+++ b/src/tests/integration/test_foundry_prove.py
@@ -53,6 +53,9 @@ def server(foundry: Foundry, no_use_booster: bool) -> Iterator[KoreServer]:
         command=kore_rpc_command,
         smt_timeout=300,
         smt_retry_limit=10,
+        fallback_on=None,
+        interim_simplification=None,
+        no_post_exec_simplify=None,
     )
 
 
diff --git a/src/tests/unit/test_solc_to_k.py b/src/tests/unit/test_solc_to_k.py
index 9da4f6421..f4d2f2bea 100644
--- a/src/tests/unit/test_solc_to_k.py
+++ b/src/tests/unit/test_solc_to_k.py
@@ -6,7 +6,7 @@
 from kevm_pyk.kevm import KEVM
 from pyk.kast.inner import KApply, KToken, KVariable
 
-from kontrol.solc_to_k import Contract, Input, _range_predicates
+from kontrol.solc_to_k import Contract, Input, _range_predicates, get_input_length
 
 from .utils import TEST_DATA_DIR
 
@@ -180,3 +180,47 @@ def test_input_to_abi(test_id: str, input: Input, expected: KApply) -> None:
 
     # Then
     assert abi == expected
+
+
+def test_get_input_length() -> None:
+    devdocs = {'_withdrawalProof': 10, '_withdrawalProof[]': 600, 'data': 600}
+    input_dict = {'name': '_withdrawalProof', 'type': 'bytes[]'}
+
+    array_lengths, dyn_len = get_input_length(input_dict, devdocs)
+    assert array_lengths == [10]
+    assert dyn_len == 600
+
+
+def test_inputs_from_abi() -> None:
+    input_dict = {
+        'components': [
+            {'internalType': 'uint256', 'name': 'nonce', 'type': 'uint256'},
+            {'internalType': 'address', 'name': 'sender', 'type': 'address'},
+            {'internalType': 'address', 'name': 'target', 'type': 'address'},
+            {'internalType': 'uint256', 'name': 'value', 'type': 'uint256'},
+            {'internalType': 'uint256', 'name': 'gasLimit', 'type': 'uint256'},
+            {'internalType': 'bytes', 'name': 'data', 'type': 'bytes'},
+        ],
+        'internalType': 'struct CallDataTest.WithdrawalTransaction',
+        'name': '_tx',
+        'type': 'tuple',
+    }
+
+    devdocs = {'_withdrawalProof': 10, '_withdrawalProof[]': 600, 'data': 600}
+    expected = Input(
+        name='_tx',
+        type='tuple',
+        components=(
+            Input(name='nonce', type='uint256', components=(), idx=0, array_lengths=None, dynamic_type_length=None),
+            Input(name='sender', type='address', components=(), idx=1, array_lengths=None, dynamic_type_length=None),
+            Input(name='target', type='address', components=(), idx=2, array_lengths=None, dynamic_type_length=None),
+            Input(name='value', type='uint256', components=(), idx=3, array_lengths=None, dynamic_type_length=None),
+            Input(name='gasLimit', type='uint256', components=(), idx=4, array_lengths=None, dynamic_type_length=None),
+            Input(name='data', type='bytes', components=(), idx=5, array_lengths=None, dynamic_type_length=600),
+        ),
+        idx=0,
+        array_lengths=None,
+        dynamic_type_length=None,
+    )
+    _input = Input.from_dict(input_dict, 0, devdocs)
+    assert _input == expected