Skip to content

Conversation

@FliegendeWurst
Copy link
Member

Related Issue

This pull request resolves #3717.

Intended Change

Fix by always using the type for Seq, not the type of the containing class.

Plan

  • Add a simple test case for usage of \values

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)
  • There are changes to the (Java) code

Ensuring quality

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@codecov
Copy link

codecov bot commented Jan 14, 2026

Codecov Report

❌ Patch coverage is 0% with 3 lines in your changes missing coverage. Please review.
✅ Project coverage is 47.97%. Comparing base (2aa39bb) to head (75024b9).
⚠️ Report is 39 commits behind head on main.

Files with missing lines Patch % Lines
.../de/uka/ilkd/key/speclang/njml/JmlTermFactory.java 0.00% 2 Missing ⚠️
...java/de/uka/ilkd/key/speclang/njml/Translator.java 0.00% 1 Missing ⚠️
Additional details and impacted files
@@             Coverage Diff              @@
##               main    #3718      +/-   ##
============================================
- Coverage     47.99%   47.97%   -0.02%     
- Complexity    16046    16052       +6     
============================================
  Files          1683     1683              
  Lines         96044    96094      +50     
  Branches      15387    15394       +7     
============================================
+ Hits          46093    46100       +7     
- Misses        44681    44722      +41     
- Partials       5270     5272       +2     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Enhanced-for loop example with \values not loadable

1 participant