Skip to content

Commit

Permalink
Updating prooftrace tests with new version and new size of function e…
Browse files Browse the repository at this point in the history
…vents
  • Loading branch information
Robertorosmaninho committed Aug 20, 2024
1 parent fe3b402 commit cc20aee
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
6 changes: 3 additions & 3 deletions pyk/src/tests/integration/kllvm/test_prooftrace.py
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ def test_proof_trace(self, hints: bytes, header: prooftrace.KoreHeader, definiti
def test_streaming_parser_iter(self, header: prooftrace.KoreHeader, hints_file: Path) -> None:
# read the hints file and get the iterator for the proof trace
it = prooftrace.LLVMRewriteTraceIterator.from_file(hints_file, header)
assert it.version == 11
assert it.version == 12

# Test that the __iter__ is working
list_of_events = list(it)
Expand Down Expand Up @@ -126,7 +126,7 @@ def test_streaming_parser_next(self, header: prooftrace.KoreHeader, hints_file:

# read the hints file and get the iterator for the proof trace
it = prooftrace.LLVMRewriteTraceIterator.from_file(hints_file, header)
assert it.version == 11
assert it.version == 12

# skip pre-trace events
while True:
Expand Down Expand Up @@ -810,7 +810,7 @@ def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeade
assert len(pt.pre_trace) == 11

# 404 post-initial-configuration events
assert len(pt.trace) == 404
assert len(pt.trace) == 419


class TestIMP5(ProofTraceTest):
Expand Down
2 changes: 1 addition & 1 deletion pyk/src/tests/integration/test_krun_proof_hints.py
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ class Test0Decrement(KRunTest, ProofTraceTest):
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\\dv{SortKConfigVar{}}("$PGM")),inj{SortNat{}, SortKItem{}}(Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()))))
"""

HINTS_OUTPUT = """version: 11
HINTS_OUTPUT = """version: 12
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
function: Lbl'UndsPipe'-'-GT-Unds'{} ()
arg: kore[\\dv{SortKConfigVar{}}("$PGM")]
Expand Down

0 comments on commit cc20aee

Please sign in to comment.