From 937c70cba90136d87eec090ba7d75901a5c9c5ef Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 17 Sep 2024 12:02:25 -0600 Subject: [PATCH] Correct how pyk loads seqstrict attribute (#4641) @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. --- pyk/regression-new/seqstrict-predicate/1.test.out | 11 ++++++++--- pyk/regression-new/skipped | 1 - pyk/src/pyk/kast/att.py | 2 +- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/pyk/regression-new/seqstrict-predicate/1.test.out b/pyk/regression-new/seqstrict-predicate/1.test.out index 1b239a340ff..772dfcc1211 100644 --- a/pyk/regression-new/seqstrict-predicate/1.test.out +++ b/pyk/regression-new/seqstrict-predicate/1.test.out @@ -1,3 +1,8 @@ - - 10 ~> .K - + + + 10 ~> .K + + + 0 + + diff --git a/pyk/regression-new/skipped b/pyk/regression-new/skipped index ea518c64d5b..f70534d2953 100644 --- a/pyk/regression-new/skipped +++ b/pyk/regression-new/skipped @@ -103,7 +103,6 @@ rand rangemap-tests-llvm rat search-bound -seqstrict-predicate set-symbolic-tests set_unification spec-rule-application diff --git a/pyk/src/pyk/kast/att.py b/pyk/src/pyk/kast/att.py index 0312e5c436a..820eb97968f 100644 --- a/pyk/src/pyk/kast/att.py +++ b/pyk/src/pyk/kast/att.py @@ -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)