Skip to content

Commit b5cbe61

Browse files
committed
Revert "small addition to the bugfix for #1336, avoiding NPE"
This reverts commit c52e5a7.
1 parent 7ff4584 commit b5cbe61

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

system/src/de/uka/ilkd/key/proof/Goal.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -621,7 +621,7 @@ public ImmutableList<Goal> apply( RuleApp p_ruleApp ) {
621621
MatchConditions newConditions = rwt.checkPrefix(ruleApp.posInOccurrence(),
622622
MatchConditions.EMPTY_MATCHCONDITIONS, proof.getServices());
623623
if(newConditions == null) {
624-
throw new RuntimeException("taclet application with unsatisfied 'checkPrefix': "
624+
throw new RuntimeException("taclet application with unsatisfied 'checkPrefix': "
625625
+ ruleApp);
626626
}
627627

system/src/de/uka/ilkd/key/strategy/TacletAppContainer.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -318,7 +318,7 @@ public RuleApp completeRuleApp(Goal p_goal, Strategy strategy) {
318318
if ( !app.complete() )
319319
app = app.tryToInstantiate ( services );
320320

321-
Taclet taclet = app.taclet();
321+
Taclet taclet = app == null ? null : app.taclet();
322322
if (taclet instanceof RewriteTaclet) {
323323
RewriteTaclet rwtaclet = (RewriteTaclet) taclet;
324324
MatchConditions check =

0 commit comments

Comments
 (0)