SMT Translation naming conflicts

[BookWood7th]

Description

The SMT translation names a function parameter "length" to a function "length", which conflicts with the length function for objects.

Reproducible

always

Steps to reproduce

1. Load example RemoveDuplicates, contract "arrayPart(int[], int)"
2. SMT Preparation Macro
3. Call any SMT solver

Expected SMT solver to launch and attempt to prove the goal.
Actually SMT solvers do not start and fail with a handled exception.

Additional information

Exceptionde.uka.ilkd.key.util.parsing.BuildingException: You used the variable `length` like a predicate or function. at <unknown>:2:23
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.semanticError(AbstractBuilder.java:173)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitAccessterm(ExpressionBuilder.java:1490)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitAccessterm(ExpressionBuilder.java:57)
	at de.uka.ilkd.key.nparser.KeYParser$AccesstermContext.accept(KeYParser.java:6585)
	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:6472)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitPrimitive_labeled_term(ExpressionBuilder.java:923)
	at de.uka.ilkd.key.nparser.KeYParser$Primitive_labeled_termContext.accept(KeYParser.java:6275)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitBracket_term(ExpressionBuilder.java:445)
	at de.uka.ilkd.key.nparser.KeYParser$Bracket_termContext.accept(KeYParser.java:5925)
	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:5827)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitStrong_arith_term_2(ExpressionBuilder.java:400)
	at de.uka.ilkd.key.nparser.KeYParser$Strong_arith_term_2Context.accept(KeYParser.java:5421)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitStrong_arith_term_1(ExpressionBuilder.java:379)
	at de.uka.ilkd.key.nparser.KeYParser$Strong_arith_term_1Context.accept(KeYParser.java:5338)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitWeak_arith_term(ExpressionBuilder.java:336)
	at de.uka.ilkd.key.nparser.KeYParser$Weak_arith_termContext.accept(KeYParser.java:5252)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitComparison_term(ExpressionBuilder.java:310)
	at de.uka.ilkd.key.nparser.KeYParser$Comparison_termContext.accept(KeYParser.java:5153)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquality_term(ExpressionBuilder.java:299)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquality_term(ExpressionBuilder.java:57)
	at de.uka.ilkd.key.nparser.KeYParser$Equality_termContext.accept(KeYParser.java:5074)
	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:4840)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitQuantifierterm(ExpressionBuilder.java:1021)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitQuantifierterm(ExpressionBuilder.java:57)
	at de.uka.ilkd.key.nparser.KeYParser$QuantifiertermContext.accept(KeYParser.java:4935)
	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:4840)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitConjunction_term(ExpressionBuilder.java:243)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitConjunction_term(ExpressionBuilder.java:57)
	at de.uka.ilkd.key.nparser.KeYParser$Conjunction_termContext.accept(KeYParser.java:4774)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitDisjunction_term(ExpressionBuilder.java:234)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitDisjunction_term(ExpressionBuilder.java:57)
	at de.uka.ilkd.key.nparser.KeYParser$Disjunction_termContext.accept(KeYParser.java:4701)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitImplication_term(ExpressionBuilder.java:227)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitImplication_term(ExpressionBuilder.java:57)
	at de.uka.ilkd.key.nparser.KeYParser$Implication_termContext.accept(KeYParser.java:4633)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquivalence_term(ExpressionBuilder.java:203)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquivalence_term(ExpressionBuilder.java:57)
	at de.uka.ilkd.key.nparser.KeYParser$Equivalence_termContext.accept(KeYParser.java:4564)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:49)
	at de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:44)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitElementary_update_term(ExpressionBuilder.java:193)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitElementary_update_term(ExpressionBuilder.java:57)
	at de.uka.ilkd.key.nparser.KeYParser$Elementary_update_termContext.accept(KeYParser.java:4497)
	at de.uka.ilkd.key.nparser.builder.AbstractBuilder.lambda$mapOf$0(AbstractBuilder.java:122)
	at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
	at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1625)
	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:122)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitParallel_term(ExpressionBuilder.java:178)
	at de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitParallel_term(ExpressionBuilder.java:57)
	at de.uka.ilkd.key.nparser.KeYParser$Parallel_termContext.accept(KeYParser.java:4429)
	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:4375)
	at de.uka.ilkd.key.nparser.KeyAst.accept(KeyAst.java:50)
	at de.uka.ilkd.key.nparser.KeyIO.parseExpression(KeyIO.java:97)
	at de.uka.ilkd.key.parser.DefaultTermParser.parse(DefaultTermParser.java:69)
	at de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler.handleDLAxioms(DefinedSymbolsHandler.java:251)
	at de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler.introduceSymbol(DefinedSymbolsHandler.java:176)
	at de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler.handle(DefinedSymbolsHandler.java:199)
	at de.uka.ilkd.key.smt.newsmt2.MasterHandler.translate(MasterHandler.java:159)
	at de.uka.ilkd.key.smt.newsmt2.MasterHandler.translate(MasterHandler.java:325)
	at de.uka.ilkd.key.smt.newsmt2.MasterHandler.translate(MasterHandler.java:313)
	at de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler.handle(IntegerOpHandler.java:101)
	at de.uka.ilkd.key.smt.newsmt2.MasterHandler.translate(MasterHandler.java:146)
	at de.uka.ilkd.key.smt.newsmt2.MasterHandler.translate(MasterHandler.java:189)
	at de.uka.ilkd.key.smt.newsmt2.ModularSMTLib2Translator.makeSMTAsserts(ModularSMTLib2Translator.java:198)
	at de.uka.ilkd.key.smt.newsmt2.ModularSMTLib2Translator.translateProblem(ModularSMTLib2Translator.java:121)
	at de.uka.ilkd.key.smt.SMTSolverImplementation.translateToCommand(SMTSolverImplementation.java:343)
	at de.uka.ilkd.key.smt.SMTSolverImplementation.run(SMTSolverImplementation.java:257)

---

• Commit: 9cc569c

[mattulbrich]

Interesting observation! Thanks for reporting.

However, the problem is not SMT-related, but has to do with the fact that a local program variable length is created in the proof obligation while there is already a symbol length used in KeY (for array length). If you do a cut with length(a) = 0 you get a very similar error message.

[BookWood7th]

I suppose a similar issue also occurs in the example "Lists with Loop Contracts" in the contract "mapIncrement_loopContract() normal behavior operation contract 0". Here there are two different variables present for "self". They are differentiated only by their hashcodes. Is this intended?
It seems like this is still present on the main branch at time of writing.