diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index f5c6072da64a54a6b36cb12c46a3dba40c47af7c..7d63f3c3a70fe2f2110aee0c02c81141e9ae36a0 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -46,14 +46,23 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
     fMethodInv inv env decls = case inv of -- TODO: very hardcoded EDSL + lambdas cannot be { return expr; } + ranged 
                                     -- Java: forall(name, bound -> expr);
                                     MethodCall (Name [Ident "forall"]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
-                                        -> let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
-                                            LQuant QAll i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LImpl (foldExp javaExpToLExprAlgebra expr env decls))
+                                        -> forall name bound expr
                                     -- Java: exists(name, bound -> expr);
                                     MethodCall (Name [Ident "exists"]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
-                                        -> let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
-                                            LQuant QAny i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LAnd (foldExp javaExpToLExprAlgebra expr env decls))
+                                        -> exists name bound expr
+                                    -- Java: forall(name, bound -> { return expr; });
+                                    MethodCall (Name [Ident "forall"]) [ExpName name ,Lambda (LambdaSingleParam (Ident bound)) (LambdaBlock (Block [BlockStmt (Return (Just expr))]))]
+                                        -> forall name bound expr
+                                    -- Java: exists(name, bound -> { return expr; });
+                                    MethodCall (Name [Ident "exists"]) [ExpName name ,Lambda (LambdaSingleParam (Ident bound)) (LambdaBlock (Block [BlockStmt (Return (Just expr))]))]
+                                        -> exists name bound expr
                                     _
                                         -> error $ "Unimplemented fMethodInv: " ++ show inv
+
+                                    where forall name bound expr = let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
+                                                                                  LQuant QAll i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LImpl (foldExp javaExpToLExprAlgebra expr env decls))
+                                          exists name bound expr = let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
+                                                                                  LQuant QAny i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LAnd (foldExp javaExpToLExprAlgebra expr env decls))
     fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: type checking
                                              ArrayIndex (ExpName name) [expr]
                                                 -> LArray (nameToVar name env decls) (javaExpToLExpr expr env decls)
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 455cd08fceceda63b4479eeb4a7218c7490731e1..dadcc669def2acf8bcd673a12f7a6852f91bc4cb 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -131,4 +131,5 @@ 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")
-blub2 = compareSpec (edslSrc, "test1") (edslSrc, "test2")
\ No newline at end of file
+blub2 = compareSpec (edslSrc, "test1") (edslSrc, "test2")
+blob = compareSpec (edslSrc, "blob1") (edslSrc, "blob1")
\ 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 9a612760cffa96d7c1de206e729493629ecf8ea3..6cd599370f7e78b355eedb3bf87b4deadb77758e 100644
--- a/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
+++ b/src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
@@ -107,6 +107,12 @@ public class Main {
         post(a[i] == oldaj);
     }
 
+    public static void blob1(int[] a)
+    {
+        pre(forall(a, i -> { return a[i] == 0; }));
+        post(true);
+    }
+
     public static void test1(int[] a)
     {
         pre(exists(a, i -> a[i+1] > a[i]));