For-each loop on Set or List gives error "Given operator is null."

[FliegendeWurst]

Description

Trying to prove a loop invariant on a for each loop that iterates over a set fails with an error message.
The loop invariant uses \index, perhaps that is not supported on types other than arrays.

Reproducible

always

Steps to reproduce

1. Load the file below
2. Run auto mode

import java.util.Set;

public class SetCount {
    /*@ public normal_behaviour
      @ ensures \result == a.seq.length;
      @*/
    int setSize(Set a) {
        int count = 0;
        /*@ loop_invariant
          @ 0 <= \index && \index <= a.seq.length
          @  && \index == count;
          @ decreases a.seq.length - \index;
          @*/
        for (Object x : a) {
            count++;
        }
        return count;
    }
}

What is your expected behavior and what was the actual behavior?

Expected: no error, for-each (enhanced for) rule is either applicable or not.
Actual: error message "Given operator is null."

Additional information

Stack trace

org.key_project.logic.TermCreationException: Given operator is null.
	at de.uka.ilkd.key.logic.TermFactory.createTerm(TermFactory.java:62)
	at de.uka.ilkd.key.logic.TermFactory.createTerm(TermFactory.java:79)
	at de.uka.ilkd.key.logic.TermBuilder.var(TermBuilder.java:381)
	at de.uka.ilkd.key.rule.metaconstruct.EnhancedForElimination.lambda$updateInvs$8(EnhancedForElimination.java:395)
	at de.uka.ilkd.key.logic.GenericTermReplacer.replace(GenericTermReplacer.java:23)
	at de.uka.ilkd.key.logic.GenericTermReplacer.lambda$replace$0(GenericTermReplacer.java:27)
	at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
	at java.base/java.util.Iterator.forEachRemaining(Iterator.java:133)
	at java.base/java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1939)
	at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
	at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
	at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:575)
	at java.base/java.util.stream.AbstractPipeline.evaluateToArrayNode(AbstractPipeline.java:260)
	at java.base/java.util.stream.ReferencePipeline.toArray(ReferencePipeline.java:616)
	at de.uka.ilkd.key.logic.GenericTermReplacer.replace(GenericTermReplacer.java:28)
	at de.uka.ilkd.key.logic.GenericTermReplacer.lambda$replace$0(GenericTermReplacer.java:27)
	at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
	at java.base/java.util.Iterator.forEachRemaining(Iterator.java:133)
	at java.base/java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1939)
	at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
	at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
	at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:575)
	at java.base/java.util.stream.AbstractPipeline.evaluateToArrayNode(AbstractPipeline.java:260)
	at java.base/java.util.stream.ReferencePipeline.toArray(ReferencePipeline.java:616)
	at de.uka.ilkd.key.logic.GenericTermReplacer.replace(GenericTermReplacer.java:28)
	at de.uka.ilkd.key.logic.GenericTermReplacer.lambda$replace$0(GenericTermReplacer.java:27)
	at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
	at java.base/java.util.Iterator.forEachRemaining(Iterator.java:133)
	at java.base/java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1939)
	at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
	at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
	at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:575)
	at java.base/java.util.stream.AbstractPipeline.evaluateToArrayNode(AbstractPipeline.java:260)
	at java.base/java.util.stream.ReferencePipeline.toArray(ReferencePipeline.java:616)
	at de.uka.ilkd.key.logic.GenericTermReplacer.replace(GenericTermReplacer.java:28)
	at de.uka.ilkd.key.rule.metaconstruct.EnhancedForElimination.lambda$updateInvs$9(EnhancedForElimination.java:394)
	at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
	at java.base/java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:179)
	at java.base/java.util.Iterator.forEachRemaining(Iterator.java:133)
	at java.base/java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1939)
	at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
	at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
	at java.base/java.util.stream.ForEachOps$ForEachOp.evaluateSequential(ForEachOps.java:151)
	at java.base/java.util.stream.ForEachOps$ForEachOp$OfRef.evaluateSequential(ForEachOps.java:174)
	at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
	at java.base/java.util.stream.ReferencePipeline.forEach(ReferencePipeline.java:596)
	at de.uka.ilkd.key.rule.metaconstruct.EnhancedForElimination.updateInvs(EnhancedForElimination.java:396)
	at de.uka.ilkd.key.rule.metaconstruct.EnhancedForElimination.instantiateIndexValues(EnhancedForElimination.java:364)
	at de.uka.ilkd.key.rule.metaconstruct.EnhancedForElimination.setInvariant(EnhancedForElimination.java:330)
	at de.uka.ilkd.key.rule.metaconstruct.EnhancedForElimination.makeIterableForLoop(EnhancedForElimination.java:281)
	at de.uka.ilkd.key.rule.metaconstruct.EnhancedForElimination.doTransform(EnhancedForElimination.java:165)
	at de.uka.ilkd.key.rule.metaconstruct.EnhancedForElimination.transform(EnhancedForElimination.java:142)
	at de.uka.ilkd.key.java.visitor.ProgramReplaceVisitor.performActionOnProgramMetaConstruct(ProgramReplaceVisitor.java:108)
	at de.uka.ilkd.key.rule.metaconstruct.ProgramTransformer.visit(ProgramTransformer.java:206)
	at de.uka.ilkd.key.java.visitor.JavaASTVisitor.doAction(JavaASTVisitor.java:88)
	at de.uka.ilkd.key.java.visitor.JavaASTWalker.walk(JavaASTWalker.java:74)
	at de.uka.ilkd.key.java.visitor.JavaASTVisitor.walk(JavaASTVisitor.java:57)
	at de.uka.ilkd.key.java.visitor.CreatingASTVisitor.walk(CreatingASTVisitor.java:60)
	at de.uka.ilkd.key.java.visitor.JavaASTWalker.walk(JavaASTWalker.java:68)
	at de.uka.ilkd.key.java.visitor.JavaASTVisitor.walk(JavaASTVisitor.java:57)
	at de.uka.ilkd.key.java.visitor.CreatingASTVisitor.walk(CreatingASTVisitor.java:60)
	at de.uka.ilkd.key.java.visitor.ProgramReplaceVisitor.start(ProgramReplaceVisitor.java:48)
	at de.uka.ilkd.key.rule.SyntacticalReplaceVisitor.replacePrg(SyntacticalReplaceVisitor.java:205)
	at de.uka.ilkd.key.rule.SyntacticalReplaceVisitor.visit(SyntacticalReplaceVisitor.java:352)
	at de.uka.ilkd.key.logic.TermImpl.execPostOrder(TermImpl.java:287)
	at de.uka.ilkd.key.rule.executor.javadl.TacletExecutor.syntacticalReplace(TacletExecutor.java:99)
	at de.uka.ilkd.key.rule.executor.javadl.RewriteTacletExecutor.replace(RewriteTacletExecutor.java:56)
	at de.uka.ilkd.key.rule.executor.javadl.RewriteTacletExecutor.replace(RewriteTacletExecutor.java:49)
	at de.uka.ilkd.key.rule.executor.javadl.RewriteTacletExecutor.applyReplacewithHelper(RewriteTacletExecutor.java:77)
	at de.uka.ilkd.key.rule.executor.javadl.RewriteTacletExecutor.applyReplacewith(RewriteTacletExecutor.java:114)
	at de.uka.ilkd.key.rule.executor.javadl.FindTacletExecutor.apply(FindTacletExecutor.java:112)
	at de.uka.ilkd.key.rule.executor.javadl.FindTacletExecutor.apply(FindTacletExecutor.java:25)
	at de.uka.ilkd.key.proof.Goal.apply(Goal.java:635)
	at org.key_project.prover.engine.impl.DefaultProver.applyAutomaticRule(DefaultProver.java:185)
	at org.key_project.prover.engine.impl.DefaultProver.doWork(DefaultProver.java:103)
	at de.uka.ilkd.key.prover.impl.ApplyStrategy.executeStrategy(ApplyStrategy.java:164)
	at de.uka.ilkd.key.prover.impl.ApplyStrategy.start(ApplyStrategy.java:132)
	at de.uka.ilkd.key.ui.MediatorProofControl$AutoModeWorker.doInBackground(MediatorProofControl.java:223)
	at de.uka.ilkd.key.ui.MediatorProofControl$AutoModeWorker.doInBackground(MediatorProofControl.java:156)
	at java.desktop/javax.swing.SwingWorker$1.call(SwingWorker.java:305)
	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
	at java.desktop/javax.swing.SwingWorker.run(SwingWorker.java:342)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
	at java.base/java.lang.Thread.run(Thread.java:1583)

---

• Commit: c95c570

[FliegendeWurst]

The same issue applies when iterating on a List or Collection.