`Imperative.Cmd.cover` translator emits `ASSERT(b)` instead of `ASSERT(¬b)`, inverting cover-claim outcomes

[PROgram52bc]

Headlines

• Status: present on origin/main (HEAD: 4c669052eede6ab851606d8169e279d739bcd641)
• Severity: critical (soundness)
• Component: Strata.DL.Imperative.ToCProverGOTO (Imperative → CProverGOTO translator)
• File / lines: Strata/DL/Imperative/ToCProverGOTO.lean:179-190

What's wrong

.cover label b should translate to ASSERT(¬b) so that a CBMC counterexample (a path where b holds) witnesses reachability of the cover claim. The translator wires the guard as expr (line 186), emitting ASSERT(b) and inverting every cover verdict.

Source	Should emit	Actually emits	CBMC verdict	Expected
cover "y" true	ASSERT(¬true)	ASSERT(true)	uncovered	covered
cover "y" false	ASSERT(¬false)	ASSERT(false)	covered	uncovered

CBMC's own coverage instrumenter cover_cover_instrumentert::instrument is the authoritative reference: *i_it = make_assertion(not_exprt(c), i_it->source_location()); (src/goto-instrument/cover_instrument_other.cpp lines 50–73).

Impact

Every cover-claim verdict from the Strata→CBMC pipeline is inverted: claims that should report "covered" report "uncovered" and vice versa. Any coverage or reachability argument built on this output is invalid.

Fix

Wrap the guard in Expr.not (already used for the analogous if/loop guards at lines 305 and 332 of the same file):

guard := Expr.not expr   -- was: guard := expr

Plan to test

• Positive: cover "y" true reported reachable (CBMC finds a counterexample to ASSERT(¬true)).
• Negative: cover "y" (x ∧ ¬x) reported unreachable.
• Round-trip: hand-written __CPROVER_cover(b) and Strata's translation of cover "y" b produce identical GOTO assert guards.