*** Experiment: UtArrayApplyForAll noop translation

UnitTestBot · Sep 13, 2022 · 2fb8861 · 2fb8861
1 parent dd27277
commit 2fb8861
Showing 1 changed file with 5 additions and 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
@@ -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")