diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected
index ce3c558705..7fb7af1906 100644
--- a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected
+++ b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected
@@ -79,8 +79,8 @@
 
 
 
-    
-    
+
+
     rule [BASIC-BLOCK-1-TO-3]: <foundry>
            <kevm>
              <k>
@@ -301,7 +301,7 @@
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
       [label(BASIC-BLOCK-1-TO-3)]
-    
+
     rule [BASIC-BLOCK-3-TO-4]: <foundry>
            <kevm>
              <k>
@@ -511,7 +511,7 @@
        andBool ( VV1_b_114b9705:Int <Int pow256
                ))))))))))
       [label(BASIC-BLOCK-3-TO-4)]
-    
+
     rule [BASIC-BLOCK-4-TO-5]: <foundry>
            <kevm>
              <k>
@@ -726,10 +726,10 @@
        andBool ( VV1_b_114b9705:Int <Int pow256
                ))))))))))
        ensures ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))
       [label(BASIC-BLOCK-4-TO-5)]
-    
+
     rule [BASIC-BLOCK-5-TO-6]: <foundry>
            <kevm>
              <k>
@@ -944,10 +944,10 @@
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-5-TO-6)]
-    
+
     rule [BASIC-BLOCK-6-TO-7]: <foundry>
            <kevm>
              <k>
@@ -1161,10 +1161,10 @@
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-6-TO-7)]
-    
+
     rule [BASIC-BLOCK-7-TO-8]: <foundry>
            <kevm>
              <k>
@@ -1376,10 +1376,10 @@
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-7-TO-8)]
-    
+
     rule [BASIC-BLOCK-8-TO-9]: <foundry>
            <kevm>
              <k>
@@ -1592,10 +1592,10 @@
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-8-TO-9)]
-    
+
     rule [BASIC-BLOCK-9-TO-10]: <foundry>
            <kevm>
              <k>
@@ -1808,10 +1808,10 @@
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-9-TO-10)]
-    
+
     rule [BASIC-BLOCK-10-TO-11]: <foundry>
            <kevm>
              <k>
@@ -2024,7 +2024,7 @@
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-10-TO-11)]
 
diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
index fa7a7991c3..822e358bea 100644
--- a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
+++ b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
@@ -288,12 +288,12 @@ Node 11:
 #And ( { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
 #And ( { true #Equals VV0_a_114b9705:Int <Int pow256 }
 #And ( { true #Equals VV1_b_114b9705:Int <Int pow256 }
-#And { true #Equals ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ==Bool true } ) ) ) ) ) ) ) ) ) ) ) )
+#And { true #Equals ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) } ) ) ) ) ) ) ) ) ) ) ) )
+
+
 
 
 
-    
-    
     rule [BASIC-BLOCK-1-TO-3]: <foundry>
            <kevm>
              <k>
@@ -514,7 +514,7 @@ Node 11:
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
       [label(BASIC-BLOCK-1-TO-3)]
-    
+
     rule [BASIC-BLOCK-3-TO-4]: <foundry>
            <kevm>
              <k>
@@ -724,7 +724,7 @@ Node 11:
        andBool ( VV1_b_114b9705:Int <Int pow256
                ))))))))))
       [label(BASIC-BLOCK-3-TO-4)]
-    
+
     rule [BASIC-BLOCK-4-TO-5]: <foundry>
            <kevm>
              <k>
@@ -939,10 +939,10 @@ Node 11:
        andBool ( VV1_b_114b9705:Int <Int pow256
                ))))))))))
        ensures ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))
       [label(BASIC-BLOCK-4-TO-5)]
-    
+
     rule [BASIC-BLOCK-5-TO-6]: <foundry>
            <kevm>
              <k>
@@ -1157,10 +1157,10 @@ Node 11:
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-5-TO-6)]
-    
+
     rule [BASIC-BLOCK-6-TO-7]: <foundry>
            <kevm>
              <k>
@@ -1374,10 +1374,10 @@ Node 11:
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-6-TO-7)]
-    
+
     rule [BASIC-BLOCK-7-TO-8]: <foundry>
            <kevm>
              <k>
@@ -1589,10 +1589,10 @@ Node 11:
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-7-TO-8)]
-    
+
     rule [BASIC-BLOCK-8-TO-9]: <foundry>
            <kevm>
              <k>
@@ -1805,10 +1805,10 @@ Node 11:
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-8-TO-9)]
-    
+
     rule [BASIC-BLOCK-9-TO-10]: <foundry>
            <kevm>
              <k>
