KeYProject · unp1 · Jul 7, 2026
diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java
@@ -35,8 +35,8 @@ public class ViewSettings extends AbstractPropertiesSettings {
 
     private static final String CLUTTER_RULESETS_DEFAULT = "notHumanReadable,obsolete,"
         + "pullOutQuantifierAll,inEqSimp_commute,inEqSimp_expand,pullOutQuantifierEx,"
-        + "inEqSimp_nonLin_divide,inEqSimp_special_nonLin,inEqSimp_nonLin,polySimp_normalise,"
-        + "polySimp_directEquations";
+        + "inEqSimp_nonLin_divide,inEqSimp_special_nonLin,inEqSimp_nonLin,inEqSimp_nonLin_multiply,"
+        + "polySimp_normalise,polySimp_directEquations";
 
     /**
      * default max number of displayed tooltip lines is 40

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategy.java
@@ -106,6 +106,17 @@ private RuleSetDispatchFeature setupInstantiationF() {
         setupInstantiationWithoutRetry(d);
         setupInEqSimpInstantiation(d);
 
+        // The multiply_2_inEq* taclets used to receive their instantiation cost from the
+        // inEqSimp_nonLin rule set (bound in setupArithPrimaryCategories above). Now that
+        // they only carry inEqSimp_nonLin_multiply, bind that rule set here explicitly.
+        // Both Model Search and DefOps must complete cross-multiplication candidates (the
+        // \assumes clause is matched during instantiation), so both get the finite stock
+        // cost; Basic keeps them uninstantiated at infinity. Model Search stays
+        // byte-identical because this reproduces the value inEqSimp_nonLin gave it.
+        bindRuleSet(d, "inEqSimp_nonLin_multiply",
+            arithNonLinInferences() || arithDefOps() ? longConst(IN_EQ_SIMP_NON_LIN_COST)
+                    : inftyConst());
+
         disableInstantiate();
         return d;
     }
@@ -114,8 +125,17 @@ private RuleSetDispatchFeature setupApprovalDispatcher() {
         final RuleSetDispatchFeature d = new RuleSetDispatchFeature();
         final IntegerLDT numbers = getServices().getTypeConverter().getIntegerLDT();
 
-        if (arithNonLinInferences()) {
-            setupMultiplyInequations(d, inftyConst());
+        if (arithNonLinInferences() || arithDefOps()) {
+            // The InEquationMultFeature bounding enforced here is what prevents
+            // cross-multiplication from running in circles: only products that are
+            // bounded by the left side of an inequation already present in the
+            // sequent are approved, so the derivable monomials are capped. In
+            // DefOps mode the check is stricter (exact match only) to avoid the
+            // saturation blow-up acceptable for Model Search.
+            // baseCost is zero on the approval dispatcher: approval only distinguishes
+            // finite (approved) from infinite (rejected), so the base cost is irrelevant
+            // here and left out to keep the approval decision identical to stock.
+            setupMultiplyInequations(d, longConst(0), inftyConst(), !arithNonLinInferences());
         }
         // these taclets are not supposed to be applied with metavariable
         // instantiations
@@ -256,6 +276,11 @@ private void setupArithPrimaryCategories(RuleSetDispatchFeature d) {
         } else {
             bindRuleSet(d, "inEqSimp_nonLin", inftyConst());
         }
+        // Cross-multiplication of inequations is now driven exclusively through the
+        // inEqSimp_nonLin_multiply rule set (the multiply_2_inEq* taclets no longer
+        // carry inEqSimp_nonLin). This keeps inEqSimp_nonLin at its stock cost so that
+        // splitEquationSucc and DefOps proofs that never cross-multiply stay on their
+        // stock search path. See setupInEqSimp for the per-mode binding.
         // polynomial division, simplification of fractions and mods
         bindRuleSet(d, "polyDivision", POLY_DIVISION_COST);
 
@@ -574,11 +599,39 @@ private void setupInEqSimp(RuleSetDispatchFeature d, IntegerLDT numbers) {
         // category "handling of non-linear inequations"
 
         if (arithNonLinInferences()) {
-            setupMultiplyInequations(d, longConst(100));
+            setupMultiplyInequations(d, longConst(IN_EQ_SIMP_NON_LIN_COST), longConst(100), false);
 
             bindRuleSet(d, "inEqSimp_split_eq", add(TopLevelFindFeature.SUCC, longConst(-100)));
 
             bindRuleSet(d, "inEqSimp_signCases", not(isInstantiated("signCasesLeft")));
+        } else if (arithDefOps()) {
+            // DefOps also cross-multiplies inequations, but - unlike Model Search - does
+            // no equation splitting, case distinctions or cuts, and only multiplies when
+            // the product exactly matches the left side of an inequation already in the
+            // sequent (onlyExactlyBounded, enforced at approval). This terminates: the
+            // monomial ordering is degree-graded, so products (which equal an existing
+            // left side) and all monomials of the resulting right side stay within the
+            // degree of the existing left sides - a finite monomial universe. DefOps
+            // proofs without integer inequations enqueue no multiply candidates and keep
+            // their stock search path.
+            //
+            // Note: inEqSimp_split_eq and inEqSimp_signCases are deliberately NOT bound
+            // here. Since the multiply_2_inEq* taclets no longer carry inEqSimp_nonLin,
+            // that rule set keeps its stock (infinite) DefOps cost, which already switches
+            // splitEquationSucc off exactly as in stock DefOps.
+            //
+            // notAllowed is finite (not infinity): an app whose \assumes is not yet matched
+            // takes this branch, and needs a finite cost to survive long enough for the
+            // assumes-completion machinery to match it and re-evaluate as exactly bounded.
+            // Non-exactly-bounded apps are ultimately rejected by the approval dispatcher.
+            // The value matches the Model Search convention above; raising it does not
+            // measurably reduce the (inherent) reordering of arithmetic proofs.
+            setupMultiplyInequations(d, longConst(IN_EQ_SIMP_NON_LIN_COST), longConst(100), true);
+        } else {
+            // Basic arithmetic: cross-multiplication is off. inEqSimp_nonLin used to be
+            // the off-switch via the (now removed) tag on the multiply taclets, so the
+            // multiply rule set must be pinned to infinity explicitly.
+            bindRuleSet(d, "inEqSimp_nonLin_multiply", inftyConst());
         }
 
         // category "normalisation of formulas"
@@ -662,7 +715,31 @@ public void setContent(Term term, MutableState mState) {}
 
     }
 
-    private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature notAllowedF) {
+    /**
+     * Sets up the cost/approval features for the cross-multiplication of inequations
+     * (rule set inEqSimp_nonLin_multiply).
+     *
+     * <p>
+     * The multiply_2_inEq* taclets used to carry the inEqSimp_nonLin rule set in addition to
+     * inEqSimp_nonLin_multiply, which contributed the base cost {@link #IN_EQ_SIMP_NON_LIN_COST}
+     * and, in DefOps mode, the infinite off-switch. They no longer do; the base cost is therefore
+     * passed in explicitly via {@code baseCost} so that inEqSimp_nonLin can keep its stock cost
+     * and DefOps proofs that never cross-multiply stay on their stock path.
+     * </p>
+     *
+     * @param d the dispatcher to bind the features to
+     * @param baseCost cost added unconditionally (previously supplied by the inEqSimp_nonLin
+     *        rule set); zero for the approval dispatcher, {@link #IN_EQ_SIMP_NON_LIN_COST} for
+     *        the cost dispatcher
+     * @param notAllowedF the costs in case the multiplication is not allowed
+     * @param onlyExactlyBounded if true, only products that exactly match the left side of
+     *        an inequation already present in the sequent are allowed (used in DefOps mode:
+     *        multiplication strictly directed at existing goal monomials); if false, products
+     *        that are merely subsumed by an existing left side are admitted as well (Model
+     *        Search: more speculative saturation)
+     */
+    private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature baseCost,
+            Feature notAllowedF, boolean onlyExactlyBounded) {
         final TermBuffer intRel = new TermBuffer();
 
         /*
@@ -691,6 +768,7 @@ private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature notAllow
         // perfect, because it is not possible to distinguish between the
         // re-cost-computation delay and the normal costs for a rule application
         bindRuleSet(d, "inEqSimp_nonLin_multiply", add(
+            baseCost,
             applyTF("multLeft", tf.nonNegMonomial),
             applyTF("multRight", tf.polynomial),
             ifZero(MatchedAssumesFeature.INSTANCE,
@@ -707,7 +785,8 @@ private void setupMultiplyInequations(RuleSetDispatchFeature d, Feature notAllow
                     not(TermSmallerThanFeature.create(FocusProjection.create(0),
                         AssumptionProjection.create(0))),
                     ifZero(exactlyBounded, longConst(0),
-                        ifZero(totallyBounded, longConst(100), notAllowedF))
+                        onlyExactlyBounded ? notAllowedF
+                                : ifZero(totallyBounded, longConst(100), notAllowedF))
                 /*
                  * ifZero ( partiallyBounded, longConst ( 400 ), notAllowedF ) ) ),
                  */

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategyFactory.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntegerStrategyFactory.java
@@ -24,7 +24,10 @@ public class IntegerStrategyFactory implements StrategyFactory {
             <li><tt>/</tt>, <tt>%</tt>, <tt>jdiv</tt>, <tt>jmod</tt>, ...</li>\
             <li><tt>int_RANGE</tt>, <tt>short_MIN</tt>, ...</li>\
             <li><tt>inInt</tt>, <tt>inByte</tt>, ...</li>\
-            <li><tt>addJint</tt>, <tt>mulJshort</tt>, ...</li></ul></html>""";
+            <li><tt>addJint</tt>, <tt>mulJshort</tt>, ...</li></ul>\
+            In addition, inequations are multiplied with each other<br>\
+            where the product is bounded by an existing inequation<br>\
+            (restricted such that termination is guaranteed).</html>""";
     public static final String TOOL_TIP_ARITHMETIC_MODEL_SEARCH = """
             <html>\
             Support for non-linear inequations and model search.<br>In addition, this performs:\

diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/ModularJavaDLStrategyFactory.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/ModularJavaDLStrategyFactory.java
@@ -49,7 +49,10 @@ public class ModularJavaDLStrategyFactory implements StrategyFactory {
             + "<li><tt>/</tt>, <tt>%</tt>, <tt>jdiv</tt>, <tt>jmod</tt>, ...</li>"
             + "<li><tt>int_RANGE</tt>, <tt>short_MIN</tt>, ...</li>"
             + "<li><tt>inInt</tt>, <tt>inByte</tt>, ...</li>"
-            + "<li><tt>addJint</tt>, <tt>mulJshort</tt>, ...</li>" + "</ul>" + "</html>";
+            + "<li><tt>addJint</tt>, <tt>mulJshort</tt>, ...</li>" + "</ul>"
+            + "In addition, inequations are multiplied with each other<br>"
+            + "where the product is bounded by an existing inequation<br>"
+            + "(restricted such that termination is guaranteed)." + "</html>";
     public static final String TOOL_TIP_ARITHMETIC_MODEL_SEARCH = "<html>"
         + "Support for non-linear inequations and model search.<br>" + "In addition, this performs:"
         + "<ul>" + "<li>Multiplication of inequations with each other</li>"

diff --git a/...ore/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerSimplificationRules.key b/...ore/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerSimplificationRules.key
@@ -955,8 +955,7 @@
             -multRight * multFacRight
             + multRight * multFacLeft
             + multLeft * multFacRight ==>)
-        \heuristics(inEqSimp_nonLin,
-            inEqSimp_nonLin_multiply)
+        \heuristics(inEqSimp_nonLin_multiply)
     };
 
     multiply_2_inEq1 {
@@ -966,8 +965,7 @@
             -multRight * multFacRight
             + multRight * multFacLeft
             + multLeft * multFacRight ==>)
-        \heuristics(inEqSimp_nonLin,
-            inEqSimp_nonLin_multiply)
+        \heuristics(inEqSimp_nonLin_multiply)
     };
 
     multiply_2_inEq2 {
@@ -977,8 +975,7 @@
             -multRight * multFacRight
             + multRight * multFacLeft
             + multLeft * multFacRight ==>)
-        \heuristics(inEqSimp_nonLin,
-            inEqSimp_nonLin_multiply)
+        \heuristics(inEqSimp_nonLin_multiply)
     };
 
     multiply_2_inEq3 {
@@ -988,8 +985,7 @@
             -multRight * multFacRight
             + multRight * multFacLeft
             + multLeft * multFacRight ==>)
-        \heuristics(inEqSimp_nonLin,
-            inEqSimp_nonLin_multiply)
+        \heuristics(inEqSimp_nonLin_multiply)
     };
 
     divide_inEq0 {

diff --git a/key.core/src/test/java/de/uka/ilkd/key/strategy/DefOpsCrossMultiplicationTest.java b/key.core/src/test/java/de/uka/ilkd/key/strategy/DefOpsCrossMultiplicationTest.java
@@ -0,0 +1,68 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.strategy;
+
+import java.nio.file.Path;
+
+import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.proof.Proof;
+
+import org.key_project.util.helper.FindResources;
+
+import org.junit.jupiter.api.Assertions;
+import org.junit.jupiter.api.Test;
+
+/**
+ * Regression test for bounded cross-multiplication of inequations in the DefOps arithmetic
+ * treatment.
+ *
+ * <p>
+ * The {@code multiply_2_inEq*} taclets used to be reachable only with the Model Search treatment.
+ * They are now also enabled - restricted to products that are exactly bounded by an inequation
+ * already present in the sequent, which keeps the strategy terminating - with DefOps. The pure
+ * arithmetic problem in {@code crossMultDefOps.key} needs such a cross-multiplication, so it now
+ * closes with DefOps as it does with Model Search, while Basic arithmetic still leaves it open.
+ * </p>
+ */
+public class DefOpsCrossMultiplicationTest {
+
+    private static final Path PROBLEM = FindResources.getTestResourcesDirectory()
+            .resolve("de/uka/ilkd/key/strategy/crossMultDefOps.key");
+
+    private boolean closesWith(String nonLinArithMode) throws Exception {
+        KeYEnvironment<?> env = KeYEnvironment.load(PROBLEM);
+        try {
+            Proof proof = env.getLoadedProof();
+            var settings = proof.getSettings().getStrategySettings();
+            var sp = settings.getActiveStrategyProperties();
+            sp.setProperty(StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY, nonLinArithMode);
+            settings.setActiveStrategyProperties(sp);
+            settings.setMaxSteps(30000);
+            proof.setActiveStrategy(
+                proof.getServices().getProfile().getDefaultStrategyFactory().create(proof, sp));
+            env.getProofControl().startAndWaitForAutoMode(proof);
+            return proof.closed();
+        } finally {
+            env.dispose();
+        }
+    }
+
+    @Test
+    public void closesWithDefOps() throws Exception {
+        Assertions.assertTrue(closesWith(StrategyProperties.NON_LIN_ARITH_DEF_OPS),
+            "cross-multiplication should let DefOps close the index-in-bounds obligation");
+    }
+
+    @Test
+    public void closesWithModelSearch() throws Exception {
+        Assertions.assertTrue(closesWith(StrategyProperties.NON_LIN_ARITH_COMPLETION),
+            "Model Search should still close the index-in-bounds obligation");
+    }
+
+    @Test
+    public void staysOpenWithBasicArithmetic() throws Exception {
+        Assertions.assertFalse(closesWith(StrategyProperties.NON_LIN_ARITH_NONE),
+            "without non-linear arithmetic the obligation cannot be closed");
+    }
+}
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt
@@ -13478,31 +13478,31 @@ multiply_2_inEq0 {
 \assumes ([leq(multFacLeft,multFacRight)]==>[]) 
 \find(leq(multLeft,multRight)==>)
 \add [geq(mul(multLeft,multFacLeft),add(add(mul(neg(multRight),multFacRight),mul(multRight,multFacLeft)),mul(multLeft,multFacRight)))]==>[] 
-\heuristics(inEqSimp_nonLin_multiply, inEqSimp_nonLin)
+\heuristics(inEqSimp_nonLin_multiply)
 Choices: integerSimplificationRules:full}
 -----------------------------------------------------
 == multiply_2_inEq1 (multiply_2_inEq1) =========================================
 multiply_2_inEq1 {
 \assumes ([geq(multFacLeft,multFacRight)]==>[]) 
 \find(leq(multLeft,multRight)==>)
 \add [leq(mul(multLeft,multFacLeft),add(add(mul(neg(multRight),multFacRight),mul(multRight,multFacLeft)),mul(multLeft,multFacRight)))]==>[] 
-\heuristics(inEqSimp_nonLin_multiply, inEqSimp_nonLin)
+\heuristics(inEqSimp_nonLin_multiply)
 Choices: integerSimplificationRules:full}
 -----------------------------------------------------
 == multiply_2_inEq2 (multiply_2_inEq2) =========================================
 multiply_2_inEq2 {
 \assumes ([leq(multFacLeft,multFacRight)]==>[]) 
 \find(geq(multLeft,multRight)==>)
 \add [leq(mul(multLeft,multFacLeft),add(add(mul(neg(multRight),multFacRight),mul(multRight,multFacLeft)),mul(multLeft,multFacRight)))]==>[] 
-\heuristics(inEqSimp_nonLin_multiply, inEqSimp_nonLin)
+\heuristics(inEqSimp_nonLin_multiply)
 Choices: integerSimplificationRules:full}
 -----------------------------------------------------
 == multiply_2_inEq3 (multiply_2_inEq3) =========================================
 multiply_2_inEq3 {
 \assumes ([geq(multFacLeft,multFacRight)]==>[]) 
 \find(geq(multLeft,multRight)==>)
 \add [geq(mul(multLeft,multFacLeft),add(add(mul(neg(multRight),multFacRight),mul(multRight,multFacLeft)),mul(multLeft,multFacRight)))]==>[] 
-\heuristics(inEqSimp_nonLin_multiply, inEqSimp_nonLin)
+\heuristics(inEqSimp_nonLin_multiply)
 Choices: integerSimplificationRules:full}
 -----------------------------------------------------
 == multiply_distribute_1 (multiply_distribute) =========================================

diff --git a/key.core/src/test/resources/de/uka/ilkd/key/strategy/crossMultDefOps.key b/key.core/src/test/resources/de/uka/ilkd/key/strategy/crossMultDefOps.key
@@ -0,0 +1,12 @@
+// Pure arithmetic core of a matrix index-in-bounds proof obligation:
+// a matrix is encoded in a one-dimensional array as (i, j) |-> a[x * j + i].
+// Showing the index stays in bounds requires cross-multiplication of the
+// hypotheses 0 <= i < x and 0 <= j < y to derive x * j + i < x * y.
+//
+// This closes with the Model Search arithmetic treatment and, since bounded
+// cross-multiplication was enabled for it, also with DefOps; with Basic
+// arithmetic it stays open. See DefOpsCrossMultiplicationTest.
+\problem {
+    \forall int x; \forall int y; \forall int i; \forall int j;
+        (0 <= i & i < x & 0 <= j & j < y -> x * j + i < x * y)
+}