W1031
W1031 — A proof obligation could not be discharged because no SMT solver was available, so the property is **unverified** rather than proved. Distinct from W1027, which means the solver ran and found a violation. Emitted only under VX_ALLOW_UNVERIFIED; without it a missing solver is an error, because silence used to be indistinguishable from success (Vx#374).
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 W1031, and this page picks it up.
Related
A tour of VxThe chapter covering the rule this code enforces.
All diagnosticsEvery code the compiler can emit, grouped by stage.
W1030A topology's device index is not a compile-time constant (
GPU[i] for a runtime i), so it cannot be resolved to a device instance and falls back to index 0. Every such spawn therefore targets the same device. Vx models one representative device per declared kind (#284), so a fleet program should index with constants or const generics.
W1033The loop of a spawn region runs on one thread although each pass writes only memory of its own, so its passes could run at the same time. The warning points at what stops it: a call the compiler cannot show writes nothing, inline MLIR, a read of a row another pass writes, bounds not known when compiling, and the like. A region that calls barrier() asks for blocks and threads, so it is warned about whenever it runs on one thread, with the first thing that stopped the split: two threads that may write the same element, a break out of a loop that holds a barrier(), a write to block-shared memory with no barrier() after it, and the like.