diff --git a/src/tests/integration/test-data/show/merge-loop-heads.expected b/src/tests/integration/test-data/show/merge-loop-heads.expected
index 32867c4f2..cf64e6988 100644
--- a/src/tests/integration/test-data/show/merge-loop-heads.expected
+++ b/src/tests/integration/test-data/show/merge-loop-heads.expected
@@ -30,7 +30,7 @@
 ┃  │   method: test%BMCLoopsTest.test_bmc(uint256)
 ┃  │
 ┃  ┊  constraint:
-┃  ┊      ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <=In...
+┃  ┊      ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <=Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 0 andBool ( pow24 <Int NUMBER_CELL:Int andBool ( NUMBER_CELL:Int <Int pow32 andBool ( 1073741824 <Int TIMESTAMP_CELL:Int andBool ( TIMESTAMP_CELL:Int <Int 34359738368 andBool ( CALLER_ID:Int <Int pow160 andBool ( ORIGIN_ID:Int <Int pow160 andBool ( VV0_n_114b9705:Int <Int pow256 andBool ( ( notBool CALLER_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool ORIGIN_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool C_BMCLOOPSTEST_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) impliesBool ( ( 0 ==K V_45741f39:Int andBool ( ( V_45741f39 ==K 0 andBool VV0_n_114b9705:Int <=Int 0 ) orBool ( V_45741f39 ==K 1 andBool #range ( 0 < VV0_n_114b9705:Int <= 1 ) ) ) ) orBool ( 0 ==K 2 andBool ( 0 <Int VV0_n_114b9705:Int andBool ( 1 <Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 2 andBool ( notBool C_BMCLOOPSTEST_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) ) ) ) ) ) )
 ┃  ┊  subst: ...
 ┃  ├─ 20
 ┃  │   k: JUMPI 1478 bool2Word ( VV0_n_114b9705:Int <=Int V_8ae8c0f0:Int ) ~> #pc [ JUMPI  ...
@@ -84,7 +84,7 @@
    ┃  │   method: test%BMCLoopsTest.test_bmc(uint256)
    ┃  │
    ┃  ┊  constraint:
-   ┃  ┊      ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <Int...
+   ┃  ┊      ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <Int VV0_n_114b9705:Int andBool ( 0 <=Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 1 andBool ( pow24 <Int NUMBER_CELL:Int andBool ( NUMBER_CELL:Int <Int pow32 andBool ( 1073741824 <Int TIMESTAMP_CELL:Int andBool ( TIMESTAMP_CELL:Int <Int 34359738368 andBool ( CALLER_ID:Int <Int pow160 andBool ( ORIGIN_ID:Int <Int pow160 andBool ( VV0_n_114b9705:Int <Int pow256 andBool ( ( notBool CALLER_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool ORIGIN_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool C_BMCLOOPSTEST_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) impliesBool ( ( 1 ==K V_45741f39:Int andBool ( ( V_45741f39 ==K 0 andBool VV0_n_114b9705:Int <=Int 0 ) orBool ( V_45741f39 ==K 1 andBool #range ( 0 < VV0_n_114b9705:Int <= 1 ) ) ) ) orBool ( 1 ==K 2 andBool ( 0 <Int VV0_n_114b9705:Int andBool ( 1 <Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 2 andBool ( notBool C_BMCLOOPSTEST_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) ) ) ) ) ) )
    ┃  ┊  subst: ...
    ┃  └─ 20
    ┃      k: JUMPI 1478 bool2Word ( VV0_n_114b9705:Int <=Int V_8ae8c0f0:Int ) ~> #pc [ JUMPI  ...
@@ -130,7 +130,7 @@
       ┃  │   method: test%BMCLoopsTest.test_bmc(uint256)
       ┃  │
       ┃  ┊  constraint:
-      ┃  ┊      ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <Int...
+      ┃  ┊      ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <Int VV0_n_114b9705:Int andBool ( 1 <Int VV0_n_114b9705:Int andBool ( 0 <=Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 2 andBool ( pow24 <Int NUMBER_CELL:Int andBool ( NUMBER_CELL:Int <Int pow32 andBool ( 1073741824 <Int TIMESTAMP_CELL:Int andBool ( TIMESTAMP_CELL:Int <Int 34359738368 andBool ( CALLER_ID:Int <Int pow160 andBool ( ORIGIN_ID:Int <Int pow160 andBool ( VV0_n_114b9705:Int <Int pow256 andBool ( ( notBool CALLER_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool ORIGIN_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool C_BMCLOOPSTEST_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) impliesBool ( ( 2 ==K V_45741f39:Int andBool ( ( V_45741f39 ==K 0 andBool VV0_n_114b9705:Int <=Int 0 ) orBool ( V_45741f39 ==K 1 andBool #range ( 0 < VV0_n_114b9705:Int <= 1 ) ) ) ) orBool ( 2 ==K 2 andBool ( 0 <Int VV0_n_114b9705:Int andBool ( 1 <Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 2 andBool ( notBool C_BMCLOOPSTEST_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) ) ) ) ) ) )
       ┃  ┊  subst: ...
       ┃  └─ 20
       ┃      k: JUMPI 1478 bool2Word ( VV0_n_114b9705:Int <=Int V_8ae8c0f0:Int ) ~> #pc [ JUMPI  ...
diff --git a/src/tests/integration/test-data/show/node-refutation.expected b/src/tests/integration/test-data/show/node-refutation.expected
index 9d114eafd..64787c0a2 100644
--- a/src/tests/integration/test-data/show/node-refutation.expected
+++ b/src/tests/integration/test-data/show/node-refutation.expected
@@ -42,7 +42,7 @@
    │   method: test%MergeTest.test_branch_merge(uint256)
    │
    │  (90 steps)
-   ├─ 12
+   ├─ 10
    │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
    │   pc: 235
    │   callDepth: 0
@@ -51,7 +51,7 @@
    │   method: test%MergeTest.test_branch_merge(uint256)
    │
    │  (1 step)
-   ├─ 13
+   ├─ 11
    │   k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
    │   pc: 235
    │   callDepth: 0
@@ -60,7 +60,7 @@
    │   method: test%MergeTest.test_branch_merge(uint256)
    │
    │  (2 steps)
-   ├─ 14 (terminal)
+   ├─ 12 (terminal)
    │   k: #halt ~> CONTINUATION:K
    │   pc: 235
    │   callDepth: 0
@@ -319,7 +319,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0
                )))))))))))))))
       [priority(20), label(BASIC-BLOCK-1-TO-3)]
     
-    rule [BASIC-BLOCK-5-TO-12]: <foundry>
+    rule [BASIC-BLOCK-5-TO-10]: <foundry>
            <kevm>
              <k>
                ( JUMPI 535 bool2Word ( 10 <=Int VV0_x_114b9705:Int )
@@ -556,9 +556,9 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
                ))))))))))))))))
-      [priority(20), label(BASIC-BLOCK-5-TO-12)]
+      [priority(20), label(BASIC-BLOCK-5-TO-10)]
     
-    rule [BASIC-BLOCK-12-TO-13]: <foundry>
+    rule [BASIC-BLOCK-10-TO-11]: <foundry>
            <kevm>
              <k>
                ( #end EVMC_SUCCESS => #halt )
@@ -797,9 +797,9 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
                ))))))))))))))))
