Skip to content

Commit

Permalink
fixes for pyk tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@theo25
theo25 committed Sep 25, 2024
1 parent de613df commit bd02511
Show file tree
Hide file tree
Showing 2 changed files with 25 additions and 31 deletions.
46 changes: 23 additions & 23 deletions pyk/src/tests/integration/kllvm/test_prooftrace.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) == 14
assert len(list_of_events) == 13

# Test the type of the events
for event in list_of_events:
Expand Down Expand Up @@ -189,8 +189,8 @@ def test_parse_proof_hint_single_rewrite(
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 2 post-initial-configuration events
assert len(pt.trace) == 2
Expand Down Expand Up @@ -259,8 +259,8 @@ def test_parse_proof_hint_reverse_no_ints(
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 9 post-initial-configuration events
assert len(pt.trace) == 9
Expand Down Expand Up @@ -384,8 +384,8 @@ def test_parse_proof_hint_non_rec_function(
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 6 post-initial-configuration events
assert len(pt.trace) == 6
Expand Down Expand Up @@ -467,8 +467,8 @@ def test_parse_proof_hint_dv(self, hints: bytes, header: prooftrace.KoreHeader,
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 3 post-initial-configuration events
assert len(pt.trace) == 3
Expand Down Expand Up @@ -548,8 +548,8 @@ def test_parse_concurrent_counters(self, hints: bytes, header: prooftrace.KoreHe
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 37 post-initial-configuration events
assert len(pt.trace) == 37
Expand Down Expand Up @@ -708,8 +708,8 @@ def test_parse_proof_hint_0_decrement(self, hints: bytes, header: prooftrace.Kor
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 1 post-initial-configuration event
assert len(pt.trace) == 1
Expand Down Expand Up @@ -737,8 +737,8 @@ def test_parse_proof_hint_1_decrement(self, hints: bytes, header: prooftrace.Kor
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 2 post-initial-configuration events
assert len(pt.trace) == 2
Expand Down Expand Up @@ -766,8 +766,8 @@ def test_parse_proof_hint_2_decrement(self, hints: bytes, header: prooftrace.Kor
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 3 post-initial-configuration events
assert len(pt.trace) == 3
Expand Down Expand Up @@ -805,8 +805,8 @@ def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeade
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 776 post-initial-configuration events
assert len(pt.trace) == 776
Expand Down Expand Up @@ -914,8 +914,8 @@ def test_parse_proof_hint_imp5(self, hints: bytes, header: prooftrace.KoreHeader
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 16 initialization events
assert len(pt.pre_trace) == 16
# 14 initialization events
assert len(pt.pre_trace) == 14

# 2 post-initial-configuration events
assert len(pt.trace) == 2
Expand Down Expand Up @@ -953,8 +953,8 @@ def test_parse_proof_hint_builtin_hook_events(
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 4 post-initial-configuration events
assert len(pt.trace) == 4
Expand Down
10 changes: 2 additions & 8 deletions pyk/src/tests/integration/test_krun_proof_hints.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,12 +31,6 @@ class Test0Decrement(KRunTest, ProofTraceTest):
"""

HINTS_OUTPUT = """version: 13
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
arg: kore[\\dv{SortKConfigVar{}}("$PGM")]
arg: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
hook: MAP.unit Lbl'Stop'Map{} ()
hook result: kore[Lbl'Stop'Map{}()]
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
arg: kore[Lbl'Stop'Map{}()]
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
Expand Down Expand Up @@ -73,8 +67,8 @@ def test_parse_proof_hint_0_decrement(self, krun: KRun, header: prooftrace.KoreH
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 1 post-initial-configuration event
assert len(pt.trace) == 1
Expand Down

0 comments on commit bd02511

Please sign in to comment.