Fix array literal transformation

ftsrg · Aug 11, 2020 · 62e3447 · 62e3447
1 parent dbd22b0
commit 62e3447
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java
@@ -773,7 +773,7 @@ private com.microsoft.z3.Expr transformArrayNeq(final ArrayNeqExpr<?, ?> expr) {
 	}
 
 	private com.microsoft.z3.Expr transformArrayLit(final ArrayLitExpr<?, ?> expr) {
-		com.microsoft.z3.ArrayExpr running = context.mkConstArray(transformer.toSort(expr.getElseElem().getType()), toTerm(expr.getElseElem()));
+		com.microsoft.z3.ArrayExpr running = context.mkConstArray(transformer.toSort(expr.getType().getIndexType()), toTerm(expr.getElseElem()));
 		for (Tuple2<? extends Expr<?>, ? extends Expr<?>> elem : expr.getElements()) {
 			running = context.mkStore(running, toTerm(elem.get1()), toTerm(elem.get2()));
 		}