diff --git a/src/LogicIR/Backend/Z3.hs b/src/LogicIR/Backend/Z3.hs
index f40a117eb81794c02836149d4c5db3a086959ff3..93b5c9e3ea77532c139958d91cdbc24a72d6e48d 100644
--- a/src/LogicIR/Backend/Z3.hs
+++ b/src/LogicIR/Backend/Z3.hs
@@ -50,7 +50,7 @@ lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray,
                       a <- a'
                       mkSelect v a
     flNil = do intSort <- mkBvSort 32
-               zero <- mkBitvector 32 0
+               zero <- mkBitvector 32 0 -- (isNull, data, length) TODO
                mkConstArray intSort zero
     fnConst n = mkBitvector 32 (fromIntegral n)
     fnUnop o a' = do a <- a'
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index fcc13143d39288e60fa79dc399cd2fd19f1ee447..d2cbd8ebf0a81a60947d207a24b7b9a563eef404 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -47,8 +47,8 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
                                     _
                                         -> error $ "Unimplemented fMethodInv: " ++ show inv
     fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: type checking
-                                             ArrayIndex (ExpName name) [ExpName index]
-                                                -> LArray (nameToVar name env decls) (LVar (nameToVar index env decls))
+                                             ArrayIndex (ExpName name) [expr]
+                                                -> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls) -- (LVar (nameToVar index env decls))
                                              _
                                                 -> error $ "Multidimensional arrays are not supported: " ++ show (arrayIndex)
     fExpName name env decls = case name of -- TODO: type checking
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 161b978e0c736b0542f61ef2431a1536c4100796..22d5505339dcc1e2f0f518da5416dc2c3219c663 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -171,4 +171,5 @@ compareSpec method1@(_, name1) method2@(_, name2) = do
 edslSrc = "javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
 testEq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec1")
 testNeq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec2")
-blub = compareSpec (edslSrc, "getMax_spec1") (edslSrc, "getMax_spec2")
\ No newline at end of file
+blub = compareSpec (edslSrc, "getMax_spec1") (edslSrc, "getMax_spec2")
+blub2 = compareSpec (edslSrc, "test1") (edslSrc, "test2")
\ No newline at end of file
diff --git a/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java b/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
index e9f2b96ae5cd1f2ecd9c1f3ce32949b558d32ae2..9a612760cffa96d7c1de206e729493629ecf8ea3 100644
--- a/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
+++ b/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
@@ -107,7 +107,21 @@ public class Main {
         post(a[i] == oldaj);
     }
 
+    public static void test1(int[] a)
+    {
+        pre(exists(a, i -> a[i+1] > a[i]));
+        post(true);
+    }
+
+    public static void test2(int[] a)
+    {
+        pre(false);
+        //pre(exists(a, i -> a[i+1] >= a[i]));
+        post(true);
+    }
+
     public static void swap_spec2(int[] a, int i, int j) {
+        pre(a != null && a[0] == 0);
         pre(a != null && a.length > 0 && i >= 0 && j > 0);
         // introducing vars to remember old values
         int oldai = a[i], oldaj = a[j];