Fixing proof hints tests

runtimeverification · Dec 13, 2024 · 7b3b12d · 7b3b12d
1 parent a9ab878
commit 7b3b12d
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 13 deletions.
diff --git 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
@@ -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