Skip to content

Preserve symbolic List frames in matcher residuals - #4162

Closed
malturki wants to merge 1 commit into
runtimeverification:masterfrom
malturki:fix/list-frame-matcher-4161
Closed

malturki wants to merge 1 commit into
runtimeverification:masterfrom
malturki:fix/list-frame-matcher-4161

Conversation

@malturki

Copy link
Copy Markdown
Contributor

Fixes #4161.

Build the unmatched List residual as remainingPrefix ++ subjectFrame instead of inserting the List frame as an element. Add regressions for empty and nonempty remaining prefixes.

Validation: both regressions fail before the fix; all 5,188 Kore tests pass. Fourmolu and HLint pass.

@jberthold jberthold left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, good find.

jberthold added a commit that referenced this pull request Sep 30, 2026
Branch adopted from PR #4162 

Fixes #4161.

Build the unmatched List residual as `remainingPrefix ++ subjectFrame`
instead of inserting the List frame as an element. Add regressions for
empty and nonempty remaining prefixes.

Validation: both regressions fail before the fix; all 5,188 Kore tests
pass. Fourmolu and HLint pass.

---------

Co-authored-by: Musab Alturki <42160792+malturki@users.noreply.github.com>
@ehildenb

Copy link
Copy Markdown
Member

Closed in favor of: #4163

@ehildenb ehildenb closed this Sep 30, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

List matcher treats a symbolic List frame as an element, allowing false proofs

3 participants