diff --git a/package/version b/package/version
index 50340d8c4..0321d8e76 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.209
+0.1.210
diff --git a/pyproject.toml b/pyproject.toml
index aee310b9a..88d7b56ea 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.209"
+version = "0.1.210"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index 07f5fb2bd..1cb35e4a4 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.209'
+VERSION: Final = '0.1.210'
diff --git a/src/tests/integration/conftest.py b/src/tests/integration/conftest.py
index 251625091..56f28d70e 100644
--- a/src/tests/integration/conftest.py
+++ b/src/tests/integration/conftest.py
@@ -70,8 +70,17 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo
             foundry_kompile(
                 foundry=Foundry(foundry_root),
                 includes=(),
-                requires=[str(TEST_DATA_DIR / 'lemmas.k'), str(TEST_DATA_DIR / 'cse-lemmas.k')],
-                imports=['LoopsTest:SUM-TO-N-INVARIANT', 'ArithmeticCallTest:CSE-LEMMAS', 'CSETest:CSE-LEMMAS'],
+                requires=[
+                    str(TEST_DATA_DIR / 'lemmas.k'),
+                    str(TEST_DATA_DIR / 'cse-lemmas.k'),
+                    str(TEST_DATA_DIR / 'pausability-lemmas.k'),
+                ],
+                imports=[
+                    'LoopsTest:SUM-TO-N-INVARIANT',
+                    'ArithmeticCallTest:CSE-LEMMAS',
+                    'CSETest:CSE-LEMMAS',
+                    'PortalTest:PAUSABILITY-LEMMAS',
+                ],
             )
 
     session_foundry_root = tmp_path_factory.mktemp('foundry')
diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all
index 7e9ea68b3..3c7ff6f55 100644
--- a/src/tests/integration/test-data/foundry-prove-all
+++ b/src/tests/integration/test-data/foundry-prove-all
@@ -185,6 +185,7 @@ PlainPrankTest.test_startPrankWithOrigin_true()
 PlainPrankTest.test_startPrank_zeroAddress_true()
 PlainPrankTest.test_stopPrank_notExistent()
 PlainPrankTest.test_prank_expectRevert()
+PortalTest.test_withdrawal_paused((uint256,address,address,uint256,uint256,bytes),uint256,(bytes32,bytes32,bytes32,bytes32),bytes[])
 PrankTest.testAddAsOwner(uint256)
 PrankTest.testAddStartPrank(uint256)
 PrankTest.testFailAddPrank(uint256)
diff --git a/src/tests/integration/test-data/foundry-prove-skip-legacy b/src/tests/integration/test-data/foundry-prove-skip-legacy
index e9b2018e0..deef1d9aa 100644
--- a/src/tests/integration/test-data/foundry-prove-skip-legacy
+++ b/src/tests/integration/test-data/foundry-prove-skip-legacy
@@ -182,6 +182,7 @@ PlainPrankTest.test_prank_zeroAddress_true()
 PlainPrankTest.test_startPrank_true()
 PlainPrankTest.test_startPrankWithOrigin_true()
 PlainPrankTest.test_startPrank_zeroAddress_true()
+PortalTest.test_withdrawal_paused((uint256,address,address,uint256,uint256,bytes),uint256,(bytes32,bytes32,bytes32,bytes32),bytes[])
 PrankTestMsgSender.test_msgsender_setup()
 PrankTestOrigin.test_origin_setup()
 PrankTest.testAddAsOwner(uint256)
