soundness: IC3 reports OK on a spec with a real violation (DieHard)

[danwt]

The default symbolic path (smart cascade → IC3/Spacer) reports a false proof: it returns OK on a spec where a real invariant violation exists. BFS, BMC, and TLC all correctly find the violation.

Repro (specl/benchmarks/comparison/DieHard.tla)

specl check DieHard.tla            # Result: OK   (method smart(IC3))  -- WRONG
specl check DieHard.tla --bfs      # INVARIANT VIOLATION (NotSolved, depth 6) -- correct
specl check DieHard.tla --bmc      # INVARIANT VIOLATION (depth 6)            -- correct
java -cp tla2tools.jar tlc2.TLC -config DieHard.cfg DieHard.tla  # NotSolved is violated -- correct

DieHard reaches big=4 in 6 steps (via the pour actions), so NotSolved (big != 4) is genuinely violated.

Characterization

• The translated model is faithful: BFS on it finds the depth-6 counterexample.
• --ic3 logs "IC3 found violation, reconstructing trace via BMC" then "BMC complete, no violations found depth=1" — the reconstruction loop in crates/specl-symbolic/src/ic3.rs (depths [1,2,4,8,16,32]) does not reproduce it, and the smart cascade returns OK (Spacer query returned L_FALSE, a false 'verified').
• The actions involved use nested if-then-else effects (SmallToBig/BigToSmall), a likely culprit for the CHC encoding.

This is a false-proof (unsound OK), the most serious checker bug class. Found by the new cross-tool soundness oracle (#94, specl/tools/soundness/oracle.sh). Until fixed, DieHard is in the oracle's known-issues allowlist.

[danwt]

Why the existing private soundness harness missed this: its specl-vs-TLC comparison (run_e2e_compare.py / run_minispec_diff.py) forces --bfs --no-auto for every specl invocation, so the symbolic backend (BMC/IC3) is never compared against TLC. DieHard is already an e2e case, but it's checked with --bfs (correct) and agrees with TLC. The fix surface is two-fold: (1) this IC3 false-proof, and (2) add symbolic profiles to the cross-tool harness so the symbolic path is covered.