comment rule generation validation for faster check

runtimeverification · Jan 23, 2025 · 4cb105a · 4cb105a
1 parent 016c6b2
commit 4cb105a
Showing 1 changed file with 7 additions and 7 deletions.
diff --git a/kevm-pyk/src/tests/integration/test_summarize.py b/kevm-pyk/src/tests/integration/test_summarize.py
@@ -60,12 +60,12 @@ def test_summarize(opcode: str) -> None:
                 claims.append(successor.to_rule(f'{opcode}-SUMMARY', claim=True))
                 print(f'[{opcode}] Edge {successor.source.id} -> {successor.target.id} is terminal or covered')
 
-            # prove the correctness of the summary
-            for claim in claims:
-                print(f'[{opcode}] Proving claim {claim.att.get(Atts.LABEL)}')
-                assert summarizer.explore(
-                    APRProof.from_claim(summarizer.kevm.definition, claim, {}, summarizer.proof_dir)
-                )
-                print(f'[{opcode}] Claim {claim.att.get(Atts.LABEL)} proved')
+            # # prove the correctness of the summary
+            # for claim in claims:
+            #     print(f'[{opcode}] Proving claim {claim.att.get(Atts.LABEL)}')
+            #     assert summarizer.explore(
+            #         APRProof.from_claim(summarizer.kevm.definition, claim, {}, summarizer.proof_dir)
+            #     )
+            #     print(f'[{opcode}] Claim {claim.att.get(Atts.LABEL)} proved')
     else:
         pytest.skip(f'{opcode} ignored')