diff --git a/src/tests/integration/test-data/foundry/src/Portal.sol b/src/tests/integration/test-data/foundry/src/Portal.sol
new file mode 100644
index 000000000..02b546b5e
--- /dev/null
+++ b/src/tests/integration/test-data/foundry/src/Portal.sol
@@ -0,0 +1,50 @@
+pragma solidity =0.8.13;
+
+library Types {
+    struct OutputRootProof {
+        bytes32 version;
+        bytes32 stateRoot;
+        bytes32 messagePasserStorageRoot;
+        bytes32 latestBlockhash;
+    }
+
+    struct WithdrawalTransaction {
+        uint256 nonce;
+        address sender;
+        address target;
+        uint256 value;
+        uint256 gasLimit;
+        bytes data;
+    }
+}
+
+contract Portal  {
+    bool paused;
+
+    /// @notice Emitted when a withdrawal transaction is proven.
+    event WithdrawalProven(address indexed from, address indexed to);
+
+    /// @notice Reverts when paused.
+    modifier whenNotPaused() {
+        require(paused == false, "Portal: paused");
+        _;
+    }
+
+    constructor() {
+        paused = true;
+    }
+
+    /// @notice Proves a withdrawal transaction.
+    function proveWithdrawalTransaction(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+        whenNotPaused
+    {
+        // Emit a `WithdrawalProven` event.
+        emit WithdrawalProven(_tx.sender, _tx.target);
+    }
+}
diff --git a/src/tests/integration/test-data/foundry/test/PortalTest.sol b/src/tests/integration/test-data/foundry/test/PortalTest.sol
new file mode 100644
index 000000000..6cd6a9a8f
--- /dev/null
+++ b/src/tests/integration/test-data/foundry/test/PortalTest.sol
@@ -0,0 +1,27 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+import "forge-std/Test.sol";
+import "../src/Portal.sol";
+
+contract PortalTest is Test {
+    Portal portalContract;
+
+    function setUp() public {
+        portalContract = new Portal();
+    }
+
+    /// @custom:kontrol-array-length-equals _withdrawalProof: 1,
+    /// @custom:kontrol-bytes-length-equals _withdrawalProof: 32,
+    function test_withdrawal_paused(
+        Types.WithdrawalTransaction memory _tx,
+        uint256 _l2OutputIndex,
+        Types.OutputRootProof calldata _outputRootProof,
+        bytes[] calldata _withdrawalProof
+    )
+        external
+    {
+        vm.expectRevert();
+        portalContract.proveWithdrawalTransaction(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
+    }
+}
\ No newline at end of file
diff --git a/src/tests/integration/test-data/pausability-lemmas.k b/src/tests/integration/test-data/pausability-lemmas.k
new file mode 100644
index 000000000..d3112597c
--- /dev/null
+++ b/src/tests/integration/test-data/pausability-lemmas.k
@@ -0,0 +1,182 @@
+requires "evm.md"
+requires "foundry.md"
+
+module PAUSABILITY-LEMMAS [symbolic]
+    imports BOOL
+    imports FOUNDRY
+    imports INT-SYMBOLIC
+
+    syntax StepSort ::= Int
+                      | Bool
+                      | Bytes
+                      | Set
+ // ------------------------
+
+    syntax KItem ::= runLemma ( StepSort )
+                   | doneLemma( StepSort )
+ // --------------------------------------
+    rule <k> runLemma(T) => doneLemma(T) ... </k>
+
+    // We need to enforce some limit on the length of bytearrays
+    // and indices into bytearrays in order to avoid chop-reasoning
+    syntax Int ::= "maxBytesLength" [alias]
+    rule maxBytesLength => 9223372036854775808
+
+
+    // Deconstruction of <<Int into #buf
+    rule X <<Int Y => #asWord ( #buf ( 32 -Int (Y /Int 8) , X ) +Bytes #buf ( Y /Int 8 , 0 ) )
+      requires 0 <=Int X andBool X <Int 2 ^Int (256 -Int Y)
+       andBool 0 <=Int Y andBool Y <=Int 256 andBool Y modInt 8 ==Int 0
+      [simplification, concrete(Y)]
+
+    //
+    // Arithmetic
+    //
+
+    // Cancellativity #1
+    rule A +Int B -Int B +Int C => A +Int C [simplification]
+
+    // Cancellativity #2
+    rule A -Int B +Int C -Int D +Int B +Int E => A -Int D +Int C +Int E [simplification]
+
+    // Cancellativity #3
+    rule ( A +Int B ) +Int C <=Int ( D +Int B ) +Int E => A +Int C <=Int D +Int E [simplification]
+
+    // Cancellativity #4
+    rule A +Int B <=Int ( A +Int C ) +Int D => B <=Int C +Int D [simplification]
+
+    // Cancellativity #5
+    rule A +Int ( (B -Int A) +Int C ) => B +Int C [simplification]
+
+    // Cancellativity #6
+    rule (A -Int B) -Int (C -Int B) => A -Int C [simplification]
+  
+    // Upper bound on (pow256 - 32) &Int lengthBytes(X)
+    rule notMaxUInt5 &Int Y <=Int Y => true
+      requires 0 <=Int Y
+      [simplification]
+
+    // Bounds on notMaxUInt5 &Int ( X +Int 31 )
+    // Note: upstream in the next round
+    rule X <=Int   notMaxUInt5 &Int ( X +Int 31 )          => true requires 0 <=Int X                   [simplification]
+    rule X <=Int   notMaxUInt5 &Int ( Y +Int 31 )          => true requires X <=Int 0 andBool 0 <=Int Y [simplification, concrete(X)]
+    rule X <=Int ( notMaxUInt5 &Int ( X +Int 31 ) ) +Int Y => true requires 0 <=Int X andBool 0 <=Int Y [simplification, concrete(Y)]
+
+    rule notMaxUInt5 &Int X +Int 31 <Int Y => true requires 0 <=Int X andBool X +Int 32 <=Int Y [simplification, concrete(Y)]
+
+    rule notMaxUInt5 &Int X +Int 31 <Int X +Int 32 => true requires 0 <=Int X [simplification]
+
+    //
+    // #asWord
+    //
+
+    // Move to function parameters
+    rule { #asWord ( X ) #Equals #asWord ( Y ) } => #Top
+      requires X ==K Y
+      [simplification]
+
+    // #asWord ignores leading zeros
+    rule #asWord ( BA1 +Bytes BA2 ) => #asWord ( BA2 )
+      requires #asInteger(BA1) ==Int 0
+      [simplification, concrete(BA1)]
+
+
+    // Equality and #range
+    rule #asWord ( #range ( #buf ( 32 , _X:Int ) , S:Int , W:Int ) ) ==Int Y:Int => false
+        requires S +Int W <=Int 32
+         andBool (2 ^Int (8 *Int W)) <=Int Y
+        [concrete(S, W, Y), simplification]
+
+    // Conversion from bytes always yields a non-negative integer
+    rule 0 <=Int #asInteger ( _ ) => true [simplification]
+
+    //
+    // #padRightToWidth
+    //
+
+    rule #padRightToWidth (W, X) => X +Bytes #buf(W -Int lengthBytes(X), 0)
+      [concrete(W), simplification]
+
+    //
+    // #range(M, START, WIDTH)
+    //
+
+    // Parameter equality
+    rule { #range (A, B, C) #Equals #range (A, B, D) } => #Top
+      requires C ==Int D
+      [simplification]
+
+    //
+    // Bytes indexing and update
+    //
+
+    rule B:Bytes [ X:Int ] => #asWord ( #range (B, X, 1) )
+      requires X <=Int lengthBytes(B)
+      [simplification(40)]
+
+    // Empty update has no effect
+    rule B:Bytes [ START:Int := b"" ] => B
+      requires 0 <=Int START andBool START <=Int lengthBytes(B)
+      [simplification]
+
+    // Consecutive quasi-contiguous byte-array update
+    rule B [ S1 := B1 ] [ S2 := B2 ] => B [ S1 := #range(B1, 0, S2 -Int S1) +Bytes B2 ]
+      requires 0 <=Int S1 andBool S1 <=Int S2 andBool S2 <=Int S1 +Int lengthBytes(B1)
+      [simplification]
+
+    // Parameter equality: byte-array update
+    rule { B1:Bytes [ S1:Int := B2:Bytes ] #Equals B3:Bytes [ S2:Int := B4:Bytes ] } => #Top
+      requires B1 ==K B3 andBool S1 ==Int S2 andBool B2 ==K B4
+      [simplification]
+
+    //
+    // SUMMARIES
+    //
+
+    // This rule cannot be used without the [symbolic] tag because it uses
+    // "existentials", which is not correct, it uses variables that are learnt
+    // from the requires and not from the structure
+
+    // copy-memory-to-memory
+    rule [test-copy-memory-to-memory-summary]:
+      <k> #execute ... </k>
+      <useGas> false </useGas>
+      <schedule> SHANGHAI </schedule>
+      <jumpDests> JUMPDESTS </jumpDests>
+      // The program and program counter are symbolic, focusing on the part we will be executing (CP)
+      <program> PROGRAM </program>
+      <pc> PCOUNT => PCOUNT +Int 44 </pc>
+      // The word stack has the appropriate form, as per the compiled code
+      <wordStack> SRC : DEST : LENGTH : WS </wordStack>
+      // The program copies LENGTH bytes of memory from SRC +Int 32 to DEST +Int OFFSET,
+      // padded with 32 zeros in case LENGTH is not divisible by 32
+      <localMem>
+        LM => LM [ DEST := #range ( LM, SRC, LENGTH ) +Bytes
+                                   #buf ( ( ( notMaxUInt5 &Int ( LENGTH +Int maxUInt5 ) ) -Int LENGTH ) , 0 ) +Bytes
+                                   #buf ( ( ( ( 32 -Int ( ( notMaxUInt5 &Int ( LENGTH +Int maxUInt5 ) ) -Int LENGTH ) ) ) modInt 32 ), 0 ) ]
+      </localMem>
+      requires
+       // The current program we are executing differs from the original one only in the hardcoded jump addresses,
+       // which are now relative to PCOUNT, and the hardcoded offset, which is now symbolic.
+               #range(PROGRAM, PCOUNT, 44) ==K b"[`\x00[\x83\x81\x10\x15a\n\x9fW\x81\x81\x01Q\x83\x82\x01R` \x01a\n\x87V[\x83\x81\x11\x15a\n\xaeW`\x00\x84\x84\x01R[P"
+                                               [ 09 := #buf(2, PCOUNT +Int 27) ]
+                                               [ 24 := #buf(2, PCOUNT +Int  3) ]
+                                               [ 33 := #buf(2, PCOUNT +Int 42) ]
+
+       // Various well-formedness constraints. In particular, the maxBytesLength-related ones are present to
+       // remove various chops that would otherwise creep into the execution, and are reasonable since byte
+       // arrays in actual programs would never reach that size.
+       andBool 0 <=Int PCOUNT
+       andBool 0 <=Int LENGTH andBool LENGTH <Int maxBytesLength
+       andBool 0 <=Int SRC    andBool SRC    <Int maxBytesLength
+       andBool 0 <=Int DEST   andBool DEST   <Int maxBytesLength
+       andBool #sizeWordStack(WS) <=Int 1015
+
+       andBool SRC +Int LENGTH <=Int DEST // No overlap between source and destination
+       andBool DEST <=Int lengthBytes(LM) // Destination starts within current memory
+       // All JUMPDESTs in the program are valid
+       andBool (PCOUNT +Int 3) in JUMPDESTS andBool (PCOUNT +Int 27) in JUMPDESTS andBool (PCOUNT +Int 42) in JUMPDESTS
+       andBool PCOUNT +Int 42 <Int 2 ^Int 16  // and fit into two bytes
+      [priority(30), concrete(JUMPDESTS, PROGRAM, PCOUNT), preserves-definedness]
+
+endmodule
\ No newline at end of file
diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected
index d69c18694..a681cd0b0 100644
--- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected
@@ -21,12 +21,12 @@
 │
 │  (1000 steps)
 ├─ 5
-│   k: #addr [ ISZERO ] ~> #exec [ ISZERO ] ~> #pc [ ISZERO ] ~> #execute ~> CONTINUATI ...
-│   pc: 4206
+│   k: #execute ~> CONTINUATION:K
+│   pc: 4447
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (827 steps)
+│  (145 steps)
 ├─ 6
 │   k: CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0 ~> #pc [ ...
 │   pc: 3785
@@ -505,9 +505,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0
                ~> #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) true
                ~> #return 128 0
-               ~> #pc [ STATICCALL ] => #addr [ ISZERO ]
-               ~> #exec [ ISZERO ]
-               ~> #pc [ ISZERO ] )
+               ~> #pc [ STATICCALL ] => .K )
                ~> #execute
                ~> _CONTINUATION
              </k>
@@ -548,10 +546,10 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( ( 164 => 1 ) : ( ( selector ( "assume(bool)" ) => 64 ) : ( ( 645326474426547203313410069153905908525362434349 => 160 ) : ( ( VV1_b_114b9705:Int => 292 ) : ( ( VV0_a_114b9705:Int => 96 ) : ( ( 280 => 4586 ) : ( ( selector ( "testFail_assume_true(uint256,uint256)" ) => 96 ) : ( .WordStack => ( 0 : ( 288 : ( 128 : ( 51016057639858100040180367130768047423658391221723556551037572491782395555780 : ( 3745 : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "testFail_assume_true(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                     ( ( 164 => 256 ) : ( ( selector ( "assume(bool)" ) => 0 ) : ( ( 645326474426547203313410069153905908525362434349 => 388 ) : ( ( VV1_b_114b9705:Int => 256 ) : ( ( VV0_a_114b9705:Int => 3771 ) : ( ( 280 => 645326474426547203313410069153905908525362434349 ) : ( ( selector ( "testFail_assume_true(uint256,uint256)" ) => 0 ) : ( .WordStack => ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "testFail_assume_true(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
-                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
+                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" )
                    </localMem>
                    <memoryUsed>
                      0
@@ -714,9 +712,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0
     rule [BASIC-BLOCK-5-TO-6]: <foundry>
            <kevm>
              <k>
-               ( #addr [ ISZERO ]
-               ~> #exec [ ISZERO ]
-               ~> #pc [ ISZERO ] => CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0
+               ( .K => CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0
                ~> #pc [ CALL ] )
                ~> #execute
                ~> _CONTINUATION
@@ -758,10 +754,10 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( ( 1 => 488 ) : ( ( 64 => 645326474426547203313410069153905908525362434349 ) : ( ( 160 => 0 ) : ( ( 292 => 594 ) : ( ( 96 => VV1_b_114b9705:Int ) : ( ( 4586 => VV0_a_114b9705:Int ) : ( ( 96 => 594 ) : ( ( 0 => VV1_b_114b9705:Int ) : ( ( 288 => VV0_a_114b9705:Int ) : ( ( 128 => 280 ) : ( ( 51016057639858100040180367130768047423658391221723556551037572491782395555780 => selector ( "testFail_assume_true(uint256,uint256)" ) ) : ( ( 3745 : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "testFail_assume_true(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) => .WordStack ) ) ) ) ) ) ) ) ) ) ) )
+                     ( ( 256 => 488 ) : ( ( 0 => 645326474426547203313410069153905908525362434349 ) : ( ( 388 => 0 ) : ( ( 256 => 594 ) : ( ( 3771 => VV1_b_114b9705:Int ) : ( ( 645326474426547203313410069153905908525362434349 => VV0_a_114b9705:Int ) : ( ( 0 => 594 ) : ( ( 594 => VV1_b_114b9705:Int ) : ( ( VV1_b_114b9705:Int => VV0_a_114b9705:Int ) : ( ( VV0_a_114b9705:Int => 280 ) : ( ( 594 => selector ( "testFail_assume_true(uint256,uint256)" ) ) : ( ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "testFail_assume_true(uint256,uint256)" ) : .WordStack ) ) ) ) => .WordStack ) ) ) ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
-                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
+                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
                    </localMem>
                    <memoryUsed>
                      0
diff --git a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
index 935342af1..6135b770d 100644
--- a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
@@ -21,12 +21,12 @@
 │
 │  (1000 steps)
 ├─ 5
-│   k: #addr [ ISZERO ] ~> #exec [ ISZERO ] ~> #pc [ ISZERO ] ~> #execute ~> CONTINUATI ...
-│   pc: 4206
+│   k: #execute ~> CONTINUATION:K
+│   pc: 4447
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (827 steps)
+│  (145 steps)
 ├─ 6
 │   k: CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0 ~> #pc [ ...
 │   pc: 3785
@@ -716,9 +716,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0
                ~> #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) true
                ~> #return 128 0
-               ~> #pc [ STATICCALL ] => #addr [ ISZERO ]
-               ~> #exec [ ISZERO ]
-               ~> #pc [ ISZERO ] )
+               ~> #pc [ STATICCALL ] => .K )
                ~> #execute
                ~> _CONTINUATION
              </k>
@@ -759,10 +757,10 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( ( 164 => 1 ) : ( ( selector ( "assume(bool)" ) => 64 ) : ( ( 645326474426547203313410069153905908525362434349 => 160 ) : ( ( VV1_b_114b9705:Int => 292 ) : ( ( VV0_a_114b9705:Int => 96 ) : ( ( 280 => 4586 ) : ( ( selector ( "test_assume_false(uint256,uint256)" ) => 96 ) : ( .WordStack => ( 0 : ( 288 : ( 128 : ( 51016057639858100040180367130768047423658391221723556551037572491782395555780 : ( 3745 : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                     ( ( 164 => 256 ) : ( ( selector ( "assume(bool)" ) => 0 ) : ( ( 645326474426547203313410069153905908525362434349 => 388 ) : ( ( VV1_b_114b9705:Int => 256 ) : ( ( VV0_a_114b9705:Int => 3771 ) : ( ( 280 => 645326474426547203313410069153905908525362434349 ) : ( ( selector ( "test_assume_false(uint256,uint256)" ) => 0 ) : ( .WordStack => ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
-                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
+                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" )
                    </localMem>
                    <memoryUsed>
                      0
@@ -925,9 +923,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0
     rule [BASIC-BLOCK-5-TO-6]: <foundry>
            <kevm>
              <k>
-               ( #addr [ ISZERO ]
-               ~> #exec [ ISZERO ]
-               ~> #pc [ ISZERO ] => CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0
+               ( .K => CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0
                ~> #pc [ CALL ] )
                ~> #execute
                ~> _CONTINUATION
@@ -969,10 +965,10 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0
                      0
                    </callValue>
                    <wordStack>
-                     ( ( 1 => 488 ) : ( ( 64 => 645326474426547203313410069153905908525362434349 ) : ( ( 160 => 0 ) : ( ( 292 => 594 ) : ( ( 96 => VV1_b_114b9705:Int ) : ( ( 4586 => VV0_a_114b9705:Int ) : ( ( 96 => 594 ) : ( ( 0 => VV1_b_114b9705:Int ) : ( ( 288 => VV0_a_114b9705:Int ) : ( ( 128 => 280 ) : ( ( 51016057639858100040180367130768047423658391221723556551037572491782395555780 => selector ( "test_assume_false(uint256,uint256)" ) ) : ( ( 3745 : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) => .WordStack ) ) ) ) ) ) ) ) ) ) ) )
+                     ( ( 256 => 488 ) : ( ( 0 => 645326474426547203313410069153905908525362434349 ) : ( ( 388 => 0 ) : ( ( 256 => 594 ) : ( ( 3771 => VV1_b_114b9705:Int ) : ( ( 645326474426547203313410069153905908525362434349 => VV0_a_114b9705:Int ) : ( ( 0 => 594 ) : ( ( 594 => VV1_b_114b9705:Int ) : ( ( VV1_b_114b9705:Int => VV0_a_114b9705:Int ) : ( ( VV0_a_114b9705:Int => 280 ) : ( ( 594 => selector ( "test_assume_false(uint256,uint256)" ) ) : ( ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(uint256,uint256)" ) : .WordStack ) ) ) ) => .WordStack ) ) ) ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
-                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
+                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
                    </localMem>
                    <memoryUsed>
                      0
diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected
index 3bddafd0f..93a9bee3c 100644
--- a/src/tests/integration/test-data/show/contracts.k.expected
+++ b/src/tests/integration/test-data/show/contracts.k.expected
@@ -11637,6 +11637,282 @@ module S2KtestZModPlainPrankTest-CONTRACT
     rule  ( selector ( "test_stopPrank_notExistent()" ) => 279002555 )
       
 
+endmodule
+
+module S2KsrcZModPortal-CONTRACT
+    imports public FOUNDRY
+    
+    syntax Contract ::= S2KsrcZModPortalContract
+    
+    syntax S2KsrcZModPortalContract ::= "S2KsrcZModPortal" [symbol(""), klabel(contract_src%Portal)]
+    
+      
+    
+    rule  ( #initBytecode ( S2KsrcZModPortal ) => #parseByteStack ( "0x608060405234801561001057600080fd5b506000805460ff191660011790556103488061002d6000396000f3fe608060405234801561001057600080fd5b506004361061002b5760003560e01c80634870496f14610030575b600080fd5b61004361003e3660046101cc565b610045565b005b60005460ff161561008d5760405162461bcd60e51b815260206004820152600e60248201526d141bdc9d185b0e881c185d5cd95960921b604482015260640160405180910390fd5b84604001516001600160a01b031685602001516001600160a01b03167fa998e9f42be9c7bd87798d599093d87d0393e08ff742a512c623afe9c6a9c61f60405160405180910390a35050505050565b634e487b7160e01b600052604160045260246000fd5b60405160c0810167ffffffffffffffff81118282101715610115576101156100dc565b60405290565b604051601f8201601f1916810167ffffffffffffffff81118282101715610144576101446100dc565b604052919050565b80356001600160a01b038116811461016357600080fd5b919050565b60006080828403121561017a57600080fd5b50919050565b60008083601f84011261019257600080fd5b50813567ffffffffffffffff8111156101aa57600080fd5b6020830191508360208260051b85010111156101c557600080fd5b9250929050565b600080600080600060e086880312156101e457600080fd5b853567ffffffffffffffff808211156101fc57600080fd5b9087019060c0828a03121561021057600080fd5b6102186100f2565b82358152602061022981850161014c565b818301526102396040850161014c565b6040830152606084013560608301526080840135608083015260a08401358381111561026457600080fd5b8085019450508a601f85011261027957600080fd5b83358381111561028b5761028b6100dc565b61029d601f8201601f1916830161011b565b8181528c838388010111156102b157600080fd5b8183870184830137600091810183019190915260a083015290975088013595506102de8960408a01610168565b945060c08801359150808211156102f457600080fd5b5061030188828901610180565b96999598509396509294939250505056fea2646970667358221220c6780a421240a4f971c9fd2210c1d2dff868ab9d69234d7dd7e6b3879edc63b264736f6c634300080d0033" ) )
+      
+    
+    syntax Field ::= S2KsrcZModPortalField
+    
+    syntax S2KsrcZModPortalField ::= "paused" [symbol(""), klabel(field_src%Portal_paused)]
+    
+    rule  ( #loc ( S2KsrcZModPortal . paused ) => 0 )
+      
+    
+    syntax Bytes ::= S2KsrcZModPortalContract "." S2KsrcZModPortalMethod [function, symbol(""), klabel(method_src%Portal)]
+    
+    syntax S2KsrcZModPortalMethod ::= "S2KproveWithdrawalTransaction" "(" Int ":" "uint256" "," Int ":" "address" "," Int ":" "address" "," Int ":" "uint256" "," Int ":" "uint256" "," Bytes ":" "bytes" "," Int ":" "uint256" "," Int ":" "bytes32" "," Int ":" "bytes32" "," Int ":" "bytes32" "," Int ":" "bytes32" "," Bytes ":" "bytes" "," Bytes ":" "bytes" ")" [symbol(""), klabel(method_src%Portal_S2KproveWithdrawalTransaction_uint256_address_address_uint256_uint256_bytes_uint256_bytes32_bytes32_bytes32_bytes32_bytes_bytes)]
+    
+    rule  ( S2KsrcZModPortal . S2KproveWithdrawalTransaction ( V0_nonce : uint256 , V1_sender : address , V2_target : address , V3_value : uint256 , V4_gasLimit : uint256 , V5_data : bytes , V6__l2OutputIndex : uint256 , V7_version : bytes32 , V8_stateRoot : bytes32 , V9_messagePasserStorageRoot : bytes32 , V10_latestBlockhash : bytes32 , V11__withdrawalProof_0 : bytes , V11__withdrawalProof_1 : bytes ) => #abiCallData ( "proveWithdrawalTransaction" , ( #tuple ( ( #uint256 ( V0_nonce ) , ( #address ( V1_sender ) , ( #address ( V2_target ) , ( #uint256 ( V3_value ) , ( #uint256 ( V4_gasLimit ) , ( #bytes ( V5_data ) , .TypedArgs ) ) ) ) ) ) ) , ( #uint256 ( V6__l2OutputIndex ) , ( #tuple ( ( #bytes32 ( V7_version ) , ( #bytes32 ( V8_stateRoot ) , ( #bytes32 ( V9_messagePasserStorageRoot ) , ( #bytes32 ( V10_latestBlockhash ) , .TypedArgs ) ) ) ) ) , ( #array ( #bytes ( V11__withdrawalProof_0 ) , 2 , ( #bytes ( V11__withdrawalProof_0 ) , ( #bytes ( V11__withdrawalProof_1 ) , .TypedArgs ) ) ) , .TypedArgs ) ) ) ) ) )
+       ensures ( #rangeUInt ( 256 , V0_nonce )
+       andBool ( #rangeAddress ( V1_sender )
+       andBool ( #rangeAddress ( V2_target )
+       andBool ( #rangeUInt ( 256 , V3_value )
+       andBool ( #rangeUInt ( 256 , V4_gasLimit )
+       andBool ( #rangeUInt ( 64 , lengthBytes ( V5_data ) )
+       andBool ( #rangeUInt ( 256 , V6__l2OutputIndex )
+       andBool ( #rangeBytes ( 32 , V7_version )
+       andBool ( #rangeBytes ( 32 , V8_stateRoot )
+       andBool ( #rangeBytes ( 32 , V9_messagePasserStorageRoot )
+       andBool ( #rangeBytes ( 32 , V10_latestBlockhash )
+       andBool ( #rangeUInt ( 64 , lengthBytes ( V11__withdrawalProof_0 ) )
+       andBool ( #rangeUInt ( 64 , lengthBytes ( V11__withdrawalProof_1 ) )
+               )))))))))))))
+      
+    
+    rule  ( selector ( "proveWithdrawalTransaction((uint256,address,address,uint256,uint256,bytes),uint256,(bytes32,bytes32,bytes32,bytes32),bytes[])" ) => 1215318383 )
+      
+
+endmodule
+
+module S2KsrcZModTypes-CONTRACT
+    imports public FOUNDRY
+    
+    syntax Contract ::= S2KsrcZModTypesContract
+    
+    syntax S2KsrcZModTypesContract ::= "S2KsrcZModTypes" [symbol(""), klabel(contract_src%Types)]
+    
+      
+    
+    rule  ( #initBytecode ( S2KsrcZModTypes ) => #parseByteStack ( "0x60566037600b82828239805160001a607314602a57634e487b7160e01b600052600060045260246000fd5b30600052607381538281f3fe73000000000000000000000000000000000000000030146080604052600080fdfea2646970667358221220271b8602691459efaaa5a820086ae32c3f9ec13daa08e922232f13afd1e262b764736f6c634300080d0033" ) )
+      
+
+endmodule
+
+module S2KtestZModPortalTest-CONTRACT
+    imports public FOUNDRY
+    
+    syntax Contract ::= S2KtestZModPortalTestContract
+    
+    syntax S2KtestZModPortalTestContract ::= "S2KtestZModPortalTest" [symbol(""), klabel(contract_test%PortalTest)]
+    
+      
+    
+    rule  ( #initBytecode ( S2KtestZModPortalTest ) => #parseByteStack ( "0x608060405260078054600160ff199182168117909255600b8054909116909117905534801561002d57600080fd5b506112828061003d6000396000f3fe608060405234801561001057600080fd5b50600436106100b45760003560e01c8063916a17c611610071578063916a17c61461011b578063b5508aa914610123578063ba414fa61461012b578063c1cd1d7c14610143578063e20c9f7114610156578063fa7626d41461015e57600080fd5b80630a9254e4146100b95780631ed7831c146100c35780633e5e3c23146100e15780633f7286f4146100e957806366d9a9a0146100f157806385226c8114610106575b600080fd5b6100c161016b565b005b6100cb6101b6565b6040516100d891906108ce565b60405180910390f35b6100cb610218565b6100cb610278565b6100f96102d8565b6040516100d8919061091b565b61010e6103c7565b6040516100d89190610a2a565b6100f9610497565b61010e61057d565b61013361064d565b60405190151581526020016100d8565b6100c1610151366004610b77565b61077a565b6100cb610861565b6007546101339060ff1681565b604051610177906108c1565b604051809103906000f080158015610193573d6000803e3d6000fd5b50601b80546001600160a01b0319166001600160a01b0392909216919091179055565b6060601480548060200260200160405190810160405280929190818152602001828054801561020e57602002820191906000526020600020905b81546001600160a01b031681526001909101906020018083116101f0575b5050505050905090565b6060601680548060200260200160405190810160405280929190818152602001828054801561020e576020028201919060005260206000209081546001600160a01b031681526001909101906020018083116101f0575050505050905090565b6060601580548060200260200160405190810160405280929190818152602001828054801561020e576020028201919060005260206000209081546001600160a01b031681526001909101906020018083116101f0575050505050905090565b60606019805480602002602001604051908101604052809291908181526020016000905b828210156103be5760008481526020908190206040805180820182526002860290920180546001600160a01b031683526001810180548351818702810187019094528084529394919385830193928301828280156103a657602002820191906000526020600020906000905b82829054906101000a900460e01b6001600160e01b031916815260200190600401906020826003010492830192600103820291508084116103685790505b505050505081525050815260200190600101906102fc565b50505050905090565b60606018805480602002602001604051908101604052809291908181526020016000905b828210156103be57838290600052602060002001805461040a90610cbd565b80601f016020809104026020016040519081016040528092919081815260200182805461043690610cbd565b80156104835780601f1061045857610100808354040283529160200191610483565b820191906000526020600020905b81548152906001019060200180831161046657829003601f168201915b5050505050815260200190600101906103eb565b6060601a805480602002602001604051908101604052809291908181526020016000905b828210156103be5760008481526020908190206040805180820182526002860290920180546001600160a01b0316835260018101805483518187028101870190945280845293949193858301939283018282801561056557602002820191906000526020600020906000905b82829054906101000a900460e01b6001600160e01b031916815260200190600401906020826003010492830192600103820291508084116105275790505b505050505081525050815260200190600101906104bb565b60606017805480602002602001604051908101604052809291908181526020016000905b828210156103be5783829060005260206000200180546105c090610cbd565b80601f01602080910402602001604051908101604052809291908181526020018280546105ec90610cbd565b80156106395780601f1061060e57610100808354040283529160200191610639565b820191906000526020600020905b81548152906001019060200180831161061c57829003601f168201915b5050505050815260200190600101906105a1565b600754600090610100900460ff161561066f5750600754610100900460ff1690565b6000737109709ecfa91a80626ff3989d68f67f5b1dd12d3b156107755760408051737109709ecfa91a80626ff3989d68f67f5b1dd12d602082018190526519985a5b195960d21b828401528251808303840181526060830190935260009290916106fd917f667f9d70ca411d70ead50d8d5c22070dafc36ad75f3dcf5e7237b22ade9aecc491608001610cf1565b60408051601f198184030181529082905261071791610d22565b6000604051808303816000865af19150503d8060008114610754576040519150601f19603f3d011682016040523d82523d6000602084013e610759565b606091505b50915050808060200190518101906107719190610d3e565b9150505b919050565b7f885cb69240a935d632d79c317109709ecfa91a80626ff3989d68f67f5b1dd12d60001c6001600160a01b031663f48448146040518163ffffffff1660e01b8152600401600060405180830381600087803b1580156107d857600080fd5b505af11580156107ec573d6000803e3d6000fd5b5050601b54604051634870496f60e01b81526001600160a01b039091169250634870496f91506108289088908890889088908890600401610e21565b600060405180830381600087803b15801561084257600080fd5b505af1158015610856573d6000803e3d6000fd5b505050505050505050565b6060601380548060200260200160405190810160405280929190818152602001828054801561020e576020028201919060005260206000209081546001600160a01b031681526001909101906020018083116101f0575050505050905090565b61037580610ed883390190565b6020808252825182820181905260009190848201906040850190845b8181101561090f5783516001600160a01b0316835292840192918401916001016108ea565b50909695505050505050565b60006020808301818452808551808352604092508286019150828160051b8701018488016000805b848110156109bf57898403603f19018652825180516001600160a01b03168552880151888501889052805188860181905290890190839060608701905b808310156109aa5783516001600160e01b0319168252928b019260019290920191908b0190610980565b50978a01979550505091870191600101610943565b50919998505050505050505050565b60005b838110156109e95781810151838201526020016109d1565b838111156109f8576000848401525b50505050565b60008151808452610a168160208601602086016109ce565b601f01601f19169290920160200192915050565b6000602080830181845280855180835260408601915060408160051b870101925083870160005b82811015610a7f57603f19888603018452610a6d8583516109fe565b94509285019290850190600101610a51565b5092979650505050505050565b634e487b7160e01b600052604160045260246000fd5b60405160c0810167ffffffffffffffff81118282101715610ac557610ac5610a8c565b60405290565b604051601f8201601f1916810167ffffffffffffffff81118282101715610af457610af4610a8c565b604052919050565b80356001600160a01b038116811461077557600080fd5b600060808284031215610b2557600080fd5b50919050565b60008083601f840112610b3d57600080fd5b50813567ffffffffffffffff811115610b5557600080fd5b6020830191508360208260051b8501011115610b7057600080fd5b9250929050565b600080600080600060e08688031215610b8f57600080fd5b853567ffffffffffffffff80821115610ba757600080fd5b9087019060c0828a031215610bbb57600080fd5b610bc3610aa2565b823581526020610bd4818501610afc565b81830152610be460408501610afc565b6040830152606084013560608301526080840135608083015260a084013583811115610c0f57600080fd5b8085019450508a601f850112610c2457600080fd5b833583811115610c3657610c36610a8c565b610c48601f8201601f19168301610acb565b8181528c83838801011115610c5c57600080fd5b8183870184830137600091810183019190915260a08301529097508801359550610c898960408a01610b13565b945060c0880135915080821115610c9f57600080fd5b50610cac88828901610b2b565b969995985093965092949392505050565b600181811c90821680610cd157607f821691505b602082108103610b2557634e487b7160e01b600052602260045260246000fd5b6001600160e01b0319831681528151600090610d148160048501602087016109ce565b919091016004019392505050565b60008251610d348184602087016109ce565b9190910192915050565b600060208284031215610d5057600080fd5b81518015158114610d6057600080fd5b9392505050565b81835281816020850137506000828201602090810191909152601f909101601f19169091010190565b81835260006020808501808196508560051b810191508460005b87811015610e145782840389528135601e19883603018112610dcb57600080fd5b8701803567ffffffffffffffff811115610de457600080fd5b803603891315610df357600080fd5b610e008682898501610d67565b9a87019a9550505090840190600101610daa565b5091979650505050505050565b60e080825286519082015260208601516001600160a01b039081166101008301526040870151166101208201526060860151610140820152608086015161016082015260a086015160c0610180830152600090610e826101a08401826109fe565b9050866020840152610eb86040840187803582526020810135602083015260408101356040830152606081013560608301525050565b82810360c0840152610ecb818587610d90565b9897505050505050505056fe608060405234801561001057600080fd5b506000805460ff191660011790556103488061002d6000396000f3fe608060405234801561001057600080fd5b506004361061002b5760003560e01c80634870496f14610030575b600080fd5b61004361003e3660046101cc565b610045565b005b60005460ff161561008d5760405162461bcd60e51b815260206004820152600e60248201526d141bdc9d185b0e881c185d5cd95960921b604482015260640160405180910390fd5b84604001516001600160a01b031685602001516001600160a01b03167fa998e9f42be9c7bd87798d599093d87d0393e08ff742a512c623afe9c6a9c61f60405160405180910390a35050505050565b634e487b7160e01b600052604160045260246000fd5b60405160c0810167ffffffffffffffff81118282101715610115576101156100dc565b60405290565b604051601f8201601f1916810167ffffffffffffffff81118282101715610144576101446100dc565b604052919050565b80356001600160a01b038116811461016357600080fd5b919050565b60006080828403121561017a57600080fd5b50919050565b60008083601f84011261019257600080fd5b50813567ffffffffffffffff8111156101aa57600080fd5b6020830191508360208260051b85010111156101c557600080fd5b9250929050565b600080600080600060e086880312156101e457600080fd5b853567ffffffffffffffff808211156101fc57600080fd5b9087019060c0828a03121561021057600080fd5b6102186100f2565b82358152602061022981850161014c565b818301526102396040850161014c565b6040830152606084013560608301526080840135608083015260a08401358381111561026457600080fd5b8085019450508a601f85011261027957600080fd5b83358381111561028b5761028b6100dc565b61029d601f8201601f1916830161011b565b8181528c838388010111156102b157600080fd5b8183870184830137600091810183019190915260a083015290975088013595506102de8960408a01610168565b945060c08801359150808211156102f457600080fd5b5061030188828901610180565b96999598509396509294939250505056fea2646970667358221220c6780a421240a4f971c9fd2210c1d2dff868ab9d69234d7dd7e6b3879edc63b264736f6c634300080d0033a2646970667358221220954346fcc74163d262620752b4f53cd68feb8af870a4f741a745efcb0bc4327964736f6c634300080d0033" ) )
+      
+    
+    syntax Field ::= S2KtestZModPortalTestField
+    
+    syntax S2KtestZModPortalTestField ::= "stdstore" [symbol(""), klabel(field_test%PortalTest_stdstore)]
+    
+    syntax S2KtestZModPortalTestField ::= "IS_TEST" [symbol(""), klabel(field_test%PortalTest_IS_TEST)]
+    
+    syntax S2KtestZModPortalTestField ::= "_failed" [symbol(""), klabel(field_test%PortalTest__failed)]
+    
+    syntax S2KtestZModPortalTestField ::= "stdChainsInitialized" [symbol(""), klabel(field_test%PortalTest_stdChainsInitialized)]
+    
+    syntax S2KtestZModPortalTestField ::= "chains" [symbol(""), klabel(field_test%PortalTest_chains)]
+    
+    syntax S2KtestZModPortalTestField ::= "defaultRpcUrls" [symbol(""), klabel(field_test%PortalTest_defaultRpcUrls)]
+    
+    syntax S2KtestZModPortalTestField ::= "idToAlias" [symbol(""), klabel(field_test%PortalTest_idToAlias)]
+    
+    syntax S2KtestZModPortalTestField ::= "fallbackToDefaultRpcUrls" [symbol(""), klabel(field_test%PortalTest_fallbackToDefaultRpcUrls)]
+    
+    syntax S2KtestZModPortalTestField ::= "gasMeteringOff" [symbol(""), klabel(field_test%PortalTest_gasMeteringOff)]
+    
+    syntax S2KtestZModPortalTestField ::= "_excludedContracts" [symbol(""), klabel(field_test%PortalTest__excludedContracts)]
+    
+    syntax S2KtestZModPortalTestField ::= "_excludedSenders" [symbol(""), klabel(field_test%PortalTest__excludedSenders)]
+    
+    syntax S2KtestZModPortalTestField ::= "_targetedContracts" [symbol(""), klabel(field_test%PortalTest__targetedContracts)]
+    
+    syntax S2KtestZModPortalTestField ::= "_targetedSenders" [symbol(""), klabel(field_test%PortalTest__targetedSenders)]
+    
+    syntax S2KtestZModPortalTestField ::= "_excludedArtifacts" [symbol(""), klabel(field_test%PortalTest__excludedArtifacts)]
+    
+    syntax S2KtestZModPortalTestField ::= "_targetedArtifacts" [symbol(""), klabel(field_test%PortalTest__targetedArtifacts)]
+    
+    syntax S2KtestZModPortalTestField ::= "_targetedArtifactSelectors" [symbol(""), klabel(field_test%PortalTest__targetedArtifactSelectors)]
+    
+    syntax S2KtestZModPortalTestField ::= "_targetedSelectors" [symbol(""), klabel(field_test%PortalTest__targetedSelectors)]
+    
+    syntax S2KtestZModPortalTestField ::= "portalContract" [symbol(""), klabel(field_test%PortalTest_portalContract)]
+    
+    rule  ( #loc ( S2KtestZModPortalTest . stdstore ) => 0 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . IS_TEST ) => 7 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . _failed ) => 7 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . stdChainsInitialized ) => 7 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . chains ) => 8 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . defaultRpcUrls ) => 9 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . idToAlias ) => 10 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . fallbackToDefaultRpcUrls ) => 11 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . gasMeteringOff ) => 11 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . _excludedContracts ) => 19 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . _excludedSenders ) => 20 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . _targetedContracts ) => 21 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . _targetedSenders ) => 22 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . _excludedArtifacts ) => 23 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . _targetedArtifacts ) => 24 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . _targetedArtifactSelectors ) => 25 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . _targetedSelectors ) => 26 )
+      
+    
+    rule  ( #loc ( S2KtestZModPortalTest . portalContract ) => 27 )
+      
+    
+    syntax Bytes ::= S2KtestZModPortalTestContract "." S2KtestZModPortalTestMethod [function, symbol(""), klabel(method_test%PortalTest)]
+    
+    syntax S2KtestZModPortalTestMethod ::= "S2KISZUndTEST" "(" ")" [symbol(""), klabel(method_test%PortalTest_S2KISZUndTEST_)]
+    
+    syntax S2KtestZModPortalTestMethod ::= "S2KexcludeArtifacts" "(" ")" [symbol(""), klabel(method_test%PortalTest_S2KexcludeArtifacts_)]
+    
+    syntax S2KtestZModPortalTestMethod ::= "S2KexcludeContracts" "(" ")" [symbol(""), klabel(method_test%PortalTest_S2KexcludeContracts_)]
+    
+    syntax S2KtestZModPortalTestMethod ::= "S2KexcludeSenders" "(" ")" [symbol(""), klabel(method_test%PortalTest_S2KexcludeSenders_)]
+    
+    syntax S2KtestZModPortalTestMethod ::= "S2Kfailed" "(" ")" [symbol(""), klabel(method_test%PortalTest_S2Kfailed_)]
+    
+    syntax S2KtestZModPortalTestMethod ::= "S2KsetUp" "(" ")" [symbol(""), klabel(method_test%PortalTest_S2KsetUp_)]
+    
+    syntax S2KtestZModPortalTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol(""), klabel(method_test%PortalTest_S2KtargetArtifactSelectors_)]
+    
+    syntax S2KtestZModPortalTestMethod ::= "S2KtargetArtifacts" "(" ")" [symbol(""), klabel(method_test%PortalTest_S2KtargetArtifacts_)]
+    
+    syntax S2KtestZModPortalTestMethod ::= "S2KtargetContracts" "(" ")" [symbol(""), klabel(method_test%PortalTest_S2KtargetContracts_)]
+    
+    syntax S2KtestZModPortalTestMethod ::= "S2KtargetSelectors" "(" ")" [symbol(""), klabel(method_test%PortalTest_S2KtargetSelectors_)]
+    
+    syntax S2KtestZModPortalTestMethod ::= "S2KtargetSenders" "(" ")" [symbol(""), klabel(method_test%PortalTest_S2KtargetSenders_)]
+    
+    syntax S2KtestZModPortalTestMethod ::= "S2KtestZUndwithdrawalZUndpaused" "(" Int ":" "uint256" "," Int ":" "address" "," Int ":" "address" "," Int ":" "uint256" "," Int ":" "uint256" "," Bytes ":" "bytes" "," Int ":" "uint256" "," Int ":" "bytes32" "," Int ":" "bytes32" "," Int ":" "bytes32" "," Int ":" "bytes32" "," Bytes ":" "bytes" ")" [symbol(""), klabel(method_test%PortalTest_S2KtestZUndwithdrawalZUndpaused_uint256_address_address_uint256_uint256_bytes_uint256_bytes32_bytes32_bytes32_bytes32_bytes)]
+    
+    rule  ( S2KtestZModPortalTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModPortalTest . S2KexcludeArtifacts ( ) => #abiCallData ( "excludeArtifacts" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModPortalTest . S2KexcludeContracts ( ) => #abiCallData ( "excludeContracts" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModPortalTest . S2KexcludeSenders ( ) => #abiCallData ( "excludeSenders" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModPortalTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModPortalTest . S2KsetUp ( ) => #abiCallData ( "setUp" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModPortalTest . S2KtargetArtifactSelectors ( ) => #abiCallData ( "targetArtifactSelectors" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModPortalTest . S2KtargetArtifacts ( ) => #abiCallData ( "targetArtifacts" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModPortalTest . S2KtargetContracts ( ) => #abiCallData ( "targetContracts" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModPortalTest . S2KtargetSelectors ( ) => #abiCallData ( "targetSelectors" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModPortalTest . S2KtargetSenders ( ) => #abiCallData ( "targetSenders" , .TypedArgs ) )
+      
+    
+    rule  ( S2KtestZModPortalTest . S2KtestZUndwithdrawalZUndpaused ( V0_nonce : uint256 , V1_sender : address , V2_target : address , V3_value : uint256 , V4_gasLimit : uint256 , V5_data : bytes , V6__l2OutputIndex : uint256 , V7_version : bytes32 , V8_stateRoot : bytes32 , V9_messagePasserStorageRoot : bytes32 , V10_latestBlockhash : bytes32 , V11__withdrawalProof_0 : bytes ) => #abiCallData ( "test_withdrawal_paused" , ( #tuple ( ( #uint256 ( V0_nonce ) , ( #address ( V1_sender ) , ( #address ( V2_target ) , ( #uint256 ( V3_value ) , ( #uint256 ( V4_gasLimit ) , ( #bytes ( V5_data ) , .TypedArgs ) ) ) ) ) ) ) , ( #uint256 ( V6__l2OutputIndex ) , ( #tuple ( ( #bytes32 ( V7_version ) , ( #bytes32 ( V8_stateRoot ) , ( #bytes32 ( V9_messagePasserStorageRoot ) , ( #bytes32 ( V10_latestBlockhash ) , .TypedArgs ) ) ) ) ) , ( #array ( #bytes ( V11__withdrawalProof_0 ) , 1 , ( #bytes ( V11__withdrawalProof_0 ) , .TypedArgs ) ) , .TypedArgs ) ) ) ) ) )
+       ensures ( #rangeUInt ( 256 , V0_nonce )
+       andBool ( #rangeAddress ( V1_sender )
+       andBool ( #rangeAddress ( V2_target )
+       andBool ( #rangeUInt ( 256 , V3_value )
+       andBool ( #rangeUInt ( 256 , V4_gasLimit )
+       andBool ( #rangeUInt ( 64 , lengthBytes ( V5_data ) )
+       andBool ( #rangeUInt ( 256 , V6__l2OutputIndex )
+       andBool ( #rangeBytes ( 32 , V7_version )
+       andBool ( #rangeBytes ( 32 , V8_stateRoot )
+       andBool ( #rangeBytes ( 32 , V9_messagePasserStorageRoot )
+       andBool ( #rangeBytes ( 32 , V10_latestBlockhash )
+       andBool ( lengthBytes ( V11__withdrawalProof_0 ) ==Int 32
+               ))))))))))))
+      
+    
+    rule  ( selector ( "IS_TEST()" ) => 4202047188 )
+      
+    
+    rule  ( selector ( "excludeArtifacts()" ) => 3041954473 )
+      
+    
+    rule  ( selector ( "excludeContracts()" ) => 3792478065 )
+      
+    
+    rule  ( selector ( "excludeSenders()" ) => 517440284 )
+      
+    
+    rule  ( selector ( "failed()" ) => 3124842406 )
+      
+    
+    rule  ( selector ( "setUp()" ) => 177362148 )
+      
+    
+    rule  ( selector ( "targetArtifactSelectors()" ) => 1725540768 )
+      
+    
+    rule  ( selector ( "targetArtifacts()" ) => 2233625729 )
+      
+    
+    rule  ( selector ( "targetContracts()" ) => 1064470260 )
+      
+    
+    rule  ( selector ( "targetSelectors()" ) => 2439649222 )
+      
+    
+    rule  ( selector ( "targetSenders()" ) => 1046363171 )
+      
+    
+    rule  ( selector ( "test_withdrawal_paused((uint256,address,address,uint256,uint256,bytes),uint256,(bytes32,bytes32,bytes32,bytes32),bytes[])" ) => 3251445116 )
+      
+
 endmodule
 
 module S2KsrcZModPrank-CONTRACT
diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected
index 91a8dcc0c..7016e1269 100644
--- a/src/tests/integration/test-data/show/foundry.k.expected
+++ b/src/tests/integration/test-data/show/foundry.k.expected
@@ -1,6 +1,7 @@
 requires "contracts.k"
 requires "requires/lemmas.k"
 requires "requires/cse-lemmas.k"
+requires "requires/pausability-lemmas.k"
 
 module FOUNDRY-MAIN
     imports public S2KsrcZModduplicatesZMod1ZModDuplicateName-VERIFICATION
@@ -80,6 +81,9 @@ module FOUNDRY-MAIN
     imports public S2KtestZModAdditionalToken-VERIFICATION
     imports public S2KtestZModMyErc20-VERIFICATION
     imports public S2KtestZModPlainPrankTest-VERIFICATION
+    imports public S2KsrcZModPortal-VERIFICATION
+    imports public S2KsrcZModTypes-VERIFICATION
+    imports public S2KtestZModPortalTest-VERIFICATION
     imports public S2KsrcZModPrank-VERIFICATION
     imports public S2KtestZModPrankTest-VERIFICATION
     imports public S2KtestZModPrankTestMsgSender-VERIFICATION
@@ -676,6 +680,28 @@ module S2KtestZModPlainPrankTest-VERIFICATION
     
     
 
+endmodule
+
+module S2KsrcZModPortal-VERIFICATION
+    imports public S2KsrcZModPortal-CONTRACT
+    
+    
+
+endmodule
+
+module S2KsrcZModTypes-VERIFICATION
+    imports public S2KsrcZModTypes-CONTRACT
+    
+    
+
+endmodule
+
+module S2KtestZModPortalTest-VERIFICATION
+    imports public S2KtestZModPortalTest-CONTRACT
+    imports public PAUSABILITY-LEMMAS
+    
+    
+
 endmodule
 
 module S2KsrcZModPrank-VERIFICATION