diff --git a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java b/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
index f1cf99f451939a04f038e05b96fef333f42ad974..89764386de8858fa07566c20a2be6f23957be5f9 100644
--- a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
+++ b/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
@@ -5,13 +5,13 @@ import static nl.uu.impress.EDSL.*;
 
 public class Main {
 
-    public static void test1(int[] b) {
+    public static void quickcheck_test1(int[] b) {
         pre(~(-a * c) == (79 & 41));
         pre(a > 0);
         pre(forall(b, i -> b[i] > -10));
     }
 
-    public static void test2(int[] b) {
+    public static void quickcheck_test2(int[] b) {
         pre(~(-a * c) == (79 & 41));
         pre(a > 0);
         pre(forall(b, i -> b[i] >= -10)); // note the >=, whereas test1 has >.
diff --git a/src/LogicIR/Eval.hs b/src/LogicIR/Eval.hs
index e9f9eeede5492f5a26f922a0aede6a03ba3c72d0..d274afafc28048b57ad39a59dbe52c02fe383f75 100644
--- a/src/LogicIR/Eval.hs
+++ b/src/LogicIR/Eval.hs
@@ -48,7 +48,7 @@ evalAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
 
           -- Things that should never happen.
           quant _ _ e1 e2 = error "Quantifiers cannot be evaluated and should be replaced using LogicIR.Rewrite.replaceQuantifiers."
-          arr v a         = error "You can't contain eval on an LExpr that contains uninstantiated arrays."
+          arr v a         = error "You can't call eval on an LExpr that contains uninstantiated arrays."
           var v           = error "You can't call eval on an LExpr that contains uninstantiated vars."
 
 -- Evaluates a binary operator expression.
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 8a67ca04a22af9639e8afa97ad018a32a0b0b745..ec442ecb9f08150f93967921ed7d71981b4f727e 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -205,15 +205,6 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
         showZ3AST :: Z3 AST -> IO String
         showZ3AST ast' = evalZ3 $ ast' >>= astToString
 
-parse :: (FilePath, String) -> (FilePath, String) -> IO (MethodDef, MethodDef)
-parse method1@(_, name1) method2@(_, name2) = do
-    -- load the methods
-    m1@(decls1, mbody1, env1) <- parseMethod method1
-    m2@(decls2, mbody2, env2) <- parseMethod method2
-    when (env1 /= env2) $ fail "inconsistent method parameters"
-    when (decls1 /= decls2) $ fail "inconsistent class declarations (TODO)"
-    return (m1, m2)
-
 -- Function that compares both the pre and the post condition for two methods.
 -- It is assumed that both methods have the same environment (parameter names, class member names, etc).
 compareSpec :: (FilePath, String) -> (FilePath, String) -> IO Bool
@@ -225,6 +216,15 @@ compareSpec method1@(_, name1) method2@(_, name2) = do
     postAns <- determineFormulaEq m1 m2 "post"
     return $ preAns && postAns
 
+parse :: (FilePath, String) -> (FilePath, String) -> IO (MethodDef, MethodDef)
+parse method1@(_, name1) method2@(_, name2) = do
+    -- load the methods
+    m1@(decls1, mbody1, env1) <- parseMethod method1
+    m2@(decls2, mbody2, env2) <- parseMethod method2
+    when (env1 /= env2) $ fail "inconsistent method parameters"
+    when (decls1 /= decls2) $ fail "inconsistent class declarations (TODO)"
+    return (m1, m2)
+
 methodDefToLExpr :: MethodDef -> MethodDef -> String -> (LExpr, LExpr)
 methodDefToLExpr m1@(decls1, _, env1) m2@(decls2, _, env2) name = do
     -- get pre/post condition