Description

This PR adds VC simplification for foldable expressions through VCImplication chains. When a refinement contains constant arithmetic, boolean expressions, conditionals, adjacent integer constants, or resolved enum literals, it folds the VC node while preserving its origin and the rest of the VC chain.

It also adds focused unit tests for both the VC folding alone and the VC simplification with both the substitution and folding.

Example

1 + 2 > 0

is simplified to

3 > 0

with origin 1 + 2 > 0

and then simplified to

true

with origin 3 > 0

Related Issue

None.

Type of change

• Bug fix
• New feature
• Documentation update
• Code refactoring

Checklist

• Added/updated tests
• mvn test passes locally
• Updated docs/README if behavior or API changed