diff --git a/Settings.hs b/Settings.hs
index edabe42e3a88235d07c41a4d67070dabe165832c..80effa43a609c5b59e2f115248edf4226f3f7887 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,7 +1,7 @@
 module Settings where
 
 testFile, postCond :: String
-testFile = "debug"
+testFile = "2d-arrays1"
 postCond = "(true)"
 
 nrOfUnroll :: Int
diff --git a/WLP.hs b/WLP.hs
index 344b1061cea00ac23943948873559bbc5acb4e86..89327e592cdb2e096b7ff6213bce0cac70f12873 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -162,12 +162,12 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
     fArrayCreateInit t dim init inh                     = (ArrayCreateInit t dim init, acc inh)
     fFieldAccess fieldAccess inh                        = (ExpName (foldFieldAccess inh fieldAccess), (acc inh))
     fMethodInv invocation inh                           = case invocation of
-                                                            MethodCall (Name [Ident "*assume"]) [e] -> (false, (if e == false then const true else imp e))
-                                                            _   -> if getCallCount (calls inh) (invocationToId invocation) >= nrOfUnroll
-                                                                   then (false, const true)
-                                                                   else let varId = getReturnVar invocation
+                                                            MethodCall (Name [Ident "*assume"]) [e] -> (false, (if e == false then const true else imp e)) -- *assume is the regular assume function
+                                                            _   -> if getCallCount (calls inh) (invocationToId invocation) >= nrOfUnroll  -- Check the recursion depth
+                                                                   then (undefined, const true) -- Recursion limit reached: we just assume the post codition will hold
+                                                                   else let varId = getReturnVar invocation     
                                                                             callWlp = wlp' (inh {acc = id, calls = incrCallCount (calls inh) (invocationToId invocation), ret = Just varId, object = getObject inh invocation}) (inlineMethod inh invocation)
-                                                                        in (callWlp (ExpName (Name [varId])), (callWlp . acc inh))
+                                                                        in (ExpName (Name [varId]), (callWlp . acc inh))
     fArrayAccess (ArrayIndex a i) inh                   = (arrayAccess a i, snd ((foldExp wlpExpAlgebra a) inh {acc = id}) . arrayAccessWlp a i inh)
     
     fExpName name inh                                   = (ExpName name, (acc inh))