[SwayamInSync]

The smoke test gates publishing a release (cppverify-release.yml runs it on each unpacked archive) and runs after every CI build. It checked less than it seemed to (plan item S8):

• it printed --version without looking at it;
• it compiled the correct program with clang++ -fverify-contracts, but never the incorrect one, so a clang++ that skipped verification passed;
• it left its temporary directory behind;
• and the release workflow named an archive cpp-verify-X-llvm-PLATFORM when --version named no LLVM release, since nothing checked the version it parsed.

Now the smoke test checks:

• that --version starts with cpp-verify's version, names the LLVM release, and names the built-in Z3;
• that the incorrect program fails with its counterexample, in text and in a JSON record;
• that clang++ -fverify-contracts writes an object for the correct program, and for the incorrect one reports verification failed: twice and writes none;
• and it removes its directory on exit.

The release workflow stops when the LLVM version it parses is empty.

The checks hold for the formats on main and for those of #104 and #105: verification failed: twice, a counterexample x = with or without the old [ssa=x_0] [type=i32] tags, and a JSON model entry named x.

Checked

The script passes on a release build. It fails, at the check meant for each, when a wrapper breaks one property:

Wrapper	The script stops with
--version without its z3 line	error: --version names no built-in Z3
cpp-verify verifies everything	error: the incorrect program verified
the counterexample note removed	error: the incorrect program's counterexample is missing
JSON without model entries	error: the incorrect program's JSON record is missing
clang++ compiles the incorrect program	error: clang++ -fverify-contracts compiled the incorrect program
clang++ without -fverify-contracts	the correct program's compile error (set -e)

Lean in CI

Since about 04:00 UTC today, every Linux CI job, main's included, stops at "Report the versions": elan installs the pinned toolchain on first use, from releases.lean-lang.org, which refuses TLS connections ([35] SSL connect error, and the same from a machine outside GitHub), so no test runs. The job now installs elan without a toolchain, unpacks the pinned Lean from its GitHub release (leanprover/lean4, lean-4.35.0-linux.tar.zst) into the directory where elan keeps it (~/.elan/toolchains/leanprover--lean4---v4.35.0), and makes it the default. elan default downloads a toolchain it does not find, so a wrong directory fails that step, not a test.