@@ -2021,10 +2021,10 @@ Node 11:
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-9-TO-10)]
-    
+
     rule [BASIC-BLOCK-10-TO-11]: <foundry>
            <kevm>
              <k>
@@ -2237,7 +2237,7 @@ Node 11:
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-10-TO-11)]
 
@@ -2260,7 +2260,7 @@ Failing nodes:
     #And ( { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
     #And ( { true #Equals VV0_a_114b9705:Int <Int pow256 }
     #And ( { true #Equals VV1_b_114b9705:Int <Int pow256 }
-    #And { true #Equals ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ==Bool true } ) ) ) ) ) ) ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_SUCCESS , failed: #lookup ( ( 46308022326495007027972728677917914892729792999299745830475596687180801507328 |-> 1 ) , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
+    #And { true #Equals ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) } ) ) ) ) ) ) ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_SUCCESS , failed: #lookup ( ( 46308022326495007027972728677917914892729792999299745830475596687180801507328 |-> 1 ) , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
   Path condition:
     #Top
   Model:
diff --git a/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected b/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected
index bc91ceb815..878c7728dc 100644
--- a/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected
+++ b/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected
@@ -104,8 +104,8 @@
 
 
 
-    
-    
+
+
     rule [BASIC-BLOCK-1-TO-3]: <foundry>
            <kevm>
              <k>
@@ -324,7 +324,7 @@
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
       [label(BASIC-BLOCK-1-TO-3)]
-    
+
     rule [BASIC-BLOCK-3-TO-4]: <foundry>
            <kevm>
              <k>
@@ -532,7 +532,7 @@
        andBool ( VV0_n_114b9705:Int <Int pow256
                ))))))))
       [label(BASIC-BLOCK-3-TO-4)]
-    
+
     rule [BASIC-BLOCK-4-TO-5]: <foundry>
            <kevm>
              <k>
@@ -743,9 +743,9 @@
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
                ))))))))
-       ensures VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       ensures VV0_n_114b9705:Int <=Int 51816696836262767
       [label(BASIC-BLOCK-4-TO-5)]
-    
+
     rule [BASIC-BLOCK-6-TO-8]: <foundry>
            <kevm>
              <k>
@@ -954,11 +954,11 @@
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
                ))))))))))
        ensures VV0_n_114b9705:Int ==K 0
       [label(BASIC-BLOCK-6-TO-8)]
-    
+
     rule [BASIC-BLOCK-7-TO-9]: <foundry>
            <kevm>
              <k>
@@ -1167,7 +1167,7 @@
        andBool ( VV0_n_114b9705:Int =/=Int 0
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
                ))))))))))
        ensures ( VV0_n_114b9705:Int =/=K 0
        andBool ( 0 <Int VV0_n_114b9705:Int
@@ -1197,7 +1197,7 @@
        andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
                ))))))))))))))))))))))))))
       [label(BASIC-BLOCK-7-TO-9)]
-    
+
     rule [BASIC-BLOCK-8-TO-10]: <foundry>
            <kevm>
              <k>
@@ -1408,7 +1408,7 @@
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                )))))))
       [label(BASIC-BLOCK-8-TO-10)]
-    
+
     rule [BASIC-BLOCK-9-TO-11]: <foundry>
            <kevm>
              <k>
@@ -1642,12 +1642,12 @@
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
        andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
        andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
                )))))))))))))))))))))))))))))))))))
       [label(BASIC-BLOCK-9-TO-11)]
-    
+
     rule [BASIC-BLOCK-10-TO-12]: <foundry>
            <kevm>
              <k>
@@ -1858,7 +1858,7 @@
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                )))))))
       [label(BASIC-BLOCK-10-TO-12)]
-    
+
     rule [BASIC-BLOCK-11-TO-13]: <foundry>
            <kevm>
              <k>
@@ -2092,7 +2092,7 @@
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
        andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
        andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
                )))))))))))))))))))))))))))))))))))
diff --git a/tests/foundry/golden/AssumeTest.testFail_assume_true(uint256,uint256).expected b/tests/foundry/golden/AssumeTest.testFail_assume_true(uint256,uint256).expected
index f72c34c46e..2c4ed40875 100644
--- a/tests/foundry/golden/AssumeTest.testFail_assume_true(uint256,uint256).expected
+++ b/tests/foundry/golden/AssumeTest.testFail_assume_true(uint256,uint256).expected
@@ -84,8 +84,8 @@
 
 
 module SUMMARY-ASSUMETEST.TESTFAIL-ASSUME-TRUE:EF68C1EA07B094FCF03E02D287B47204FA02108E3334C204F81DEA4C78FD1289
