Solving the FP completeness issues in #1723 #3023

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.