Adding the assert to verify that we're producing the `LLVMPatternMa…

…tchingFailureEvent` correctly
runtimeverification · Sep 18, 2024 · 29781e3 · 29781e3
1 parent c4c6cb6
commit 29781e3
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py
@@ -808,9 +808,14 @@ def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeade
         # 12 initialization events
         assert len(pt.pre_trace) == 12
 
-        # 404 post-initial-configuration events
+        # 776 post-initial-configuration events
         assert len(pt.trace) == 776
 
+        # Assert that we have a pattern matching failure as the 135th event
+        assert pt.trace[135].is_step_event() and isinstance(
+            pt.trace[135].step_event, prooftrace.LLVMPatternMatchingFailureEvent
+        )
+
 
 class TestIMP5(ProofTraceTest):
     KOMPILE_DEFINITION = """