spotless fixes

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java

@@ -7,7 +7,6 @@
 import java.util.Arrays;
 import java.util.List;
 
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.FormulaTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabel;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java

@@ -77,7 +77,7 @@ public void updateLabels(TermLabelState state, Services services,
                 for (IfFormulaInstantiation ifInst : ta.ifFormulaInstantiations()) {
                     final Term assumesFml = ifInst.getConstrainedFormula();
                     FormulaTermLabel ifLabel = StayOnFormulaTermLabelPolicy.searchFormulaTermLabel(
-                            assumesFml.getLabels());
+                        assumesFml.getLabels());
                     if (ifLabel != null) {
                         ifLabels.put(ifInst.getConstrainedFormula(), ifLabel);
                     }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java

@@ -10,7 +10,6 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.FormulaTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelState;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java

@@ -15,7 +15,6 @@
 import de.uka.ilkd.key.java.reference.ReferencePrefix;
 import de.uka.ilkd.key.java.statement.MethodFrame;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.op.ElementaryUpdate;
 import de.uka.ilkd.key.logic.op.LocationVariable;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/CutHeapObjectsFeature.java

@@ -8,7 +8,6 @@
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.Equality;
 import de.uka.ilkd.key.logic.op.Junctor;
 import de.uka.ilkd.key.proof.Goal;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.symbolic_execution.strategy;
 
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.JavaProfile;
@@ -61,7 +60,8 @@ protected Feature setupApprovalF() {
                     TacletApp ta = (TacletApp) app;
                     if (ta.ifFormulaInstantiations() != null) {
                         for (IfFormulaInstantiation ifi : ta.ifFormulaInstantiations()) {
-                            if (ifi.getConstrainedFormula().containsLabel(SymbolicExecutionUtil.RESULT_LABEL)) {
+                            if (ifi.getConstrainedFormula()
+                                    .containsLabel(SymbolicExecutionUtil.RESULT_LABEL)) {
                                 hasLabel = true;
                             }
                         }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java

@@ -487,7 +487,7 @@ public static SiteProofVariableValueInput createExtractReturnVariableValueSequen
         Term modalityTerm = services.getTermBuilder().dia(newJavaBlock, newTerm);
         // Get the updates from the return node which includes the value interested in.
         Term originalModifiedFormula =
-                methodReturnNode.getAppliedRuleApp().posInOccurrence().sequentLevelFormula();
+            methodReturnNode.getAppliedRuleApp().posInOccurrence().sequentLevelFormula();
         ImmutableList<Term> originalUpdates =
             TermBuilder.goBelowUpdates2(originalModifiedFormula).first;
         // Create Sequent to prove with new succedent.
@@ -3053,7 +3053,8 @@ public static Sequent createSequentToProveWithNewSuccedent(Node node, PosInOccur
         }
         Sequent sequentToProve;
         sequentToProve = newSuccedentToProve != null ? originalSequentWithoutMethodFrame
-                .addFormula(newSuccedentToProve, false, true).sequent() : originalSequentWithoutMethodFrame;
+                .addFormula(newSuccedentToProve, false, true).sequent()
+                : originalSequentWithoutMethodFrame;
         if (additionalAntecedent != null) {
             sequentToProve = sequentToProve
                     .addFormula(additionalAntecedent, true, false).sequent();

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java

@@ -9,7 +9,6 @@
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.logic.JavaBlock;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.TermLabelManager;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.pp.PosTableLayouter;

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java

@@ -15,7 +15,6 @@
 import de.uka.ilkd.key.java.declaration.VariableSpecification;
 import de.uka.ilkd.key.ldt.HeapLDT;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/SelfcompositionStateExpansionMacro.java

@@ -70,7 +70,8 @@ protected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc) {
     protected boolean ruleApplicationInContextAllowed(RuleApp ruleApp, PosInOccurrence pio,
             Goal goal) {
         String ruleName = ruleApp.rule().name().toString();
-        if (!"andLeft".equals(ruleName)) return true;
+        if (!"andLeft".equals(ruleName))
+            return true;
         return !(pio.sequentLevelFormula().op() instanceof UpdateApplication);
     }
 

key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java

@@ -49,7 +49,7 @@ protected void addToAntec(Semisequent semi, TermLabelState termLabelState,
                 : "information flow taclets must have " + "exactly one add!";
         final Term replacement = replacements.iterator().next();
         updateStrategyInfo(services.getProof().openEnabledGoals().head(),
-                replacement);
+            replacement);
         super.addToAntec(semi, termLabelState, labelHint, currentSequent, pos,
             applicationPosInOccurrence, matchCond, goal, tacletApp, services);
     }

key.core/src/main/java/de/uka/ilkd/key/logic/Sequent.java

@@ -8,7 +8,6 @@
 import java.util.Set;
 
 import de.uka.ilkd.key.logic.label.TermLabel;
-import de.uka.ilkd.key.logic.op.QuantifiableVariable;
 
 import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;

key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java

@@ -6,7 +6,6 @@
 
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.TermLabelManager.TermLabelConfiguration;
 import de.uka.ilkd.key.logic.op.Modality;
 import de.uka.ilkd.key.proof.init.Profile;

key.core/src/main/java/de/uka/ilkd/key/macros/AbstractBlastingMacro.java

@@ -17,8 +17,8 @@
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Semisequent;
 import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.SortCollector;
+import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.op.Equality;
 import de.uka.ilkd.key.logic.op.JFunction;

key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java

@@ -694,7 +694,8 @@ public static String posInOccurrence2Proof(Sequent seq, PosInOccurrence pos) {
         if (pos == null) {
             return "";
         }
-        return " (formula \"" + seq.formulaNumberInSequent(pos.isInAntec(), pos.sequentLevelFormula())
+        return " (formula \""
+            + seq.formulaNumberInSequent(pos.isInAntec(), pos.sequentLevelFormula())
             + "\")" + posInTerm2Proof(pos.posInTerm());
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinIsApplicable.java

@@ -97,7 +97,8 @@ private ProspectivePartner areProspectivePartners(Goal g1, PosInOccurrence pio,
 
             }
             if (formula.equalsModProperty(referenceFormula, RENAMING_PROPERTY)) {
-                return new ProspectivePartner(referenceFormula, g1.node(), pio.sequentLevelFormula(),
+                return new ProspectivePartner(referenceFormula, g1.node(),
+                    pio.sequentLevelFormula(),
                     update1, g2.node(), sf, update2);
             }
         }

key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinProcessor.java

@@ -205,10 +205,10 @@ private Term createPhi() {
             partner.getSequent(1).antecedent(), partner.getCommonFormula());
         Term partnerFormula = partner.getFormula(0);
         Collection<Term> delta1 = computeDifference(partner.getSequent(0).succedent(), commonDelta,
-                partnerFormula);
+            partnerFormula);
         Term formula = partner.getFormula(1);
         Collection<Term> delta2 = computeDifference(partner.getSequent(1).succedent(), commonDelta,
-                formula);
+            formula);
 
         Collection<Term> gamma1 =
             computeDifference(partner.getSequent(0).antecedent(), commonGamma, null);

key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java

@@ -338,7 +338,7 @@ private PosInOccurrence findInNewSequent(PosInOccurrence oldPos, Sequent newSequ
                 : newSequent.succedent();
         for (Term newFormula : semiSeq.asList()) {
             if (newFormula.equalsModProperty(oldFormula,
-                    ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY)) {
+                ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY)) {
                 return oldPos.replaceConstrainedFormula(newFormula);
             }
         }

key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java

@@ -25,7 +25,6 @@
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
 import de.uka.ilkd.key.logic.label.ParameterlessTermLabel;

key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java

@@ -173,7 +173,8 @@ public boolean equalsModProofIrrelevancy(Object obj) {
     @Override
     public int hashCodeModProofIrrelevancy() {
         return Objects.hash(rule(), getHeapContext(),
-                ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(posInOccurrence().sequentLevelFormula()),
+            ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY
+                    .hashCodeModThisProperty(posInOccurrence().sequentLevelFormula()),
             posInOccurrence().posInTerm());
     }
 

key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java

@@ -1395,7 +1395,7 @@ public Term setUpValidityGoal(final Goal goal, final Term[] updates,
             if (goal != null) {
                 Term uAssumptions = tb.applySequential(updates, tb.and(assumptions));
                 goal.addFormula(
-                        uAssumptions, true,
+                    uAssumptions, true,
                     false);
 
                 ImmutableArray<TermLabel> labels = TermLabelManager.instantiateLabels(
@@ -1552,7 +1552,7 @@ public void setUpUsageGoal(final Goal goal, final Term[] updates,
             goal.addFormula(uAssumptions, true, false);
             Term uAssumptions1 = tb.applySequential(updates, buildUsageFormula(goal));
             goal.changeFormula(
-                    uAssumptions1,
+                uAssumptions1,
                 occurrence);
             TermLabelManager.refactorGoal(termLabelState, services, occurrence, application.rule(),
                 goal, null, null);

key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstantiation.java

@@ -5,8 +5,8 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Term;
-
 import de.uka.ilkd.key.logic.equality.ProofIrrelevancyProperty;
+
 import org.key_project.util.EqualsModProofIrrelevancy;
 
 
@@ -29,11 +29,12 @@ default boolean equalsModProofIrrelevancy(Object obj) {
             return false;
         }
         return getConstrainedFormula().equalsModProperty(that.getConstrainedFormula(),
-                ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY);
+            ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY);
     }
 
     @Override
     default int hashCodeModProofIrrelevancy() {
-        return getConstrainedFormula().hashCodeModProperty(ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY);
+        return getConstrainedFormula()
+                .hashCodeModProperty(ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY);
     }
 }

key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java

@@ -98,7 +98,7 @@ public class LoopApplyHeadRule implements BuiltInRule {
         Goal result = goal.split(1).head();
         Term uAssumptions = tb.apply(update, tb.prog(modality.kind(), newJavaBlock, target.sub(0)));
         result.changeFormula(
-                uAssumptions,
+            uAssumptions,
             ruleApp.pio);
         return ImmutableSLList.<Goal>nil().append(goal);
     }

key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java

@@ -22,7 +22,6 @@
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.ProgramPrefix;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.label.ParameterlessTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelManager;

key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java

@@ -195,7 +195,7 @@ private ImmutableList<Goal> applyForModelFields(Goal goal, ModelFieldInstantiati
             final Term actualSelfNotNull = tb.not(tb.equals(inst.receiver, tb.NULL()));
             Term uAssumptions = tb.apply(inst.update, actualSelfNotNull, null);
             nullGoal.changeFormula(
-                    uAssumptions,
+                uAssumptions,
                 ruleApp.posInOccurrence());
         }
 

key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java

@@ -409,9 +409,9 @@ private RuleApp makeReplaceKnownTacletApp(Term formula, boolean inAntecedent,
 
         PosInOccurrence applicatinPIO =
             new PosInOccurrence(formula, PosInTerm.getTopLevel(), // TODO: This
-                                                                                      // should be
-                                                                                      // the precise
-                                                                                      // sub term
+                                                                  // should be
+                                                                  // the precise
+                                                                  // sub term
                 inAntecedent); // It is required to create a new PosInOccurrence because formula and
                                // pio.constrainedFormula().formula() are only equals module
                                // renamings and term labels
@@ -465,15 +465,15 @@ private Instantiation computeInstantiation(Services services, PosInOccurrence os
             if (!ante.equals(cf)) {
                 if (ante.op() != Junctor.TRUE) {
                     context.put(new TermReplacementKey(ante),
-                            new PosInOccurrence(ante, PosInTerm.getTopLevel(), true));
+                        new PosInOccurrence(ante, PosInTerm.getTopLevel(), true));
                 }
             }
         }
         for (Term succ : seq.succedent()) {
             if (!succ.equals(cf)) {
                 if (succ.op() != Junctor.FALSE) {
                     context.put(new TermReplacementKey(succ),
-                            new PosInOccurrence(succ, PosInTerm.getTopLevel(), false));
+                        new PosInOccurrence(succ, PosInTerm.getTopLevel(), false));
                 }
             }
         }
@@ -575,7 +575,8 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) {
         }
 
         // applicable to the formula?
-        return applicableTo(goal.proof().getServices(), pio.sequentLevelFormula(), pio.isInAntec(), goal,
+        return applicableTo(goal.proof().getServices(), pio.sequentLevelFormula(), pio.isInAntec(),
+            goal,
             null);
     }
 

key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java

@@ -320,7 +320,8 @@ public boolean equalsModProofIrrelevancy(Object o) {
     @Override
     public int hashCodeModProofIrrelevancy() {
         return Objects.hash(super.hashCodeModProofIrrelevancy(),
-                ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(pos.sequentLevelFormula()),
+            ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY
+                    .hashCodeModThisProperty(pos.sequentLevelFormula()),
             pos.posInTerm());
     }
 

key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java

@@ -498,8 +498,9 @@ public boolean equalsModProofIrrelevancy(Object o) {
             while (!if1.isEmpty() && !if2.isEmpty()) {
                 Term term = if1.head();
                 Term head = if2.head();
-                if (!(boolean) ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.
-                        equalsModThisProperty(term, head)) break;
+                if (!(boolean) ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY
+                        .equalsModThisProperty(term, head))
+                    break;
                 if1 = if1.tail();
                 if2 = if2.tail();
             }
@@ -534,7 +535,8 @@ public int hashCode() {
     public int hashCodeModProofIrrelevancy() {
         if (hashcode2 == 0) {
             Term term = ifSequent.getFormulabyNr(1);
-            hashcode2 = ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(term);
+            hashcode2 =
+                ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(term);
             if (hashcode2 == 0) {
                 hashcode2 = -1;
             }
@@ -960,7 +962,7 @@ public enum TacletOperation {
      */
     @Override
     public @NonNull ImmutableList<Goal> apply(Goal goal, Services services, RuleApp tacletApp) {
-        return getExecutor().apply((Goal)goal, services, tacletApp);
+        return getExecutor().apply((Goal) goal, services, tacletApp);
     }
 
     public TacletExecutor<? extends Taclet> getExecutor() {

key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java

@@ -35,7 +35,6 @@
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
 import de.uka.ilkd.key.logic.label.ParameterlessTermLabel;
@@ -624,7 +623,7 @@ private void prepareBodyPreservesBranch(TermLabelState termLabelState, Services
 
         Term uAssumptions = tb.applySequential(uBeforeLoopDefAnonVariant, guardTrueBody);
         bodyGoal.changeFormula(
-                uAssumptions,
+            uAssumptions,
             ruleApp.posInOccurrence());
     }
 

key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelMerger.java

@@ -8,7 +8,6 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelManager;
 

key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelRefactoring.java

@@ -7,7 +7,6 @@
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.label.LabelCollection;
 import de.uka.ilkd.key.logic.label.TermLabel;

key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java

@@ -209,7 +209,7 @@ public final MatchConditions matchIf(Iterable<IfFormulaInstantiation> p_toMatch,
             assert itIfSequent.hasNext()
                     : "p_toMatch and assumes sequent must have same number of elements";
             newMC = matchIf(ImmutableSLList.<IfFormulaInstantiation>nil().prepend(candidateInst),
-                    itIfSequent.next(), p_matchCond, p_services).getMatchConditions();
+                itIfSequent.next(), p_matchCond, p_services).getMatchConditions();
 
             if (newMC.isEmpty()) {
                 return null;

key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java

@@ -15,7 +15,6 @@
 import de.uka.ilkd.key.logic.PosInTerm;
 import de.uka.ilkd.key.logic.Semisequent;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.TermServices;
 import de.uka.ilkd.key.logic.op.*;