KeYProject · mattulbrich · Aug 15, 2026 · Aug 15, 2026 · Aug 15, 2026 · Aug 15, 2026
diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java
@@ -19,6 +19,7 @@
 import de.uka.ilkd.key.logic.JavaBlock;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.nparser.KeyAst;
+import de.uka.ilkd.key.pp.Notation;
 import de.uka.ilkd.key.proof.*;
 import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
 import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo;
@@ -243,6 +244,14 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
             ProofScriptEngine pse = new ProofScriptEngine(proof);
             pse.setInitiallySelectedGoal(goal);
             pse.getStateMap().getUserData().set(USER_DATA_JML_OBTAIN_VAR_MAP, obtainMap);
+            pse.getStateMap().getValueInjector().addConverter(Integer.class, ObtainAwareTerm.class,
+                oat -> {
+                    String numberStr = Notation.NumLiteral.printNumberTerm(oat.term);
+                    if (numberStr == null)
+                        throw new ScriptException(
+                            "Expected a number literal, but got: " + oat.term);
+                    return Integer.parseInt(numberStr);
+                });
             pse.getStateMap().getValueInjector().addConverter(JTerm.class, ObtainAwareTerm.class,
                 oat -> oat.resolve(obtainMap, goal.proof().getServices()));
             // TODO: Perhaps have holes also in JML?
@@ -251,6 +260,8 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
                 oat -> new TermWithHoles(oat.resolve(obtainMap, goal.proof().getServices())));
             pse.getStateMap().getValueInjector().addConverter(boolean.class, ObtainAwareTerm.class,
                 oat -> Boolean.parseBoolean(oat.term.toString()));
