eqTermCut application not properly saved #3691
Description
Description
When using eqTermCut on typed seqGet expressions, the result cannot be saved properly. When reloading it fails with the error:
Could not find sort: List at <unknown>:2:25 (<unknown>:2:25)
Reproducible
always
Steps to reproduce
Expected behavior: proof reload works without error
Actual behavior: proof fails to load
In the loaded proof, you can reproduce the issue by using eqTermCut on (fr.up.xlim.sic.ig.jerboa.jme.model.JMENode)self.nodes.seq[i_0] in the second formula. Use self.nodes.seq[i_0] to instantiate the rule.
Additional information
Details
Proof could only be loaded partially.
In summary 2 not loadable rule application(s) have been detected.
The first one:
Error loading proof.
Line 2309, goal 2149, rule eqTermCut not available or not applicable in this context. (file: /home/arne/src/Jerboa-KeY-case-study/fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__hasCorrectDimensionsNodes(int)).JML accessible clause.0.proof.gz; caused by: Error loading proof.
Line 2309, goal 2149, rule eqTermCut not available or not applicable in this context. (file: /home/arne/src/Jerboa-KeY-case-study/fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__hasCorrectDimensionsNodes(int)).JML accessible clause.0.proof.gz; caused by: Could not find sort: List at <unknown>:2:25 (<unknown>:2:25)))
at de.uka.ilkd.key.gui.WindowUserInterfaceControl.loadingFinished(WindowUserInterfaceControl.java:521)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:282)
at de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:75)
at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:125)
at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:118)
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)
Caused by: Error loading proof.
Line 2309, goal 2149, rule eqTermCut not available or not applicable in this context. (file: /home/arne/src/Jerboa-KeY-case-study/fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__hasCorrectDimensionsNodes(int)).JML accessible clause.0.proof.gz; caused by: Could not find sort: List at <unknown>:2:25 (<unknown>:2:25))
at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.reportError(IntermediateProofReplayer.java:857)
at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.replay(IntermediateProofReplayer.java:274)
at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.replay(IntermediateProofReplayer.java:189)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.replayProof(AbstractProblemLoader.java:663)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadSelectedProof(AbstractProblemLoader.java:343)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:279)
... 9 more
Caused by: Could not find sort: List at <unknown>:2:25 (<unknown>:2:25)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.semanticError(AbstractBuilder.java:172)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.lookupVarfuncId(DefaultBuilder.java:179)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitAccessterm(ExpressionBuilder.java:1501)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitAccessterm(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$AccesstermContext.accept(KeYParser.java:6603)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitPrimitive_term(KeYParserBaseVisitor.java:570)
at de.uka.ilkd.key.nparser.KeYParser$Primitive_termContext.accept(KeYParser.java:6490)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitPrimitive_labeled_term(ExpressionBuilder.java:944)
at de.uka.ilkd.key.nparser.KeYParser$Primitive_labeled_termContext.accept(KeYParser.java:6293)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitBracket_term(ExpressionBuilder.java:453)
at de.uka.ilkd.key.nparser.KeYParser$Bracket_termContext.accept(KeYParser.java:5943)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitAtom_prefix(KeYParserBaseVisitor.java:500)
at de.uka.ilkd.key.nparser.KeYParser$Atom_prefixContext.accept(KeYParser.java:5845)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitStrong_arith_term_2(ExpressionBuilder.java:408)
at de.uka.ilkd.key.nparser.KeYParser$Strong_arith_term_2Context.accept(KeYParser.java:5439)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitStrong_arith_term_1(ExpressionBuilder.java:387)
at de.uka.ilkd.key.nparser.KeYParser$Strong_arith_term_1Context.accept(KeYParser.java:5356)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitWeak_arith_term(ExpressionBuilder.java:343)
at de.uka.ilkd.key.nparser.KeYParser$Weak_arith_termContext.accept(KeYParser.java:5270)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitComparison_term(ExpressionBuilder.java:317)
at de.uka.ilkd.key.nparser.KeYParser$Comparison_termContext.accept(KeYParser.java:5171)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquality_term(ExpressionBuilder.java:306)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquality_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Equality_termContext.accept(KeYParser.java:5092)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitTerm60(KeYParserBaseVisitor.java:409)
at de.uka.ilkd.key.nparser.KeYParser$Term60Context.accept(KeYParser.java:4858)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitConjunction_term(ExpressionBuilder.java:250)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitConjunction_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Conjunction_termContext.accept(KeYParser.java:4792)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitDisjunction_term(ExpressionBuilder.java:241)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitDisjunction_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Disjunction_termContext.accept(KeYParser.java:4719)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitImplication_term(ExpressionBuilder.java:234)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitImplication_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Implication_termContext.accept(KeYParser.java:4651)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquivalence_term(ExpressionBuilder.java:208)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquivalence_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Equivalence_termContext.accept(KeYParser.java:4582)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitElementary_update_term(ExpressionBuilder.java:198)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitElementary_update_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Elementary_update_termContext.accept(KeYParser.java:4515)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.lambda$mapOf$0(AbstractBuilder.java:121)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
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.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.mapOf(AbstractBuilder.java:121)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitParallel_term(ExpressionBuilder.java:183)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitParallel_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Parallel_termContext.accept(KeYParser.java:4447)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitTerm(KeYParserBaseVisitor.java:360)
at de.uka.ilkd.key.nparser.KeYParser$TermContext.accept(KeYParser.java:4393)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.lambda$mapOf$0(AbstractBuilder.java:121)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
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.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.mapOf(AbstractBuilder.java:121)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitArgument_list(ExpressionBuilder.java:1165)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitArgument_list(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Argument_listContext.accept(KeYParser.java:7602)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitArguments(ExpressionBuilder.java:1546)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitAccessterm(ExpressionBuilder.java:1479)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitAccessterm(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$AccesstermContext.accept(KeYParser.java:6603)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitPrimitive_term(KeYParserBaseVisitor.java:570)
at de.uka.ilkd.key.nparser.KeYParser$Primitive_termContext.accept(KeYParser.java:6490)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitPrimitive_labeled_term(ExpressionBuilder.java:944)
at de.uka.ilkd.key.nparser.KeYParser$Primitive_labeled_termContext.accept(KeYParser.java:6293)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitBracket_term(ExpressionBuilder.java:453)
at de.uka.ilkd.key.nparser.KeYParser$Bracket_termContext.accept(KeYParser.java:5943)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitAtom_prefix(KeYParserBaseVisitor.java:500)
at de.uka.ilkd.key.nparser.KeYParser$Atom_prefixContext.accept(KeYParser.java:5845)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitStrong_arith_term_2(ExpressionBuilder.java:408)
at de.uka.ilkd.key.nparser.KeYParser$Strong_arith_term_2Context.accept(KeYParser.java:5439)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitStrong_arith_term_1(ExpressionBuilder.java:387)
at de.uka.ilkd.key.nparser.KeYParser$Strong_arith_term_1Context.accept(KeYParser.java:5356)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitWeak_arith_term(ExpressionBuilder.java:343)
at de.uka.ilkd.key.nparser.KeYParser$Weak_arith_termContext.accept(KeYParser.java:5270)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitComparison_term(ExpressionBuilder.java:317)
at de.uka.ilkd.key.nparser.KeYParser$Comparison_termContext.accept(KeYParser.java:5171)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquality_term(ExpressionBuilder.java:306)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquality_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Equality_termContext.accept(KeYParser.java:5092)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitTerm60(KeYParserBaseVisitor.java:409)
at de.uka.ilkd.key.nparser.KeYParser$Term60Context.accept(KeYParser.java:4858)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitConjunction_term(ExpressionBuilder.java:250)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitConjunction_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Conjunction_termContext.accept(KeYParser.java:4792)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitDisjunction_term(ExpressionBuilder.java:241)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitDisjunction_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Disjunction_termContext.accept(KeYParser.java:4719)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitImplication_term(ExpressionBuilder.java:234)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitImplication_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Implication_termContext.accept(KeYParser.java:4651)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquivalence_term(ExpressionBuilder.java:208)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquivalence_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Equivalence_termContext.accept(KeYParser.java:4582)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitElementary_update_term(ExpressionBuilder.java:198)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitElementary_update_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Elementary_update_termContext.accept(KeYParser.java:4515)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.lambda$mapOf$0(AbstractBuilder.java:121)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
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.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.mapOf(AbstractBuilder.java:121)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitParallel_term(ExpressionBuilder.java:183)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitParallel_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Parallel_termContext.accept(KeYParser.java:4447)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitTerm(KeYParserBaseVisitor.java:360)
at de.uka.ilkd.key.nparser.KeYParser$TermContext.accept(KeYParser.java:4393)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.lambda$mapOf$0(AbstractBuilder.java:121)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
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.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.mapOf(AbstractBuilder.java:121)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitArgument_list(ExpressionBuilder.java:1165)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitArgument_list(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Argument_listContext.accept(KeYParser.java:7602)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitArguments(ExpressionBuilder.java:1546)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitAccessterm(ExpressionBuilder.java:1479)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitAccessterm(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$AccesstermContext.accept(KeYParser.java:6603)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitPrimitive_term(KeYParserBaseVisitor.java:570)
at de.uka.ilkd.key.nparser.KeYParser$Primitive_termContext.accept(KeYParser.java:6490)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitPrimitive_labeled_term(ExpressionBuilder.java:944)
at de.uka.ilkd.key.nparser.KeYParser$Primitive_labeled_termContext.accept(KeYParser.java:6293)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitBracket_term(ExpressionBuilder.java:453)
at de.uka.ilkd.key.nparser.KeYParser$Bracket_termContext.accept(KeYParser.java:5943)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitAtom_prefix(KeYParserBaseVisitor.java:500)
at de.uka.ilkd.key.nparser.KeYParser$Atom_prefixContext.accept(KeYParser.java:5845)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitStrong_arith_term_2(ExpressionBuilder.java:408)
at de.uka.ilkd.key.nparser.KeYParser$Strong_arith_term_2Context.accept(KeYParser.java:5439)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitStrong_arith_term_1(ExpressionBuilder.java:387)
at de.uka.ilkd.key.nparser.KeYParser$Strong_arith_term_1Context.accept(KeYParser.java:5356)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitWeak_arith_term(ExpressionBuilder.java:343)
at de.uka.ilkd.key.nparser.KeYParser$Weak_arith_termContext.accept(KeYParser.java:5270)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitComparison_term(ExpressionBuilder.java:317)
at de.uka.ilkd.key.nparser.KeYParser$Comparison_termContext.accept(KeYParser.java:5171)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquality_term(ExpressionBuilder.java:306)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquality_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Equality_termContext.accept(KeYParser.java:5092)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitTerm60(KeYParserBaseVisitor.java:409)
at de.uka.ilkd.key.nparser.KeYParser$Term60Context.accept(KeYParser.java:4858)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitConjunction_term(ExpressionBuilder.java:250)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitConjunction_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Conjunction_termContext.accept(KeYParser.java:4792)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitDisjunction_term(ExpressionBuilder.java:241)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitDisjunction_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Disjunction_termContext.accept(KeYParser.java:4719)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitImplication_term(ExpressionBuilder.java:234)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitImplication_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Implication_termContext.accept(KeYParser.java:4651)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquivalence_term(ExpressionBuilder.java:208)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquivalence_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Equivalence_termContext.accept(KeYParser.java:4582)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:48)
at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:46)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitElementary_update_term(ExpressionBuilder.java:198)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitElementary_update_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Elementary_update_termContext.accept(KeYParser.java:4515)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.lambda$mapOf$0(AbstractBuilder.java:121)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
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.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.uka.ilkd.key.nparser.builder.AbstractBuilder.mapOf(AbstractBuilder.java:121)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitParallel_term(ExpressionBuilder.java:183)
at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitParallel_term(ExpressionBuilder.java:62)
at de.uka.ilkd.key.nparser.KeYParser$Parallel_termContext.accept(KeYParser.java:4447)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitTerm(KeYParserBaseVisitor.java:360)
at de.uka.ilkd.key.nparser.KeYParser$TermContext.accept(KeYParser.java:4393)
at de.uka.ilkd.key.nparser.KeyAst.accept(KeyAst.java:58)
at de.uka.ilkd.key.nparser.KeyIO.interpretExpression(KeyIO.java:101)
at de.uka.ilkd.key.nparser.KeyIO.parseExpression(KeyIO.java:92)
at de.uka.ilkd.key.parser.DefaultTermParser.parse(DefaultTermParser.java:69)
at de.uka.ilkd.key.parser.DefaultTermParser.parse(DefaultTermParser.java:50)
at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.parseTerm(IntermediateProofReplayer.java:963)
at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.parseSV2(IntermediateProofReplayer.java:1037)
at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.constructInsts(IntermediateProofReplayer.java:928)
at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.constructTacletApp(IntermediateProofReplayer.java:501)
at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.replay(IntermediateProofReplayer.java:252)
... 13 more