Skip to content

Add preserves-definedness to attributes recognized by pyk #4784

Open
@palinatolmach

Description

@palinatolmach

Related: runtimeverification/kontrol#977
Follow up to #4681.

We should add support for the preserves-definedness attribute, in addition to smt-lemma , symbolic, and concrete added previously in https://github.com/runtimeverification/k/pull/4681/files, since it's commonly used in Kontrol lemmas.

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions