experiments with a.length

src/SimpleFormulaChecker.hs

@@ -131,5 +131,6 @@ testEq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec1")
 testNeq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec2")
 blub = compareSpec (edslSrc, "getMax_spec1") (edslSrc, "getMax_spec2")
 blub2 = compareSpec (edslSrc, "test1") (edslSrc, "test2")
+blub2_ = compareSpec (edslSrc, "test1_") (edslSrc, "test2")
 blob = compareSpec (edslSrc, "blob1") (edslSrc, "blob1")
 nullTest = compareSpec (edslSrc, "null1") (edslSrc, "null2")
\ No newline at end of file

src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java

@@ -127,6 +127,11 @@ public class Main {
         post(true);
     }
 
+     public static void test1_(int[] a)  {
+        pre(exists(a, i -> a[i+1] > a[i] && (a.length > i+1)));
+        post(true);
+    }
+
     public static void test2(int[] a)  {
         pre(false);
         //pre(exists(a, i -> a[i+1] >= a[i]));