small improvements

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'

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

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

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];