removing ==Bool from expected files

runtimeverification · Aug 24, 2023 · dd3b023 · dd3b023
1 parent b8fe221
commit dd3b023
Show file tree

Hide file tree

Showing 6 changed files with 102 additions and 102 deletions.
diff --git a/...ests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected b/...ests/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/...c/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/...c/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
@@ -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
                )))))))))))))))))))))))))))))))))))