KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

Hackeython smt mod #3418

Closed BookWood7th closed 5 months ago

BookWood7th commented 5 months ago

Intended Change

SMT-Translation translates mod as an uninterpreted symbol. As div is translated as is, and SMT has an axiom stating a = a div b * b + a mod b. mod in SMT will be the same as in KeY.

Type of pull request

Ensuring quality

Additional information and contact(s)

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

codecov[bot] commented 5 months ago

Codecov Report

All modified and coverable lines are covered by tests :white_check_mark:

Project coverage is 37.77%. Comparing base (1fb0c10) to head (d15f5d3). Report is 13 commits behind head on main.

Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #3418 +/- ## ============================================ - Coverage 37.77% 37.77% -0.01% Complexity 17031 17031 ============================================ Files 2076 2076 Lines 126950 126951 +1 Branches 21381 21381 ============================================ Hits 47952 47952 Misses 73092 73092 - Partials 5906 5907 +1 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.