diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key
index 7982511fa67..097408d7e72 100644
--- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key
+++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key
@@ -42,6 +42,7 @@
         \find(\modality{#normalassign}{..
                     #loc = #seCharByteShortInt0 * #seCharByteShortInt1;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                 \add(==> inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1)))
@@ -56,6 +57,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seCharByteShortInt * #seLong;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                 \add(==> inLong(mul(#seCharByteShortInt, #seLong)))
@@ -70,6 +72,7 @@
         \find(\modality{#normalassign}{..
                        #loc=#seLong * #seCharByteShortInt;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                 \add(==> inLong(mul(#seLong, #seCharByteShortInt)))
@@ -84,6 +87,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seLong0 * #seLong1;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inLong(mul(#seLong0, #seLong1)))
@@ -280,6 +284,7 @@
         \find(\modality{#normalassign}{..
                     #loc = #seCharByteShortInt0 - #seCharByteShortInt1;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1)))
@@ -294,6 +299,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seCharByteShortInt - #seLong;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inLong(sub(#seCharByteShortInt, #seLong)))
@@ -308,6 +314,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seLong - #seCharByteShortInt;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inLong(sub(#seLong, #seCharByteShortInt)))
@@ -323,6 +330,7 @@
         \find(\modality{#normalassign}{..
                      #loc=#seLong0 - #seLong1;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inLong(sub(#seLong0, #seLong1)))
@@ -339,6 +347,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seCharByteShortInt0 + #seCharByteShortInt1;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inInt(add(#seCharByteShortInt0, #seCharByteShortInt1)))
@@ -354,6 +363,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seCharByteShortInt + #seLong;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inLong(add(#seCharByteShortInt, #seLong)))
@@ -369,6 +379,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seLong + #seCharByteShortInt;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inLong(add(#seLong, #seCharByteShortInt)))
@@ -384,6 +395,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seLong0 + #seLong1;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inLong(add(#seLong0, #seLong1)))
@@ -541,6 +553,7 @@
         \find(\modality{#normalassign}{..
                    #loc=#seCharByteShortInt0 >> #se;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inInt(shiftright(#seLong0, #se)))
@@ -556,6 +569,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seLong0 >> #se;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inInt(shiftright(#seLong0, #se)))
@@ -573,6 +587,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seCharByteShortInt0 << #se; ...}
                 \endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inInt(shiftleft(#seCharByteShortInt0, #se)))
@@ -588,6 +603,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seLong0 << #se;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inLong(shiftleft(#seLong0, #se)))
@@ -605,6 +621,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seCharByteShortInt0 >>> #se; ...}
                 \endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inLong(unsignedshiftrightJint(#seCharByteShortInt0, #se)))
@@ -620,6 +637,7 @@
         \find(\modality{#normalassign}{..
                     #loc=#seLong0 >>> #se;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inLong(unsignedshiftrightJlong(#seLong0, #se)))
@@ -638,6 +656,7 @@
         \find(\modality{#normalassign}{..
                     #loc = - #seCharByteShortInt;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inInt(neg(#seCharByteShortInt)))
@@ -652,6 +671,7 @@
         \find(\modality{#normalassign}{..
                     #loc = - #seLong;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inLong(neg(#seLong)))
@@ -686,6 +706,7 @@
         \find(\modality{#normalassign}{..
                     #loc = (byte) #seShort;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inByte(#seShort))
@@ -700,6 +721,7 @@
         \find(\modality{#normalassign}{..
                     #loc = (byte) #seInt;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inByte(#seInt))
@@ -714,6 +736,7 @@
         \find(\modality{#normalassign}{..
                     #loc = (byte) #seLong;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inByte(#seLong))
@@ -728,6 +751,7 @@
         \find(\modality{#normalassign}{..
                    #loc = (short) #seInt;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inShort(#seInt))
@@ -742,6 +766,7 @@
         \find(\modality{#normalassign}{..
                     #loc = (short) #seLong;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inShort(#seLong))
@@ -754,6 +779,7 @@
 
     narrowingIntCastLong {
         \find(\modality{#normalassign}{.. #loc = (int) #seLong; ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inInt(#seLong))
@@ -768,6 +794,7 @@
         \find(\modality{#normalassign}{..
                     #loc = (char) #seByte;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inChar(#seByte))
@@ -783,6 +810,7 @@
         \find(\modality{#normalassign}{..
                     #loc = (char) #seShort;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inChar(#seShort))
@@ -798,6 +826,7 @@
         \find(\modality{#normalassign}{..
                     #loc = (char) #seInt;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inChar(#seInt))
@@ -812,6 +841,7 @@
         \find(\modality{#normalassign}{..
                     #loc = (char) #seLong;
                 ...}\endmodality (post))
+        \sameUpdateLevel
         (intRules:arithmeticSemanticsCheckingOF) {
             "Overflow check":
                  \add(==> inChar(#seLong))
diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/IntSemanticsTest.java b/key.core/src/test/java/de/uka/ilkd/key/rule/IntSemanticsTest.java
new file mode 100644
index 00000000000..70f8b8fffa8
--- /dev/null
+++ b/key.core/src/test/java/de/uka/ilkd/key/rule/IntSemanticsTest.java
@@ -0,0 +1,70 @@
+/* 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.rule;
+
+import java.io.File;
+
+import de.uka.ilkd.key.api.KeYApi;
+import de.uka.ilkd.key.api.ProofApi;
+import de.uka.ilkd.key.api.ProofManagementApi;
+import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.io.ProblemLoaderException;
+
+import org.key_project.util.helper.FindResources;
+
+import org.junit.jupiter.api.Assertions;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.ValueSource;
+
+/**
+ * These tests check that the integer taclet options still work as intended, for example that the
+ * additional branches for overflow checks are still generated correctly. At the moment, for each of
+ * the three taclet options there is one positive (provable) and one negative (unprovable) test.
+ *
+ * @author Wolfram Pfeifer
+ */
+class IntSemanticsTest {
+    private static final File TEST_DIR = new File(FindResources.getTestResourcesDirectory(),
+        "/de/uka/ilkd/key/rule/intSemantics/");
+
+    /**
+     * This test checks that certain proofs containing integer corner cases are reloadable.
+     *
+     * @param filename name of the .proof file containing a closed proof and also setting the
+     *        desired taclet option for the integer semantics.
+     * @throws ProblemLoaderException should not happen
+     */
+    @ParameterizedTest
+    @ValueSource(strings = { "java/mJava.proof",
+        "uncheckedOF/mBigint.proof",
+        "checkedOF/mOFCheck.proof" })
+    void testSemanticsProvable(String filename) throws ProblemLoaderException {
+        File proofFile = new File(TEST_DIR, filename);
+        ProofManagementApi pmapi = KeYApi.loadProof(proofFile);
+        Proof proof = pmapi.getLoadedProof().getProof();
+        // Proof should be reloaded completely now. If not, the int semantics are probably broken.
+        Assertions.assertTrue(proof.closed());
+    }
+
+    /**
+     * This test checks that certain contracts are not provable with the selected integer semantics.
+     *
+     * @param filename name of the .key file that points to the contract. The desired integer
+     *        semantics need to be set correctly here!
+     * @throws ProblemLoaderException should not happen
+     */
+    @ParameterizedTest
+    @ValueSource(strings = { "java/mJavaWrong.key",
+        "uncheckedOF/mBigintWrong.key",
+        "checkedOF/mOFCheckWrong.key", })
+    void testSemanticsUnprovable(String filename) throws ProblemLoaderException {
+        File keyFile = new File(TEST_DIR, filename);
+        ProofManagementApi pmapi = KeYApi.loadFromKeyFile(keyFile);
+        ProofApi proofApi = pmapi.getLoadedProof();
+        Proof proof = proofApi.getProof();
+        proofApi.getEnv().getProofControl().startAndWaitForAutoMode(proof);
+        // we expect that exactly one branch (the overflow check) is open now:
+        Assertions.assertEquals(1, proof.openGoals().size());
+    }
+}
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
index f17dc2bbc68..2e397ca646a 100644
--- 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
@@ -1,5 +1,5 @@
 # This files contains representation of taclets, which are accepted and revised.
-# Date: Fri Jun 21 16:10:16 CEST 2024
+# Date: Wed Jun 26 12:45:30 CEST 2024
 
 == abortJavaCardTransactionAPI (abortJavaCardTransactionAPI) =========================================
 abortJavaCardTransactionAPI {
@@ -1304,7 +1304,7 @@ assignmentAdditionInt {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seCharByteShortInt0 + #seCharByteShortInt1;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaAddInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaAddInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1313,7 +1313,7 @@ assignmentAdditionLong {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seCharByteShortInt + #seLong;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seCharByteShortInt,#seLong)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seCharByteShortInt,#seLong)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1322,7 +1322,7 @@ assignmentAdditionLong2 {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seLong + #seCharByteShortInt;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong,#seCharByteShortInt)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong,#seCharByteShortInt)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1331,7 +1331,7 @@ assignmentAdditionLong3 {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seLong0 + #seLong1;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong0,#seLong1)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaAddLong(#seLong0,#seLong1)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1644,7 +1644,7 @@ assignmentMultiplicationInt {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seCharByteShortInt0 * #seCharByteShortInt1;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaMulInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaMulInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1653,7 +1653,7 @@ assignmentMultiplicationLong {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seCharByteShortInt * #seLong;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seCharByteShortInt,#seLong)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seCharByteShortInt,#seLong)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1662,7 +1662,7 @@ assignmentMultiplicationLong2 {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seLong * #seCharByteShortInt;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong,#seCharByteShortInt)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong,#seCharByteShortInt)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1671,7 +1671,7 @@ assignmentMultiplicationLong3 {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seLong0 * #seLong1;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong0,#seLong1)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaMulLong(#seLong0,#seLong1)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1680,7 +1680,7 @@ assignmentShiftLeftInt {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seCharByteShortInt0 << #se;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftInt(#seCharByteShortInt0,#se)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftInt(#seCharByteShortInt0,#se)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1689,7 +1689,7 @@ assignmentShiftLeftLong {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seLong0 << #se;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftLong(#seLong0,#se)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftLeftLong(#seLong0,#se)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1698,7 +1698,7 @@ assignmentShiftRightInt {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seCharByteShortInt0 >> #se;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1707,7 +1707,7 @@ assignmentShiftRightLong {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seLong0 >> #se;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightLong(#seLong0,#se)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaShiftRightLong(#seLong0,#se)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1774,7 +1774,7 @@ assignmentSubtractionInt {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seCharByteShortInt0 - #seCharByteShortInt1;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaSubInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaSubInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1783,7 +1783,7 @@ assignmentSubtractionLong {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seCharByteShortInt - #seLong;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seCharByteShortInt,#seLong)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seCharByteShortInt,#seLong)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1792,7 +1792,7 @@ assignmentSubtractionLong2 {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seLong - #seCharByteShortInt;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong,#seCharByteShortInt)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong,#seCharByteShortInt)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1801,7 +1801,7 @@ assignmentSubtractionLong3 {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seLong0 - #seLong1;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong0,#seLong1)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaSubLong(#seLong0,#seLong1)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1810,7 +1810,7 @@ assignmentUnsignedShiftRightInt {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seCharByteShortInt0 >>> #se;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightInt(#seCharByteShortInt0,#se)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -1819,7 +1819,7 @@ assignmentUnsignedShiftRightLong {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = #seLong0 >>> #se;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightLong(#seLong0,#se)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaUnsignedShiftRightLong(#seLong0,#se)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -5400,7 +5400,7 @@ Choices: sequences:on}
 defOfSeqUpd {
 \find(seqUpd(seq,idx,value))
 \varcond(\notFreeIn(uSub (variable), seq (Seq term)), \notFreeIn(uSub (variable), value (any term)), \notFreeIn(uSub (variable), idx (int term)))
-\replacewith(seqDef{uSub (variable)}(Z(0(#)),seqLen(seq),if-then-else(equals(uSub,idx),value,any::seqGet(seq,uSub))))
+\replacewith(seqDef{uSub (variable)}(Z(0(#)),seqLen(seq),if-then-else(equals(uSub,idx),value,any::seqGet(seq,uSub)))) 
 
 Choices: sequences:on}
 -----------------------------------------------------
@@ -9697,7 +9697,7 @@ Choices: sequences:on}
 == getOfSeqUpd (getOfSeqUpd) =========================================
 getOfSeqUpd {
 \find(alpha::seqGet(seqUpd(seq,idx,value),jdx))
-\replacewith(if-then-else(and(and(leq(Z(0(#)),jdx),lt(jdx,seqLen(seq))),equals(idx,jdx)),alpha::cast(value),alpha::seqGet(seq,jdx)))
+\replacewith(if-then-else(and(and(leq(Z(0(#)),jdx),lt(jdx,seqLen(seq))),equals(idx,jdx)),alpha::cast(value),alpha::seqGet(seq,jdx))) 
 \heuristics(simplify_enlarging)
 Choices: sequences:on}
 -----------------------------------------------------
@@ -12135,7 +12135,7 @@ Choices: sequences:on}
 == lenOfSeqUpd (lenOfSeqUpd) =========================================
 lenOfSeqUpd {
 \find(seqLen(seqUpd(seq,idx,value)))
-\replacewith(seqLen(seq))
+\replacewith(seqLen(seq)) 
 \heuristics(simplify)
 Choices: sequences:on}
 -----------------------------------------------------
@@ -13516,7 +13516,7 @@ narrowingByteCastInt {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = (byte) #seInt;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seInt)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seInt)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -13525,7 +13525,7 @@ narrowingByteCastLong {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = (byte) #seLong;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seLong)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seLong)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -13534,7 +13534,7 @@ narrowingByteCastShort {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = (byte) #seShort;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seShort)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastByte(#seShort)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -13570,7 +13570,7 @@ narrowingCharCastByte {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = (char) #seByte;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seByte)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seByte)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -13579,7 +13579,7 @@ narrowingCharCastInt {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = (char) #seInt;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seInt)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seInt)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -13588,7 +13588,7 @@ narrowingCharCastLong {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = (char) #seLong;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seLong)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seLong)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -13597,7 +13597,7 @@ narrowingCharCastShort {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = (char) #seShort;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seShort)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastChar(#seShort)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -13615,7 +13615,7 @@ narrowingIntCastLong {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = (int) #seLong;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaCastInt(#seLong)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastInt(#seLong)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -13642,7 +13642,7 @@ narrowingShortCastInt {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = (short) #seInt;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seInt)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seInt)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -13651,7 +13651,7 @@ narrowingShortCastLong {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = (short) #seLong;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seLong)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaCastShort(#seLong)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -16555,7 +16555,7 @@ Choices: true}
 == ssubsortDirect (ssubsortDirect) =========================================
 ssubsortDirect {
 \find(ssubsort(alphSub::ssort,alph::ssort))
-\replacewith(true)
+\replacewith(true) 
 \heuristics(simplify)
 Choices: true}
 -----------------------------------------------------
@@ -16563,14 +16563,14 @@ Choices: true}
 ssubsortSup {
 \find(ssubsort(alph::ssort,alphSub::ssort))
 \varcond(\not\same(alphSub, alph))
-\replacewith(false)
+\replacewith(false) 
 \heuristics(simplify)
 Choices: true}
 -----------------------------------------------------
 == ssubsortTop (ssubsortTop) =========================================
 ssubsortTop {
 \find(ssubsort(s,anySORT))
-\replacewith(true)
+\replacewith(true) 
 \heuristics(simplify)
 Choices: true}
 -----------------------------------------------------
@@ -17071,8 +17071,8 @@ Choices: programRules:Java}
 -----------------------------------------------------
 == subsortTrans (subsortTrans) =========================================
 subsortTrans {
-\assumes ([ssubsort(s1,s2),ssubsort(s2,s3)]==>[])
-\add [ssubsort(s1,s3)]==>[]
+\assumes ([ssubsort(s1,s2),ssubsort(s2,s3)]==>[]) 
+\add [ssubsort(s1,s3)]==>[] 
 \heuristics(simplify_enlarging)
 Choices: true}
 -----------------------------------------------------
@@ -18209,7 +18209,7 @@ unaryMinusInt {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = -#seCharByteShortInt;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusInt(#seCharByteShortInt)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusInt(#seCharByteShortInt)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
@@ -18218,7 +18218,7 @@ unaryMinusLong {
 \find(#normalassign ((modal operator))|{{ ..
   #loc = -#seLong;
 ... }}| (post))
-\replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusLong(#seLong)),#normalassign(post))) 
+\sameUpdateLevel\replacewith(update-application(elem-update(#loc (program Variable))(javaUnaryMinusLong(#seLong)),#normalassign(post))) 
 \heuristics(executeIntegerAssignment)
 Choices: programRules:Java}
 -----------------------------------------------------
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/checkedOF/IntSemanticsCheckedOF.java b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/checkedOF/IntSemanticsCheckedOF.java
new file mode 100644
index 00000000000..15b37ab05f9
--- /dev/null
+++ b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/checkedOF/IntSemanticsCheckedOF.java
@@ -0,0 +1,21 @@
+/*@ code_safe_math @*/        // this is ignored by KeY currently, just for documentation
+/*@ spec_bigint_math @*/      // this is the default
+class IntSemanticsCheckedOF {
+
+    // provable with overflow check taclet option, since no overflow can occur with this precondition
+    /*@ normal_behavior
+      @  requires Integer.MIN_VALUE <= a + b <= Integer.MAX_VALUE;
+      @  ensures \result == a + b;
+      @*/
+    int mOFCheck(int a, int b) {
+        return a + b;
+    }
+
+    // not provable with overflow check taclet option (separate branch for overflow check stays open)
+    /*@ normal_behavior
+      @  ensures \result == a + b;
+      @*/
+    int mOFCheckWrong(int a, int b) {
+        return a + b;
+    }
+}
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/checkedOF/mOFCheck.proof b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/checkedOF/mOFCheck.proof
new file mode 100644
index 00000000000..e656a374036
--- /dev/null
+++ b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/checkedOF/mOFCheck.proof
@@ -0,0 +1,241 @@
+\profile "Java Profile";
+
+\settings // Proof-Settings-Config-File
+{ 
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:arithmeticSemanticsCheckingOF",
+        "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",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+     },
+    "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" : "JavaCardDLStrategy",
+        "MaximumNumberOfAutomaticApplications" : 7000,
+        "Timeout" : -1,
+        "options" : { 
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED",
+            "DEP_OPTIONS_KEY" : "DEP_ON",
+            "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
+            "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
+            "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_ON",
+            "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",
+            "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 ".";
+
+\proofObligation 
+// Proof-Obligation settings
+{ 
+    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
+    "contract" : "IntSemanticsCheckedOF[IntSemanticsCheckedOF::mOFCheck(int,int)].JML normal_behavior operation contract.0",
+    "name" : "IntSemanticsCheckedOF[IntSemanticsCheckedOF::mOFCheck(int,int)].JML normal_behavior operation contract.0"
+ }
+
+\proof {
+(keyLog "0" (keyUser "wolfram" ) (keyVersion "a442cdfee288a794b45d4bdc941b89bf985f3722"))
+
+(autoModeTime "940")
+
+(branch "dummy ID"
+ (builtin "One Step Simplification" (formula "1") (newnames "heapAtPre,o,f"))
+(rule "expandInRangeInt" (formula "1") (term "1,1,0,0,0"))
+(rule "expandInRangeInt" (formula "1") (term "0,1,0,0,0"))
+(rule "replace_int_MIN" (formula "1") (term "0,1,1,1,0,0,0"))
+(rule "replace_int_MAX" (formula "1") (term "1,0,1,1,0,0,0"))
+(rule "replace_int_MIN" (formula "1") (term "0,1,0,1,0,0,0"))
+(rule "replace_int_MAX" (formula "1") (term "1,0,0,1,0,0,0"))
+(rule "impRight" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "3"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "4"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "3"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "4"))
+(rule "andLeft" (formula "6"))
+(rule "andLeft" (formula "1"))
+(rule "notLeft" (formula "2"))
+(rule "inEqSimp_commuteLeq" (formula "5"))
+(rule "inEqSimp_commuteLeq" (formula "7"))
+(rule "inEqSimp_homoInEq0" (formula "10"))
+(rule "polySimp_mulComm0" (formula "10") (term "1,0"))
+(rule "polySimp_rightDist" (formula "10") (term "1,0"))
+(rule "polySimp_mulComm0" (formula "10") (term "0,1,0"))
+(rule "polySimp_addAssoc" (formula "10") (term "0"))
+(rule "inEqSimp_homoInEq0" (formula "9"))
+(rule "mul_literals" (formula "9") (term "1,0"))
+(rule "polySimp_addComm1" (formula "9") (term "0"))
+(rule "polySimp_addComm0" (formula "9") (term "0,0"))
+(rule "assignment" (formula "13") (term "1"))
+ (builtin "One Step Simplification" (formula "13"))
+(rule "inEqSimp_sepNegMonomial1" (formula "10"))
+(rule "polySimp_mulLiterals" (formula "10") (term "0"))
+(rule "polySimp_elimOne" (formula "10") (term "0"))
+(rule "inEqSimp_sepPosMonomial1" (formula "9"))
+(rule "polySimp_mulComm0" (formula "9") (term "1"))
+(rule "polySimp_rightDist" (formula "9") (term "1"))
+(rule "mul_literals" (formula "9") (term "0,1"))
+(rule "inEqSimp_exactShadow3" (formula "9") (ifseqformula "6"))
+(rule "polySimp_rightDist" (formula "9") (term "0,0"))
+(rule "polySimp_mulLiterals" (formula "9") (term "1,0,0"))
+(rule "mul_literals" (formula "9") (term "0,0,0"))
+(rule "polySimp_elimOne" (formula "9") (term "1,0,0"))
+(rule "polySimp_addComm1" (formula "9") (term "0"))
+(rule "add_literals" (formula "9") (term "0,0"))
+(rule "inEqSimp_sepPosMonomial1" (formula "9"))
+(rule "mul_literals" (formula "9") (term "1"))
+(rule "inEqSimp_subsumption1" (formula "9") (ifseqformula "5"))
+(rule "leq_literals" (formula "9") (term "0"))
+ (builtin "One Step Simplification" (formula "9"))
+(rule "true_left" (formula "9"))
+(rule "inEqSimp_exactShadow3" (formula "7") (ifseqformula "10"))
+(rule "mul_literals" (formula "7") (term "0,0"))
+(rule "polySimp_addAssoc" (formula "7") (term "0"))
+(rule "add_literals" (formula "7") (term "0,0"))
+(rule "inEqSimp_sepNegMonomial1" (formula "7"))
+(rule "polySimp_mulLiterals" (formula "7") (term "0"))
+(rule "polySimp_elimOne" (formula "7") (term "0"))
+(rule "inEqSimp_subsumption0" (formula "7") (ifseqformula "4"))
+(rule "leq_literals" (formula "7") (term "0"))
+ (builtin "One Step Simplification" (formula "7"))
+(rule "true_left" (formula "7"))
+(rule "methodBodyExpand" (formula "13") (term "1") (newnames "heapBefore_mOFCheck,savedHeapBefore_mOFCheck"))
+ (builtin "One Step Simplification" (formula "13"))
+(rule "returnUnfold" (formula "13") (term "1") (inst "#v0=i"))
+(rule "variableDeclarationAssign" (formula "13") (term "1"))
+(rule "variableDeclaration" (formula "13") (term "1") (newnames "i"))
+(rule "assignmentAdditionInt" (formula "13") (term "1"))
+(branch "Overflow check"
+    (builtin "One Step Simplification" (formula "13"))
+   (rule "expandInRangeInt" (formula "13"))
+   (rule "replace_int_MIN" (formula "13") (term "0,1"))
+   (rule "replace_int_MAX" (formula "13") (term "1,0"))
+   (rule "inEqSimp_homoInEq0" (formula "13") (term "1"))
+   (rule "mul_literals" (formula "13") (term "1,0,1"))
+   (rule "polySimp_addComm1" (formula "13") (term "0,1"))
+   (rule "polySimp_addComm0" (formula "13") (term "0,0,1"))
+   (rule "inEqSimp_homoInEq0" (formula "13") (term "0"))
+   (rule "polySimp_mulComm0" (formula "13") (term "1,0,0"))
+   (rule "polySimp_rightDist" (formula "13") (term "1,0,0"))
+   (rule "polySimp_mulComm0" (formula "13") (term "0,1,0,0"))
+   (rule "polySimp_addAssoc" (formula "13") (term "0,0"))
+   (rule "inEqSimp_sepPosMonomial1" (formula "13") (term "1"))
+   (rule "polySimp_mulComm0" (formula "13") (term "1,1"))
+   (rule "polySimp_rightDist" (formula "13") (term "1,1"))
+   (rule "mul_literals" (formula "13") (term "0,1,1"))
+   (rule "replace_known_left" (formula "13") (term "1") (ifseqformula "9"))
+    (builtin "One Step Simplification" (formula "13"))
+   (rule "inEqSimp_geqRight" (formula "13"))
+   (rule "times_zero_1" (formula "1") (term "1,0,0"))
+   (rule "add_zero_right" (formula "1") (term "0,0"))
+   (rule "polySimp_addAssoc" (formula "1") (term "0"))
+   (rule "polySimp_addAssoc" (formula "1") (term "0,0"))
+   (rule "add_literals" (formula "1") (term "0,0,0"))
+   (rule "inEqSimp_sepNegMonomial0" (formula "1"))
+   (rule "polySimp_mulLiterals" (formula "1") (term "0"))
+   (rule "polySimp_elimOne" (formula "1") (term "0"))
+   (rule "inEqSimp_subsumption1" (formula "10") (ifseqformula "1"))
+   (rule "inEqSimp_homoInEq0" (formula "10") (term "0"))
+   (rule "polySimp_mulComm0" (formula "10") (term "1,0,0"))
+   (rule "polySimp_rightDist" (formula "10") (term "1,0,0"))
+   (rule "mul_literals" (formula "10") (term "0,1,0,0"))
+   (rule "polySimp_mulLiterals" (formula "10") (term "1,1,0,0"))
+   (rule "polySimp_elimOne" (formula "10") (term "1,1,0,0"))
+   (rule "polySimp_addAssoc" (formula "10") (term "0,0"))
+   (rule "polySimp_addComm1" (formula "10") (term "0,0,0"))
+   (rule "add_literals" (formula "10") (term "0,0,0,0"))
+   (rule "polySimp_pullOutFactor2b" (formula "10") (term "0,0"))
+   (rule "add_literals" (formula "10") (term "1,1,0,0"))
+   (rule "times_zero_1" (formula "10") (term "1,0,0"))
+   (rule "add_zero_right" (formula "10") (term "0,0"))
+   (rule "qeq_literals" (formula "10") (term "0"))
+    (builtin "One Step Simplification" (formula "10"))
+   (rule "true_left" (formula "10"))
+   (rule "inEqSimp_contradInEq0" (formula "1") (ifseqformula "10"))
+   (rule "andLeft" (formula "1"))
+   (rule "inEqSimp_homoInEq1" (formula "1"))
+   (rule "polySimp_mulComm0" (formula "1") (term "1,0"))
+   (rule "polySimp_rightDist" (formula "1") (term "1,0"))
+   (rule "polySimp_mulLiterals" (formula "1") (term "1,1,0"))
+   (rule "mul_literals" (formula "1") (term "0,1,0"))
+   (rule "polySimp_elimOne" (formula "1") (term "1,1,0"))
+   (rule "polySimp_addAssoc" (formula "1") (term "0"))
+   (rule "polySimp_addComm1" (formula "1") (term "0,0"))
+   (rule "add_literals" (formula "1") (term "0,0,0"))
+   (rule "polySimp_pullOutFactor2b" (formula "1") (term "0"))
+   (rule "add_literals" (formula "1") (term "1,1,0"))
+   (rule "times_zero_1" (formula "1") (term "1,0"))
+   (rule "add_zero_right" (formula "1") (term "0"))
+   (rule "leq_literals" (formula "1"))
+   (rule "closeFalse" (formula "1"))
+)
+(branch "Case 2"
+    (builtin "One Step Simplification" (formula "13"))
+   (rule "translateJavaAddInt" (formula "13") (term "0,1,0"))
+   (rule "methodCallReturn" (formula "13") (term "1"))
+   (rule "assignment" (formula "13") (term "1"))
+    (builtin "One Step Simplification" (formula "13"))
+   (rule "methodCallEmpty" (formula "13") (term "1"))
+   (rule "tryEmpty" (formula "13") (term "1"))
+   (rule "emptyModality" (formula "13") (term "1"))
+    (builtin "One Step Simplification" (formula "13") (ifInst ""  (formula "11")))
+   (rule "closeTrue" (formula "13"))
+)
+)
+}
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/checkedOF/mOFCheckWrong.key b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/checkedOF/mOFCheckWrong.key
new file mode 100644
index 00000000000..487f88372d2
--- /dev/null
+++ b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/checkedOF/mOFCheckWrong.key
@@ -0,0 +1,28 @@
+\settings {
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:arithmeticSemanticsCheckingOF",
+        "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",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+    }
+}
+
+\javaSource ".";
+
+\chooseContract "IntSemanticsCheckedOF[IntSemanticsCheckedOF::mOFCheckWrong(int,int)].JML normal_behavior operation contract.0";
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/java/IntSemanticsJava.java b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/java/IntSemanticsJava.java
new file mode 100644
index 00000000000..d15fba954b9
--- /dev/null
+++ b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/java/IntSemanticsJava.java
@@ -0,0 +1,20 @@
+/*@ code_java_math @*/        // this is ignored by KeY currently, just for documentation
+/*@ spec_bigint_math @*/      // this is the default
+class IntSemanticsJava {
+
+    // provable with java integer semantics in code (wraparound of int)
+    /*@ normal_behavior
+      @  ensures \result == Integer.MIN_VALUE;
+      @*/
+    int mJava() {
+        return Integer.MAX_VALUE + 1;
+    }
+
+    // not provable with java integer semantics in code
+    /*@ normal_behavior
+      @  ensures \result == Integer.MAX_VALUE + 1;
+      @*/
+    int mJavaWrong() {
+        return Integer.MAX_VALUE + 1;
+    }
+}
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/java/intSemanticsJava.key b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/java/intSemanticsJava.key
new file mode 100644
index 00000000000..2f57bd54d2e
--- /dev/null
+++ b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/java/intSemanticsJava.key
@@ -0,0 +1,28 @@
+\settings {
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:javaSemantics",
+        "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",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+    }
+}
+
+\javaSource ".";
+
+\chooseContract
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/java/mJava.proof b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/java/mJava.proof
new file mode 100644
index 00000000000..6b1d128cfdf
--- /dev/null
+++ b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/java/mJava.proof
@@ -0,0 +1,132 @@
+\profile "Java Profile";
+
+\settings // Proof-Settings-Config-File
+{ 
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:javaSemantics",
+        "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",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+     },
+    "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" : "JavaCardDLStrategy",
+        "MaximumNumberOfAutomaticApplications" : 10000,
+        "Timeout" : -1,
+        "options" : { 
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED",
+            "DEP_OPTIONS_KEY" : "DEP_ON",
+            "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
+            "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
+            "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_ON",
+            "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",
+            "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 ".";
+
+\proofObligation 
+// Proof-Obligation settings
+{ 
+    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
+    "contract" : "IntSemanticsJava[IntSemanticsJava::mJava()].JML normal_behavior operation contract.0",
+    "name" : "IntSemanticsJava[IntSemanticsJava::mJava()].JML normal_behavior operation contract.0"
+ }
+
+\proof {
+(keyLog "0" (keyUser "wolfram" ) (keyVersion "7f892ecb2af976fa9780876087af8978f3eed91b"))
+
+(autoModeTime "147")
+
+(branch "dummy ID"
+ (builtin "One Step Simplification" (formula "1") (newnames "heapAtPre,o,f"))
+(rule "impRight" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "notLeft" (formula "2"))
+(rule "assignment" (formula "7"))
+(rule "methodBodyExpand" (formula "7") (term "1") (newnames "heapBefore_mJava,savedHeapBefore_mJava"))
+ (builtin "One Step Simplification" (formula "7"))
+(rule "returnUnfold" (formula "7") (term "1") (inst "#v0=i"))
+(rule "variableDeclarationAssign" (formula "7") (term "1"))
+(rule "variableDeclaration" (formula "7") (term "1") (newnames "i"))
+(rule "assignmentAdditionInt" (formula "7") (term "1"))
+ (builtin "One Step Simplification" (formula "7"))
+(rule "translateJavaAddInt" (formula "7") (term "0,1,0"))
+(rule "expand_addJint" (formula "7") (term "0,1,0"))
+(rule "add_literals" (formula "7") (term "0,0,1,0"))
+(rule "expand_moduloInteger" (formula "7") (term "0,1,0"))
+(rule "replace_int_RANGE" (formula "7") (term "1,1,0,1,0"))
+(rule "replace_int_HALFRANGE" (formula "7") (term "0,0,1,0,1,0"))
+(rule "replace_int_MIN" (formula "7") (term "0,0,1,0"))
+(rule "add_literals" (formula "7") (term "0,1,0,1,0"))
+(rule "mod_axiom" (formula "7") (term "1,0,1,0"))
+(rule "polySimp_mulLiterals" (formula "7") (term "1,1,0,1,0"))
+(rule "div_literals" (formula "7") (term "0,1,1,0,1,0"))
+(rule "mul_literals" (formula "7") (term "1,1,0,1,0"))
+(rule "add_literals" (formula "7") (term "1,0,1,0"))
+(rule "add_zero_right" (formula "7") (term "0,1,0"))
+(rule "methodCallReturn" (formula "7") (term "1"))
+(rule "assignment" (formula "7") (term "1"))
+ (builtin "One Step Simplification" (formula "7"))
+(rule "methodCallEmpty" (formula "7") (term "1"))
+(rule "tryEmpty" (formula "7") (term "1"))
+(rule "emptyModality" (formula "7") (term "1"))
+ (builtin "One Step Simplification" (formula "7") (ifInst ""  (formula "5")))
+(rule "closeTrue" (formula "7"))
+)
+}
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/java/mJavaWrong.key b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/java/mJavaWrong.key
new file mode 100644
index 00000000000..7dfbcaa6042
--- /dev/null
+++ b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/java/mJavaWrong.key
@@ -0,0 +1,28 @@
+\settings {
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:javaSemantics",
+        "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",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+    }
+}
+
+\javaSource ".";
+
+\chooseContract "IntSemanticsJava[IntSemanticsJava::mJavaWrong()].JML normal_behavior operation contract.0";
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/uncheckedOF/IntSemanticsUncheckedOF.java b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/uncheckedOF/IntSemanticsUncheckedOF.java
new file mode 100644
index 00000000000..8eb56eeaf71
--- /dev/null
+++ b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/uncheckedOF/IntSemanticsUncheckedOF.java
@@ -0,0 +1,20 @@
+/*@ code_bigint_math @*/      // this is ignored by KeY currently, just for documentation
+/*@ spec_bigint_math @*/      // this is the default
+class IntSemanticsUncheckedOF {
+
+    // provable with bigint semantics in code and in spec
+    /*@ normal_behavior
+      @  ensures \result == Integer.MAX_VALUE + 1;
+      @*/
+    int mBigint() {
+        return Integer.MAX_VALUE + 1;
+    }
+
+    // not provable with bigint semantics in code and in spec
+    /*@ normal_behavior
+      @  ensures \result == Integer.MIN_VALUE;
+      @*/
+    int mBigintWrong() {
+        return Integer.MAX_VALUE + 1;
+    }
+}
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/uncheckedOF/intSemanticsUncheckedOF.key b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/uncheckedOF/intSemanticsUncheckedOF.key
new file mode 100644
index 00000000000..2b1787d0531
--- /dev/null
+++ b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/uncheckedOF/intSemanticsUncheckedOF.key
@@ -0,0 +1,28 @@
+\settings {
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "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",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+    }
+}
+
+\javaSource ".";
+
+\chooseContract
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/uncheckedOF/mBigint.proof b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/uncheckedOF/mBigint.proof
new file mode 100644
index 00000000000..9a1f69c94e0
--- /dev/null
+++ b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/uncheckedOF/mBigint.proof
@@ -0,0 +1,121 @@
+\profile "Java Profile";
+
+\settings // Proof-Settings-Config-File
+{ 
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "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",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+     },
+    "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" : "JavaCardDLStrategy",
+        "MaximumNumberOfAutomaticApplications" : 10000,
+        "Timeout" : -1,
+        "options" : { 
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED",
+            "DEP_OPTIONS_KEY" : "DEP_ON",
+            "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
+            "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
+            "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_ON",
+            "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",
+            "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 ".";
+
+\proofObligation 
+// Proof-Obligation settings
+{ 
+    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
+    "contract" : "IntSemanticsUncheckedOF[IntSemanticsUncheckedOF::mBigint()].JML normal_behavior operation contract.0",
+    "name" : "IntSemanticsUncheckedOF[IntSemanticsUncheckedOF::mBigint()].JML normal_behavior operation contract.0"
+ }
+
+\proof {
+(keyLog "0" (keyUser "wolfram" ) (keyVersion "7f892ecb2af976fa9780876087af8978f3eed91b"))
+
+(autoModeTime "126")
+
+(branch "dummy ID"
+ (builtin "One Step Simplification" (formula "1") (newnames "heapAtPre,o,f"))
+(rule "add_literals" (formula "1") (term "1,0,0,0,1"))
+(rule "impRight" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "andLeft" (formula "1"))
+(rule "notLeft" (formula "2"))
+(rule "assignment" (formula "7"))
+(rule "methodBodyExpand" (formula "7") (term "1") (newnames "heapBefore_mBigint,savedHeapBefore_mBigint"))
+ (builtin "One Step Simplification" (formula "7"))
+(rule "returnUnfold" (formula "7") (term "1") (inst "#v0=i"))
+(rule "variableDeclarationAssign" (formula "7") (term "1"))
+(rule "variableDeclaration" (formula "7") (term "1") (newnames "i"))
+(rule "assignmentAdditionInt" (formula "7") (term "1"))
+ (builtin "One Step Simplification" (formula "7"))
+(rule "translateJavaAddInt" (formula "7") (term "0,1,0"))
+(rule "add_literals" (formula "7") (term "0,1,0"))
+(rule "methodCallReturn" (formula "7") (term "1"))
+(rule "assignment" (formula "7") (term "1"))
+ (builtin "One Step Simplification" (formula "7"))
+(rule "methodCallEmpty" (formula "7") (term "1"))
+(rule "tryEmpty" (formula "7") (term "1"))
+(rule "emptyModality" (formula "7") (term "1"))
+ (builtin "One Step Simplification" (formula "7") (ifInst ""  (formula "5")))
+(rule "closeTrue" (formula "7"))
+)
+}
diff --git a/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/uncheckedOF/mBigintWrong.key b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/uncheckedOF/mBigintWrong.key
new file mode 100644
index 00000000000..299ed6b8d2d
--- /dev/null
+++ b/key.core/src/test/resources/de/uka/ilkd/key/rule/intSemantics/uncheckedOF/mBigintWrong.key
@@ -0,0 +1,28 @@
+\settings {
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "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",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+    }
+}
+
+\javaSource ".";
+
+\chooseContract "IntSemanticsUncheckedOF[IntSemanticsUncheckedOF::mBigintWrong()].JML normal_behavior operation contract.0";