Skip to content

Commit

Permalink
Correct how pyk loads seqstrict attribute (#4641)
Browse files Browse the repository at this point in the history
@ACassimiro discovered a bug where we aren't allowing arguments on the
`seqstrict` attribute in pyk.

This PR addresses this, and enables a previously failing test in
`regression-new` that was due to this bug.
  • Loading branch information
ehildenb authored Sep 17, 2024
1 parent 861cda4 commit 937c70c
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 5 deletions.
11 changes: 8 additions & 3 deletions pyk/regression-new/seqstrict-predicate/1.test.out
Original file line number Diff line number Diff line change
@@ -1,3 +1,8 @@
<k>
10 ~> .K
</k>
<generatedTop>
<k>
10 ~> .K
</k>
<generatedCounter>
0
</generatedCounter>
</generatedTop>
1 change: 0 additions & 1 deletion pyk/regression-new/skipped
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,6 @@ rand
rangemap-tests-llvm
rat
search-bound
seqstrict-predicate
set-symbolic-tests
set_unification
spec-rule-application
Expand Down
2 changes: 1 addition & 1 deletion pyk/src/pyk/kast/att.py
Original file line number Diff line number Diff line change
Expand Up @@ -336,7 +336,7 @@ class Atts:
PROJECTION: Final = AttKey('projection', type=_NONE)
RIGHT: Final = AttKey('right', type=_ANY) # RIGHT and RIGHT_INTERNAL on the Frontend
SIMPLIFICATION: Final = AttKey('simplification', type=_ANY)
SEQSTRICT: Final = AttKey('seqstrict', type=_NONE)
SEQSTRICT: Final = AttKey('seqstrict', type=_ANY)
SORT: Final = AttKey('org.kframework.kore.Sort', type=_ANY)
SOURCE: Final = AttKey('org.kframework.attributes.Source', type=_PATH)
STRICT: Final = AttKey('strict', type=_ANY)
Expand Down

0 comments on commit 937c70c

Please sign in to comment.