Function add_junit_test_cases 

fn add_junit_test_cases(
    test_suite: &mut TestSuite,
    test_name: &str,
    test_result: &TestResult,
    verbosity: u8,
)

Adds JUnit test cases for a test result.

Invariant campaigns are expanded into per-predicate and per-handler cases so CI can report contract-level execution without losing failure attribution.