diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index c500be701e..e2a5491000 100644
--- a/kevm-pyk/pyproject.toml
+++ b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.585"
+version = "1.0.586"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
index dbab82e2fd..342794dcb2 100644
--- a/kevm-pyk/src/kevm_pyk/__init__.py
+++ b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.585'
+VERSION: Final = '1.0.586'
diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py
index c3143a46c0..1cb9ca3b45 100644
--- a/kevm-pyk/src/kevm_pyk/kevm.py
+++ b/kevm-pyk/src/kevm_pyk/kevm.py
@@ -690,7 +690,7 @@ def compute_jumpdests(sections: list[KInner]) -> KInner:
 
 
 def _process_jumpdests(bytecode: bytes, offset: int) -> list[KToken]:
-    """Computes the location of JUMPDEST opcodes from a given bytecode.
+    """Computes the location of JUMPDEST opcodes from a given bytecode while avoiding bytes from within the PUSH opcodes.
 
     :param bytecode: The bytecode of the contract as bytes.
     :type bytecode: bytes
@@ -699,4 +699,16 @@ def _process_jumpdests(bytecode: bytes, offset: int) -> list[KToken]:
     :return:  A list of intToken instances representing the positions of all found jump destinations in the bytecode adjusted by the offset.
     :rtype: list[KToken]
     """
-    return [intToken(offset + i) for i, byte in enumerate(bytecode) if byte == 0x5B]
+    push1 = 0x60
+    push32 = 0x7F
+    jumpdest = 0x5B
+    i = 0
+    jumpdests: list[KToken] = []
+    while i < len(bytecode):
+        if push1 <= bytecode[i] <= push32:
+            i += bytecode[i] - push1 + 2
+        else:
+            if bytecode[i] == jumpdest:
+                jumpdests.append(intToken(offset + i))
+            i += 1
+    return jumpdests
diff --git a/kevm-pyk/src/tests/unit/test_kevm.py b/kevm-pyk/src/tests/unit/test_kevm.py
index 39e4389c1e..4dc2a2a02b 100644
--- a/kevm-pyk/src/tests/unit/test_kevm.py
+++ b/kevm-pyk/src/tests/unit/test_kevm.py
@@ -106,6 +106,7 @@ def test_kinner_to_hex(test_id: str, input: KInner, result: KInner) -> None:
         ],
         set_of([token(68), token(104), token(105), token(106), token(108)]),
     ),
+    ('jump_to_push', [token(bytes.fromhex('6001600055600A56605B5B'))], set_of([token(10)])),
 ]
 
 
diff --git a/package/version b/package/version
index 4d1a4dc836..d38a0a2765 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-1.0.585
+1.0.586
diff --git a/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k
index b470162431..998ff13da0 100644
--- a/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k
+++ b/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k
@@ -143,7 +143,7 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW-0-SPEC
                  <jumpDests>
                      ( SetItem ( 1001 ) ( SetItem ( 102 ) ( SetItem ( 1097 ) ( SetItem ( 1117 ) ( SetItem ( 1163 ) ( SetItem ( 1189 ) ( SetItem ( 1209 ) ( SetItem ( 1217 ) ( SetItem ( 1231 ) ( SetItem ( 1259 ) ( SetItem ( 1276 ) ( SetItem ( 1304 ) ( SetItem ( 1393 ) ( SetItem ( 1413 ) ( SetItem ( 1509 ) ( SetItem ( 151 ) ( SetItem ( 1529 ) ( SetItem ( 1579 ) ( SetItem ( 16 ) ( SetItem ( 1615 ) ( SetItem ( 1723 ) ( SetItem ( 1785 ) ( SetItem ( 1809 ) ( SetItem ( 1818 ) ( SetItem ( 1854 ) ( SetItem ( 1885 ) ( SetItem ( 1929 ) ( SetItem ( 1963 ) ( SetItem ( 1977 ) ( SetItem ( 2006 ) ( SetItem ( 2026 ) ( SetItem ( 2062 ) ( SetItem ( 211 ) ( SetItem ( 2170 ) ( SetItem ( 2232 ) ( SetItem ( 2256 ) ( SetItem ( 2292 ) ( SetItem ( 2323 ) ( SetItem ( 2367 ) ( SetItem ( 2401 ) ( SetItem ( 2415 ) ( SetItem ( 2444 ) ( SetItem ( 2464 ) ( SetItem ( 2498 ) ( SetItem ( 256 ) ( SetItem ( 261 ) ( SetItem ( 2640 ) ( SetItem ( 2666 ) ( SetItem ( 269 ) ( SetItem ( 2727 ) ( SetItem ( 2732 ) ( SetItem ( 2756 ) ( SetItem ( 2760 ) ( SetItem ( 2765 ) ( SetItem ( 2779 ) ( SetItem ( 2807 ) ( SetItem ( 282 ) ( SetItem ( 2824 ) ( SetItem ( 2852 ) ( SetItem ( 291 ) ( SetItem ( 2941 ) ( SetItem ( 2961 ) ( SetItem ( 299 ) ( SetItem ( 3057 ) ( SetItem ( 307 ) ( SetItem ( 3077 ) ( SetItem ( 3126 ) ( SetItem ( 315 ) ( SetItem ( 317 ) ( SetItem ( 3222 ) ( SetItem ( 3236 ) ( SetItem ( 325 ) ( SetItem ( 3264 ) ( SetItem ( 3281 ) ( SetItem ( 3309 ) ( SetItem ( 333 ) ( SetItem ( 3398 ) ( SetItem ( 3418 ) ( SetItem ( 346 ) ( SetItem ( 3514 ) ( SetItem ( 3534 ) ( SetItem ( 354 ) ( SetItem ( 3585 ) ( SetItem ( 3595 ) ( SetItem ( 3597 ) ( SetItem ( 367 ) ( SetItem ( 3697 ) ( SetItem ( 3713 ) ( SetItem ( 3716 ) ( SetItem ( 375 ) ( SetItem ( 383 ) ( SetItem ( 3870 ) ( SetItem ( 3896 ) ( SetItem ( 391 ) ( SetItem ( 3957 ) ( SetItem ( 3962 ) ( SetItem ( 3967 ) ( SetItem ( 3984 ) ( SetItem ( 3996 ) ( SetItem ( 4024 ) ( SetItem ( 4061 ) ( SetItem ( 407 ) ( SetItem ( 4073 ) ( SetItem ( 4113 ) ( SetItem ( 4174 ) ( SetItem ( 4216 ) ( SetItem ( 4237 ) ( SetItem ( 4252 ) ( SetItem ( 4255 ) ( SetItem ( 4279 ) ( SetItem ( 4294 ) ( SetItem ( 4300 ) ( SetItem ( 4339 ) ( SetItem ( 4378 ) ( SetItem ( 4409 ) ( SetItem ( 4422 ) ( SetItem ( 4442 ) ( SetItem ( 446 ) ( SetItem ( 4474 ) ( SetItem ( 4480 ) ( SetItem ( 4515 ) ( SetItem ( 4529 ) ( SetItem ( 4547 ) ( SetItem ( 4557 ) ( SetItem ( 4575 ) ( SetItem ( 4591 ) ( SetItem ( 4615 ) ( SetItem ( 4645 ) ( SetItem ( 470 ) ( SetItem ( 4700 ) ( SetItem ( 4705 ) ( SetItem ( 4716 ) ( SetItem ( 4721 ) ( SetItem ( 4723 ) ( SetItem ( 4731 ) ( SetItem ( 4749 ) ( SetItem ( 4757 ) ( SetItem ( 4768 ) ( SetItem ( 4773 ) ( SetItem ( 478 ) ( SetItem ( 4790 ) ( SetItem ( 486 ) ( SetItem ( 494 ) ( SetItem ( 502 ) ( SetItem ( 515 ) ( SetItem ( 573 ) ( SetItem ( 603 ) ( SetItem ( 613 ) ( SetItem ( 709 ) ( SetItem ( 805 ) ( SetItem ( 819 ) ( SetItem ( 847 ) ( SetItem ( 864 ) ( SetItem ( 892 ) SetItem ( 981 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                       =>
-                     ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                     ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
diff --git a/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k
index a7fd833423..3dd65adb3a 100644
--- a/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k
+++ b/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k
@@ -143,7 +143,7 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW_FAIL-0-SPEC
                  <jumpDests>
                    ( SetItem ( 1001 ) ( SetItem ( 102 ) ( SetItem ( 1097 ) ( SetItem ( 1117 ) ( SetItem ( 1163 ) ( SetItem ( 1189 ) ( SetItem ( 1209 ) ( SetItem ( 1217 ) ( SetItem ( 1231 ) ( SetItem ( 1259 ) ( SetItem ( 1276 ) ( SetItem ( 1304 ) ( SetItem ( 1393 ) ( SetItem ( 1413 ) ( SetItem ( 1509 ) ( SetItem ( 151 ) ( SetItem ( 1529 ) ( SetItem ( 1579 ) ( SetItem ( 16 ) ( SetItem ( 1615 ) ( SetItem ( 1723 ) ( SetItem ( 1785 ) ( SetItem ( 1809 ) ( SetItem ( 1818 ) ( SetItem ( 1854 ) ( SetItem ( 1885 ) ( SetItem ( 1929 ) ( SetItem ( 1963 ) ( SetItem ( 1977 ) ( SetItem ( 2006 ) ( SetItem ( 2026 ) ( SetItem ( 2062 ) ( SetItem ( 211 ) ( SetItem ( 2170 ) ( SetItem ( 2232 ) ( SetItem ( 2256 ) ( SetItem ( 2292 ) ( SetItem ( 2323 ) ( SetItem ( 2367 ) ( SetItem ( 2401 ) ( SetItem ( 2415 ) ( SetItem ( 2444 ) ( SetItem ( 2464 ) ( SetItem ( 2498 ) ( SetItem ( 256 ) ( SetItem ( 261 ) ( SetItem ( 2640 ) ( SetItem ( 2666 ) ( SetItem ( 269 ) ( SetItem ( 2727 ) ( SetItem ( 2732 ) ( SetItem ( 2756 ) ( SetItem ( 2760 ) ( SetItem ( 2765 ) ( SetItem ( 2779 ) ( SetItem ( 2807 ) ( SetItem ( 282 ) ( SetItem ( 2824 ) ( SetItem ( 2852 ) ( SetItem ( 291 ) ( SetItem ( 2941 ) ( SetItem ( 2961 ) ( SetItem ( 299 ) ( SetItem ( 3057 ) ( SetItem ( 307 ) ( SetItem ( 3077 ) ( SetItem ( 3126 ) ( SetItem ( 315 ) ( SetItem ( 317 ) ( SetItem ( 3222 ) ( SetItem ( 3236 ) ( SetItem ( 325 ) ( SetItem ( 3264 ) ( SetItem ( 3281 ) ( SetItem ( 3309 ) ( SetItem ( 333 ) ( SetItem ( 3398 ) ( SetItem ( 3418 ) ( SetItem ( 346 ) ( SetItem ( 3514 ) ( SetItem ( 3534 ) ( SetItem ( 354 ) ( SetItem ( 3585 ) ( SetItem ( 3595 ) ( SetItem ( 3597 ) ( SetItem ( 367 ) ( SetItem ( 3697 ) ( SetItem ( 3713 ) ( SetItem ( 3716 ) ( SetItem ( 375 ) ( SetItem ( 383 ) ( SetItem ( 3870 ) ( SetItem ( 3896 ) ( SetItem ( 391 ) ( SetItem ( 3957 ) ( SetItem ( 3962 ) ( SetItem ( 3967 ) ( SetItem ( 3984 ) ( SetItem ( 3996 ) ( SetItem ( 4024 ) ( SetItem ( 4061 ) ( SetItem ( 407 ) ( SetItem ( 4073 ) ( SetItem ( 4113 ) ( SetItem ( 4174 ) ( SetItem ( 4216 ) ( SetItem ( 4237 ) ( SetItem ( 4252 ) ( SetItem ( 4255 ) ( SetItem ( 4279 ) ( SetItem ( 4294 ) ( SetItem ( 4300 ) ( SetItem ( 4339 ) ( SetItem ( 4378 ) ( SetItem ( 4409 ) ( SetItem ( 4422 ) ( SetItem ( 4442 ) ( SetItem ( 446 ) ( SetItem ( 4474 ) ( SetItem ( 4480 ) ( SetItem ( 4515 ) ( SetItem ( 4529 ) ( SetItem ( 4547 ) ( SetItem ( 4557 ) ( SetItem ( 4575 ) ( SetItem ( 4591 ) ( SetItem ( 4615 ) ( SetItem ( 4645 ) ( SetItem ( 470 ) ( SetItem ( 4700 ) ( SetItem ( 4705 ) ( SetItem ( 4716 ) ( SetItem ( 4721 ) ( SetItem ( 4723 ) ( SetItem ( 4731 ) ( SetItem ( 4749 ) ( SetItem ( 4757 ) ( SetItem ( 4768 ) ( SetItem ( 4773 ) ( SetItem ( 478 ) ( SetItem ( 4790 ) ( SetItem ( 486 ) ( SetItem ( 494 ) ( SetItem ( 502 ) ( SetItem ( 515 ) ( SetItem ( 573 ) ( SetItem ( 603 ) ( SetItem ( 613 ) ( SetItem ( 709 ) ( SetItem ( 805 ) ( SetItem ( 819 ) ( SetItem ( 847 ) ( SetItem ( 864 ) ( SetItem ( 892 ) SetItem ( 981 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
diff --git a/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k
index 97a1f9b956..e76c5c2f5a 100644
--- a/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k
+++ b/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k
@@ -143,7 +143,7 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCALLSTOADDRESS-0-SPEC
                  <jumpDests>
                    ( SetItem ( 1001 ) ( SetItem ( 102 ) ( SetItem ( 1097 ) ( SetItem ( 1117 ) ( SetItem ( 1163 ) ( SetItem ( 1189 ) ( SetItem ( 1209 ) ( SetItem ( 1217 ) ( SetItem ( 1231 ) ( SetItem ( 1259 ) ( SetItem ( 1276 ) ( SetItem ( 1304 ) ( SetItem ( 1393 ) ( SetItem ( 1413 ) ( SetItem ( 1509 ) ( SetItem ( 151 ) ( SetItem ( 1529 ) ( SetItem ( 1579 ) ( SetItem ( 16 ) ( SetItem ( 1615 ) ( SetItem ( 1723 ) ( SetItem ( 1785 ) ( SetItem ( 1809 ) ( SetItem ( 1818 ) ( SetItem ( 1854 ) ( SetItem ( 1885 ) ( SetItem ( 1929 ) ( SetItem ( 1963 ) ( SetItem ( 1977 ) ( SetItem ( 2006 ) ( SetItem ( 2026 ) ( SetItem ( 2062 ) ( SetItem ( 211 ) ( SetItem ( 2170 ) ( SetItem ( 2232 ) ( SetItem ( 2256 ) ( SetItem ( 2292 ) ( SetItem ( 2323 ) ( SetItem ( 2367 ) ( SetItem ( 2401 ) ( SetItem ( 2415 ) ( SetItem ( 2444 ) ( SetItem ( 2464 ) ( SetItem ( 2498 ) ( SetItem ( 256 ) ( SetItem ( 261 ) ( SetItem ( 2640 ) ( SetItem ( 2666 ) ( SetItem ( 269 ) ( SetItem ( 2727 ) ( SetItem ( 2732 ) ( SetItem ( 2756 ) ( SetItem ( 2760 ) ( SetItem ( 2765 ) ( SetItem ( 2779 ) ( SetItem ( 2807 ) ( SetItem ( 282 ) ( SetItem ( 2824 ) ( SetItem ( 2852 ) ( SetItem ( 291 ) ( SetItem ( 2941 ) ( SetItem ( 2961 ) ( SetItem ( 299 ) ( SetItem ( 3057 ) ( SetItem ( 307 ) ( SetItem ( 3077 ) ( SetItem ( 3126 ) ( SetItem ( 315 ) ( SetItem ( 317 ) ( SetItem ( 3222 ) ( SetItem ( 3236 ) ( SetItem ( 325 ) ( SetItem ( 3264 ) ( SetItem ( 3281 ) ( SetItem ( 3309 ) ( SetItem ( 333 ) ( SetItem ( 3398 ) ( SetItem ( 3418 ) ( SetItem ( 346 ) ( SetItem ( 3514 ) ( SetItem ( 3534 ) ( SetItem ( 354 ) ( SetItem ( 3585 ) ( SetItem ( 3595 ) ( SetItem ( 3597 ) ( SetItem ( 367 ) ( SetItem ( 3697 ) ( SetItem ( 3713 ) ( SetItem ( 3716 ) ( SetItem ( 375 ) ( SetItem ( 383 ) ( SetItem ( 3870 ) ( SetItem ( 3896 ) ( SetItem ( 391 ) ( SetItem ( 3957 ) ( SetItem ( 3962 ) ( SetItem ( 3967 ) ( SetItem ( 3984 ) ( SetItem ( 3996 ) ( SetItem ( 4024 ) ( SetItem ( 4061 ) ( SetItem ( 407 ) ( SetItem ( 4073 ) ( SetItem ( 4113 ) ( SetItem ( 4174 ) ( SetItem ( 4216 ) ( SetItem ( 4237 ) ( SetItem ( 4252 ) ( SetItem ( 4255 ) ( SetItem ( 4279 ) ( SetItem ( 4294 ) ( SetItem ( 4300 ) ( SetItem ( 4339 ) ( SetItem ( 4378 ) ( SetItem ( 4409 ) ( SetItem ( 4422 ) ( SetItem ( 4442 ) ( SetItem ( 446 ) ( SetItem ( 4474 ) ( SetItem ( 4480 ) ( SetItem ( 4515 ) ( SetItem ( 4529 ) ( SetItem ( 4547 ) ( SetItem ( 4557 ) ( SetItem ( 4575 ) ( SetItem ( 4591 ) ( SetItem ( 4615 ) ( SetItem ( 4645 ) ( SetItem ( 470 ) ( SetItem ( 4700 ) ( SetItem ( 4705 ) ( SetItem ( 4716 ) ( SetItem ( 4721 ) ( SetItem ( 4723 ) ( SetItem ( 4731 ) ( SetItem ( 4749 ) ( SetItem ( 4757 ) ( SetItem ( 4768 ) ( SetItem ( 4773 ) ( SetItem ( 478 ) ( SetItem ( 4790 ) ( SetItem ( 486 ) ( SetItem ( 494 ) ( SetItem ( 502 ) ( SetItem ( 515 ) ( SetItem ( 573 ) ( SetItem ( 603 ) ( SetItem ( 613 ) ( SetItem ( 709 ) ( SetItem ( 805 ) ( SetItem ( 819 ) ( SetItem ( 847 ) ( SetItem ( 864 ) ( SetItem ( 892 ) SetItem ( 981 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
diff --git a/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k
index ea22345d83..31fdc65a90 100644
--- a/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k
+++ b/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k
@@ -143,7 +143,7 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC
                  <jumpDests>
                    ( SetItem ( 1001 ) ( SetItem ( 102 ) ( SetItem ( 1097 ) ( SetItem ( 1117 ) ( SetItem ( 1163 ) ( SetItem ( 1189 ) ( SetItem ( 1209 ) ( SetItem ( 1217 ) ( SetItem ( 1231 ) ( SetItem ( 1259 ) ( SetItem ( 1276 ) ( SetItem ( 1304 ) ( SetItem ( 1393 ) ( SetItem ( 1413 ) ( SetItem ( 1509 ) ( SetItem ( 151 ) ( SetItem ( 1529 ) ( SetItem ( 1579 ) ( SetItem ( 16 ) ( SetItem ( 1615 ) ( SetItem ( 1723 ) ( SetItem ( 1785 ) ( SetItem ( 1809 ) ( SetItem ( 1818 ) ( SetItem ( 1854 ) ( SetItem ( 1885 ) ( SetItem ( 1929 ) ( SetItem ( 1963 ) ( SetItem ( 1977 ) ( SetItem ( 2006 ) ( SetItem ( 2026 ) ( SetItem ( 2062 ) ( SetItem ( 211 ) ( SetItem ( 2170 ) ( SetItem ( 2232 ) ( SetItem ( 2256 ) ( SetItem ( 2292 ) ( SetItem ( 2323 ) ( SetItem ( 2367 ) ( SetItem ( 2401 ) ( SetItem ( 2415 ) ( SetItem ( 2444 ) ( SetItem ( 2464 ) ( SetItem ( 2498 ) ( SetItem ( 256 ) ( SetItem ( 261 ) ( SetItem ( 2640 ) ( SetItem ( 2666 ) ( SetItem ( 269 ) ( SetItem ( 2727 ) ( SetItem ( 2732 ) ( SetItem ( 2756 ) ( SetItem ( 2760 ) ( SetItem ( 2765 ) ( SetItem ( 2779 ) ( SetItem ( 2807 ) ( SetItem ( 282 ) ( SetItem ( 2824 ) ( SetItem ( 2852 ) ( SetItem ( 291 ) ( SetItem ( 2941 ) ( SetItem ( 2961 ) ( SetItem ( 299 ) ( SetItem ( 3057 ) ( SetItem ( 307 ) ( SetItem ( 3077 ) ( SetItem ( 3126 ) ( SetItem ( 315 ) ( SetItem ( 317 ) ( SetItem ( 3222 ) ( SetItem ( 3236 ) ( SetItem ( 325 ) ( SetItem ( 3264 ) ( SetItem ( 3281 ) ( SetItem ( 3309 ) ( SetItem ( 333 ) ( SetItem ( 3398 ) ( SetItem ( 3418 ) ( SetItem ( 346 ) ( SetItem ( 3514 ) ( SetItem ( 3534 ) ( SetItem ( 354 ) ( SetItem ( 3585 ) ( SetItem ( 3595 ) ( SetItem ( 3597 ) ( SetItem ( 367 ) ( SetItem ( 3697 ) ( SetItem ( 3713 ) ( SetItem ( 3716 ) ( SetItem ( 375 ) ( SetItem ( 383 ) ( SetItem ( 3870 ) ( SetItem ( 3896 ) ( SetItem ( 391 ) ( SetItem ( 3957 ) ( SetItem ( 3962 ) ( SetItem ( 3967 ) ( SetItem ( 3984 ) ( SetItem ( 3996 ) ( SetItem ( 4024 ) ( SetItem ( 4061 ) ( SetItem ( 407 ) ( SetItem ( 4073 ) ( SetItem ( 4113 ) ( SetItem ( 4174 ) ( SetItem ( 4216 ) ( SetItem ( 4237 ) ( SetItem ( 4252 ) ( SetItem ( 4255 ) ( SetItem ( 4279 ) ( SetItem ( 4294 ) ( SetItem ( 4300 ) ( SetItem ( 4339 ) ( SetItem ( 4378 ) ( SetItem ( 4409 ) ( SetItem ( 4422 ) ( SetItem ( 4442 ) ( SetItem ( 446 ) ( SetItem ( 4474 ) ( SetItem ( 4480 ) ( SetItem ( 4515 ) ( SetItem ( 4529 ) ( SetItem ( 4547 ) ( SetItem ( 4557 ) ( SetItem ( 4575 ) ( SetItem ( 4591 ) ( SetItem ( 4615 ) ( SetItem ( 4645 ) ( SetItem ( 470 ) ( SetItem ( 4700 ) ( SetItem ( 4705 ) ( SetItem ( 4716 ) ( SetItem ( 4721 ) ( SetItem ( 4723 ) ( SetItem ( 4731 ) ( SetItem ( 4749 ) ( SetItem ( 4757 ) ( SetItem ( 4768 ) ( SetItem ( 4773 ) ( SetItem ( 478 ) ( SetItem ( 4790 ) ( SetItem ( 486 ) ( SetItem ( 494 ) ( SetItem ( 502 ) ( SetItem ( 515 ) ( SetItem ( 573 ) ( SetItem ( 603 ) ( SetItem ( 613 ) ( SetItem ( 709 ) ( SetItem ( 805 ) ( SetItem ( 819 ) ( SetItem ( 847 ) ( SetItem ( 864 ) ( SetItem ( 892 ) SetItem ( 981 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
@@ -487,7 +487,7 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC
                    b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\xdd\x80a\x00\x1f`\x009`\x00\xf3\xfe`\x80`@R4\x80\x15`\x0fW`\x00\x80\xfd[P`\x046\x10`FW`\x005`\xe0\x1c\x80c\x15\xe6z\xa6\x14`KW\x80c03A;\x14`]W\x80c]3\xa2\x7f\x14`wW\x80cak\x8d\x05\x14`\x7fW[`\x00\x80\xfd[`[`V6`\x04`\x8fV[`\x01UV[\x00[`e`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`e`\x01T\x81V[`[`\x8a6`\x04`\x8fV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xa0W`\x00\x80\xfd[P5\x91\x90PV\xfe\xa2dipfsX\"\x12 k\xdd\x86\x85\x7f\xfc\x83n#6Y\x8de\xd5'\xc1*\x92U3\x1e\xbcVQ\x12,\xdc\x15\x7fVH\xf5dsolcC\x00\x08\r\x003"
                  </program>
                  <jumpDests>
-                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 491460923342184218035706888008750043977755113263 => 263400868551549723330807389252719309078400616203 )
diff --git a/tests/specs/kontrol/test-countertest-testincrement-0-spec.k b/tests/specs/kontrol/test-countertest-testincrement-0-spec.k
index 68007c03a5..36f71fe482 100644
--- a/tests/specs/kontrol/test-countertest-testincrement-0-spec.k
+++ b/tests/specs/kontrol/test-countertest-testincrement-0-spec.k
@@ -143,7 +143,7 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC
                  <jumpDests>
                    ( SetItem ( 1019 ) ( SetItem ( 102 ) ( SetItem ( 1028 ) ( SetItem ( 1040 ) ( SetItem ( 1068 ) ( SetItem ( 1155 ) ( SetItem ( 1175 ) ( SetItem ( 1249 ) ( SetItem ( 1269 ) ( SetItem ( 1359 ) ( SetItem ( 1395 ) ( SetItem ( 140 ) ( SetItem ( 1401 ) ( SetItem ( 1404 ) ( SetItem ( 1440 ) ( SetItem ( 1471 ) ( SetItem ( 1515 ) ( SetItem ( 1549 ) ( SetItem ( 1563 ) ( SetItem ( 1592 ) ( SetItem ( 16 ) ( SetItem ( 1612 ) ( SetItem ( 1648 ) ( SetItem ( 1756 ) ( SetItem ( 1818 ) ( SetItem ( 1842 ) ( SetItem ( 1878 ) ( SetItem ( 1909 ) ( SetItem ( 1953 ) ( SetItem ( 1987 ) ( SetItem ( 200 ) ( SetItem ( 2001 ) ( SetItem ( 2030 ) ( SetItem ( 2050 ) ( SetItem ( 2062 ) ( SetItem ( 2090 ) ( SetItem ( 2177 ) ( SetItem ( 2197 ) ( SetItem ( 2281 ) ( SetItem ( 2301 ) ( SetItem ( 234 ) ( SetItem ( 239 ) ( SetItem ( 2391 ) ( SetItem ( 2427 ) ( SetItem ( 2434 ) ( SetItem ( 2436 ) ( SetItem ( 247 ) ( SetItem ( 2470 ) ( SetItem ( 260 ) ( SetItem ( 2612 ) ( SetItem ( 2638 ) ( SetItem ( 269 ) ( SetItem ( 2699 ) ( SetItem ( 2704 ) ( SetItem ( 2728 ) ( SetItem ( 2732 ) ( SetItem ( 2737 ) ( SetItem ( 277 ) ( SetItem ( 2833 ) ( SetItem ( 285 ) ( SetItem ( 2946 ) ( SetItem ( 304 ) ( SetItem ( 3128 ) ( SetItem ( 3132 ) ( SetItem ( 328 ) ( SetItem ( 3286 ) ( SetItem ( 3312 ) ( SetItem ( 336 ) ( SetItem ( 3373 ) ( SetItem ( 3378 ) ( SetItem ( 3383 ) ( SetItem ( 3400 ) ( SetItem ( 3413 ) ( SetItem ( 3441 ) ( SetItem ( 3478 ) ( SetItem ( 349 ) ( SetItem ( 3490 ) ( SetItem ( 3530 ) ( SetItem ( 3591 ) ( SetItem ( 363 ) ( SetItem ( 3633 ) ( SetItem ( 3654 ) ( SetItem ( 3669 ) ( SetItem ( 368 ) ( SetItem ( 3687 ) ( SetItem ( 3694 ) ( SetItem ( 3697 ) ( SetItem ( 370 ) ( SetItem ( 3721 ) ( SetItem ( 3736 ) ( SetItem ( 3742 ) ( SetItem ( 378 ) ( SetItem ( 3781 ) ( SetItem ( 3820 ) ( SetItem ( 3851 ) ( SetItem ( 3864 ) ( SetItem ( 3882 ) ( SetItem ( 3889 ) ( SetItem ( 3909 ) ( SetItem ( 391 ) ( SetItem ( 3941 ) ( SetItem ( 3947 ) ( SetItem ( 3982 ) ( SetItem ( 399 ) ( SetItem ( 3996 ) ( SetItem ( 4014 ) ( SetItem ( 4024 ) ( SetItem ( 4042 ) ( SetItem ( 4058 ) ( SetItem ( 407 ) ( SetItem ( 4082 ) ( SetItem ( 4112 ) ( SetItem ( 415 ) ( SetItem ( 4157 ) ( SetItem ( 4162 ) ( SetItem ( 4173 ) ( SetItem ( 4178 ) ( SetItem ( 4180 ) ( SetItem ( 4188 ) ( SetItem ( 4206 ) ( SetItem ( 4221 ) ( SetItem ( 4228 ) ( SetItem ( 423 ) ( SetItem ( 4245 ) ( SetItem ( 4252 ) ( SetItem ( 4283 ) ( SetItem ( 439 ) ( SetItem ( 478 ) ( SetItem ( 486 ) ( SetItem ( 499 ) ( SetItem ( 557 ) ( SetItem ( 587 ) ( SetItem ( 597 ) ( SetItem ( 693 ) ( SetItem ( 789 ) ( SetItem ( 825 ) ( SetItem ( 933 ) SetItem ( 995 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 96 ) ( SetItem ( 91 ) ( SetItem ( 217 ) ( SetItem ( 116 ) ( SetItem ( 114 ) ( SetItem ( 112 ) ( SetItem ( 107 ) ( SetItem ( 179 ) ( SetItem ( 162 ) ( SetItem ( 122 ) ( SetItem ( 186 ) ( SetItem ( 155 ) SetItem ( 140 ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 96 ) ( SetItem ( 91 ) ( SetItem ( 217 ) ( SetItem ( 114 ) ( SetItem ( 112 ) ( SetItem ( 107 ) ( SetItem ( 179 ) ( SetItem ( 162 ) ( SetItem ( 122 ) ( SetItem ( 186 ) ( SetItem ( 155 ) SetItem ( 140 ) ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
@@ -781,7 +781,7 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC
                  <jumpDests>
                    ( SetItem ( 3490 ) ( SetItem ( 2434 ) ( SetItem ( 2050 ) ( SetItem ( 4162 ) ( SetItem ( 2946 ) ( SetItem ( 1155 ) ( SetItem ( 995 ) ( SetItem ( 1987 ) ( SetItem ( 1440 ) ( SetItem ( 2177 ) ( SetItem ( 1249 ) ( SetItem ( 1953 ) ( SetItem ( 2470 ) ( SetItem ( 486 ) ( SetItem ( 102 ) ( SetItem ( 3654 ) ( SetItem ( 423 ) ( SetItem ( 391 ) ( SetItem ( 3591 ) ( SetItem ( 3687 ) ( SetItem ( 260 ) ( SetItem ( 2436 ) ( SetItem ( 1028 ) ( SetItem ( 4228 ) ( SetItem ( 3941 ) ( SetItem ( 3909 ) ( SetItem ( 933 ) ( SetItem ( 3781 ) ( SetItem ( 3530 ) ( SetItem ( 2090 ) ( SetItem ( 234 ) ( SetItem ( 3882 ) ( SetItem ( 4042 ) ( SetItem ( 363 ) ( SetItem ( 1515 ) ( SetItem ( 3851 ) ( SetItem ( 3947 ) ( SetItem ( 587 ) ( SetItem ( 2699 ) ( SetItem ( 328 ) ( SetItem ( 3400 ) ( SetItem ( 200 ) ( SetItem ( 2728 ) ( SetItem ( 2281 ) ( SetItem ( 3721 ) ( SetItem ( 2062 ) ( SetItem ( 4206 ) ( SetItem ( 4014 ) ( SetItem ( 3982 ) ( SetItem ( 2030 ) ( SetItem ( 3694 ) ( SetItem ( 2638 ) ( SetItem ( 1359 ) ( SetItem ( 399 ) ( SetItem ( 239 ) ( SetItem ( 1068 ) ( SetItem ( 140 ) ( SetItem ( 1612 ) ( SetItem ( 2732 ) ( SetItem ( 3820 ) ( SetItem ( 3373 ) ( SetItem ( 269 ) ( SetItem ( 4173 ) ( SetItem ( 557 ) ( SetItem ( 1549 ) ( SetItem ( 3378 ) ( SetItem ( 370 ) ( SetItem ( 4178 ) ( SetItem ( 1842 ) ( SetItem ( 4082 ) ( SetItem ( 1395 ) ( SetItem ( 499 ) ( SetItem ( 304 ) ( SetItem ( 368 ) ( SetItem ( 336 ) ( SetItem ( 4112 ) ( SetItem ( 16 ) ( SetItem ( 1040 ) ( SetItem ( 3312 ) ( SetItem ( 1648 ) ( SetItem ( 2704 ) ( SetItem ( 3441 ) ( SetItem ( 3889 ) ( SetItem ( 2833 ) ( SetItem ( 2001 ) ( SetItem ( 3633 ) ( SetItem ( 3697 ) ( SetItem ( 2737 ) ( SetItem ( 3478 ) ( SetItem ( 3286 ) ( SetItem ( 1878 ) ( SetItem ( 3383 ) ( SetItem ( 2391 ) ( SetItem ( 439 ) ( SetItem ( 407 ) ( SetItem ( 1175 ) ( SetItem ( 247 ) ( SetItem ( 4180 ) ( SetItem ( 2612 ) ( SetItem ( 277 ) ( SetItem ( 3413 ) ( SetItem ( 4245 ) ( SetItem ( 2197 ) ( SetItem ( 1269 ) ( SetItem ( 789 ) ( SetItem ( 1909 ) ( SetItem ( 597 ) ( SetItem ( 3669 ) ( SetItem ( 693 ) ( SetItem ( 378 ) ( SetItem ( 1818 ) ( SetItem ( 4058 ) ( SetItem ( 2427 ) ( SetItem ( 4283 ) ( SetItem ( 1019 ) ( SetItem ( 1563 ) ( SetItem ( 3128 ) ( SetItem ( 3864 ) ( SetItem ( 4024 ) ( SetItem ( 1592 ) ( SetItem ( 3736 ) ( SetItem ( 1401 ) ( SetItem ( 825 ) ( SetItem ( 478 ) ( SetItem ( 3742 ) ( SetItem ( 1471 ) ( SetItem ( 415 ) ( SetItem ( 1404 ) ( SetItem ( 3132 ) ( SetItem ( 4188 ) ( SetItem ( 4252 ) ( SetItem ( 3996 ) ( SetItem ( 1756 ) ( SetItem ( 285 ) ( SetItem ( 349 ) ( SetItem ( 4157 ) ( SetItem ( 4221 ) SetItem ( 2301 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 76 ) ( SetItem ( 65 ) ( SetItem ( 60 ) ( SetItem ( 15 ) ( SetItem ( 81 ) ( SetItem ( 83 ) ( SetItem ( 85 ) ( SetItem ( 91 ) ( SetItem ( 109 ) ( SetItem ( 131 ) ( SetItem ( 124 ) ( SetItem ( 186 ) ( SetItem ( 155 ) SetItem ( 148 ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 76 ) ( SetItem ( 65 ) ( SetItem ( 60 ) ( SetItem ( 15 ) ( SetItem ( 81 ) ( SetItem ( 83 ) ( SetItem ( 91 ) ( SetItem ( 109 ) ( SetItem ( 131 ) ( SetItem ( 124 ) ( SetItem ( 186 ) ( SetItem ( 155 ) SetItem ( 148 ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
diff --git a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k
index 7d4c632962..edbdda5fb0 100644
--- a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k
+++ b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k
@@ -143,7 +143,7 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC
                  <jumpDests>
                    ( SetItem ( 10007 ) ( SetItem ( 10035 ) ( SetItem ( 10053 ) ( SetItem ( 1030 ) ( SetItem ( 1054 ) ( SetItem ( 1074 ) ( SetItem ( 1082 ) ( SetItem ( 113 ) ( SetItem ( 1150 ) ( SetItem ( 1159 ) ( SetItem ( 1217 ) ( SetItem ( 1247 ) ( SetItem ( 1257 ) ( SetItem ( 1271 ) ( SetItem ( 1299 ) ( SetItem ( 1378 ) ( SetItem ( 1398 ) ( SetItem ( 1459 ) ( SetItem ( 1479 ) ( SetItem ( 1486 ) ( SetItem ( 151 ) ( SetItem ( 1582 ) ( SetItem ( 16 ) ( SetItem ( 1678 ) ( SetItem ( 1692 ) ( SetItem ( 1720 ) ( SetItem ( 1807 ) ( SetItem ( 1827 ) ( SetItem ( 1898 ) ( SetItem ( 1922 ) ( SetItem ( 1981 ) ( SetItem ( 1998 ) ( SetItem ( 2023 ) ( SetItem ( 2059 ) ( SetItem ( 2167 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2253 ) ( SetItem ( 2262 ) ( SetItem ( 2338 ) ( SetItem ( 2358 ) ( SetItem ( 2370 ) ( SetItem ( 2372 ) ( SetItem ( 2386 ) ( SetItem ( 2414 ) ( SetItem ( 2493 ) ( SetItem ( 2513 ) ( SetItem ( 2579 ) ( SetItem ( 2615 ) ( SetItem ( 2619 ) ( SetItem ( 2655 ) ( SetItem ( 2686 ) ( SetItem ( 2730 ) ( SetItem ( 2764 ) ( SetItem ( 2778 ) ( SetItem ( 2807 ) ( SetItem ( 2827 ) ( SetItem ( 2841 ) ( SetItem ( 2869 ) ( SetItem ( 2948 ) ( SetItem ( 2968 ) ( SetItem ( 3034 ) ( SetItem ( 304 ) ( SetItem ( 3070 ) ( SetItem ( 3147 ) ( SetItem ( 3167 ) ( SetItem ( 3228 ) ( SetItem ( 3281 ) ( SetItem ( 3307 ) ( SetItem ( 3327 ) ( SetItem ( 3390 ) ( SetItem ( 3410 ) ( SetItem ( 3416 ) ( SetItem ( 3452 ) ( SetItem ( 3560 ) ( SetItem ( 3622 ) ( SetItem ( 3646 ) ( SetItem ( 3660 ) ( SetItem ( 3688 ) ( SetItem ( 371 ) ( SetItem ( 376 ) ( SetItem ( 3767 ) ( SetItem ( 3787 ) ( SetItem ( 3848 ) ( SetItem ( 3868 ) ( SetItem ( 3882 ) ( SetItem ( 390 ) ( SetItem ( 3910 ) ( SetItem ( 395 ) ( SetItem ( 397 ) ( SetItem ( 3989 ) ( SetItem ( 4025 ) ( SetItem ( 405 ) ( SetItem ( 4056 ) ( SetItem ( 4100 ) ( SetItem ( 413 ) ( SetItem ( 4134 ) ( SetItem ( 4148 ) ( SetItem ( 4177 ) ( SetItem ( 4197 ) ( SetItem ( 4231 ) ( SetItem ( 426 ) ( SetItem ( 435 ) ( SetItem ( 4373 ) ( SetItem ( 4399 ) ( SetItem ( 443 ) ( SetItem ( 4460 ) ( SetItem ( 4465 ) ( SetItem ( 4489 ) ( SetItem ( 4493 ) ( SetItem ( 4498 ) ( SetItem ( 451 ) ( SetItem ( 4512 ) ( SetItem ( 4540 ) ( SetItem ( 459 ) ( SetItem ( 4627 ) ( SetItem ( 4647 ) ( SetItem ( 467 ) ( SetItem ( 4721 ) ( SetItem ( 475 ) ( SetItem ( 4797 ) ( SetItem ( 4811 ) ( SetItem ( 483 ) ( SetItem ( 4839 ) ( SetItem ( 4935 ) ( SetItem ( 496 ) ( SetItem ( 4961 ) ( SetItem ( 4981 ) ( SetItem ( 504 ) ( SetItem ( 5064 ) ( SetItem ( 512 ) ( SetItem ( 5160 ) ( SetItem ( 5174 ) ( SetItem ( 520 ) ( SetItem ( 5202 ) ( SetItem ( 5304 ) ( SetItem ( 5324 ) ( SetItem ( 533 ) ( SetItem ( 5402 ) ( SetItem ( 541 ) ( SetItem ( 5442 ) ( SetItem ( 5469 ) ( SetItem ( 549 ) ( SetItem ( 5567 ) ( SetItem ( 557 ) ( SetItem ( 5587 ) ( SetItem ( 565 ) ( SetItem ( 5666 ) ( SetItem ( 5702 ) ( SetItem ( 5717 ) ( SetItem ( 5728 ) ( SetItem ( 573 ) ( SetItem ( 5762 ) ( SetItem ( 5772 ) ( SetItem ( 581 ) ( SetItem ( 5883 ) ( SetItem ( 589 ) ( SetItem ( 5938 ) ( SetItem ( 5993 ) ( SetItem ( 6009 ) ( SetItem ( 605 ) ( SetItem ( 6122 ) ( SetItem ( 613 ) ( SetItem ( 6177 ) ( SetItem ( 621 ) ( SetItem ( 6232 ) ( SetItem ( 6248 ) ( SetItem ( 6275 ) ( SetItem ( 629 ) ( SetItem ( 6314 ) ( SetItem ( 6339 ) ( SetItem ( 6349 ) ( SetItem ( 6357 ) ( SetItem ( 6363 ) ( SetItem ( 6367 ) ( SetItem ( 637 ) ( SetItem ( 6373 ) ( SetItem ( 645 ) ( SetItem ( 6527 ) ( SetItem ( 6553 ) ( SetItem ( 658 ) ( SetItem ( 6614 ) ( SetItem ( 6619 ) ( SetItem ( 6624 ) ( SetItem ( 6641 ) ( SetItem ( 6654 ) ( SetItem ( 6667 ) ( SetItem ( 6680 ) ( SetItem ( 6698 ) ( SetItem ( 672 ) ( SetItem ( 6721 ) ( SetItem ( 6728 ) ( SetItem ( 6756 ) ( SetItem ( 6793 ) ( SetItem ( 6805 ) ( SetItem ( 6845 ) ( SetItem ( 6906 ) ( SetItem ( 6948 ) ( SetItem ( 6969 ) ( SetItem ( 6984 ) ( SetItem ( 6987 ) ( SetItem ( 700 ) ( SetItem ( 7011 ) ( SetItem ( 7028 ) ( SetItem ( 7052 ) ( SetItem ( 7072 ) ( SetItem ( 7111 ) ( SetItem ( 7139 ) ( SetItem ( 7157 ) ( SetItem ( 7170 ) ( SetItem ( 7231 ) ( SetItem ( 7250 ) ( SetItem ( 7311 ) ( SetItem ( 7329 ) ( SetItem ( 7345 ) ( SetItem ( 7365 ) ( SetItem ( 7397 ) ( SetItem ( 7403 ) ( SetItem ( 7438 ) ( SetItem ( 7452 ) ( SetItem ( 7470 ) ( SetItem ( 7480 ) ( SetItem ( 7502 ) ( SetItem ( 7520 ) ( SetItem ( 7544 ) ( SetItem ( 7564 ) ( SetItem ( 7582 ) ( SetItem ( 7622 ) ( SetItem ( 7647 ) ( SetItem ( 7664 ) ( SetItem ( 7675 ) ( SetItem ( 7694 ) ( SetItem ( 7711 ) ( SetItem ( 7753 ) ( SetItem ( 7771 ) ( SetItem ( 7779 ) ( SetItem ( 7821 ) ( SetItem ( 7863 ) ( SetItem ( 7877 ) ( SetItem ( 789 ) ( SetItem ( 7919 ) ( SetItem ( 7941 ) ( SetItem ( 7973 ) ( SetItem ( 7997 ) ( SetItem ( 8029 ) ( SetItem ( 8089 ) ( SetItem ( 809 ) ( SetItem ( 8094 ) ( SetItem ( 8102 ) ( SetItem ( 8104 ) ( SetItem ( 8118 ) ( SetItem ( 8123 ) ( SetItem ( 8143 ) ( SetItem ( 8157 ) ( SetItem ( 8162 ) ( SetItem ( 8193 ) ( SetItem ( 8202 ) ( SetItem ( 8230 ) ( SetItem ( 8248 ) ( SetItem ( 8272 ) ( SetItem ( 8296 ) ( SetItem ( 8303 ) ( SetItem ( 8324 ) ( SetItem ( 8347 ) ( SetItem ( 8375 ) ( SetItem ( 8387 ) ( SetItem ( 8400 ) ( SetItem ( 8419 ) ( SetItem ( 8442 ) ( SetItem ( 8454 ) ( SetItem ( 8466 ) ( SetItem ( 8507 ) ( SetItem ( 8544 ) ( SetItem ( 8553 ) ( SetItem ( 8573 ) ( SetItem ( 8651 ) ( SetItem ( 8664 ) ( SetItem ( 867 ) ( SetItem ( 8692 ) ( SetItem ( 8730 ) ( SetItem ( 8743 ) ( SetItem ( 8772 ) ( SetItem ( 8797 ) ( SetItem ( 8802 ) ( SetItem ( 8808 ) ( SetItem ( 8810 ) ( SetItem ( 8873 ) ( SetItem ( 8892 ) ( SetItem ( 8968 ) ( SetItem ( 9000 ) ( SetItem ( 9060 ) ( SetItem ( 9065 ) ( SetItem ( 9073 ) ( SetItem ( 9075 ) ( SetItem ( 9089 ) ( SetItem ( 9094 ) ( SetItem ( 9114 ) ( SetItem ( 9128 ) ( SetItem ( 9133 ) ( SetItem ( 9164 ) ( SetItem ( 9173 ) ( SetItem ( 9201 ) ( SetItem ( 9219 ) ( SetItem ( 9243 ) ( SetItem ( 9267 ) ( SetItem ( 9274 ) ( SetItem ( 9295 ) ( SetItem ( 9318 ) ( SetItem ( 9346 ) ( SetItem ( 9358 ) ( SetItem ( 936 ) ( SetItem ( 9371 ) ( SetItem ( 9390 ) ( SetItem ( 9413 ) ( SetItem ( 9425 ) ( SetItem ( 9437 ) ( SetItem ( 9478 ) ( SetItem ( 9515 ) ( SetItem ( 9524 ) ( SetItem ( 9544 ) ( SetItem ( 962 ) ( SetItem ( 9622 ) ( SetItem ( 9654 ) ( SetItem ( 9692 ) ( SetItem ( 9697 ) ( SetItem ( 9711 ) ( SetItem ( 9716 ) ( SetItem ( 9729 ) ( SetItem ( 9738 ) ( SetItem ( 9752 ) ( SetItem ( 9757 ) ( SetItem ( 9778 ) ( SetItem ( 982 ) ( SetItem ( 9830 ) ( SetItem ( 9839 ) ( SetItem ( 9880 ) ( SetItem ( 9937 ) ( SetItem ( 9949 ) ( SetItem ( 9967 ) ( SetItem ( 9983 ) SetItem ( 9990 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 77 ) ( SetItem ( 16 ) ( SetItem ( 84 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
diff --git a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k
index b509ad60fa..e0ce79b9c6 100644
--- a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k
+++ b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k
@@ -143,7 +143,7 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_MESSAGE-0-SPEC
                  <jumpDests>
                    ( SetItem ( 10007 ) ( SetItem ( 10035 ) ( SetItem ( 10053 ) ( SetItem ( 1030 ) ( SetItem ( 1054 ) ( SetItem ( 1074 ) ( SetItem ( 1082 ) ( SetItem ( 113 ) ( SetItem ( 1150 ) ( SetItem ( 1159 ) ( SetItem ( 1217 ) ( SetItem ( 1247 ) ( SetItem ( 1257 ) ( SetItem ( 1271 ) ( SetItem ( 1299 ) ( SetItem ( 1378 ) ( SetItem ( 1398 ) ( SetItem ( 1459 ) ( SetItem ( 1479 ) ( SetItem ( 1486 ) ( SetItem ( 151 ) ( SetItem ( 1582 ) ( SetItem ( 16 ) ( SetItem ( 1678 ) ( SetItem ( 1692 ) ( SetItem ( 1720 ) ( SetItem ( 1807 ) ( SetItem ( 1827 ) ( SetItem ( 1898 ) ( SetItem ( 1922 ) ( SetItem ( 1981 ) ( SetItem ( 1998 ) ( SetItem ( 2023 ) ( SetItem ( 2059 ) ( SetItem ( 2167 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2253 ) ( SetItem ( 2262 ) ( SetItem ( 2338 ) ( SetItem ( 2358 ) ( SetItem ( 2370 ) ( SetItem ( 2372 ) ( SetItem ( 2386 ) ( SetItem ( 2414 ) ( SetItem ( 2493 ) ( SetItem ( 2513 ) ( SetItem ( 2579 ) ( SetItem ( 2615 ) ( SetItem ( 2619 ) ( SetItem ( 2655 ) ( SetItem ( 2686 ) ( SetItem ( 2730 ) ( SetItem ( 2764 ) ( SetItem ( 2778 ) ( SetItem ( 2807 ) ( SetItem ( 2827 ) ( SetItem ( 2841 ) ( SetItem ( 2869 ) ( SetItem ( 2948 ) ( SetItem ( 2968 ) ( SetItem ( 3034 ) ( SetItem ( 304 ) ( SetItem ( 3070 ) ( SetItem ( 3147 ) ( SetItem ( 3167 ) ( SetItem ( 3228 ) ( SetItem ( 3281 ) ( SetItem ( 3307 ) ( SetItem ( 3327 ) ( SetItem ( 3390 ) ( SetItem ( 3410 ) ( SetItem ( 3416 ) ( SetItem ( 3452 ) ( SetItem ( 3560 ) ( SetItem ( 3622 ) ( SetItem ( 3646 ) ( SetItem ( 3660 ) ( SetItem ( 3688 ) ( SetItem ( 371 ) ( SetItem ( 376 ) ( SetItem ( 3767 ) ( SetItem ( 3787 ) ( SetItem ( 3848 ) ( SetItem ( 3868 ) ( SetItem ( 3882 ) ( SetItem ( 390 ) ( SetItem ( 3910 ) ( SetItem ( 395 ) ( SetItem ( 397 ) ( SetItem ( 3989 ) ( SetItem ( 4025 ) ( SetItem ( 405 ) ( SetItem ( 4056 ) ( SetItem ( 4100 ) ( SetItem ( 413 ) ( SetItem ( 4134 ) ( SetItem ( 4148 ) ( SetItem ( 4177 ) ( SetItem ( 4197 ) ( SetItem ( 4231 ) ( SetItem ( 426 ) ( SetItem ( 435 ) ( SetItem ( 4373 ) ( SetItem ( 4399 ) ( SetItem ( 443 ) ( SetItem ( 4460 ) ( SetItem ( 4465 ) ( SetItem ( 4489 ) ( SetItem ( 4493 ) ( SetItem ( 4498 ) ( SetItem ( 451 ) ( SetItem ( 4512 ) ( SetItem ( 4540 ) ( SetItem ( 459 ) ( SetItem ( 4627 ) ( SetItem ( 4647 ) ( SetItem ( 467 ) ( SetItem ( 4721 ) ( SetItem ( 475 ) ( SetItem ( 4797 ) ( SetItem ( 4811 ) ( SetItem ( 483 ) ( SetItem ( 4839 ) ( SetItem ( 4935 ) ( SetItem ( 496 ) ( SetItem ( 4961 ) ( SetItem ( 4981 ) ( SetItem ( 504 ) ( SetItem ( 5064 ) ( SetItem ( 512 ) ( SetItem ( 5160 ) ( SetItem ( 5174 ) ( SetItem ( 520 ) ( SetItem ( 5202 ) ( SetItem ( 5304 ) ( SetItem ( 5324 ) ( SetItem ( 533 ) ( SetItem ( 5402 ) ( SetItem ( 541 ) ( SetItem ( 5442 ) ( SetItem ( 5469 ) ( SetItem ( 549 ) ( SetItem ( 5567 ) ( SetItem ( 557 ) ( SetItem ( 5587 ) ( SetItem ( 565 ) ( SetItem ( 5666 ) ( SetItem ( 5702 ) ( SetItem ( 5717 ) ( SetItem ( 5728 ) ( SetItem ( 573 ) ( SetItem ( 5762 ) ( SetItem ( 5772 ) ( SetItem ( 581 ) ( SetItem ( 5883 ) ( SetItem ( 589 ) ( SetItem ( 5938 ) ( SetItem ( 5993 ) ( SetItem ( 6009 ) ( SetItem ( 605 ) ( SetItem ( 6122 ) ( SetItem ( 613 ) ( SetItem ( 6177 ) ( SetItem ( 621 ) ( SetItem ( 6232 ) ( SetItem ( 6248 ) ( SetItem ( 6275 ) ( SetItem ( 629 ) ( SetItem ( 6314 ) ( SetItem ( 6339 ) ( SetItem ( 6349 ) ( SetItem ( 6357 ) ( SetItem ( 6363 ) ( SetItem ( 6367 ) ( SetItem ( 637 ) ( SetItem ( 6373 ) ( SetItem ( 645 ) ( SetItem ( 6527 ) ( SetItem ( 6553 ) ( SetItem ( 658 ) ( SetItem ( 6614 ) ( SetItem ( 6619 ) ( SetItem ( 6624 ) ( SetItem ( 6641 ) ( SetItem ( 6654 ) ( SetItem ( 6667 ) ( SetItem ( 6680 ) ( SetItem ( 6698 ) ( SetItem ( 672 ) ( SetItem ( 6721 ) ( SetItem ( 6728 ) ( SetItem ( 6756 ) ( SetItem ( 6793 ) ( SetItem ( 6805 ) ( SetItem ( 6845 ) ( SetItem ( 6906 ) ( SetItem ( 6948 ) ( SetItem ( 6969 ) ( SetItem ( 6984 ) ( SetItem ( 6987 ) ( SetItem ( 700 ) ( SetItem ( 7011 ) ( SetItem ( 7028 ) ( SetItem ( 7052 ) ( SetItem ( 7072 ) ( SetItem ( 7111 ) ( SetItem ( 7139 ) ( SetItem ( 7157 ) ( SetItem ( 7170 ) ( SetItem ( 7231 ) ( SetItem ( 7250 ) ( SetItem ( 7311 ) ( SetItem ( 7329 ) ( SetItem ( 7345 ) ( SetItem ( 7365 ) ( SetItem ( 7397 ) ( SetItem ( 7403 ) ( SetItem ( 7438 ) ( SetItem ( 7452 ) ( SetItem ( 7470 ) ( SetItem ( 7480 ) ( SetItem ( 7502 ) ( SetItem ( 7520 ) ( SetItem ( 7544 ) ( SetItem ( 7564 ) ( SetItem ( 7582 ) ( SetItem ( 7622 ) ( SetItem ( 7647 ) ( SetItem ( 7664 ) ( SetItem ( 7675 ) ( SetItem ( 7694 ) ( SetItem ( 7711 ) ( SetItem ( 7753 ) ( SetItem ( 7771 ) ( SetItem ( 7779 ) ( SetItem ( 7821 ) ( SetItem ( 7863 ) ( SetItem ( 7877 ) ( SetItem ( 789 ) ( SetItem ( 7919 ) ( SetItem ( 7941 ) ( SetItem ( 7973 ) ( SetItem ( 7997 ) ( SetItem ( 8029 ) ( SetItem ( 8089 ) ( SetItem ( 809 ) ( SetItem ( 8094 ) ( SetItem ( 8102 ) ( SetItem ( 8104 ) ( SetItem ( 8118 ) ( SetItem ( 8123 ) ( SetItem ( 8143 ) ( SetItem ( 8157 ) ( SetItem ( 8162 ) ( SetItem ( 8193 ) ( SetItem ( 8202 ) ( SetItem ( 8230 ) ( SetItem ( 8248 ) ( SetItem ( 8272 ) ( SetItem ( 8296 ) ( SetItem ( 8303 ) ( SetItem ( 8324 ) ( SetItem ( 8347 ) ( SetItem ( 8375 ) ( SetItem ( 8387 ) ( SetItem ( 8400 ) ( SetItem ( 8419 ) ( SetItem ( 8442 ) ( SetItem ( 8454 ) ( SetItem ( 8466 ) ( SetItem ( 8507 ) ( SetItem ( 8544 ) ( SetItem ( 8553 ) ( SetItem ( 8573 ) ( SetItem ( 8651 ) ( SetItem ( 8664 ) ( SetItem ( 867 ) ( SetItem ( 8692 ) ( SetItem ( 8730 ) ( SetItem ( 8743 ) ( SetItem ( 8772 ) ( SetItem ( 8797 ) ( SetItem ( 8802 ) ( SetItem ( 8808 ) ( SetItem ( 8810 ) ( SetItem ( 8873 ) ( SetItem ( 8892 ) ( SetItem ( 8968 ) ( SetItem ( 9000 ) ( SetItem ( 9060 ) ( SetItem ( 9065 ) ( SetItem ( 9073 ) ( SetItem ( 9075 ) ( SetItem ( 9089 ) ( SetItem ( 9094 ) ( SetItem ( 9114 ) ( SetItem ( 9128 ) ( SetItem ( 9133 ) ( SetItem ( 9164 ) ( SetItem ( 9173 ) ( SetItem ( 9201 ) ( SetItem ( 9219 ) ( SetItem ( 9243 ) ( SetItem ( 9267 ) ( SetItem ( 9274 ) ( SetItem ( 9295 ) ( SetItem ( 9318 ) ( SetItem ( 9346 ) ( SetItem ( 9358 ) ( SetItem ( 936 ) ( SetItem ( 9371 ) ( SetItem ( 9390 ) ( SetItem ( 9413 ) ( SetItem ( 9425 ) ( SetItem ( 9437 ) ( SetItem ( 9478 ) ( SetItem ( 9515 ) ( SetItem ( 9524 ) ( SetItem ( 9544 ) ( SetItem ( 962 ) ( SetItem ( 9622 ) ( SetItem ( 9654 ) ( SetItem ( 9692 ) ( SetItem ( 9697 ) ( SetItem ( 9711 ) ( SetItem ( 9716 ) ( SetItem ( 9729 ) ( SetItem ( 9738 ) ( SetItem ( 9752 ) ( SetItem ( 9757 ) ( SetItem ( 9778 ) ( SetItem ( 982 ) ( SetItem ( 9830 ) ( SetItem ( 9839 ) ( SetItem ( 9880 ) ( SetItem ( 9937 ) ( SetItem ( 9949 ) ( SetItem ( 9967 ) ( SetItem ( 9983 ) SetItem ( 9990 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 77 ) ( SetItem ( 16 ) ( SetItem ( 84 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
diff --git a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k
index 1eb0948e74..2f08def8c8 100644
--- a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k
+++ b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k
@@ -143,7 +143,7 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_RETURNVALUE-0-SPEC
                  <jumpDests>
                    ( SetItem ( 10007 ) ( SetItem ( 10035 ) ( SetItem ( 10053 ) ( SetItem ( 1030 ) ( SetItem ( 1054 ) ( SetItem ( 1074 ) ( SetItem ( 1082 ) ( SetItem ( 113 ) ( SetItem ( 1150 ) ( SetItem ( 1159 ) ( SetItem ( 1217 ) ( SetItem ( 1247 ) ( SetItem ( 1257 ) ( SetItem ( 1271 ) ( SetItem ( 1299 ) ( SetItem ( 1378 ) ( SetItem ( 1398 ) ( SetItem ( 1459 ) ( SetItem ( 1479 ) ( SetItem ( 1486 ) ( SetItem ( 151 ) ( SetItem ( 1582 ) ( SetItem ( 16 ) ( SetItem ( 1678 ) ( SetItem ( 1692 ) ( SetItem ( 1720 ) ( SetItem ( 1807 ) ( SetItem ( 1827 ) ( SetItem ( 1898 ) ( SetItem ( 1922 ) ( SetItem ( 1981 ) ( SetItem ( 1998 ) ( SetItem ( 2023 ) ( SetItem ( 2059 ) ( SetItem ( 2167 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2253 ) ( SetItem ( 2262 ) ( SetItem ( 2338 ) ( SetItem ( 2358 ) ( SetItem ( 2370 ) ( SetItem ( 2372 ) ( SetItem ( 2386 ) ( SetItem ( 2414 ) ( SetItem ( 2493 ) ( SetItem ( 2513 ) ( SetItem ( 2579 ) ( SetItem ( 2615 ) ( SetItem ( 2619 ) ( SetItem ( 2655 ) ( SetItem ( 2686 ) ( SetItem ( 2730 ) ( SetItem ( 2764 ) ( SetItem ( 2778 ) ( SetItem ( 2807 ) ( SetItem ( 2827 ) ( SetItem ( 2841 ) ( SetItem ( 2869 ) ( SetItem ( 2948 ) ( SetItem ( 2968 ) ( SetItem ( 3034 ) ( SetItem ( 304 ) ( SetItem ( 3070 ) ( SetItem ( 3147 ) ( SetItem ( 3167 ) ( SetItem ( 3228 ) ( SetItem ( 3281 ) ( SetItem ( 3307 ) ( SetItem ( 3327 ) ( SetItem ( 3390 ) ( SetItem ( 3410 ) ( SetItem ( 3416 ) ( SetItem ( 3452 ) ( SetItem ( 3560 ) ( SetItem ( 3622 ) ( SetItem ( 3646 ) ( SetItem ( 3660 ) ( SetItem ( 3688 ) ( SetItem ( 371 ) ( SetItem ( 376 ) ( SetItem ( 3767 ) ( SetItem ( 3787 ) ( SetItem ( 3848 ) ( SetItem ( 3868 ) ( SetItem ( 3882 ) ( SetItem ( 390 ) ( SetItem ( 3910 ) ( SetItem ( 395 ) ( SetItem ( 397 ) ( SetItem ( 3989 ) ( SetItem ( 4025 ) ( SetItem ( 405 ) ( SetItem ( 4056 ) ( SetItem ( 4100 ) ( SetItem ( 413 ) ( SetItem ( 4134 ) ( SetItem ( 4148 ) ( SetItem ( 4177 ) ( SetItem ( 4197 ) ( SetItem ( 4231 ) ( SetItem ( 426 ) ( SetItem ( 435 ) ( SetItem ( 4373 ) ( SetItem ( 4399 ) ( SetItem ( 443 ) ( SetItem ( 4460 ) ( SetItem ( 4465 ) ( SetItem ( 4489 ) ( SetItem ( 4493 ) ( SetItem ( 4498 ) ( SetItem ( 451 ) ( SetItem ( 4512 ) ( SetItem ( 4540 ) ( SetItem ( 459 ) ( SetItem ( 4627 ) ( SetItem ( 4647 ) ( SetItem ( 467 ) ( SetItem ( 4721 ) ( SetItem ( 475 ) ( SetItem ( 4797 ) ( SetItem ( 4811 ) ( SetItem ( 483 ) ( SetItem ( 4839 ) ( SetItem ( 4935 ) ( SetItem ( 496 ) ( SetItem ( 4961 ) ( SetItem ( 4981 ) ( SetItem ( 504 ) ( SetItem ( 5064 ) ( SetItem ( 512 ) ( SetItem ( 5160 ) ( SetItem ( 5174 ) ( SetItem ( 520 ) ( SetItem ( 5202 ) ( SetItem ( 5304 ) ( SetItem ( 5324 ) ( SetItem ( 533 ) ( SetItem ( 5402 ) ( SetItem ( 541 ) ( SetItem ( 5442 ) ( SetItem ( 5469 ) ( SetItem ( 549 ) ( SetItem ( 5567 ) ( SetItem ( 557 ) ( SetItem ( 5587 ) ( SetItem ( 565 ) ( SetItem ( 5666 ) ( SetItem ( 5702 ) ( SetItem ( 5717 ) ( SetItem ( 5728 ) ( SetItem ( 573 ) ( SetItem ( 5762 ) ( SetItem ( 5772 ) ( SetItem ( 581 ) ( SetItem ( 5883 ) ( SetItem ( 589 ) ( SetItem ( 5938 ) ( SetItem ( 5993 ) ( SetItem ( 6009 ) ( SetItem ( 605 ) ( SetItem ( 6122 ) ( SetItem ( 613 ) ( SetItem ( 6177 ) ( SetItem ( 621 ) ( SetItem ( 6232 ) ( SetItem ( 6248 ) ( SetItem ( 6275 ) ( SetItem ( 629 ) ( SetItem ( 6314 ) ( SetItem ( 6339 ) ( SetItem ( 6349 ) ( SetItem ( 6357 ) ( SetItem ( 6363 ) ( SetItem ( 6367 ) ( SetItem ( 637 ) ( SetItem ( 6373 ) ( SetItem ( 645 ) ( SetItem ( 6527 ) ( SetItem ( 6553 ) ( SetItem ( 658 ) ( SetItem ( 6614 ) ( SetItem ( 6619 ) ( SetItem ( 6624 ) ( SetItem ( 6641 ) ( SetItem ( 6654 ) ( SetItem ( 6667 ) ( SetItem ( 6680 ) ( SetItem ( 6698 ) ( SetItem ( 672 ) ( SetItem ( 6721 ) ( SetItem ( 6728 ) ( SetItem ( 6756 ) ( SetItem ( 6793 ) ( SetItem ( 6805 ) ( SetItem ( 6845 ) ( SetItem ( 6906 ) ( SetItem ( 6948 ) ( SetItem ( 6969 ) ( SetItem ( 6984 ) ( SetItem ( 6987 ) ( SetItem ( 700 ) ( SetItem ( 7011 ) ( SetItem ( 7028 ) ( SetItem ( 7052 ) ( SetItem ( 7072 ) ( SetItem ( 7111 ) ( SetItem ( 7139 ) ( SetItem ( 7157 ) ( SetItem ( 7170 ) ( SetItem ( 7231 ) ( SetItem ( 7250 ) ( SetItem ( 7311 ) ( SetItem ( 7329 ) ( SetItem ( 7345 ) ( SetItem ( 7365 ) ( SetItem ( 7397 ) ( SetItem ( 7403 ) ( SetItem ( 7438 ) ( SetItem ( 7452 ) ( SetItem ( 7470 ) ( SetItem ( 7480 ) ( SetItem ( 7502 ) ( SetItem ( 7520 ) ( SetItem ( 7544 ) ( SetItem ( 7564 ) ( SetItem ( 7582 ) ( SetItem ( 7622 ) ( SetItem ( 7647 ) ( SetItem ( 7664 ) ( SetItem ( 7675 ) ( SetItem ( 7694 ) ( SetItem ( 7711 ) ( SetItem ( 7753 ) ( SetItem ( 7771 ) ( SetItem ( 7779 ) ( SetItem ( 7821 ) ( SetItem ( 7863 ) ( SetItem ( 7877 ) ( SetItem ( 789 ) ( SetItem ( 7919 ) ( SetItem ( 7941 ) ( SetItem ( 7973 ) ( SetItem ( 7997 ) ( SetItem ( 8029 ) ( SetItem ( 8089 ) ( SetItem ( 809 ) ( SetItem ( 8094 ) ( SetItem ( 8102 ) ( SetItem ( 8104 ) ( SetItem ( 8118 ) ( SetItem ( 8123 ) ( SetItem ( 8143 ) ( SetItem ( 8157 ) ( SetItem ( 8162 ) ( SetItem ( 8193 ) ( SetItem ( 8202 ) ( SetItem ( 8230 ) ( SetItem ( 8248 ) ( SetItem ( 8272 ) ( SetItem ( 8296 ) ( SetItem ( 8303 ) ( SetItem ( 8324 ) ( SetItem ( 8347 ) ( SetItem ( 8375 ) ( SetItem ( 8387 ) ( SetItem ( 8400 ) ( SetItem ( 8419 ) ( SetItem ( 8442 ) ( SetItem ( 8454 ) ( SetItem ( 8466 ) ( SetItem ( 8507 ) ( SetItem ( 8544 ) ( SetItem ( 8553 ) ( SetItem ( 8573 ) ( SetItem ( 8651 ) ( SetItem ( 8664 ) ( SetItem ( 867 ) ( SetItem ( 8692 ) ( SetItem ( 8730 ) ( SetItem ( 8743 ) ( SetItem ( 8772 ) ( SetItem ( 8797 ) ( SetItem ( 8802 ) ( SetItem ( 8808 ) ( SetItem ( 8810 ) ( SetItem ( 8873 ) ( SetItem ( 8892 ) ( SetItem ( 8968 ) ( SetItem ( 9000 ) ( SetItem ( 9060 ) ( SetItem ( 9065 ) ( SetItem ( 9073 ) ( SetItem ( 9075 ) ( SetItem ( 9089 ) ( SetItem ( 9094 ) ( SetItem ( 9114 ) ( SetItem ( 9128 ) ( SetItem ( 9133 ) ( SetItem ( 9164 ) ( SetItem ( 9173 ) ( SetItem ( 9201 ) ( SetItem ( 9219 ) ( SetItem ( 9243 ) ( SetItem ( 9267 ) ( SetItem ( 9274 ) ( SetItem ( 9295 ) ( SetItem ( 9318 ) ( SetItem ( 9346 ) ( SetItem ( 9358 ) ( SetItem ( 936 ) ( SetItem ( 9371 ) ( SetItem ( 9390 ) ( SetItem ( 9413 ) ( SetItem ( 9425 ) ( SetItem ( 9437 ) ( SetItem ( 9478 ) ( SetItem ( 9515 ) ( SetItem ( 9524 ) ( SetItem ( 9544 ) ( SetItem ( 962 ) ( SetItem ( 9622 ) ( SetItem ( 9654 ) ( SetItem ( 9692 ) ( SetItem ( 9697 ) ( SetItem ( 9711 ) ( SetItem ( 9716 ) ( SetItem ( 9729 ) ( SetItem ( 9738 ) ( SetItem ( 9752 ) ( SetItem ( 9757 ) ( SetItem ( 9778 ) ( SetItem ( 982 ) ( SetItem ( 9830 ) ( SetItem ( 9839 ) ( SetItem ( 9880 ) ( SetItem ( 9937 ) ( SetItem ( 9949 ) ( SetItem ( 9967 ) ( SetItem ( 9983 ) SetItem ( 9990 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 16 ) ( SetItem ( 86 ) ( SetItem ( 48 ) ( SetItem ( 91 ) ( SetItem ( 343 ) ( SetItem ( 377 ) ( SetItem ( 361 ) ( SetItem ( 331 ) ( SetItem ( 384 ) ( SetItem ( 274 ) ( SetItem ( 224 ) ( SetItem ( 233 ) ( SetItem ( 116 ) ( SetItem ( 110 ) ( SetItem ( 105 ) ( SetItem ( 170 ) ( SetItem ( 172 ) ( SetItem ( 132 ) ( SetItem ( 123 ) ( SetItem ( 151 ) ( SetItem ( 146 ) ( SetItem ( 401 ) ( SetItem ( 447 ) SetItem ( 429 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 86 ) ( SetItem ( 48 ) ( SetItem ( 91 ) ( SetItem ( 343 ) ( SetItem ( 377 ) ( SetItem ( 361 ) ( SetItem ( 331 ) ( SetItem ( 384 ) ( SetItem ( 274 ) ( SetItem ( 224 ) ( SetItem ( 233 ) ( SetItem ( 110 ) ( SetItem ( 105 ) ( SetItem ( 172 ) ( SetItem ( 132 ) ( SetItem ( 123 ) ( SetItem ( 151 ) ( SetItem ( 146 ) ( SetItem ( 401 ) ( SetItem ( 447 ) SetItem ( 429 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
diff --git a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k
index d3631bb499..6e1813638e 100644
--- a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k
+++ b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k
@@ -143,7 +143,7 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_BYTES4-0-SPEC
                  <jumpDests>
                    ( SetItem ( 10007 ) ( SetItem ( 10035 ) ( SetItem ( 10053 ) ( SetItem ( 1030 ) ( SetItem ( 1054 ) ( SetItem ( 1074 ) ( SetItem ( 1082 ) ( SetItem ( 113 ) ( SetItem ( 1150 ) ( SetItem ( 1159 ) ( SetItem ( 1217 ) ( SetItem ( 1247 ) ( SetItem ( 1257 ) ( SetItem ( 1271 ) ( SetItem ( 1299 ) ( SetItem ( 1378 ) ( SetItem ( 1398 ) ( SetItem ( 1459 ) ( SetItem ( 1479 ) ( SetItem ( 1486 ) ( SetItem ( 151 ) ( SetItem ( 1582 ) ( SetItem ( 16 ) ( SetItem ( 1678 ) ( SetItem ( 1692 ) ( SetItem ( 1720 ) ( SetItem ( 1807 ) ( SetItem ( 1827 ) ( SetItem ( 1898 ) ( SetItem ( 1922 ) ( SetItem ( 1981 ) ( SetItem ( 1998 ) ( SetItem ( 2023 ) ( SetItem ( 2059 ) ( SetItem ( 2167 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2253 ) ( SetItem ( 2262 ) ( SetItem ( 2338 ) ( SetItem ( 2358 ) ( SetItem ( 2370 ) ( SetItem ( 2372 ) ( SetItem ( 2386 ) ( SetItem ( 2414 ) ( SetItem ( 2493 ) ( SetItem ( 2513 ) ( SetItem ( 2579 ) ( SetItem ( 2615 ) ( SetItem ( 2619 ) ( SetItem ( 2655 ) ( SetItem ( 2686 ) ( SetItem ( 2730 ) ( SetItem ( 2764 ) ( SetItem ( 2778 ) ( SetItem ( 2807 ) ( SetItem ( 2827 ) ( SetItem ( 2841 ) ( SetItem ( 2869 ) ( SetItem ( 2948 ) ( SetItem ( 2968 ) ( SetItem ( 3034 ) ( SetItem ( 304 ) ( SetItem ( 3070 ) ( SetItem ( 3147 ) ( SetItem ( 3167 ) ( SetItem ( 3228 ) ( SetItem ( 3281 ) ( SetItem ( 3307 ) ( SetItem ( 3327 ) ( SetItem ( 3390 ) ( SetItem ( 3410 ) ( SetItem ( 3416 ) ( SetItem ( 3452 ) ( SetItem ( 3560 ) ( SetItem ( 3622 ) ( SetItem ( 3646 ) ( SetItem ( 3660 ) ( SetItem ( 3688 ) ( SetItem ( 371 ) ( SetItem ( 376 ) ( SetItem ( 3767 ) ( SetItem ( 3787 ) ( SetItem ( 3848 ) ( SetItem ( 3868 ) ( SetItem ( 3882 ) ( SetItem ( 390 ) ( SetItem ( 3910 ) ( SetItem ( 395 ) ( SetItem ( 397 ) ( SetItem ( 3989 ) ( SetItem ( 4025 ) ( SetItem ( 405 ) ( SetItem ( 4056 ) ( SetItem ( 4100 ) ( SetItem ( 413 ) ( SetItem ( 4134 ) ( SetItem ( 4148 ) ( SetItem ( 4177 ) ( SetItem ( 4197 ) ( SetItem ( 4231 ) ( SetItem ( 426 ) ( SetItem ( 435 ) ( SetItem ( 4373 ) ( SetItem ( 4399 ) ( SetItem ( 443 ) ( SetItem ( 4460 ) ( SetItem ( 4465 ) ( SetItem ( 4489 ) ( SetItem ( 4493 ) ( SetItem ( 4498 ) ( SetItem ( 451 ) ( SetItem ( 4512 ) ( SetItem ( 4540 ) ( SetItem ( 459 ) ( SetItem ( 4627 ) ( SetItem ( 4647 ) ( SetItem ( 467 ) ( SetItem ( 4721 ) ( SetItem ( 475 ) ( SetItem ( 4797 ) ( SetItem ( 4811 ) ( SetItem ( 483 ) ( SetItem ( 4839 ) ( SetItem ( 4935 ) ( SetItem ( 496 ) ( SetItem ( 4961 ) ( SetItem ( 4981 ) ( SetItem ( 504 ) ( SetItem ( 5064 ) ( SetItem ( 512 ) ( SetItem ( 5160 ) ( SetItem ( 5174 ) ( SetItem ( 520 ) ( SetItem ( 5202 ) ( SetItem ( 5304 ) ( SetItem ( 5324 ) ( SetItem ( 533 ) ( SetItem ( 5402 ) ( SetItem ( 541 ) ( SetItem ( 5442 ) ( SetItem ( 5469 ) ( SetItem ( 549 ) ( SetItem ( 5567 ) ( SetItem ( 557 ) ( SetItem ( 5587 ) ( SetItem ( 565 ) ( SetItem ( 5666 ) ( SetItem ( 5702 ) ( SetItem ( 5717 ) ( SetItem ( 5728 ) ( SetItem ( 573 ) ( SetItem ( 5762 ) ( SetItem ( 5772 ) ( SetItem ( 581 ) ( SetItem ( 5883 ) ( SetItem ( 589 ) ( SetItem ( 5938 ) ( SetItem ( 5993 ) ( SetItem ( 6009 ) ( SetItem ( 605 ) ( SetItem ( 6122 ) ( SetItem ( 613 ) ( SetItem ( 6177 ) ( SetItem ( 621 ) ( SetItem ( 6232 ) ( SetItem ( 6248 ) ( SetItem ( 6275 ) ( SetItem ( 629 ) ( SetItem ( 6314 ) ( SetItem ( 6339 ) ( SetItem ( 6349 ) ( SetItem ( 6357 ) ( SetItem ( 6363 ) ( SetItem ( 6367 ) ( SetItem ( 637 ) ( SetItem ( 6373 ) ( SetItem ( 645 ) ( SetItem ( 6527 ) ( SetItem ( 6553 ) ( SetItem ( 658 ) ( SetItem ( 6614 ) ( SetItem ( 6619 ) ( SetItem ( 6624 ) ( SetItem ( 6641 ) ( SetItem ( 6654 ) ( SetItem ( 6667 ) ( SetItem ( 6680 ) ( SetItem ( 6698 ) ( SetItem ( 672 ) ( SetItem ( 6721 ) ( SetItem ( 6728 ) ( SetItem ( 6756 ) ( SetItem ( 6793 ) ( SetItem ( 6805 ) ( SetItem ( 6845 ) ( SetItem ( 6906 ) ( SetItem ( 6948 ) ( SetItem ( 6969 ) ( SetItem ( 6984 ) ( SetItem ( 6987 ) ( SetItem ( 700 ) ( SetItem ( 7011 ) ( SetItem ( 7028 ) ( SetItem ( 7052 ) ( SetItem ( 7072 ) ( SetItem ( 7111 ) ( SetItem ( 7139 ) ( SetItem ( 7157 ) ( SetItem ( 7170 ) ( SetItem ( 7231 ) ( SetItem ( 7250 ) ( SetItem ( 7311 ) ( SetItem ( 7329 ) ( SetItem ( 7345 ) ( SetItem ( 7365 ) ( SetItem ( 7397 ) ( SetItem ( 7403 ) ( SetItem ( 7438 ) ( SetItem ( 7452 ) ( SetItem ( 7470 ) ( SetItem ( 7480 ) ( SetItem ( 7502 ) ( SetItem ( 7520 ) ( SetItem ( 7544 ) ( SetItem ( 7564 ) ( SetItem ( 7582 ) ( SetItem ( 7622 ) ( SetItem ( 7647 ) ( SetItem ( 7664 ) ( SetItem ( 7675 ) ( SetItem ( 7694 ) ( SetItem ( 7711 ) ( SetItem ( 7753 ) ( SetItem ( 7771 ) ( SetItem ( 7779 ) ( SetItem ( 7821 ) ( SetItem ( 7863 ) ( SetItem ( 7877 ) ( SetItem ( 789 ) ( SetItem ( 7919 ) ( SetItem ( 7941 ) ( SetItem ( 7973 ) ( SetItem ( 7997 ) ( SetItem ( 8029 ) ( SetItem ( 8089 ) ( SetItem ( 809 ) ( SetItem ( 8094 ) ( SetItem ( 8102 ) ( SetItem ( 8104 ) ( SetItem ( 8118 ) ( SetItem ( 8123 ) ( SetItem ( 8143 ) ( SetItem ( 8157 ) ( SetItem ( 8162 ) ( SetItem ( 8193 ) ( SetItem ( 8202 ) ( SetItem ( 8230 ) ( SetItem ( 8248 ) ( SetItem ( 8272 ) ( SetItem ( 8296 ) ( SetItem ( 8303 ) ( SetItem ( 8324 ) ( SetItem ( 8347 ) ( SetItem ( 8375 ) ( SetItem ( 8387 ) ( SetItem ( 8400 ) ( SetItem ( 8419 ) ( SetItem ( 8442 ) ( SetItem ( 8454 ) ( SetItem ( 8466 ) ( SetItem ( 8507 ) ( SetItem ( 8544 ) ( SetItem ( 8553 ) ( SetItem ( 8573 ) ( SetItem ( 8651 ) ( SetItem ( 8664 ) ( SetItem ( 867 ) ( SetItem ( 8692 ) ( SetItem ( 8730 ) ( SetItem ( 8743 ) ( SetItem ( 8772 ) ( SetItem ( 8797 ) ( SetItem ( 8802 ) ( SetItem ( 8808 ) ( SetItem ( 8810 ) ( SetItem ( 8873 ) ( SetItem ( 8892 ) ( SetItem ( 8968 ) ( SetItem ( 9000 ) ( SetItem ( 9060 ) ( SetItem ( 9065 ) ( SetItem ( 9073 ) ( SetItem ( 9075 ) ( SetItem ( 9089 ) ( SetItem ( 9094 ) ( SetItem ( 9114 ) ( SetItem ( 9128 ) ( SetItem ( 9133 ) ( SetItem ( 9164 ) ( SetItem ( 9173 ) ( SetItem ( 9201 ) ( SetItem ( 9219 ) ( SetItem ( 9243 ) ( SetItem ( 9267 ) ( SetItem ( 9274 ) ( SetItem ( 9295 ) ( SetItem ( 9318 ) ( SetItem ( 9346 ) ( SetItem ( 9358 ) ( SetItem ( 936 ) ( SetItem ( 9371 ) ( SetItem ( 9390 ) ( SetItem ( 9413 ) ( SetItem ( 9425 ) ( SetItem ( 9437 ) ( SetItem ( 9478 ) ( SetItem ( 9515 ) ( SetItem ( 9524 ) ( SetItem ( 9544 ) ( SetItem ( 962 ) ( SetItem ( 9622 ) ( SetItem ( 9654 ) ( SetItem ( 9692 ) ( SetItem ( 9697 ) ( SetItem ( 9711 ) ( SetItem ( 9716 ) ( SetItem ( 9729 ) ( SetItem ( 9738 ) ( SetItem ( 9752 ) ( SetItem ( 9757 ) ( SetItem ( 9778 ) ( SetItem ( 982 ) ( SetItem ( 9830 ) ( SetItem ( 9839 ) ( SetItem ( 9880 ) ( SetItem ( 9937 ) ( SetItem ( 9949 ) ( SetItem ( 9967 ) ( SetItem ( 9983 ) SetItem ( 9990 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 77 ) ( SetItem ( 16 ) ( SetItem ( 84 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
diff --git a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k
index 350d818327..d3469b1192 100644
--- a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k
+++ b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k
@@ -143,7 +143,7 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FAILANDSUCCESS-0-SPEC
                  <jumpDests>
                    ( SetItem ( 10007 ) ( SetItem ( 10035 ) ( SetItem ( 10053 ) ( SetItem ( 1030 ) ( SetItem ( 1054 ) ( SetItem ( 1074 ) ( SetItem ( 1082 ) ( SetItem ( 113 ) ( SetItem ( 1150 ) ( SetItem ( 1159 ) ( SetItem ( 1217 ) ( SetItem ( 1247 ) ( SetItem ( 1257 ) ( SetItem ( 1271 ) ( SetItem ( 1299 ) ( SetItem ( 1378 ) ( SetItem ( 1398 ) ( SetItem ( 1459 ) ( SetItem ( 1479 ) ( SetItem ( 1486 ) ( SetItem ( 151 ) ( SetItem ( 1582 ) ( SetItem ( 16 ) ( SetItem ( 1678 ) ( SetItem ( 1692 ) ( SetItem ( 1720 ) ( SetItem ( 1807 ) ( SetItem ( 1827 ) ( SetItem ( 1898 ) ( SetItem ( 1922 ) ( SetItem ( 1981 ) ( SetItem ( 1998 ) ( SetItem ( 2023 ) ( SetItem ( 2059 ) ( SetItem ( 2167 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2253 ) ( SetItem ( 2262 ) ( SetItem ( 2338 ) ( SetItem ( 2358 ) ( SetItem ( 2370 ) ( SetItem ( 2372 ) ( SetItem ( 2386 ) ( SetItem ( 2414 ) ( SetItem ( 2493 ) ( SetItem ( 2513 ) ( SetItem ( 2579 ) ( SetItem ( 2615 ) ( SetItem ( 2619 ) ( SetItem ( 2655 ) ( SetItem ( 2686 ) ( SetItem ( 2730 ) ( SetItem ( 2764 ) ( SetItem ( 2778 ) ( SetItem ( 2807 ) ( SetItem ( 2827 ) ( SetItem ( 2841 ) ( SetItem ( 2869 ) ( SetItem ( 2948 ) ( SetItem ( 2968 ) ( SetItem ( 3034 ) ( SetItem ( 304 ) ( SetItem ( 3070 ) ( SetItem ( 3147 ) ( SetItem ( 3167 ) ( SetItem ( 3228 ) ( SetItem ( 3281 ) ( SetItem ( 3307 ) ( SetItem ( 3327 ) ( SetItem ( 3390 ) ( SetItem ( 3410 ) ( SetItem ( 3416 ) ( SetItem ( 3452 ) ( SetItem ( 3560 ) ( SetItem ( 3622 ) ( SetItem ( 3646 ) ( SetItem ( 3660 ) ( SetItem ( 3688 ) ( SetItem ( 371 ) ( SetItem ( 376 ) ( SetItem ( 3767 ) ( SetItem ( 3787 ) ( SetItem ( 3848 ) ( SetItem ( 3868 ) ( SetItem ( 3882 ) ( SetItem ( 390 ) ( SetItem ( 3910 ) ( SetItem ( 395 ) ( SetItem ( 397 ) ( SetItem ( 3989 ) ( SetItem ( 4025 ) ( SetItem ( 405 ) ( SetItem ( 4056 ) ( SetItem ( 4100 ) ( SetItem ( 413 ) ( SetItem ( 4134 ) ( SetItem ( 4148 ) ( SetItem ( 4177 ) ( SetItem ( 4197 ) ( SetItem ( 4231 ) ( SetItem ( 426 ) ( SetItem ( 435 ) ( SetItem ( 4373 ) ( SetItem ( 4399 ) ( SetItem ( 443 ) ( SetItem ( 4460 ) ( SetItem ( 4465 ) ( SetItem ( 4489 ) ( SetItem ( 4493 ) ( SetItem ( 4498 ) ( SetItem ( 451 ) ( SetItem ( 4512 ) ( SetItem ( 4540 ) ( SetItem ( 459 ) ( SetItem ( 4627 ) ( SetItem ( 4647 ) ( SetItem ( 467 ) ( SetItem ( 4721 ) ( SetItem ( 475 ) ( SetItem ( 4797 ) ( SetItem ( 4811 ) ( SetItem ( 483 ) ( SetItem ( 4839 ) ( SetItem ( 4935 ) ( SetItem ( 496 ) ( SetItem ( 4961 ) ( SetItem ( 4981 ) ( SetItem ( 504 ) ( SetItem ( 5064 ) ( SetItem ( 512 ) ( SetItem ( 5160 ) ( SetItem ( 5174 ) ( SetItem ( 520 ) ( SetItem ( 5202 ) ( SetItem ( 5304 ) ( SetItem ( 5324 ) ( SetItem ( 533 ) ( SetItem ( 5402 ) ( SetItem ( 541 ) ( SetItem ( 5442 ) ( SetItem ( 5469 ) ( SetItem ( 549 ) ( SetItem ( 5567 ) ( SetItem ( 557 ) ( SetItem ( 5587 ) ( SetItem ( 565 ) ( SetItem ( 5666 ) ( SetItem ( 5702 ) ( SetItem ( 5717 ) ( SetItem ( 5728 ) ( SetItem ( 573 ) ( SetItem ( 5762 ) ( SetItem ( 5772 ) ( SetItem ( 581 ) ( SetItem ( 5883 ) ( SetItem ( 589 ) ( SetItem ( 5938 ) ( SetItem ( 5993 ) ( SetItem ( 6009 ) ( SetItem ( 605 ) ( SetItem ( 6122 ) ( SetItem ( 613 ) ( SetItem ( 6177 ) ( SetItem ( 621 ) ( SetItem ( 6232 ) ( SetItem ( 6248 ) ( SetItem ( 6275 ) ( SetItem ( 629 ) ( SetItem ( 6314 ) ( SetItem ( 6339 ) ( SetItem ( 6349 ) ( SetItem ( 6357 ) ( SetItem ( 6363 ) ( SetItem ( 6367 ) ( SetItem ( 637 ) ( SetItem ( 6373 ) ( SetItem ( 645 ) ( SetItem ( 6527 ) ( SetItem ( 6553 ) ( SetItem ( 658 ) ( SetItem ( 6614 ) ( SetItem ( 6619 ) ( SetItem ( 6624 ) ( SetItem ( 6641 ) ( SetItem ( 6654 ) ( SetItem ( 6667 ) ( SetItem ( 6680 ) ( SetItem ( 6698 ) ( SetItem ( 672 ) ( SetItem ( 6721 ) ( SetItem ( 6728 ) ( SetItem ( 6756 ) ( SetItem ( 6793 ) ( SetItem ( 6805 ) ( SetItem ( 6845 ) ( SetItem ( 6906 ) ( SetItem ( 6948 ) ( SetItem ( 6969 ) ( SetItem ( 6984 ) ( SetItem ( 6987 ) ( SetItem ( 700 ) ( SetItem ( 7011 ) ( SetItem ( 7028 ) ( SetItem ( 7052 ) ( SetItem ( 7072 ) ( SetItem ( 7111 ) ( SetItem ( 7139 ) ( SetItem ( 7157 ) ( SetItem ( 7170 ) ( SetItem ( 7231 ) ( SetItem ( 7250 ) ( SetItem ( 7311 ) ( SetItem ( 7329 ) ( SetItem ( 7345 ) ( SetItem ( 7365 ) ( SetItem ( 7397 ) ( SetItem ( 7403 ) ( SetItem ( 7438 ) ( SetItem ( 7452 ) ( SetItem ( 7470 ) ( SetItem ( 7480 ) ( SetItem ( 7502 ) ( SetItem ( 7520 ) ( SetItem ( 7544 ) ( SetItem ( 7564 ) ( SetItem ( 7582 ) ( SetItem ( 7622 ) ( SetItem ( 7647 ) ( SetItem ( 7664 ) ( SetItem ( 7675 ) ( SetItem ( 7694 ) ( SetItem ( 7711 ) ( SetItem ( 7753 ) ( SetItem ( 7771 ) ( SetItem ( 7779 ) ( SetItem ( 7821 ) ( SetItem ( 7863 ) ( SetItem ( 7877 ) ( SetItem ( 789 ) ( SetItem ( 7919 ) ( SetItem ( 7941 ) ( SetItem ( 7973 ) ( SetItem ( 7997 ) ( SetItem ( 8029 ) ( SetItem ( 8089 ) ( SetItem ( 809 ) ( SetItem ( 8094 ) ( SetItem ( 8102 ) ( SetItem ( 8104 ) ( SetItem ( 8118 ) ( SetItem ( 8123 ) ( SetItem ( 8143 ) ( SetItem ( 8157 ) ( SetItem ( 8162 ) ( SetItem ( 8193 ) ( SetItem ( 8202 ) ( SetItem ( 8230 ) ( SetItem ( 8248 ) ( SetItem ( 8272 ) ( SetItem ( 8296 ) ( SetItem ( 8303 ) ( SetItem ( 8324 ) ( SetItem ( 8347 ) ( SetItem ( 8375 ) ( SetItem ( 8387 ) ( SetItem ( 8400 ) ( SetItem ( 8419 ) ( SetItem ( 8442 ) ( SetItem ( 8454 ) ( SetItem ( 8466 ) ( SetItem ( 8507 ) ( SetItem ( 8544 ) ( SetItem ( 8553 ) ( SetItem ( 8573 ) ( SetItem ( 8651 ) ( SetItem ( 8664 ) ( SetItem ( 867 ) ( SetItem ( 8692 ) ( SetItem ( 8730 ) ( SetItem ( 8743 ) ( SetItem ( 8772 ) ( SetItem ( 8797 ) ( SetItem ( 8802 ) ( SetItem ( 8808 ) ( SetItem ( 8810 ) ( SetItem ( 8873 ) ( SetItem ( 8892 ) ( SetItem ( 8968 ) ( SetItem ( 9000 ) ( SetItem ( 9060 ) ( SetItem ( 9065 ) ( SetItem ( 9073 ) ( SetItem ( 9075 ) ( SetItem ( 9089 ) ( SetItem ( 9094 ) ( SetItem ( 9114 ) ( SetItem ( 9128 ) ( SetItem ( 9133 ) ( SetItem ( 9164 ) ( SetItem ( 9173 ) ( SetItem ( 9201 ) ( SetItem ( 9219 ) ( SetItem ( 9243 ) ( SetItem ( 9267 ) ( SetItem ( 9274 ) ( SetItem ( 9295 ) ( SetItem ( 9318 ) ( SetItem ( 9346 ) ( SetItem ( 9358 ) ( SetItem ( 936 ) ( SetItem ( 9371 ) ( SetItem ( 9390 ) ( SetItem ( 9413 ) ( SetItem ( 9425 ) ( SetItem ( 9437 ) ( SetItem ( 9478 ) ( SetItem ( 9515 ) ( SetItem ( 9524 ) ( SetItem ( 9544 ) ( SetItem ( 962 ) ( SetItem ( 9622 ) ( SetItem ( 9654 ) ( SetItem ( 9692 ) ( SetItem ( 9697 ) ( SetItem ( 9711 ) ( SetItem ( 9716 ) ( SetItem ( 9729 ) ( SetItem ( 9738 ) ( SetItem ( 9752 ) ( SetItem ( 9757 ) ( SetItem ( 9778 ) ( SetItem ( 982 ) ( SetItem ( 9830 ) ( SetItem ( 9839 ) ( SetItem ( 9880 ) ( SetItem ( 9937 ) ( SetItem ( 9949 ) ( SetItem ( 9967 ) ( SetItem ( 9983 ) SetItem ( 9990 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 77 ) ( SetItem ( 16 ) ( SetItem ( 84 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
diff --git a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k
index 8174547f28..4f1c87767d 100644
--- a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k
+++ b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k
@@ -143,7 +143,7 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC
                  <jumpDests>
                    ( SetItem ( 10007 ) ( SetItem ( 10035 ) ( SetItem ( 10053 ) ( SetItem ( 1030 ) ( SetItem ( 1054 ) ( SetItem ( 1074 ) ( SetItem ( 1082 ) ( SetItem ( 113 ) ( SetItem ( 1150 ) ( SetItem ( 1159 ) ( SetItem ( 1217 ) ( SetItem ( 1247 ) ( SetItem ( 1257 ) ( SetItem ( 1271 ) ( SetItem ( 1299 ) ( SetItem ( 1378 ) ( SetItem ( 1398 ) ( SetItem ( 1459 ) ( SetItem ( 1479 ) ( SetItem ( 1486 ) ( SetItem ( 151 ) ( SetItem ( 1582 ) ( SetItem ( 16 ) ( SetItem ( 1678 ) ( SetItem ( 1692 ) ( SetItem ( 1720 ) ( SetItem ( 1807 ) ( SetItem ( 1827 ) ( SetItem ( 1898 ) ( SetItem ( 1922 ) ( SetItem ( 1981 ) ( SetItem ( 1998 ) ( SetItem ( 2023 ) ( SetItem ( 2059 ) ( SetItem ( 2167 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2253 ) ( SetItem ( 2262 ) ( SetItem ( 2338 ) ( SetItem ( 2358 ) ( SetItem ( 2370 ) ( SetItem ( 2372 ) ( SetItem ( 2386 ) ( SetItem ( 2414 ) ( SetItem ( 2493 ) ( SetItem ( 2513 ) ( SetItem ( 2579 ) ( SetItem ( 2615 ) ( SetItem ( 2619 ) ( SetItem ( 2655 ) ( SetItem ( 2686 ) ( SetItem ( 2730 ) ( SetItem ( 2764 ) ( SetItem ( 2778 ) ( SetItem ( 2807 ) ( SetItem ( 2827 ) ( SetItem ( 2841 ) ( SetItem ( 2869 ) ( SetItem ( 2948 ) ( SetItem ( 2968 ) ( SetItem ( 3034 ) ( SetItem ( 304 ) ( SetItem ( 3070 ) ( SetItem ( 3147 ) ( SetItem ( 3167 ) ( SetItem ( 3228 ) ( SetItem ( 3281 ) ( SetItem ( 3307 ) ( SetItem ( 3327 ) ( SetItem ( 3390 ) ( SetItem ( 3410 ) ( SetItem ( 3416 ) ( SetItem ( 3452 ) ( SetItem ( 3560 ) ( SetItem ( 3622 ) ( SetItem ( 3646 ) ( SetItem ( 3660 ) ( SetItem ( 3688 ) ( SetItem ( 371 ) ( SetItem ( 376 ) ( SetItem ( 3767 ) ( SetItem ( 3787 ) ( SetItem ( 3848 ) ( SetItem ( 3868 ) ( SetItem ( 3882 ) ( SetItem ( 390 ) ( SetItem ( 3910 ) ( SetItem ( 395 ) ( SetItem ( 397 ) ( SetItem ( 3989 ) ( SetItem ( 4025 ) ( SetItem ( 405 ) ( SetItem ( 4056 ) ( SetItem ( 4100 ) ( SetItem ( 413 ) ( SetItem ( 4134 ) ( SetItem ( 4148 ) ( SetItem ( 4177 ) ( SetItem ( 4197 ) ( SetItem ( 4231 ) ( SetItem ( 426 ) ( SetItem ( 435 ) ( SetItem ( 4373 ) ( SetItem ( 4399 ) ( SetItem ( 443 ) ( SetItem ( 4460 ) ( SetItem ( 4465 ) ( SetItem ( 4489 ) ( SetItem ( 4493 ) ( SetItem ( 4498 ) ( SetItem ( 451 ) ( SetItem ( 4512 ) ( SetItem ( 4540 ) ( SetItem ( 459 ) ( SetItem ( 4627 ) ( SetItem ( 4647 ) ( SetItem ( 467 ) ( SetItem ( 4721 ) ( SetItem ( 475 ) ( SetItem ( 4797 ) ( SetItem ( 4811 ) ( SetItem ( 483 ) ( SetItem ( 4839 ) ( SetItem ( 4935 ) ( SetItem ( 496 ) ( SetItem ( 4961 ) ( SetItem ( 4981 ) ( SetItem ( 504 ) ( SetItem ( 5064 ) ( SetItem ( 512 ) ( SetItem ( 5160 ) ( SetItem ( 5174 ) ( SetItem ( 520 ) ( SetItem ( 5202 ) ( SetItem ( 5304 ) ( SetItem ( 5324 ) ( SetItem ( 533 ) ( SetItem ( 5402 ) ( SetItem ( 541 ) ( SetItem ( 5442 ) ( SetItem ( 5469 ) ( SetItem ( 549 ) ( SetItem ( 5567 ) ( SetItem ( 557 ) ( SetItem ( 5587 ) ( SetItem ( 565 ) ( SetItem ( 5666 ) ( SetItem ( 5702 ) ( SetItem ( 5717 ) ( SetItem ( 5728 ) ( SetItem ( 573 ) ( SetItem ( 5762 ) ( SetItem ( 5772 ) ( SetItem ( 581 ) ( SetItem ( 5883 ) ( SetItem ( 589 ) ( SetItem ( 5938 ) ( SetItem ( 5993 ) ( SetItem ( 6009 ) ( SetItem ( 605 ) ( SetItem ( 6122 ) ( SetItem ( 613 ) ( SetItem ( 6177 ) ( SetItem ( 621 ) ( SetItem ( 6232 ) ( SetItem ( 6248 ) ( SetItem ( 6275 ) ( SetItem ( 629 ) ( SetItem ( 6314 ) ( SetItem ( 6339 ) ( SetItem ( 6349 ) ( SetItem ( 6357 ) ( SetItem ( 6363 ) ( SetItem ( 6367 ) ( SetItem ( 637 ) ( SetItem ( 6373 ) ( SetItem ( 645 ) ( SetItem ( 6527 ) ( SetItem ( 6553 ) ( SetItem ( 658 ) ( SetItem ( 6614 ) ( SetItem ( 6619 ) ( SetItem ( 6624 ) ( SetItem ( 6641 ) ( SetItem ( 6654 ) ( SetItem ( 6667 ) ( SetItem ( 6680 ) ( SetItem ( 6698 ) ( SetItem ( 672 ) ( SetItem ( 6721 ) ( SetItem ( 6728 ) ( SetItem ( 6756 ) ( SetItem ( 6793 ) ( SetItem ( 6805 ) ( SetItem ( 6845 ) ( SetItem ( 6906 ) ( SetItem ( 6948 ) ( SetItem ( 6969 ) ( SetItem ( 6984 ) ( SetItem ( 6987 ) ( SetItem ( 700 ) ( SetItem ( 7011 ) ( SetItem ( 7028 ) ( SetItem ( 7052 ) ( SetItem ( 7072 ) ( SetItem ( 7111 ) ( SetItem ( 7139 ) ( SetItem ( 7157 ) ( SetItem ( 7170 ) ( SetItem ( 7231 ) ( SetItem ( 7250 ) ( SetItem ( 7311 ) ( SetItem ( 7329 ) ( SetItem ( 7345 ) ( SetItem ( 7365 ) ( SetItem ( 7397 ) ( SetItem ( 7403 ) ( SetItem ( 7438 ) ( SetItem ( 7452 ) ( SetItem ( 7470 ) ( SetItem ( 7480 ) ( SetItem ( 7502 ) ( SetItem ( 7520 ) ( SetItem ( 7544 ) ( SetItem ( 7564 ) ( SetItem ( 7582 ) ( SetItem ( 7622 ) ( SetItem ( 7647 ) ( SetItem ( 7664 ) ( SetItem ( 7675 ) ( SetItem ( 7694 ) ( SetItem ( 7711 ) ( SetItem ( 7753 ) ( SetItem ( 7771 ) ( SetItem ( 7779 ) ( SetItem ( 7821 ) ( SetItem ( 7863 ) ( SetItem ( 7877 ) ( SetItem ( 789 ) ( SetItem ( 7919 ) ( SetItem ( 7941 ) ( SetItem ( 7973 ) ( SetItem ( 7997 ) ( SetItem ( 8029 ) ( SetItem ( 8089 ) ( SetItem ( 809 ) ( SetItem ( 8094 ) ( SetItem ( 8102 ) ( SetItem ( 8104 ) ( SetItem ( 8118 ) ( SetItem ( 8123 ) ( SetItem ( 8143 ) ( SetItem ( 8157 ) ( SetItem ( 8162 ) ( SetItem ( 8193 ) ( SetItem ( 8202 ) ( SetItem ( 8230 ) ( SetItem ( 8248 ) ( SetItem ( 8272 ) ( SetItem ( 8296 ) ( SetItem ( 8303 ) ( SetItem ( 8324 ) ( SetItem ( 8347 ) ( SetItem ( 8375 ) ( SetItem ( 8387 ) ( SetItem ( 8400 ) ( SetItem ( 8419 ) ( SetItem ( 8442 ) ( SetItem ( 8454 ) ( SetItem ( 8466 ) ( SetItem ( 8507 ) ( SetItem ( 8544 ) ( SetItem ( 8553 ) ( SetItem ( 8573 ) ( SetItem ( 8651 ) ( SetItem ( 8664 ) ( SetItem ( 867 ) ( SetItem ( 8692 ) ( SetItem ( 8730 ) ( SetItem ( 8743 ) ( SetItem ( 8772 ) ( SetItem ( 8797 ) ( SetItem ( 8802 ) ( SetItem ( 8808 ) ( SetItem ( 8810 ) ( SetItem ( 8873 ) ( SetItem ( 8892 ) ( SetItem ( 8968 ) ( SetItem ( 9000 ) ( SetItem ( 9060 ) ( SetItem ( 9065 ) ( SetItem ( 9073 ) ( SetItem ( 9075 ) ( SetItem ( 9089 ) ( SetItem ( 9094 ) ( SetItem ( 9114 ) ( SetItem ( 9128 ) ( SetItem ( 9133 ) ( SetItem ( 9164 ) ( SetItem ( 9173 ) ( SetItem ( 9201 ) ( SetItem ( 9219 ) ( SetItem ( 9243 ) ( SetItem ( 9267 ) ( SetItem ( 9274 ) ( SetItem ( 9295 ) ( SetItem ( 9318 ) ( SetItem ( 9346 ) ( SetItem ( 9358 ) ( SetItem ( 936 ) ( SetItem ( 9371 ) ( SetItem ( 9390 ) ( SetItem ( 9413 ) ( SetItem ( 9425 ) ( SetItem ( 9437 ) ( SetItem ( 9478 ) ( SetItem ( 9515 ) ( SetItem ( 9524 ) ( SetItem ( 9544 ) ( SetItem ( 962 ) ( SetItem ( 9622 ) ( SetItem ( 9654 ) ( SetItem ( 9692 ) ( SetItem ( 9697 ) ( SetItem ( 9711 ) ( SetItem ( 9716 ) ( SetItem ( 9729 ) ( SetItem ( 9738 ) ( SetItem ( 9752 ) ( SetItem ( 9757 ) ( SetItem ( 9778 ) ( SetItem ( 982 ) ( SetItem ( 9830 ) ( SetItem ( 9839 ) ( SetItem ( 9880 ) ( SetItem ( 9937 ) ( SetItem ( 9949 ) ( SetItem ( 9967 ) ( SetItem ( 9983 ) SetItem ( 9990 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 77 ) ( SetItem ( 16 ) ( SetItem ( 84 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
diff --git a/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k b/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k
index a14f1fa11d..876f2ba817 100644
--- a/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k
+++ b/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k
@@ -143,7 +143,7 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC
                  <jumpDests>
                    ( SetItem ( 102 ) ( SetItem ( 1075 ) ( SetItem ( 1095 ) ( SetItem ( 1101 ) ( SetItem ( 1137 ) ( SetItem ( 1245 ) ( SetItem ( 1307 ) ( SetItem ( 1331 ) ( SetItem ( 1340 ) ( SetItem ( 140 ) ( SetItem ( 1415 ) ( SetItem ( 1451 ) ( SetItem ( 1458 ) ( SetItem ( 1538 ) ( SetItem ( 1558 ) ( SetItem ( 16 ) ( SetItem ( 1648 ) ( SetItem ( 1684 ) ( SetItem ( 1691 ) ( SetItem ( 1693 ) ( SetItem ( 1729 ) ( SetItem ( 1760 ) ( SetItem ( 1804 ) ( SetItem ( 1838 ) ( SetItem ( 1852 ) ( SetItem ( 1881 ) ( SetItem ( 1901 ) ( SetItem ( 1937 ) ( SetItem ( 200 ) ( SetItem ( 2045 ) ( SetItem ( 2107 ) ( SetItem ( 2131 ) ( SetItem ( 2167 ) ( SetItem ( 2198 ) ( SetItem ( 2242 ) ( SetItem ( 2276 ) ( SetItem ( 2290 ) ( SetItem ( 2319 ) ( SetItem ( 2339 ) ( SetItem ( 234 ) ( SetItem ( 2373 ) ( SetItem ( 239 ) ( SetItem ( 247 ) ( SetItem ( 249 ) ( SetItem ( 2515 ) ( SetItem ( 2541 ) ( SetItem ( 257 ) ( SetItem ( 2602 ) ( SetItem ( 2607 ) ( SetItem ( 2631 ) ( SetItem ( 2635 ) ( SetItem ( 2640 ) ( SetItem ( 270 ) ( SetItem ( 2736 ) ( SetItem ( 279 ) ( SetItem ( 2792 ) ( SetItem ( 287 ) ( SetItem ( 2905 ) ( SetItem ( 295 ) ( SetItem ( 303 ) ( SetItem ( 3087 ) ( SetItem ( 3091 ) ( SetItem ( 311 ) ( SetItem ( 324 ) ( SetItem ( 3245 ) ( SetItem ( 3271 ) ( SetItem ( 332 ) ( SetItem ( 3332 ) ( SetItem ( 3337 ) ( SetItem ( 3342 ) ( SetItem ( 3359 ) ( SetItem ( 3372 ) ( SetItem ( 340 ) ( SetItem ( 3400 ) ( SetItem ( 3437 ) ( SetItem ( 3449 ) ( SetItem ( 3489 ) ( SetItem ( 353 ) ( SetItem ( 3550 ) ( SetItem ( 3592 ) ( SetItem ( 361 ) ( SetItem ( 3613 ) ( SetItem ( 3628 ) ( SetItem ( 3631 ) ( SetItem ( 3655 ) ( SetItem ( 3672 ) ( SetItem ( 369 ) ( SetItem ( 3711 ) ( SetItem ( 3750 ) ( SetItem ( 377 ) ( SetItem ( 3781 ) ( SetItem ( 3794 ) ( SetItem ( 3812 ) ( SetItem ( 3819 ) ( SetItem ( 3839 ) ( SetItem ( 3871 ) ( SetItem ( 3877 ) ( SetItem ( 3912 ) ( SetItem ( 3926 ) ( SetItem ( 393 ) ( SetItem ( 3944 ) ( SetItem ( 3954 ) ( SetItem ( 3972 ) ( SetItem ( 3988 ) ( SetItem ( 401 ) ( SetItem ( 4012 ) ( SetItem ( 4065 ) ( SetItem ( 4114 ) ( SetItem ( 4119 ) ( SetItem ( 4128 ) ( SetItem ( 4138 ) ( SetItem ( 414 ) ( SetItem ( 4147 ) ( SetItem ( 4186 ) ( SetItem ( 4210 ) ( SetItem ( 4218 ) ( SetItem ( 422 ) ( SetItem ( 4220 ) ( SetItem ( 4292 ) ( SetItem ( 4307 ) ( SetItem ( 4314 ) ( SetItem ( 434 ) ( SetItem ( 4346 ) ( SetItem ( 462 ) ( SetItem ( 497 ) ( SetItem ( 555 ) ( SetItem ( 585 ) ( SetItem ( 595 ) ( SetItem ( 691 ) ( SetItem ( 787 ) ( SetItem ( 869 ) ( SetItem ( 889 ) ( SetItem ( 945 ) ( SetItem ( 971 ) SetItem ( 991 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 69 ) ( SetItem ( 16 ) ( SetItem ( 350 ) ( SetItem ( 318 ) ( SetItem ( 311 ) ( SetItem ( 296 ) ( SetItem ( 214 ) ( SetItem ( 224 ) ( SetItem ( 222 ) ( SetItem ( 118 ) ( SetItem ( 101 ) ( SetItem ( 132 ) ( SetItem ( 123 ) ( SetItem ( 190 ) ( SetItem ( 151 ) SetItem ( 142 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 69 ) ( SetItem ( 16 ) ( SetItem ( 350 ) ( SetItem ( 318 ) ( SetItem ( 311 ) ( SetItem ( 296 ) ( SetItem ( 214 ) ( SetItem ( 224 ) ( SetItem ( 222 ) ( SetItem ( 118 ) ( SetItem ( 132 ) ( SetItem ( 123 ) ( SetItem ( 190 ) ( SetItem ( 151 ) SetItem ( 142 ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
@@ -471,7 +471,7 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC
                  <jumpDests>
                    ( SetItem ( 102 ) ( SetItem ( 1075 ) ( SetItem ( 1095 ) ( SetItem ( 1101 ) ( SetItem ( 1137 ) ( SetItem ( 1245 ) ( SetItem ( 1307 ) ( SetItem ( 1331 ) ( SetItem ( 1340 ) ( SetItem ( 140 ) ( SetItem ( 1415 ) ( SetItem ( 1451 ) ( SetItem ( 1458 ) ( SetItem ( 1538 ) ( SetItem ( 1558 ) ( SetItem ( 16 ) ( SetItem ( 1648 ) ( SetItem ( 1684 ) ( SetItem ( 1691 ) ( SetItem ( 1693 ) ( SetItem ( 1729 ) ( SetItem ( 1760 ) ( SetItem ( 1804 ) ( SetItem ( 1838 ) ( SetItem ( 1852 ) ( SetItem ( 1881 ) ( SetItem ( 1901 ) ( SetItem ( 1937 ) ( SetItem ( 200 ) ( SetItem ( 2045 ) ( SetItem ( 2107 ) ( SetItem ( 2131 ) ( SetItem ( 2167 ) ( SetItem ( 2198 ) ( SetItem ( 2242 ) ( SetItem ( 2276 ) ( SetItem ( 2290 ) ( SetItem ( 2319 ) ( SetItem ( 2339 ) ( SetItem ( 234 ) ( SetItem ( 2373 ) ( SetItem ( 239 ) ( SetItem ( 247 ) ( SetItem ( 249 ) ( SetItem ( 2515 ) ( SetItem ( 2541 ) ( SetItem ( 257 ) ( SetItem ( 2602 ) ( SetItem ( 2607 ) ( SetItem ( 2631 ) ( SetItem ( 2635 ) ( SetItem ( 2640 ) ( SetItem ( 270 ) ( SetItem ( 2736 ) ( SetItem ( 279 ) ( SetItem ( 2792 ) ( SetItem ( 287 ) ( SetItem ( 2905 ) ( SetItem ( 295 ) ( SetItem ( 303 ) ( SetItem ( 3087 ) ( SetItem ( 3091 ) ( SetItem ( 311 ) ( SetItem ( 324 ) ( SetItem ( 3245 ) ( SetItem ( 3271 ) ( SetItem ( 332 ) ( SetItem ( 3332 ) ( SetItem ( 3337 ) ( SetItem ( 3342 ) ( SetItem ( 3359 ) ( SetItem ( 3372 ) ( SetItem ( 340 ) ( SetItem ( 3400 ) ( SetItem ( 3437 ) ( SetItem ( 3449 ) ( SetItem ( 3489 ) ( SetItem ( 353 ) ( SetItem ( 3550 ) ( SetItem ( 3592 ) ( SetItem ( 361 ) ( SetItem ( 3613 ) ( SetItem ( 3628 ) ( SetItem ( 3631 ) ( SetItem ( 3655 ) ( SetItem ( 3672 ) ( SetItem ( 369 ) ( SetItem ( 3711 ) ( SetItem ( 3750 ) ( SetItem ( 377 ) ( SetItem ( 3781 ) ( SetItem ( 3794 ) ( SetItem ( 3812 ) ( SetItem ( 3819 ) ( SetItem ( 3839 ) ( SetItem ( 3871 ) ( SetItem ( 3877 ) ( SetItem ( 3912 ) ( SetItem ( 3926 ) ( SetItem ( 393 ) ( SetItem ( 3944 ) ( SetItem ( 3954 ) ( SetItem ( 3972 ) ( SetItem ( 3988 ) ( SetItem ( 401 ) ( SetItem ( 4012 ) ( SetItem ( 4065 ) ( SetItem ( 4114 ) ( SetItem ( 4119 ) ( SetItem ( 4128 ) ( SetItem ( 4138 ) ( SetItem ( 414 ) ( SetItem ( 4147 ) ( SetItem ( 4186 ) ( SetItem ( 4210 ) ( SetItem ( 4218 ) ( SetItem ( 422 ) ( SetItem ( 4220 ) ( SetItem ( 4292 ) ( SetItem ( 4307 ) ( SetItem ( 4314 ) ( SetItem ( 434 ) ( SetItem ( 4346 ) ( SetItem ( 462 ) ( SetItem ( 497 ) ( SetItem ( 555 ) ( SetItem ( 585 ) ( SetItem ( 595 ) ( SetItem ( 691 ) ( SetItem ( 787 ) ( SetItem ( 869 ) ( SetItem ( 889 ) ( SetItem ( 945 ) ( SetItem ( 971 ) SetItem ( 991 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 258 ) ( SetItem ( 98 ) ( SetItem ( 65 ) ( SetItem ( 161 ) ( SetItem ( 70 ) ( SetItem ( 197 ) ( SetItem ( 171 ) ( SetItem ( 297 ) ( SetItem ( 265 ) ( SetItem ( 169 ) ( SetItem ( 137 ) ( SetItem ( 79 ) ( SetItem ( 243 ) ( SetItem ( 48 ) ( SetItem ( 16 ) ( SetItem ( 118 ) SetItem ( 89 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 79 ) ( SetItem ( 70 ) ( SetItem ( 65 ) ( SetItem ( 16 ) ( SetItem ( 89 ) ( SetItem ( 98 ) ( SetItem ( 297 ) ( SetItem ( 265 ) ( SetItem ( 243 ) ( SetItem ( 258 ) ( SetItem ( 171 ) ( SetItem ( 169 ) ( SetItem ( 161 ) SetItem ( 137 ) ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
diff --git a/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k b/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k
index 07b305f36d..3f9f590e36 100644
--- a/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k
+++ b/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k
@@ -143,7 +143,7 @@ module TEST-SAFETEST-TESTWITHDRAWFUZZ-UINT96-0-SPEC
                  <jumpDests>
                    ( SetItem ( 1074 ) ( SetItem ( 1136 ) ( SetItem ( 1160 ) ( SetItem ( 1169 ) ( SetItem ( 1205 ) ( SetItem ( 1236 ) ( SetItem ( maxSInt8 ) ( SetItem ( 1280 ) ( SetItem ( 1314 ) ( SetItem ( 1328 ) ( SetItem ( 1357 ) ( SetItem ( 1377 ) ( SetItem ( 1413 ) ( SetItem ( 1521 ) ( SetItem ( 1583 ) ( SetItem ( 1607 ) ( SetItem ( 1643 ) ( SetItem ( 1674 ) ( SetItem ( 1718 ) ( SetItem ( 1752 ) ( SetItem ( 1766 ) ( SetItem ( 1795 ) ( SetItem ( 1815 ) ( SetItem ( 1849 ) ( SetItem ( 198 ) ( SetItem ( 1991 ) ( SetItem ( 2017 ) ( SetItem ( 205 ) ( SetItem ( 2078 ) ( SetItem ( 2083 ) ( SetItem ( 210 ) ( SetItem ( 2107 ) ( SetItem ( 2111 ) ( SetItem ( 2116 ) ( SetItem ( 2209 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2300 ) ( SetItem ( 231 ) ( SetItem ( 233 ) ( SetItem ( 2370 ) ( SetItem ( 2390 ) ( SetItem ( 2420 ) ( SetItem ( 2426 ) ( SetItem ( 2431 ) ( SetItem ( 245 ) ( SetItem ( 2492 ) ( SetItem ( 254 ) ( SetItem ( 2562 ) ( SetItem ( 2582 ) ( SetItem ( 2611 ) ( SetItem ( 2615 ) ( SetItem ( 267 ) ( SetItem ( 2711 ) ( SetItem ( 276 ) ( SetItem ( 2824 ) ( SetItem ( 288 ) ( SetItem ( 297 ) ( SetItem ( 309 ) ( SetItem ( 3155 ) ( SetItem ( 318 ) ( SetItem ( 3181 ) ( SetItem ( 3242 ) ( SetItem ( 3247 ) ( SetItem ( 3252 ) ( SetItem ( 3269 ) ( SetItem ( 3281 ) ( SetItem ( 330 ) ( SetItem ( 3309 ) ( SetItem ( 3346 ) ( SetItem ( 3358 ) ( SetItem ( 339 ) ( SetItem ( 3398 ) ( SetItem ( 3459 ) ( SetItem ( 3501 ) ( SetItem ( 352 ) ( SetItem ( 3522 ) ( SetItem ( 3537 ) ( SetItem ( 3540 ) ( SetItem ( 3564 ) ( SetItem ( 3579 ) ( SetItem ( 3585 ) ( SetItem ( 3624 ) ( SetItem ( 364 ) ( SetItem ( 3663 ) ( SetItem ( 3694 ) ( SetItem ( 3707 ) ( SetItem ( 3725 ) ( SetItem ( 373 ) ( SetItem ( 3748 ) ( SetItem ( 3755 ) ( SetItem ( 3775 ) ( SetItem ( 3807 ) ( SetItem ( 3813 ) ( SetItem ( 3848 ) ( SetItem ( 386 ) ( SetItem ( 3862 ) ( SetItem ( 3880 ) ( SetItem ( 3890 ) ( SetItem ( 3908 ) ( SetItem ( 3924 ) ( SetItem ( 3957 ) ( SetItem ( 3978 ) ( SetItem ( 398 ) ( SetItem ( 4025 ) ( SetItem ( 4031 ) ( SetItem ( 4036 ) ( SetItem ( 4047 ) ( SetItem ( 4054 ) ( SetItem ( 4056 ) ( SetItem ( 407 ) ( SetItem ( 4099 ) ( SetItem ( 419 ) ( SetItem ( 428 ) ( SetItem ( 440 ) ( SetItem ( 449 ) ( SetItem ( 465 ) ( SetItem ( 477 ) ( SetItem ( 492 ) ( SetItem ( 497 ) ( SetItem ( 509 ) ( SetItem ( 518 ) ( SetItem ( 530 ) ( SetItem ( 539 ) ( SetItem ( 551 ) ( SetItem ( 565 ) ( SetItem ( 577 ) ( SetItem ( 605 ) ( SetItem ( 640 ) ( SetItem ( 698 ) ( SetItem ( 728 ) ( SetItem ( 738 ) ( SetItem ( 834 ) ( SetItem ( 89 ) ( SetItem ( 930 ) SetItem ( 966 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 73 ) ( SetItem ( 68 ) ( SetItem ( 62 ) ( SetItem ( 15 ) ( SetItem ( 84 ) ( SetItem ( 93 ) ( SetItem ( 91 ) ( SetItem ( 136 ) SetItem ( 155 ) ) ) ) ) ) ) ) )
+                    ( SetItem ( 73 ) ( SetItem ( 68 ) ( SetItem ( 62 ) ( SetItem ( 15 ) ( SetItem ( 84 ) ( SetItem ( 93 ) ( SetItem ( 91 ) SetItem ( 136 ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )