Fix namespace collision and SMACK assert encoding in BoogieToStrata#1149

Merged

PROgram52bc merged 21 commits into

mainfrom

May 20, 2026

Commits on May 8, 2026

Fix namespace collision and SMACK assert encoding in BoogieToStrata

David Deng
and
claude
committed
Refactor name collision fix: use global name set with entity-type prefix

David Deng
and
claude
committed
Remove Prune option to fix CI integration test failures

David Deng
and
claude
committed
Fix #1152
David Deng
committed

Commits on May 11, 2026

Fix rename consistency, tighten SMACK pattern, and add regression tests

David Deng
and
claude
committed
fix: eliminate duplicate spec block for SMACK assert_ procedures

David Deng
and
claude
committed
fix: replace silent IdentifierExpr.Decl null fallback with exception

David Deng
and
claude
committed
test: add regression test for InferModifies=true on Boogie without modifies clauses

David Deng
and
claude
committed
refactor: extract ClaimOrRename into static method and document InferModifies

David Deng
and
claude
committed

Commits on May 18, 2026

fix: wrap synthetic Requires mutation in try/finally
David Deng
committed
test: add .expect for OldExprRenameCollision
David Deng
committed
test: add .expect for InferModifiesGlobal
David Deng
committed

Commits on May 19, 2026

refactor: thread smack parameter into StrataGenerator
David Deng
committed
feat: gate assert_.<type> requires injection on smack flag
David Deng
committed
feat: add --smack CLI flag to BoogieToStrata
David Deng
committed
test: make integration runner marker-aware for --smack
David Deng
committed
test: add {:smack} marker and remove stale comment in SmackAssert.bpl
David Deng
committed
test: extend SmackAssertDuplicateSpec for requires-already-present case
David Deng
committed
test: add {:smack} marker to AssertPrefixFalsePositive.bpl
David Deng
committed
test: add {:smack} marker to InferModifiesGlobal.bpl
David Deng
committed
test: pin down --smack off-by-default behavior
David Deng
committed