E6024
E6024 — A proof obligation could not be discharged because no SMT solver was available. Fails the compilation by default: an undischarged obligation is not a proved one, and treating the two alike is what let a missing z3 certify every seam in silence (Vx#374). Set VX_ALLOW_UNVERIFIED=1 to downgrade this to W1031 and compile anyway.
No example yet
No fixture in the test suite asserts this code, so there is no program here that is known to trigger it. That is a gap in our coverage rather than a statement about the code.
Contributing one is a good first change — add a fixture under tests/ with a CHECK line naming E6024, and this page picks it up.
Related
Topologies and memoryThe chapter covering the rule this code enforces.
All diagnosticsEvery code the compiler can emit, grouped by stage.
E6023An
impl transfer lowering whose declared tile shape is not the shape the transfer at hand actually moves. A lowering is selected by edge, so nothing else relates the two, and the raw:: primitives take their extents from the declaration: a smaller declaration copies part of the tile and leaves the rest uninitialised, a larger one stores past the end (observed as a SIGSEGV).
E6025A placement naming a location the machine does not have: a memory space no declared topology holds, written either as the space or as the device that would hold it. The derivation between the two spellings has a like-named fallback, so an undeclared name resolves to a space that exists only in the placement that mentions it.