Fix: Resolve reveal statement crashes in match cases

[fabiomadge]

Problem

Reveal statements inside match cases were causing Boogie assertion failures, making the following code crash:

datatype Color = Red | Blue
method Test(color: Color) {
  match color
  case Red => 
    assert L: true; 
    reveal L;  // This would crash
  case Blue =>
}

Error: Process terminated. Assertion failed. in Boogie library

Root Cause

The issue was in the cloning process during match case flattening:

• AssertStmt and HideRevealStmt created separate AssertLabel objects during cloning
• The E field was filled on the AssertStmt's AssertLabel during Boogie generation
• The HideRevealStmt accessed a different cloned AssertLabel object with a null E field
• This caused the Boogie assertion failure when trying to use the unfilled expression

Solution

Fixed the cloning mechanism to ensure object identity preservation:

1. Added assertLabelClones dictionary to Cloner class using the standard pattern
2. Implemented CloneAssertLabel() method using GetOrCreate() like other clone methods
3. Updated AssertLabel.Clone() to use the shared cloning mechanism
4. Modified both AssertStmt and HideRevealStmt to use the shared cloning

This ensures that both statements reference the same cloned AssertLabel objects, so when the E field is filled during Boogie generation, the reveal statement can access it correctly.

Testing

• ✅ Added regression test git-issue-6268.dfy
• ✅ Verified fix resolves the crash
• ✅ Confirmed no regressions in existing functionality
• ✅ Follows established codebase patterns

Technical Details

The fix uses the same GetOrCreate() pattern used by other clone dictionaries in the Cloner class:

• Dictionary<AssertLabel, AssertLabel> assertLabelClones
• Ensures same original AssertLabel → same cloned AssertLabel
• Maintains object relationships needed for Boogie generation

Fixes #6268

[fabiomadge]

✅ News Entry Corrected

Fixed News Entry Issues:

1. ✅ Correct Naming: Changed from (issue number) to (PR number) as required
2. ✅ User-Focused Content: Rewrote for Dafny users rather than developers:
   • Before: Technical details about "cloning of AssertLabel objects during match case flattening"
   • After: User-visible behavior: "Reveal statements now work correctly inside match case bodies"

Content:

Reveal statements now work correctly inside match case bodies. Previously, using reveal statements within match cases would cause verification failures.

Now properly follows the contribution guidelines for release notes.