KeYProject · wadoon · Mar 31, 2024 · Mar 31, 2024 · Apr 4, 2024 · Apr 4, 2024
diff --git a/build.gradle b/build.gradle
@@ -64,9 +64,12 @@ subprojects {
 
     repositories {
         mavenCentral()
-        maven {
+        maven { // cleary if needed?!
             url 'https://git.key-project.org/api/v4/projects/35/packages/maven'
         }
+        maven { // remove if docking frames 1.1.3p2 on Maven Central
+            url "https://s01.oss.sonatype.org/content/repositories/snapshots/"
+        }
     }
 
     dependencies {
@@ -77,8 +80,6 @@ subprojects {
         testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.2'
         testImplementation project(':key.util')
 
-        testCompileOnly 'junit:junit:4.13.2'
-        testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.2'
         testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.2'
 
         implementation("org.jspecify:jspecify:0.3.0")

diff --git a/key.core.example/src/main/java/module-info.java b/key.core.example/src/main/java/module-info.java
@@ -0,0 +1,10 @@
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (31.03.24)
+ */
+module org.key_project.core.example {
+    requires org.key_project.core;
+    requires org.key_project.util;
+    requires org.slf4j;
+}
diff --git a/key.core.proof_references/src/main/java/module-info.java b/key.core.proof_references/src/main/java/module-info.java
@@ -0,0 +1,10 @@
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (31.03.24)
+ */
+module org.key_project.proof_references {
+    requires org.key_project.core;
+    requires org.key_project.ncore;
+    requires org.key_project.util;
+}
diff --git a/key.core.rifl/src/main/java/module-info.java b/key.core.rifl/src/main/java/module-info.java
@@ -0,0 +1,13 @@
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (31.03.24)
+ */
+module org.key_project.core.rifl {
+    exports de.uka.ilkd.key.util.rifl;
+    requires org.key_project.core;
+    requires key.recoder;
+    requires java.xml;
+    requires org.slf4j;
+    requires org.key_project.util;
+}
diff --git a/key.core.symbolic_execution.example/src/main/java/module-info.java b/key.core.symbolic_execution.example/src/main/java/module-info.java
@@ -0,0 +1,11 @@
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (31.03.24)
+ */
+module key.core.symbolic_execution.example {
+    requires transitive org.key_project.symbolic_execution;
+    requires org.key_project.core;
+    requires org.key_project.util;
+    requires org.slf4j;
+}
diff --git a/...BlockContractValidityTermLabelUpdate.java → ...BlockContractValidityTermLabelUpdate.java b/...BlockContractValidityTermLabelUpdate.java → ...BlockContractValidityTermLabelUpdate.java
@@ -1,7 +1,7 @@
 /* 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.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.Set;
 
@@ -15,6 +15,7 @@
 import de.uka.ilkd.key.rule.LoopContractInternalRule;
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.RuleApp;
+import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
 import org.key_project.logic.Name;

diff --git a/...ey/rule/label/FormulaTermLabelMerger.java → ...ecution/label/FormulaTermLabelMerger.java b/...ey/rule/label/FormulaTermLabelMerger.java → ...ecution/label/FormulaTermLabelMerger.java
@@ -1,7 +1,7 @@
 /* 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.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.ArrayList;
 import java.util.Arrays;
@@ -11,6 +11,7 @@
 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.rule.label.TermLabelMerger;
 
 /**
  * The {@link TermLabelMerger} used to merge {@link FormulaTermLabel}s.

diff --git a/...le/label/FormulaTermLabelRefactoring.java → ...on/label/FormulaTermLabelRefactoring.java b/...le/label/FormulaTermLabelRefactoring.java → ...on/label/FormulaTermLabelRefactoring.java
@@ -1,7 +1,7 @@
 /* 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.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.*;
 
@@ -15,6 +15,8 @@
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor;
+import de.uka.ilkd.key.rule.label.StayOnOperatorTermLabelPolicy;
+import de.uka.ilkd.key.rule.label.TermLabelRefactoring;
 import de.uka.ilkd.key.rule.merge.CloseAfterMerge;
 import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;
 

diff --git a/...ey/rule/label/FormulaTermLabelUpdate.java → ...ecution/label/FormulaTermLabelUpdate.java b/...ey/rule/label/FormulaTermLabelUpdate.java → ...ecution/label/FormulaTermLabelUpdate.java
@@ -1,7 +1,7 @@
 /* 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.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.Collections;
 import java.util.LinkedHashMap;
@@ -21,6 +21,7 @@
 import de.uka.ilkd.key.rule.Taclet.TacletLabelHint;
 import de.uka.ilkd.key.rule.Taclet.TacletLabelHint.TacletOperation;
 import de.uka.ilkd.key.rule.TacletApp;
+import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;
 
 import org.key_project.logic.Name;

diff --git a/...y/rule/label/LoopBodyTermLabelUpdate.java → ...cution/label/LoopBodyTermLabelUpdate.java b/...y/rule/label/LoopBodyTermLabelUpdate.java → ...cution/label/LoopBodyTermLabelUpdate.java
@@ -1,7 +1,7 @@
 /* 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.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.Set;
 
@@ -13,6 +13,7 @@
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.rule.WhileInvariantRule;
+import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
 import org.key_project.logic.Name;

diff --git a/...variantNormalBehaviorTermLabelUpdate.java → ...variantNormalBehaviorTermLabelUpdate.java b/...variantNormalBehaviorTermLabelUpdate.java → ...variantNormalBehaviorTermLabelUpdate.java
@@ -1,7 +1,7 @@
 /* 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.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.Set;
 
@@ -13,6 +13,7 @@
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.rule.WhileInvariantRule;
+import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
 import org.key_project.logic.Name;

diff --git a/...eInCheckBranchesTermLabelRefactoring.java → ...eInCheckBranchesTermLabelRefactoring.java b/...eInCheckBranchesTermLabelRefactoring.java → ...eInCheckBranchesTermLabelRefactoring.java
@@ -1,7 +1,7 @@
 /* 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.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.PosInOccurrence;
@@ -18,6 +18,7 @@
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.UseOperationContractRule;
 import de.uka.ilkd.key.rule.WhileInvariantRule;
+import de.uka.ilkd.key.rule.label.TermLabelRefactoring;
 
 import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;

diff --git a/...e/label/StayOnFormulaTermLabelPolicy.java → ...n/label/StayOnFormulaTermLabelPolicy.java b/...e/label/StayOnFormulaTermLabelPolicy.java → ...n/label/StayOnFormulaTermLabelPolicy.java
@@ -1,7 +1,7 @@
 /* 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.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.Deque;
 import java.util.LinkedHashSet;
@@ -18,6 +18,7 @@
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.Taclet.TacletLabelHint;
 import de.uka.ilkd.key.rule.Taclet.TacletLabelHint.TacletOperation;
+import de.uka.ilkd.key.rule.label.TermLabelPolicy;
 import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;
 
 import org.key_project.util.collection.ImmutableArray;

diff --git a/...bel/SymbolicExecutionTermLabelUpdate.java → ...bel/SymbolicExecutionTermLabelUpdate.java b/...bel/SymbolicExecutionTermLabelUpdate.java → ...bel/SymbolicExecutionTermLabelUpdate.java
@@ -1,7 +1,7 @@
 /* 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.label;
+package de.uka.ilkd.key.symbolic_execution.label;
 
 import java.util.Set;
 
@@ -12,6 +12,7 @@
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelState;
 import de.uka.ilkd.key.rule.*;
+import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 
 import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;

diff --git a/...ecution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionTermination.java b/...ecution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionTermination.java
@@ -8,7 +8,6 @@
 import de.uka.ilkd.key.logic.op.IProgramVariable;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.symbolic_execution.SymbolicExecutionTreeBuilder;
-import de.uka.ilkd.key.symbolic_execution.model.impl.ExecutionTermination;
 
 import org.key_project.logic.sort.Sort;
 
@@ -19,7 +18,9 @@
  * in case of exceptional termination.
  * </p>
  * <p>
- * The default implementation is {@link ExecutionTermination} which is instantiated via a
+ * The default implementation is
+ * {@link de.uka.ilkd.key.symbolic_execution.model.impl.ExecutionTermination}
+ * which is instantiated via a
  * {@link SymbolicExecutionTreeBuilder} instance.
  * </p>
  *

diff --git a/...rc/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java b/...rc/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java
@@ -18,20 +18,20 @@
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.prover.GoalChooserBuilder;
 import de.uka.ilkd.key.rule.BuiltInRule;
-import de.uka.ilkd.key.rule.label.BlockContractValidityTermLabelUpdate;
-import de.uka.ilkd.key.rule.label.FormulaTermLabelMerger;
-import de.uka.ilkd.key.rule.label.FormulaTermLabelRefactoring;
-import de.uka.ilkd.key.rule.label.FormulaTermLabelUpdate;
-import de.uka.ilkd.key.rule.label.LoopBodyTermLabelUpdate;
-import de.uka.ilkd.key.rule.label.LoopInvariantNormalBehaviorTermLabelUpdate;
-import de.uka.ilkd.key.rule.label.RemoveInCheckBranchesTermLabelRefactoring;
-import de.uka.ilkd.key.rule.label.StayOnFormulaTermLabelPolicy;
 import de.uka.ilkd.key.rule.label.StayOnOperatorTermLabelPolicy;
-import de.uka.ilkd.key.rule.label.SymbolicExecutionTermLabelUpdate;
 import de.uka.ilkd.key.rule.label.TermLabelPolicy;
 import de.uka.ilkd.key.rule.label.TermLabelRefactoring;
 import de.uka.ilkd.key.rule.label.TermLabelUpdate;
 import de.uka.ilkd.key.strategy.StrategyFactory;
+import de.uka.ilkd.key.symbolic_execution.label.BlockContractValidityTermLabelUpdate;
+import de.uka.ilkd.key.symbolic_execution.label.FormulaTermLabelMerger;
+import de.uka.ilkd.key.symbolic_execution.label.FormulaTermLabelRefactoring;
+import de.uka.ilkd.key.symbolic_execution.label.FormulaTermLabelUpdate;
+import de.uka.ilkd.key.symbolic_execution.label.LoopBodyTermLabelUpdate;
+import de.uka.ilkd.key.symbolic_execution.label.LoopInvariantNormalBehaviorTermLabelUpdate;
+import de.uka.ilkd.key.symbolic_execution.label.RemoveInCheckBranchesTermLabelRefactoring;
+import de.uka.ilkd.key.symbolic_execution.label.StayOnFormulaTermLabelPolicy;
+import de.uka.ilkd.key.symbolic_execution.label.SymbolicExecutionTermLabelUpdate;
 import de.uka.ilkd.key.symbolic_execution.rule.ModalitySideProofRule;
 import de.uka.ilkd.key.symbolic_execution.rule.QuerySideProofRule;
 import de.uka.ilkd.key.symbolic_execution.strategy.SymbolicExecutionGoalChooserBuilder;

diff --git a/...orKeepUpdatesForBreakpointconditions.java → ...orKeepUpdatesForBreakpointconditions.java b/...orKeepUpdatesForBreakpointconditions.java → ...orKeepUpdatesForBreakpointconditions.java
@@ -1,13 +1,14 @@
 /* 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.proof;
+package de.uka.ilkd.key.symbolic_execution.proof;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.LocationVariable;
 import de.uka.ilkd.key.logic.op.Modality;
-import de.uka.ilkd.key.strategy.IBreakpointStopCondition;
+import de.uka.ilkd.key.proof.TermProgramVariableCollector;
+import de.uka.ilkd.key.symbolic_execution.strategy.IBreakpointStopCondition;
 import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractConditionalBreakpoint;
 import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.IBreakpoint;
 

diff --git a/...on/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/BreakpointStopCondition.java b/...on/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/BreakpointStopCondition.java
@@ -15,7 +15,6 @@
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.prover.impl.SingleRuleApplicationInfo;
 import de.uka.ilkd.key.rule.RuleApp;
-import de.uka.ilkd.key.strategy.IBreakpointStopCondition;
 import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.IBreakpoint;
 
 /**

diff --git a/...ey/strategy/IBreakpointStopCondition.java → ...on/strategy/IBreakpointStopCondition.java b/...ey/strategy/IBreakpointStopCondition.java → ...on/strategy/IBreakpointStopCondition.java
@@ -1,7 +1,7 @@
 /* This file is part of KeY - https://key-project.org
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
-package de.uka.ilkd.key.strategy;
+package de.uka.ilkd.key.symbolic_execution.strategy;
 
 import java.util.Set;
 

diff --git a/...de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionBreakpointStopCondition.java b/...de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionBreakpointStopCondition.java
@@ -14,7 +14,6 @@
 import de.uka.ilkd.key.proof.NodeInfo;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.rule.RuleApp;
-import de.uka.ilkd.key.strategy.IBreakpointStopCondition;
 import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.IBreakpoint;
 
 /**

diff --git a/key.core.symbolic_execution/src/main/java/module-info.java b/key.core.symbolic_execution/src/main/java/module-info.java
@@ -0,0 +1,13 @@
+import de.uka.ilkd.key.proof.init.DefaultProfileResolver;
+import de.uka.ilkd.key.proof.init.POExtension;
+import de.uka.ilkd.key.symbolic_execution.po.TruthValuePOExtension;
+import de.uka.ilkd.key.symbolic_execution.profile.SymbolicExecutionJavaProfileDefaultProfileResolver;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (31.03.24)
+ */
+module org.key_project.symbolic_execution{exports de.uka.ilkd.key.symbolic_execution;exports de.uka.ilkd.key.symbolic_execution.model;exports de.uka.ilkd.key.symbolic_execution.po;exports de.uka.ilkd.key.symbolic_execution.profile;exports de.uka.ilkd.key.symbolic_execution.strategy;exports de.uka.ilkd.key.symbolic_execution.strategy.breakpoint;exports de.uka.ilkd.key.symbolic_execution.util;requires java.xml;requires org.key_project.core;requires org.key_project.ncore;requires org.key_project.util;requires java.desktop;requires org.slf4j;requires org.jspecify;
+
+provides DefaultProfileResolver with SymbolicExecutionJavaProfileDefaultProfileResolver;provides POExtension with TruthValuePOExtension;}
diff --git a/...t/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java b/...t/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java
@@ -20,7 +20,6 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
-import de.uka.ilkd.key.proof.TermProgramVariableCollectorKeepUpdatesForBreakpointconditions;
 import de.uka.ilkd.key.proof.init.FunctionalOperationContractPO;
 import de.uka.ilkd.key.proof.init.ProofInputException;
 import de.uka.ilkd.key.proof.init.ProofOblInput;
@@ -39,6 +38,7 @@
 import de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO;
 import de.uka.ilkd.key.symbolic_execution.po.ProgramMethodSubsetPO;
 import de.uka.ilkd.key.symbolic_execution.profile.SymbolicExecutionJavaProfile;
+import de.uka.ilkd.key.symbolic_execution.proof.TermProgramVariableCollectorKeepUpdatesForBreakpointconditions;
 import de.uka.ilkd.key.symbolic_execution.strategy.*;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;

diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java
@@ -21,12 +21,12 @@
 import de.uka.ilkd.key.settings.ProofDependentSMTSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSMTSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
-import de.uka.ilkd.key.settings.TestGenerationSettings;
 import de.uka.ilkd.key.smt.*;
 import de.uka.ilkd.key.smt.lang.SMTSort;
 import de.uka.ilkd.key.smt.model.Model;
 import de.uka.ilkd.key.smt.solvertypes.SolverType;
 import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
+import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;

diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java
@@ -20,15 +20,15 @@
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
-import de.uka.ilkd.key.settings.TestGenerationSettings;
 import de.uka.ilkd.key.smt.SMTSolver;
 import de.uka.ilkd.key.smt.model.Heap;
 import de.uka.ilkd.key.smt.model.Model;
 import de.uka.ilkd.key.smt.model.ObjectVal;
-import de.uka.ilkd.key.smt.testgen.TestGenerationLog;
 import de.uka.ilkd.key.testgen.oracle.OracleGenerator;
 import de.uka.ilkd.key.testgen.oracle.OracleMethod;
 import de.uka.ilkd.key.testgen.oracle.OracleMethodCall;
+import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
+import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLog;
 import de.uka.ilkd.key.util.KeYConstants;
 
 import org.key_project.logic.op.Function;

diff --git a/...kd/key/macros/SemanticsBlastingMacro.java → ...estgen/macros/SemanticsBlastingMacro.java b/...kd/key/macros/SemanticsBlastingMacro.java → ...estgen/macros/SemanticsBlastingMacro.java
@@ -1,11 +1,12 @@
 /* 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.macros;
+package de.uka.ilkd.key.testgen.macros;
 
 import java.util.HashSet;
 import java.util.Set;
 
+import de.uka.ilkd.key.macros.AbstractBlastingMacro;
 import de.uka.ilkd.key.proof.rulefilter.RuleFilter;
 import de.uka.ilkd.key.rule.Rule;