Bug in rule application for floating point comparsion

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

Description

When trying to apply the lesser-or-equal than distinction rule to a floating point comparison on the master branch, the rule is not applied and an exception is thrown that is only visible in the terminal log.

Reproducible

always

Steps to reproduce

1. Open KeY
2. Load the following program:

class Bug {

    private float rPos;

    /*@ normal_behavior 
     @ requires (0.0 <= rPos & rPos <= 100.0);
     @ ensures (rPos >= 25.0);
     @ assignable rPos;
     */
    public void runController(){
        if (this.rPos <= 51.0) {
            this.rPos = 100.0;
        } else {
            this.rPos -= 1.0;
        }
    }
}

3. Run auto mode; this should result in the Bug-incomplete.proof.
4. Click on x=x_1<=51.0; and choose lesser-or-equal than distinction
5. The rule will not be applied, there will be no UI error message, you will however find an error message in the terminal

Steps to reproduce

This depends a little bit on the current state of floating points in KeY, I think there's two options:

• Do error handling and show a UI visible error saying that this operation is currently unsupported
• Apply a distinction rule for floating points

Additional information

Terminal log of error:

Exception in thread "AWT-EventQueue-0" de.uka.ilkd.key.logic.TermCreationException: Building a term failed. Normally there is an arity mismatch or one of the subterms' sorts is not compatible (e.g. like the '2' in "true & 2")
The top level operator was leq(Sort: Formula); its expected arg sorts were:
1.) sort: int, sort hash: 1944308833
2.) sort: int, sort hash: 1944308833

The subterms were:
1.) x_1<<origin(<none> (implicit)) ([ensures @ file Bug.java @ line 8, ensures (implicit), assignable (implicit)])>>(sort: float, sort hash: 1126995741)
2.) DFP(0(2(1(1(2(6(5(1(2(9(2(4(4(7(3(2(3(6(4(#))))))))))))))))))))(sort: double, sort hash: 839856028)

	at de.uka.ilkd.key.logic.op.AbstractSortedOperator.additionalValidTopLevel(AbstractSortedOperator.java:120)
	at de.uka.ilkd.key.logic.op.AbstractOperator.validTopLevelException(AbstractOperator.java:104)
	at de.uka.ilkd.key.logic.op.AbstractSortedOperator.validTopLevelException(AbstractSortedOperator.java:16)
	at de.uka.ilkd.key.logic.TermImpl.checked(TermImpl.java:137)
	at de.uka.ilkd.key.logic.TermFactory.doCreateTerm(TermFactory.java:146)
	at de.uka.ilkd.key.logic.TermFactory.createTerm(TermFactory.java:69)
	at de.uka.ilkd.key.logic.TermFactory.createTerm(TermFactory.java:98)
	at de.uka.ilkd.key.rule.SyntacticalReplaceVisitor.visit(SyntacticalReplaceVisitor.java:352)
	at de.uka.ilkd.key.logic.TermImpl.execPostOrder(TermImpl.java:261)
	at de.uka.ilkd.key.logic.TermImpl.execPostOrder(TermImpl.java:258)
	at de.uka.ilkd.key.rule.executor.javadl.TacletExecutor.syntacticalReplace(TacletExecutor.java:97)
	at de.uka.ilkd.key.rule.executor.javadl.RewriteTacletExecutor.replace(RewriteTacletExecutor.java:70)
	at de.uka.ilkd.key.rule.executor.javadl.RewriteTacletExecutor.replace(RewriteTacletExecutor.java:52)
	at de.uka.ilkd.key.rule.executor.javadl.RewriteTacletExecutor.applyReplacewithHelper(RewriteTacletExecutor.java:91)
	at de.uka.ilkd.key.rule.executor.javadl.RewriteTacletExecutor.applyReplacewith(RewriteTacletExecutor.java:139)
	at de.uka.ilkd.key.rule.executor.javadl.FindTacletExecutor.apply(FindTacletExecutor.java:116)
	at de.uka.ilkd.key.rule.Taclet.apply(Taclet.java:890)
	at de.uka.ilkd.key.rule.TacletApp.execute(TacletApp.java:411)
	at de.uka.ilkd.key.proof.Goal.apply(Goal.java:664)
	at de.uka.ilkd.key.control.AbstractProofControl.applyInteractive(AbstractProofControl.java:256)
	at de.uka.ilkd.key.control.AbstractProofControl.selectedTaclet(AbstractProofControl.java:227)
	at de.uka.ilkd.key.control.AbstractProofControl.selectedTaclet(AbstractProofControl.java:197)
	at de.uka.ilkd.key.ui.MediatorProofControl.selectedTaclet(MediatorProofControl.java:46)
	at de.uka.ilkd.key.gui.nodeviews.CurrentGoalView.selectedTaclet(CurrentGoalView.java:311)
	at de.uka.ilkd.key.gui.nodeviews.CurrentGoalViewMenu$MenuControl.actionPerformed(CurrentGoalViewMenu.java:535)
	at java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1967)
	at java.desktop/javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2308)
	at java.desktop/javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:405)
	at java.desktop/javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:262)
	at java.desktop/javax.swing.AbstractButton.doClick(AbstractButton.java:369)
	at java.desktop/javax.swing.plaf.basic.BasicMenuItemUI.doClick(BasicMenuItemUI.java:1020)
	at java.desktop/javax.swing.plaf.basic.BasicMenuItemUI$Handler.mouseReleased(BasicMenuItemUI.java:1064)
	at java.desktop/java.awt.AWTEventMulticaster.mouseReleased(AWTEventMulticaster.java:297)
	at java.desktop/java.awt.Component.processMouseEvent(Component.java:6635)
	at java.desktop/javax.swing.JComponent.processMouseEvent(JComponent.java:3342)
	at java.desktop/java.awt.Component.processEvent(Component.java:6400)
	at java.desktop/java.awt.Container.processEvent(Container.java:2263)
	at java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5011)
	at java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)
	at java.desktop/java.awt.Component.dispatchEvent(Component.java:4843)
	at java.desktop/java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4918)
	at java.desktop/java.awt.LightweightDispatcher.processMouseEvent(Container.java:4547)
	at java.desktop/java.awt.LightweightDispatcher.dispatchEvent(Container.java:4488)
	at java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2307)
	at java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2772)
	at java.desktop/java.awt.Component.dispatchEvent(Component.java:4843)
	at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:772)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)
	at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:715)
	at java.base/java.security.AccessController.doPrivileged(Native Method)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)
	at java.desktop/java.awt.EventQueue$5.run(EventQueue.java:745)
	at java.desktop/java.awt.EventQueue$5.run(EventQueue.java:743)
	at java.base/java.security.AccessController.doPrivileged(Native Method)
	at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)
	at java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:742)
	at java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)
	at java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)
	at java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
	at java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)

---

Works on:

• Latest release
• Commit: 6fb977367cbee54bce377d593a8383699cad17f0 (master branch)

---

Information:

• created_at: 2022-10-24T12:07:25.089Z
• updated_at: 2022-12-14T12:55:51.064Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 3