smtgcc mid-year update
Project / Subsystem
gcc / gcc
Date
2026-07-01
Proposer
Krister Walfridsson <krister.walfridsson@gmail.com>
Source type
public_inbox
Consensus
Proposed
Sentiment
—/10
Technical tradeoffs
- • Adopting Bitwuzla improved performance but requires integrating and maintaining support for a new SMT solver.
- • Expanding backend support increases complexity but broadens the tool's applicability.
- • Testing with `-fno-strict-aliasing` and `-fno-section-anchors` limits the scope of validation but allows for broader initial testing (e.g., on the Linux kernel).
All attributes
- project
- gcc
- subsystem
- gcc
- patch_id
- —
- discussion_id
- Pine.NEB.4.64.2607011339410.4763@gateway.kwa
- source_type
- public_inbox
- title
- smtgcc mid-year update
- headline
- smtgcc mid-year update
- tldr
- Update on smtgcc, a translation validator for GCC, highlighting performance improvements, real-world testing, backend support, and ongoing GCC test suite runs.
- proposer
- Krister Walfridsson <krister.walfridsson@gmail.com>
- consensus
- Proposed
- outcome
- proposed
- sentiment_score
- —
- technical_tradeoffs
-
- • Adopting Bitwuzla improved performance but requires integrating and maintaining support for a new SMT solver.
- • Expanding backend support increases complexity but broadens the tool's applicability.
- • Testing with `-fno-strict-aliasing` and `-fno-section-anchors` limits the scope of validation but allows for broader initial testing (e.g., on the Linux kernel).
- series_id
- —
- series_role
- standalone
- series_parts
- []
- tags
-
- • gcc
- • smtgcc
- • testing
- • compiler-validation
- • performance
- bugzilla_url
- —
- date
- 2026-07-01T00:00:00.000Z
smtgcc mid-year update
Krister Walfridsson provides a mid-year update on smtgcc, his translation validator for GCC. Significant performance improvements have been achieved, reducing timeouts by 90% through the addition of the Bitwuzla SMT solver and better canonicalization. Smtgcc is now capable of finding issues in real-world software, with two bugs found during Linux kernel compilation. The smtgcc-tv-backend now supports AArch64, RISC-V, BPF, SH, and m68k targets. Weekly runs of the GCC test suite continue, with testing focused on specific optimization levels and architectures, and with known limitations regarding type-based aliasing and section anchors.