From 7b3b12dd3f7e6002f145f6224d6c23d24ef0c5ca Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Fri, 13 Dec 2024 16:22:53 -0300 Subject: [PATCH] Fixing proof hints tests --- .../integration/kllvm/test_prooftrace.py | 24 +++++++++---------- .../integration/test_krun_proof_hints.py | 2 +- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py index 8ef5cb9495..5eb8494729 100644 --- a/pyk/src/tests/integration/kllvm/test_prooftrace.py +++ b/pyk/src/tests/integration/kllvm/test_prooftrace.py @@ -103,7 +103,7 @@ def test_streaming_parser_iter(self, header: prooftrace.KoreHeader, hints_file: list_of_events = list(it) # Test length of the list - assert len(list_of_events) == 13 + assert len(list_of_events) == 17 # Test the type of the events for event in list_of_events: @@ -190,7 +190,7 @@ def test_parse_proof_hint_single_rewrite( assert pt is not None # 10 initialization events - assert len(pt.pre_trace) == 10 + assert len(pt.pre_trace) == 14 # 2 post-initial-configuration events assert len(pt.trace) == 2 @@ -260,7 +260,7 @@ def test_parse_proof_hint_reverse_no_ints( assert pt is not None # 10 initialization events - assert len(pt.pre_trace) == 10 + assert len(pt.pre_trace) == 14 # 9 post-initial-configuration events assert len(pt.trace) == 9 @@ -385,7 +385,7 @@ def test_parse_proof_hint_non_rec_function( assert pt is not None # 10 initialization events - assert len(pt.pre_trace) == 10 + assert len(pt.pre_trace) == 14 # 6 post-initial-configuration events assert len(pt.trace) == 6 @@ -468,7 +468,7 @@ def test_parse_proof_hint_dv(self, hints: bytes, header: prooftrace.KoreHeader, assert pt is not None # 10 initialization events - assert len(pt.pre_trace) == 10 + assert len(pt.pre_trace) == 14 # 3 post-initial-configuration events assert len(pt.trace) == 3 @@ -549,7 +549,7 @@ def test_parse_concurrent_counters(self, hints: bytes, header: prooftrace.KoreHe assert pt is not None # 10 initialization events - assert len(pt.pre_trace) == 10 + assert len(pt.pre_trace) == 14 # 37 post-initial-configuration events assert len(pt.trace) == 37 @@ -709,7 +709,7 @@ def test_parse_proof_hint_0_decrement(self, hints: bytes, header: prooftrace.Kor assert pt is not None # 10 initialization events - assert len(pt.pre_trace) == 10 + assert len(pt.pre_trace) == 14 # 1 post-initial-configuration event assert len(pt.trace) == 1 @@ -738,7 +738,7 @@ def test_parse_proof_hint_1_decrement(self, hints: bytes, header: prooftrace.Kor assert pt is not None # 10 initialization events - assert len(pt.pre_trace) == 10 + assert len(pt.pre_trace) == 14 # 2 post-initial-configuration events assert len(pt.trace) == 2 @@ -767,7 +767,7 @@ def test_parse_proof_hint_2_decrement(self, hints: bytes, header: prooftrace.Kor assert pt is not None # 10 initialization events - assert len(pt.pre_trace) == 10 + assert len(pt.pre_trace) == 14 # 3 post-initial-configuration events assert len(pt.trace) == 3 @@ -806,7 +806,7 @@ def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeade assert pt is not None # 10 initialization events - assert len(pt.pre_trace) == 10 + assert len(pt.pre_trace) == 14 # 776 post-initial-configuration events assert len(pt.trace) == 776 @@ -915,7 +915,7 @@ def test_parse_proof_hint_imp5(self, hints: bytes, header: prooftrace.KoreHeader assert pt is not None # 14 initialization events - assert len(pt.pre_trace) == 14 + assert len(pt.pre_trace) == 20 # 2 post-initial-configuration events assert len(pt.trace) == 2 @@ -954,7 +954,7 @@ def test_parse_proof_hint_builtin_hook_events( assert pt is not None # 10 initialization events - assert len(pt.pre_trace) == 10 + assert len(pt.pre_trace) == 14 # 4 post-initial-configuration events assert len(pt.trace) == 4 diff --git a/pyk/src/tests/integration/test_krun_proof_hints.py b/pyk/src/tests/integration/test_krun_proof_hints.py index 008f6fd64f..5052b1e5bc 100644 --- a/pyk/src/tests/integration/test_krun_proof_hints.py +++ b/pyk/src/tests/integration/test_krun_proof_hints.py @@ -68,7 +68,7 @@ def test_parse_proof_hint_0_decrement(self, krun: KRun, header: prooftrace.KoreH assert pt is not None # 10 initialization events - assert len(pt.pre_trace) == 10 + assert len(pt.pre_trace) == 14 # 1 post-initial-configuration event assert len(pt.trace) == 1