From 2fb88618f2995fa7531bd9462105b8a963e207b3 Mon Sep 17 00:00:00 2001 From: Dmitrii Timofeev Date: Tue, 13 Sep 2022 12:11:09 +0300 Subject: [PATCH] *** Experiment: UtArrayApplyForAll noop translation --- .../main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt index 4f0d7516d4..5313f8647b 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt @@ -414,7 +414,11 @@ open class Z3TranslatorVisitor( override fun visit(expr: UtArrayShiftIndexes): Expr = error("translate of UtArrayShiftIndexes expression") - override fun visit(expr: UtArrayApplyForAll): Expr = error("translate of UtArrayApplyForAll expression") + // Hypothesis: UtArrayApplyForAll is kept by the rewriter only the corresponding array is not accessed, + // so we don't actually need constraints on its elements (I am not sure, just an experiment) + // Previous implementation: + // error("translate of UtArrayApplyForAll expression") + override fun visit(expr: UtArrayApplyForAll): Expr = expr.arrayExpression.accept(this) override fun visit(expr: UtStringToArray): Expr = error("translate of UtStringToArray expression")