-    
-    
+
+
            <kevm>
              <k>
                ( #execute
@@ -305,7 +305,7 @@ module SUMMARY-ASSUMETEST.TESTFAIL-ASSUME-TRUE:EF68C1EA07B094FCF03E02D287B47204F
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
       [label(BASIC-BLOCK-1-TO-3)]
-    
+
            <kevm>
              <k>
                ( CALL 9223372036854772808 645326474426547203313410069153905908525362434349 0 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
@@ -514,7 +514,7 @@ module SUMMARY-ASSUMETEST.TESTFAIL-ASSUME-TRUE:EF68C1EA07B094FCF03E02D287B47204F
        andBool ( VV1_b_114b9705:Int <Int pow256
                ))))))))))
       [label(BASIC-BLOCK-3-TO-4)]
-    
+
            <kevm>
              <k>
                ( #checkCall 728815563385977040452943777879061427756277306518 0
@@ -728,10 +728,10 @@ module SUMMARY-ASSUMETEST.TESTFAIL-ASSUME-TRUE:EF68C1EA07B094FCF03E02D287B47204F
        andBool ( VV1_b_114b9705:Int <Int pow256
                ))))))))))
        ensures ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))
       [label(BASIC-BLOCK-4-TO-5)]
-    
+
            <kevm>
              <k>
                ( #gas [ MSTORE , MSTORE 192 46308022326495007027972728677917914892729792999299745830475596687180801507328 ]
@@ -945,10 +945,10 @@ module SUMMARY-ASSUMETEST.TESTFAIL-ASSUME-TRUE:EF68C1EA07B094FCF03E02D287B47204F
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-5-TO-6)]
-    
+
            <kevm>
              <k>
                ( #gasExec ( LONDON , JUMP 2621 )
@@ -1161,10 +1161,10 @@ module SUMMARY-ASSUMETEST.TESTFAIL-ASSUME-TRUE:EF68C1EA07B094FCF03E02D287B47204F
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-6-TO-7)]
-    
+
            <kevm>
              <k>
                ( CALL 9223372036854765663 645326474426547203313410069153905908525362434349 0 388 100 388 0 => #checkCall 728815563385977040452943777879061427756277306518 0
@@ -1375,10 +1375,10 @@ module SUMMARY-ASSUMETEST.TESTFAIL-ASSUME-TRUE:EF68C1EA07B094FCF03E02D287B47204F
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-7-TO-8)]
-    
+
            <kevm>
              <k>
                ( #checkCall 728815563385977040452943777879061427756277306518 0
@@ -1590,10 +1590,10 @@ module SUMMARY-ASSUMETEST.TESTFAIL-ASSUME-TRUE:EF68C1EA07B094FCF03E02D287B47204F
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-8-TO-9)]
-    
+
            <kevm>
              <k>
                ( #end EVMC_SUCCESS => #halt )
@@ -1805,10 +1805,10 @@ module SUMMARY-ASSUMETEST.TESTFAIL-ASSUME-TRUE:EF68C1EA07B094FCF03E02D287B47204F
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-9-TO-10)]
-    
+
            <kevm>
              <k>
                #halt
@@ -2020,7 +2020,7 @@ module SUMMARY-ASSUMETEST.TESTFAIL-ASSUME-TRUE:EF68C1EA07B094FCF03E02D287B47204F
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-10-TO-11)]
 
diff --git a/tests/foundry/golden/AssumeTest.test_assume_false(uint256,uint256).expected b/tests/foundry/golden/AssumeTest.test_assume_false(uint256,uint256).expected
index 36e1427d4a..ec143b47fc 100644
--- a/tests/foundry/golden/AssumeTest.test_assume_false(uint256,uint256).expected
+++ b/tests/foundry/golden/AssumeTest.test_assume_false(uint256,uint256).expected
@@ -292,13 +292,13 @@ Node 11:
 #And ( { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
 #And ( { true #Equals VV0_a_114b9705:Int <Int pow256 }
 #And ( { true #Equals VV1_b_114b9705:Int <Int pow256 }
-#And { true #Equals ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ==Bool true } ) ) ) ) ) ) ) ) ) ) ) )
+#And { true #Equals ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) } ) ) ) ) ) ) ) ) ) ) ) )
 
 
 
 module SUMMARY-ASSUMETEST.TEST-ASSUME-FALSE:FBA71744BDCE72BC45B9A84C3AB97CE0D7193B08F9D2C0C8DED04097536C129C
