Skip to content

Commit 6b7b3f7

Browse files
Stevengreclaude
andcommitted
test(cse): add H2/H4 structure preservation assertions to test
Verify in test_cse_callee_proof: - H4: no NDBranch in reuse proof (0 ndbranches) - H2: splits match baseline (reuse_splits == baseline_splits) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 8173e28 commit 6b7b3f7

1 file changed

Lines changed: 7 additions & 0 deletions

File tree

kmir/src/tests/integration/test_integration.py

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -987,3 +987,10 @@ def test_cse_callee_proof(tmp_path: Path) -> None:
987987
prover.advance_proof(reuse_proof, max_iterations=1000)
988988

989989
assert reuse_proof.passed, f'CSE reuse proof should pass, status={reuse_proof.status}'
990+
991+
# Step 7: Verify structure preservation (H2, H4)
992+
r_kcfg = reuse_proof.kcfg
993+
assert len(list(r_kcfg.ndbranches())) == 0, 'H4: CSE must not produce NDBranch'
994+
b_splits = len(list(baseline.kcfg.splits()))
995+
r_splits = len(list(r_kcfg.splits()))
996+
assert b_splits == r_splits, f'H2: splits mismatch baseline={b_splits} reuse={r_splits}'

0 commit comments

Comments
 (0)