Skip to content

fix(Core): complete bv128 literal support in FormatCore and Translate#1436

Open
kondylidou wants to merge 1 commit into
strata-org:mainfrom
kondylidou:fix/bv128-literal-roundtrip
Open

fix(Core): complete bv128 literal support in FormatCore and Translate#1436
kondylidou wants to merge 1 commit into
strata-org:mainfrom
kondylidou:fix/bv128-literal-roundtrip

Conversation

@kondylidou

Copy link
Copy Markdown
Contributor

FormatCore's bitvec catch-all arm discarded the actual constant value and emitted bv64(128) for any 128-bit literal — wrong type and wrong value. Translate had no bv128Lit case, causing Core→DDM translation to fail for programs with 128-bit literals.

Add explicit bv128 arms to both, mirroring the existing bv64 pattern.

Warning: This repository will shortly undergo a split into several separate repositories. If you're creating a PR that crosses the boundaries between these repositories, you may want to hold off until the split is complete or be prepared to rework your PR into multiple PRs once the split is complete.

The code that will be moved includes:

  • Strata/DDM/*
  • Strata/Languages/Boole/*
  • Strata/Languages/Python/* along with Tools/Python/*
  • Tools/BoogieToStrata

FormatCore's bitvec catch-all arm discarded the actual constant value
and emitted bv64(128) for any 128-bit literal — wrong type and wrong
value. Translate had no bv128Lit case, causing Core→DDM translation
to fail for programs with 128-bit literals.

Add explicit bv128 arms to both, mirroring the existing bv64 pattern.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@kondylidou
kondylidou requested a review from a team July 8, 2026 11:27
@shigoel shigoel added the CSLib PRs and issues marked with this label indicate contributions from/for the CSLib community. label Jul 8, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Core CSLib PRs and issues marked with this label indicate contributions from/for the CSLib community. Waiting-For-Review

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants