Fix overflow checking

[WolframPfeifer]

The purpose of this PR is to repair the overflow checking of KeY and thus fix #3352.

TODO:

• [x] fix creation of branches for overflow checking
• [x] fix the actual proof obligation of the overflow check (should use inInt(...), inRangeInt(...), taclets in inRules(Un)CheckedSemantics.key)
• [x] throw an error if a choice used in a taclet does not exist
• [ ] activate the taclet option corresponding to the code_safe_math/code_java_math annotation
• [ ] create a user-level documentation (based on https://github.com/KeYProject/key/wiki/Spec-math-modes, but updated)
• [ ] create test cases (certain POs that are only provable when the "correct" semantics are used)