Alias expansion is used when checking a refinement, but the current VC simplification history does not record it. The earlier alias derivation feature from #160 and #184 was removed during the migration to VC simplification in #261.
For example, E_A2_04_CsvChunker reports Expected: Positive(buffered), Found: Nat(buffered), and counterexample buffered == 0. Here Nat(x) means x >= 0 and Positive(x) means x > 0, but the diagnostic contains no step that reveals those definitions.
Preserve the alias expansions used in a failed check as structured diagnostic data for both the found and expected refinements. A client should be able to show the substituted definitions and navigate back to the alias names. Add a regression test for this example or an equivalent mismatch.
Alias expansion is used when checking a refinement, but the current VC simplification history does not record it. The earlier alias derivation feature from #160 and #184 was removed during the migration to VC simplification in #261.
For example,
E_A2_04_CsvChunkerreportsExpected: Positive(buffered),Found: Nat(buffered), and counterexamplebuffered == 0. HereNat(x)meansx >= 0andPositive(x)meansx > 0, but the diagnostic contains no step that reveals those definitions.Preserve the alias expansions used in a failed check as structured diagnostic data for both the found and expected refinements. A client should be able to show the substituted definitions and navigate back to the alias names. Add a regression test for this example or an equivalent mismatch.