-    
-    
+
+
            <kevm>
              <k>
                ( #execute
@@ -518,7 +518,7 @@ module SUMMARY-ASSUMETEST.TEST-ASSUME-FALSE:FBA71744BDCE72BC45B9A84C3AB97CE0D719
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
       [label(BASIC-BLOCK-1-TO-3)]
-    
+
            <kevm>
              <k>
                ( CALL 9223372036854772765 645326474426547203313410069153905908525362434349 0 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
@@ -727,7 +727,7 @@ module SUMMARY-ASSUMETEST.TEST-ASSUME-FALSE:FBA71744BDCE72BC45B9A84C3AB97CE0D719
        andBool ( VV1_b_114b9705:Int <Int pow256
                ))))))))))
       [label(BASIC-BLOCK-3-TO-4)]
-    
+
            <kevm>
              <k>
                ( #checkCall 728815563385977040452943777879061427756277306518 0
@@ -941,10 +941,10 @@ module SUMMARY-ASSUMETEST.TEST-ASSUME-FALSE:FBA71744BDCE72BC45B9A84C3AB97CE0D719
        andBool ( VV1_b_114b9705:Int <Int pow256
                ))))))))))
        ensures ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))
       [label(BASIC-BLOCK-4-TO-5)]
-    
+
            <kevm>
              <k>
                ( #gas [ MSTORE , MSTORE 192 46308022326495007027972728677917914892729792999299745830475596687180801507328 ]
@@ -1158,10 +1158,10 @@ module SUMMARY-ASSUMETEST.TEST-ASSUME-FALSE:FBA71744BDCE72BC45B9A84C3AB97CE0D719
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-5-TO-6)]
-    
+
            <kevm>
              <k>
                ( #gasExec ( LONDON , JUMP 2621 )
@@ -1374,10 +1374,10 @@ module SUMMARY-ASSUMETEST.TEST-ASSUME-FALSE:FBA71744BDCE72BC45B9A84C3AB97CE0D719
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-6-TO-7)]
-    
+
            <kevm>
              <k>
                ( CALL 9223372036854765620 645326474426547203313410069153905908525362434349 0 388 100 388 0 => #checkCall 728815563385977040452943777879061427756277306518 0
@@ -1588,10 +1588,10 @@ module SUMMARY-ASSUMETEST.TEST-ASSUME-FALSE:FBA71744BDCE72BC45B9A84C3AB97CE0D719
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-7-TO-8)]
-    
+
            <kevm>
              <k>
                ( #checkCall 728815563385977040452943777879061427756277306518 0
@@ -1803,10 +1803,10 @@ module SUMMARY-ASSUMETEST.TEST-ASSUME-FALSE:FBA71744BDCE72BC45B9A84C3AB97CE0D719
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-8-TO-9)]
-    
+
            <kevm>
              <k>
                ( #end EVMC_SUCCESS => #halt )
@@ -2018,10 +2018,10 @@ module SUMMARY-ASSUMETEST.TEST-ASSUME-FALSE:FBA71744BDCE72BC45B9A84C3AB97CE0D719
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-9-TO-10)]
-    
+
            <kevm>
              <k>
                #halt
@@ -2233,7 +2233,7 @@ module SUMMARY-ASSUMETEST.TEST-ASSUME-FALSE:FBA71744BDCE72BC45B9A84C3AB97CE0D719
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
                ))))))))))))
       [label(BASIC-BLOCK-10-TO-11)]
 
@@ -2256,7 +2256,7 @@ Failing nodes:
     #And ( { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
     #And ( { true #Equals VV0_a_114b9705:Int <Int pow256 }
     #And ( { true #Equals VV1_b_114b9705:Int <Int pow256 }
-    #And { true #Equals ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ==Bool true } ) ) ) ) ) ) ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_SUCCESS , failed: #lookup ( ( 46308022326495007027972728677917914892729792999299745830475596687180801507328 |-> 1 ) , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
+    #And { true #Equals ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) } ) ) ) ) ) ) ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_SUCCESS , failed: #lookup ( ( 46308022326495007027972728677917914892729792999299745830475596687180801507328 |-> 1 ) , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
   Path condition:
     #Top
 