+            pse.getStateMap().getValueInjector().addConverter(String.class, ObtainAwareTerm.class,
+                oat -> oat.term.toString());
             LOGGER.debug("---- Script");
             LOGGER.debug(renderedProof.stream()
                     .map(ScriptCommandAst::asCommandLine)

diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/Notation.java b/key.core/src/main/java/de/uka/ilkd/key/pp/Notation.java
@@ -620,7 +620,7 @@ public void print(JTerm t, LogicPrinter sp) {
      * The standard concrete syntax for the number literal indicator `Z'. This is only used in the
      * `Pretty&amp;Untrue' syntax.
      */
-    static final class NumLiteral extends Notation {
+    public static final class NumLiteral extends Notation {
         public NumLiteral() {
             super(120);
         }

diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/AutoCommand.java
@@ -87,8 +87,12 @@ public void execute(ScriptCommandAst args) throws ScriptException, InterruptedEx
             OriginalValue ov = orgValues.get(entry.getKey());
             if (ov != null) {
                 ov.oldValue = activeStrategyProperties.getProperty(ov.settingName);
-                activeStrategyProperties.setProperty(ov.settingName,
-                    "true".equals(entry.getValue()) ? ov.trueValue : ov.falseValue);
+                String key = state.getValueInjector().convert(entry.getValue(), String.class);
+                String value = ov.stringMap.get(key);
+                if (value == null) {
+                    throw new ScriptException("Invalid value for " + entry.getKey() + ": " + key);
+                }
+                activeStrategyProperties.setProperty(ov.settingName, value);
             }
         }
 
@@ -132,9 +136,14 @@ public void execute(ScriptCommandAst args) throws ScriptException, InterruptedEx
 
     private Map<String, OriginalValue> prepareOriginalValues() {
         var res = new HashMap<String, OriginalValue>();
+        // Deprecated: Will be removed soon
         res.put("modelSearch",
             new OriginalValue(NON_LIN_ARITH_OPTIONS_KEY, NON_LIN_ARITH_COMPLETION,
                 NON_LIN_ARITH_DEF_OPS));
+        res.put("arithmetic",
+            new OriginalValue(NON_LIN_ARITH_OPTIONS_KEY,
+                Map.of("basic", NON_LIN_ARITH_NONE, "defOps",
+                    NON_LIN_ARITH_DEF_OPS, "modelsearch", NON_LIN_ARITH_COMPLETION)));
         res.put("expandQueries",
             new OriginalValue(QUERYAXIOM_OPTIONS_KEY, QUERYAXIOM_ON, QUERYAXIOM_OFF));
         res.put("classAxioms",
@@ -210,9 +219,28 @@ public static class Parameters implements ValueInjector.VerifyableParameters {
         public @Nullable String breakpoint = null;
 
         @Flag(value = "modelsearch")
-        @Documentation("Enable model search. Better for some (types of) arithmetic problems. Sometimes a lot worse.")
+        @Deprecated
+        @Documentation("Deprecated. Use arithmetic=modelsearch instead.")
         public boolean modelSearch;
 
+        @Option(value = "arithmetic")
+        @Documentation("""
+                Specify the arithmetic strategy to handle division and modulo operations:
+                - *`basic`*: Basic arithmetic support:
+                  - Simplification of polynomial expressions
+                  - Computation of Gröbner Bases for polynomials in the antecedent
+                  - (Partial) Omega procedure for handling linear inequations</li>" + "</ul>"
+                - *`defOps`*: Automatically expand defined symbols like: `/`, `%`, `jdiv`, `jmod` ..., `int_RANGE`, ...
+                In addition, inequations are multiplied with each other where the product is bounded by an existing
+                inequation (restricted such that termination is guaranteed).
+                - *`modelsearch`*: Support for non-linear inequations and model search. In addition, this performs
+                (a) multiplication of inequations with each other and (b) systematic case distinctions (cuts).
+                This method is guaranteed to find counterexamples for invalid goals that only contain polynomial
+                (in)equations. Such counterexamples turn up as trivially unprovable goals. It is also able to prove many
+                more valid goals involving (in)equations, but will in general not terminate on such goals.
+                """)
+        public @Nullable String arithmetic;
+
         @Flag(value = "expandQueries")
         @Documentation("Automatically expand occurrences of query symbols using additional modalities on the sequent.")
         public boolean expandQueries;
@@ -259,23 +287,23 @@ public void verifyParameters() throws IllegalArgumentException, InjectionExcepti
 
     private static final class OriginalValue {
         private final String settingName;
-        private final String trueValue;
-        private final String falseValue;
+        private final Map<String, String> stringMap;
         private @Nullable String oldValue;
 
         private OriginalValue(String settingName, String trueValue, String falseValue) {
-            this.settingName = settingName;
-            this.trueValue = trueValue;
+            this(settingName, Map.of("true", trueValue, "false", falseValue));
+        }
 
-            this.falseValue = falseValue;
+        private OriginalValue(String settingName, Map<String, String> stringMap) {
+            this.settingName = settingName;
+            this.stringMap = stringMap;
         }
 
         @Override
         public String toString() {
             return "OriginalValue{" +
                 "settingName='" + settingName + '\'' +
-                ", trueValue='" + trueValue + '\'' +
-                ", falseValue='" + falseValue + '\'' +
+                ", stringMap=" + stringMap +
                 ", oldValue='" + oldValue + '\'' +
                 '}';
         }

diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java
@@ -185,7 +185,7 @@ public static ProofCollection automaticJavaDL() throws IOException {
          * pervar g = c.group("- one subprocess is created for each group
          * perFile-one subprocess is created for each file
          */
-        settings.setForkMode(ForkMode.PERGROUP);
+        settings.setForkMode(ForkMode.NOFORK);
 
         /*
          * Enable or disable proof reloading.
@@ -240,7 +240,7 @@ public static ProofCollection automaticJavaDL() throws IOException {
          * test can be restricted to these groups (for debugging).
          */
         // runOnlyOn = group1, group2 (the space after each comma is mandatory)
-        // settings.setRunOnlyOn("performance, performancePOConstruction");
+        settings.setRunOnlyOn("example-algos");
 
         settings.setKeySettings(GenerateUnitTestsUtil.loadFromFile("automaticJAVADL.properties"));
 
@@ -415,6 +415,10 @@ public static ProofCollection automaticJavaDL() throws IOException {
         g.provable("heap/verifyThis11_1_Maximum/project.key");
         g.provable("heap/fm12_01_LRS/lcp.key");
         g.provable("heap/SemanticSlicing/project.key");
+        g.provable("heap/verifyThis26_01_hIndex/compute.key");
+        g.provable("heap/verifyThis26_01_hIndex/compute_opt.key");
+        g.provable("heap/verifyThis26_01_hIndex/lemma1.key");
+        g.provable("heap/verifyThis26_01_hIndex/update.key");
 
         g = c.group("funOfIF");
         g.provable("heap/information_flow/ArrayList_contains.key");

diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/README.txt b/key.ui/examples/heap/verifyThis26_01_hIndex/README.txt
@@ -0,0 +1,16 @@
+example.name = H-Index Computation
+example.file = hIndex.key
+example.additionalFile.1 = src/HIndex.java
+example.path = Benchmarks/VerifyThis2026
+
+This is a KeY solution to challenge 1 of VerifyThis 2026.
+
+The h-Index is an (in)famous metrics in research.
+This challenge deals with efficient computation and updates of h indices.
+
+See also challenge.pdf in the example directory.
+
+The example uses the recently introduced JML proof scripts.
+You hence need to run it using the "Script-aware" automation button
+
+@author Mattias Ulbrich
diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/challenge.pdf b/key.ui/examples/heap/verifyThis26_01_hIndex/challenge.pdf
diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/compute.key b/key.ui/examples/heap/verifyThis26_01_hIndex/compute.key
@@ -0,0 +1,89 @@
+\profile "Java Profile";
+
+\settings {
+    "Choice" : {
+        "JavaCard" : "JavaCard:on",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:on",
+        "bigint" : "bigint:on",
+        "finalFields" : "finalFields:immutable",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:arithmeticSemanticsIgnoringOF",
+        "integerSimplificationRules" : "integerSimplificationRules:full",
+        "javaLoopTreatment" : "javaLoopTreatment:efficient",
+        "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
+        "methodExpansion" : "methodExpansion:modularOnly",
+        "modelFields" : "modelFields:treatAsAxiom",
+        "moreSeqRules" : "moreSeqRules:off",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "soundDefaultContracts" : "soundDefaultContracts:on"
+    },
+    "Labels" : {
+        "UseOriginLabels" : true
+    },
+    "NewSMT" : {
+
+    },
+    "SMTSettings" : {
+        "SelectedTaclets" : [
+
+        ],
+        "UseBuiltUniqueness" : false,
+        "explicitTypeHierarchy" : false,
+        "instantiateHierarchyAssumptions" : true,
+        "integersMaximum" : 2147483645,
+        "integersMinimum" : -2147483645,
+        "invariantForall" : false,
+        "maxGenericSorts" : 2,
+        "useConstantsForBigOrSmallIntegers" : true,
+        "useUninterpretedMultiplication" : true
+    },
+    "Strategy" : {
+        "ActiveStrategy" : "Modular JavaDL Strategy",
+        "MaximumNumberOfAutomaticApplications" : 200000,
+        "Timeout" : -1,
+        "options" : {
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
+            "DEP_OPTIONS_KEY" : "DEP_ON",
+            "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL",
+            "LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
+            "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
+            "MPS_OPTIONS_KEY" : "MPS_MERGE",
+            "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
+            "OSS_OPTIONS_KEY" : "OSS_ON",
+            "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
+            "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
+            "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
+            "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
+            "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST",
+            "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
+            "VBT_PHASE" : "VBT_SYM_EX"
+        }
+    }
+} 
+
+
+\javaSource "src";
+
+\proofObligation 
+// 
+{
+    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
+    "contract" : "HIndex[HIndex::compute([I)].JML normal_behavior operation contract.0",
+    "name" : "HIndex[HIndex::compute([I)].JML normal_behavior operation contract.0"
+}
+
+\proofScript { macro "script-auto"; }
+
diff --git a/key.ui/examples/heap/verifyThis26_01_hIndex/compute_opt.key b/key.ui/examples/heap/verifyThis26_01_hIndex/compute_opt.key
@@ -0,0 +1,89 @@
+\profile "Java Profile";
+
+\settings {
+    "Choice" : {
+        "JavaCard" : "JavaCard:on",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:on",
+        "bigint" : "bigint:on",
+        "finalFields" : "finalFields:immutable",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:arithmeticSemanticsIgnoringOF",
+        "integerSimplificationRules" : "integerSimplificationRules:full",
+        "javaLoopTreatment" : "javaLoopTreatment:efficient",
+        "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
+        "methodExpansion" : "methodExpansion:modularOnly",
+        "modelFields" : "modelFields:treatAsAxiom",
+        "moreSeqRules" : "moreSeqRules:off",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "soundDefaultContracts" : "soundDefaultContracts:on"
+    },
+    "Labels" : {
+        "UseOriginLabels" : true
+    },
+    "NewSMT" : {
+
+    },
+    "SMTSettings" : {
+        "SelectedTaclets" : [
+
+        ],
+        "UseBuiltUniqueness" : false,
+        "explicitTypeHierarchy" : false,
+        "instantiateHierarchyAssumptions" : true,
+        "integersMaximum" : 2147483645,
+        "integersMinimum" : -2147483645,
+        "invariantForall" : false,
+        "maxGenericSorts" : 2,
+        "useConstantsForBigOrSmallIntegers" : true,
+        "useUninterpretedMultiplication" : true
+    },
+    "Strategy" : {
+        "ActiveStrategy" : "Modular JavaDL Strategy",
+        "MaximumNumberOfAutomaticApplications" : 200000,
+        "Timeout" : -1,
+        "options" : {
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
+            "DEP_OPTIONS_KEY" : "DEP_ON",
+            "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL",
+            "LOOP_OPTIONS_KEY" : "LOOP_INVARIANT",
+            "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
+            "MPS_OPTIONS_KEY" : "MPS_MERGE",
+            "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
+            "OSS_OPTIONS_KEY" : "OSS_ON",
+            "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
+            "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
+            "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
+            "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
+            "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST",
+            "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
+            "VBT_PHASE" : "VBT_SYM_EX"
+        }
+    }
+} 
+
+
+\javaSource "src";
+
+\proofObligation 
+// 
+{
+    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
+    "contract" : "HIndex[HIndex::compute_opt([I)].JML normal_behavior operation contract.0",
+    "name" : "HIndex[HIndex::compute_opt([I)].JML normal_behavior operation contract.0"
+}
+
+\proofScript { macro "script-auto"; }
+