Skip to content

Fix JVM analysis aborts after rejected symbolic assumptions - #550

Merged
CaelmBleidd merged 2 commits into
mainfrom
caelmbleidd/jvm-assume-symbolic-pruning
Oct 16, 2026
Merged

CaelmBleidd merged 2 commits into
mainfrom
caelmbleidd/jvm-assume-symbolic-pruning

Conversation

@CaelmBleidd

Copy link
Copy Markdown
Member

Engine.assumeSymbolic could hide a rejected scope.assert behind Unit, then complete the call on a dead scope and abort the analysis. Build the guarded assumption as a pure expression and assert once, so rejection prunes its state while other states continue. Concrete and null references keep their existing behavior.

Validation: the public-path reproducer fails on main with the original StepScope exception; all four focused regression tests pass after the fix, including a guarded concrete alternative. Changed Kotlin files pass strict Detekt against a temporary baseline generated from the original main source; the three pre-existing findings and the repository baseline remain unchanged.

@CaelmBleidd
CaelmBleidd merged commit dd1ed53 into main Oct 16, 2026
6 checks passed
@CaelmBleidd
CaelmBleidd deleted the caelmbleidd/jvm-assume-symbolic-pruning branch October 16, 2026 13:06
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.

1 participant