diff --git a/tests/foundry/golden/LoopsTest.sum_N(uint256).expected b/tests/foundry/golden/LoopsTest.sum_N(uint256).expected
index 40167d221a..6682159897 100644
--- a/tests/foundry/golden/LoopsTest.sum_N(uint256).expected
+++ b/tests/foundry/golden/LoopsTest.sum_N(uint256).expected
@@ -115,8 +115,8 @@
 
 
 module SUMMARY-LOOPSTEST.SUM-N:031A8A7FD8A89EA433A5C7307FD8E6EE86FED775C4188C1078F3DE94C1EE710D
-    
-    
+
+
            <kevm>
              <k>
                ( #execute
@@ -334,7 +334,7 @@ module SUMMARY-LOOPSTEST.SUM-N:031A8A7FD8A89EA433A5C7307FD8E6EE86FED775C4188C107
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
       [label(BASIC-BLOCK-1-TO-3)]
-    
+
            <kevm>
              <k>
                ( CALL 9223372036854772793 645326474426547203313410069153905908525362434349 0 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
@@ -541,7 +541,7 @@ module SUMMARY-LOOPSTEST.SUM-N:031A8A7FD8A89EA433A5C7307FD8E6EE86FED775C4188C107
        andBool ( VV0_n_114b9705:Int <Int pow256
                ))))))))
       [label(BASIC-BLOCK-3-TO-4)]
-    
+
            <kevm>
              <k>
                ( #checkCall 728815563385977040452943777879061427756277306518 0
@@ -751,9 +751,9 @@ module SUMMARY-LOOPSTEST.SUM-N:031A8A7FD8A89EA433A5C7307FD8E6EE86FED775C4188C107
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
                ))))))))
-       ensures VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       ensures VV0_n_114b9705:Int <=Int 51816696836262767
       [label(BASIC-BLOCK-4-TO-5)]
-    
+
            <kevm>
              <k>
                ( JUMPI 1569 bool2Word ( VV0_n_114b9705:Int ==Int 0 )
@@ -961,11 +961,11 @@ module SUMMARY-LOOPSTEST.SUM-N:031A8A7FD8A89EA433A5C7307FD8E6EE86FED775C4188C107
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
                ))))))))))
        ensures VV0_n_114b9705:Int ==K 0
       [label(BASIC-BLOCK-6-TO-8)]
-    
+
            <kevm>
              <k>
                ( JUMPI 1569 bool2Word ( VV0_n_114b9705:Int ==Int 0 )
@@ -1173,7 +1173,7 @@ module SUMMARY-LOOPSTEST.SUM-N:031A8A7FD8A89EA433A5C7307FD8E6EE86FED775C4188C107
        andBool ( VV0_n_114b9705:Int =/=Int 0
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
                ))))))))))
        ensures ( VV0_n_114b9705:Int =/=K 0
        andBool ( 0 <Int VV0_n_114b9705:Int
@@ -1203,7 +1203,7 @@ module SUMMARY-LOOPSTEST.SUM-N:031A8A7FD8A89EA433A5C7307FD8E6EE86FED775C4188C107
        andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
                ))))))))))))))))))))))))))
       [label(BASIC-BLOCK-7-TO-9)]
-    
+
            <kevm>
              <k>
                ( #end EVMC_SUCCESS => #halt )
@@ -1413,7 +1413,7 @@ module SUMMARY-LOOPSTEST.SUM-N:031A8A7FD8A89EA433A5C7307FD8E6EE86FED775C4188C107
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                )))))))
       [label(BASIC-BLOCK-8-TO-10)]
-    
+
            <kevm>
              <k>
                ( #end EVMC_SUCCESS => #halt )
@@ -1646,12 +1646,12 @@ module SUMMARY-LOOPSTEST.SUM-N:031A8A7FD8A89EA433A5C7307FD8E6EE86FED775C4188C107
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
        andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
        andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
                )))))))))))))))))))))))))))))))))))
       [label(BASIC-BLOCK-9-TO-11)]
-    
+
            <kevm>
              <k>
                #halt
@@ -1861,7 +1861,7 @@ module SUMMARY-LOOPSTEST.SUM-N:031A8A7FD8A89EA433A5C7307FD8E6EE86FED775C4188C107
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                )))))))
       [label(BASIC-BLOCK-10-TO-12)]
-    
+
            <kevm>
              <k>
                #halt
@@ -2094,7 +2094,7 @@ module SUMMARY-LOOPSTEST.SUM-N:031A8A7FD8A89EA433A5C7307FD8E6EE86FED775C4188C107
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
        andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
        andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
                )))))))))))))))))))))))))))))))))))