Skip to content

fix: handle non-internalized terms in semiring reifier#12474

Merged
leodemoura merged 1 commit intomasterfrom
lean-12428
Feb 14, 2026
Merged

fix: handle non-internalized terms in semiring reifier#12474
leodemoura merged 1 commit intomasterfrom
lean-12428

Conversation

@leodemoura
Copy link
Member

This PR fixes a panic in grind where sreifyCore? could encounter power subterms not yet internalized in the E-graph during nested propagation. The ring reifier (reifyCore?) already had a defensive alreadyInternalized check before creating variables, but the semiring reifier (sreifyCore?) was missing this guard. When propagatePower decomposed a ^ (b₁ + b₂) into a^b₁ * a^b₂ and the resulting terms triggered further propagation, the semiring reifier could be called on subterms not yet in the E-graph, causing markTerm to fail.

Closes #12428

🤖 Generated with Claude Code

This PR fixes a panic in `grind` where `sreifyCore?` could encounter
power subterms not yet internalized in the E-graph during nested
propagation. The ring reifier (`reifyCore?`) already had a defensive
`alreadyInternalized` check before creating variables, but the semiring
reifier (`sreifyCore?`) was missing this guard. When `propagatePower`
decomposed `a ^ (b₁ + b₂)` into `a^b₁ * a^b₂` and the resulting terms
triggered further propagation, the semiring reifier could be called on
subterms not yet in the E-graph, causing `markTerm` to fail.

Closes #12428

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@leodemoura leodemoura added the changelog-tactics User facing tactics label Feb 14, 2026
@leodemoura leodemoura enabled auto-merge February 14, 2026 00:58
@leodemoura leodemoura added this pull request to the merge queue Feb 14, 2026
Merged via the queue into master with commit 187a8c1 Feb 14, 2026
21 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-tactics User facing tactics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

internal grind error, term has not been internalized

1 participant