-      [priority(20), label(BASIC-BLOCK-12-TO-13)]
+      [priority(20), label(BASIC-BLOCK-10-TO-11)]
     
-    rule [BASIC-BLOCK-13-TO-14]: <foundry>
+    rule [BASIC-BLOCK-11-TO-12]: <foundry>
            <kevm>
              <k>
                #halt
@@ -1038,7 +1038,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0
        andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
        andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
                ))))))))))))))))
-      [priority(20), label(BASIC-BLOCK-13-TO-14)]
+      [priority(20), label(BASIC-BLOCK-11-TO-12)]
 
 endmodule
 0 Failure nodes. (0 pending and 0 failing)
diff --git a/src/tests/integration/test-data/show/split-node.expected b/src/tests/integration/test-data/show/split-node.expected
index 62345bf0b..b12252bd5 100644
--- a/src/tests/integration/test-data/show/split-node.expected
+++ b/src/tests/integration/test-data/show/split-node.expected
@@ -44,7 +44,7 @@
 ┃ (branch)
 ┣━━┓ subst: .Subst
 ┃  ┃ constraint:
-┃  ┃     VV0_addr_114b9705:Int ==Int 4914609233421842180357068880087500439777551132...
+┃  ┃     VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043977755113263
 ┃  │
 ┃  └─ 70 (leaf, refuted)
 ┃      k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
@@ -55,7 +55,7 @@
 ┃
 ┗━━┓ subst: .Subst
    ┃ constraint:
-   ┃     ( notBool VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043...
+   ┃     ( notBool VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043977755113263 )
    │
    ├─ 71 (split)
    │   k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
@@ -67,7 +67,7 @@
    ┃ (branch)
    ┣━━┓ subst: .Subst
    ┃  ┃ constraint:
-   ┃  ┃     VV0_addr_114b9705:Int ==Int 6453264744265472033134100691539059085253624343...
+   ┃  ┃     VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908525362434349
    ┃  │
    ┃  └─ 72 (leaf, refuted)
    ┃      k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
@@ -78,7 +78,7 @@
    ┃
    ┗━━┓ subst: .Subst
       ┃ constraint:
-      ┃     ( notBool VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908...
+      ┃     ( notBool VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908525362434349 )
       │
       ├─ 73 (split)
       │   k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
@@ -90,7 +90,7 @@
       ┃ (branch)
       ┣━━┓ subst: .Subst
       ┃  ┃ constraint:
-      ┃  ┃     VV0_addr_114b9705:Int ==Int 7288155633859770404529437778790614277562773065...
+      ┃  ┃     VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427756277306518
       ┃  │
       ┃  └─ 74 (leaf, refuted)
       ┃      k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
@@ -101,7 +101,7 @@
       ┃
       ┗━━┓ subst: .Subst
          ┃ constraint:
-         ┃     ( notBool VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427...
+         ┃     ( notBool VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427756277306518 )
          │
          ├─ 75
          │   k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
@@ -226,9 +226,9 @@
          │   method: test%PrankTest.testSymbolicStartPrank(address)
          │
          ┊  constraint:
-         ┊      ( notBool VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043...
-         ┊      ( notBool VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908...
-         ┊      ( notBool VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427...
+         ┊      ( notBool VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043977755113263 )
+         ┊      ( notBool VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908525362434349 )
+         ┊      ( notBool VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427756277306518 )
          ┊  subst: ...
          └─ 10 (leaf, target, terminal)
              k: #halt ~> CONTINUATION:K