Skip to content

Commit 907f7b1

Browse files
authored
Fix NPE in dependency contract feature (caused by pulled out expression) (#3675)
2 parents c95c570 + c4179c2 commit 907f7b1

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DependencyContractFeature.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,9 @@ public final class DependencyContractFeature extends BinaryFeature {
3030
private void removePreviouslyUsedSteps(JTerm focus, Goal goal,
3131
List<PosInOccurrence> steps) {
3232
for (RuleApp app : goal.appliedRuleApps()) {
33-
JTerm term = (JTerm) app.posInOccurrence().subTerm();
3433
if (app.rule() instanceof UseDependencyContractRule
35-
&& RENAMING_TERM_PROPERTY.equalsModThisProperty(term, focus)) {
34+
&& RENAMING_TERM_PROPERTY.equalsModThisProperty(app.posInOccurrence().subTerm(),
35+
focus)) {
3636
final IBuiltInRuleApp bapp = (IBuiltInRuleApp) app;
3737
for (PosInOccurrence ifInst : bapp.assumesInsts()) {
3838
steps.remove(ifInst);

0 commit comments

Comments
 (0)