key
key copied to clipboard
Solving the FP completeness issues in #1723
Related Issue
This pull request answers to issue #1723.
Intended Change
Floats and doubles are currently incorrectly insufficiently handled when they appear in one expression.
Casts need to be added and casts need to be dealt with. ...
- [x] introducing casts where needed
- [ ] adding rules / SMT support for such casts.
Type of pull request
- [x] Bug fix (non-breaking change which fixes an issue)
- [x] Refactoring (behaviour should not change or only minimally change)
- [ ] New feature (non-breaking change which adds functionality)
- [ ] Breaking change (fix or feature that would cause existing functionality to change)
- [x] There are changes to the (Java) code
- [x] There are changes to the taclet rule base
- [ ] There are changes to the deployment/CI infrastructure (gradle, github, ...)
- [ ] Other:
Ensuring quality
- [x] I made sure that introduced/changed code has been well documented (javadoc).
- [x] I added new test case(s) for new functionality.
- [x] I have tested the feature as follows: small 2-liners
- [ ] I have checked that runtime performance has not deteriorated
Additional information and contact(s)
It's still W I P.
@samysweb
The contributions within this pull request will be licensed under GPL2-or-later wihtin KeY.