Test org.utbot.examples.collections.MapsPart2Test#testPutAllEntries is flaky - sometimes we have an infinite recursion in org.utbot.engine.pc.Z3EvaluatorVisitor during resolving models for java.util.Map.
To Reproduce
Run org.utbot.examples.collections.MapsPart2Test#testPutAllEntries a few times - 10 should be enough.
Expected behavior
All tests are successful.
Actual behavior
Approximately half of tests fail with java.lang.StackOverflowError because of infinite recursion.
Visual proofs (screenshots, logs, images)
java.lang.StackOverflowError
at java.base/java.util.IdentityHashMap.hash(IdentityHashMap.java:297)
at java.base/java.util.IdentityHashMap.put(IdentityHashMap.java:428)
at com.microsoft.z3.IDecRefQueue.storeReference(IDecRefQueue.java:58)
at com.microsoft.z3.AST.addToReferenceQueue(AST.java:199)
at com.microsoft.z3.Z3Object.<init>(Z3Object.java:34)
at com.microsoft.z3.AST.<init>(AST.java:189)
at com.microsoft.z3.Expr.<init>(Expr.java:2097)
at com.microsoft.z3.BitVecExpr.<init>(BitVecExpr.java:42)
at com.microsoft.z3.BitVecNum.<init>(BitVecNum.java:82)
at com.microsoft.z3.Expr.create(Expr.java:2139)
at com.microsoft.z3.Model.eval(Model.java:215)
at com.microsoft.z3.Z3ExtensionKt.eval(Z3Extension.kt:8)
at org.utbot.engine.pc.Z3EvaluatorVisitor.eval(Z3EvaluatorVisitor.kt:60)
at org.utbot.engine.pc.Z3EvaluatorVisitor.visit(Z3EvaluatorVisitor.kt:171)
at org.utbot.engine.pc.Z3EvaluatorVisitor.visit(Z3EvaluatorVisitor.kt:22)
at org.utbot.engine.pc.UtAddrExpression.accept(UtExpression.kt:513)
at org.utbot.engine.pc.Z3EvaluatorVisitor.eval(Z3EvaluatorVisitor.kt:58)
at org.utbot.engine.pc.Z3EvaluatorVisitor.visit(Z3EvaluatorVisitor.kt:247)
at org.utbot.engine.pc.Z3EvaluatorVisitor.visit(Z3EvaluatorVisitor.kt:22)
at org.utbot.engine.pc.UtArraySelectExpression.accept(UtExpression.kt:215)
at org.utbot.engine.pc.Z3EvaluatorVisitor.eval(Z3EvaluatorVisitor.kt:58)
at org.utbot.engine.pc.Z3EvaluatorVisitor.visit(Z3EvaluatorVisitor.kt:171)
at org.utbot.engine.pc.Z3EvaluatorVisitor.visit(Z3EvaluatorVisitor.kt:22)
at org.utbot.engine.pc.UtAddrExpression.accept(UtExpression.kt:513)
Description
Test
org.utbot.examples.collections.MapsPart2Test#testPutAllEntries
is flaky - sometimes we have an infinite recursion inorg.utbot.engine.pc.Z3EvaluatorVisitor
during resolving models forjava.util.Map
.To Reproduce
Run
org.utbot.examples.collections.MapsPart2Test#testPutAllEntries
a few times - 10 should be enough.Expected behavior
All tests are successful.
Actual behavior
Approximately half of tests fail with
java.lang.StackOverflowError
because of infinite recursion.Visual proofs (screenshots, logs, images)
Environment
Default
UtSettings
.Additional context
No additional context.