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.