Bring the Test-Comp conformance work into develop (follow-up to #55/#56) - #57

Merged

GuilhermeBn198 merged 15 commits into

feat/castle-juliet-baseline

Aug 22, 2026

Commits on Aug 16, 2026

docs: plan Test-Comp conformance and review the Crab-LLVM dependency

GuilhermeBn198
and
claude
committed
8606a7e
docs: plan the --add-invariants revival via Clam dev16

GuilhermeBn198
and
claude
committed
82e8161
docs(plans): fix the installed binary path and declare v5 comparability

GuilhermeBn198
and
claude
committed
bad55b8
fix(invariants): refuse --add-invariants instead of ignoring it

GuilhermeBn198
and
claude
committed
1a8c6a3
feat(invariants): bring --add-invariants back on Clam dev16

GuilhermeBn198
and
claude
committed
6f806fe
feat(test-comp): emit a Test-Comp test suite, and fix the three bugs that made it impossible

GuilhermeBn198
and
claude
committed
231ce71
chore: ignore the unit-test build tree

GuilhermeBn198
and
claude
committed
8a4de91
ci: gate on TestCov reproducing the emitted test suites

GuilhermeBn198
and
claude
committed
11934bb
docs(testcomp): record the falsifiability check, and what it exposed

GuilhermeBn198
and
claude
committed
ea10a2b
ci: fire on feat/** branches, for pushes and for stacked PRs

GuilhermeBn198
and
claude
committed
9da09d4
ci: cover feature branches via pull_request only, not also via push

GuilhermeBn198
and
claude
committed
d37521a
fix(testcomp): keep the KEEP_WORK notice off stdout

GuilhermeBn198
and
claude
committed
80383b5
docs: investigate finding K, and add a progress checklist

GuilhermeBn198
and
claude
committed
3be786c

Commits on Aug 17, 2026

fix(verdict): keep a violation that was found before the budget expired

GuilhermeBn198
and
claude
committed
c4ef3a3
Merge pull request #56 from hbgit/feat/testcomp-conformance
hbgit
authored
6eecbda