diff --git a/experiments/wermer2/Experiment.hs b/experiments/wermer2/Experiment.hs
index aad8ddec0e88e9d65849c634054ceff128da7ca1..38a3c39a885ed1e178a647b23da07c3d5a06cbb2 100644
--- a/experiments/wermer2/Experiment.hs
+++ b/experiments/wermer2/Experiment.hs
@@ -4,27 +4,73 @@ module Experiment where
 import Javawlp.API 
 import Javawlp.Engine.HelperFunctions
 import Javawlp.Engine.Verifier
+import Javawlp.Engine.WLP
 
 import Language.Java.Syntax
 import Z3.Monad
+import Data.List
+import System.IO.Unsafe
+import System.FilePath
+import System.Directory
 
+-- specify the wlp global configuration here
+wlpConfiguretion = WLPConf {
+      nrOfUnroll=1,
+      ignoreLibMethods=False,
+      ignoreMainMethod =False
+   }
 
-
-checkMutant original mutantDir methodName postcond = do 
+-- Calculate the wlps of an orginal java method and its mutant, then compare them.
+-- Example: 
+--
+--    checkMutant Triangle mutantdir tritype1 ["returnValue==0", "returnValue==1"]
+--
+-- This will check the method tritype1 in subjects/src/Triangle.java vs mdir/Triangle.java
+--
+checkMutant :: String -> FilePath  -> String -> [String] -> IO (Maybe Bool)
+checkMutant original mutantDir methodName postconds = do 
     let srcName = original ++ ".java"
-    (typeEnv1,decls1,methodNames1) <- parseJava ("./subjects/src/" ++ srcName) 
-    (typeEnv2,decls2,methodNames2) <- parseJava (mutantDir ++ "/"  ++ srcName) 
+    let srcPath    = "./subjects/src" </>  srcName
+    let mutantPath = mutantDir </> srcName
+    (typeEnv1,decls1,methodNames1) <- parseJava srcPath
+    (typeEnv2,decls2,methodNames2) <- parseJava mutantPath 
     
     let mname = Ident methodName
-    let q = post_ postcond
-    p1 <- wlpMethod defaultConf typeEnv1 decls1 mname q
-    p2 <- wlpMethod defaultConf typeEnv2 decls2 mname q
-    let tocheck    = PreNot (p1 ==* p2)
-    let (result,_) = unsafeIsSatisfiable (extendEnv typeEnv1 decls1 mname) decls1 tocheck
-    case result of
-       Sat   -> putStrLn "** KILLED."
-       Unsat -> putStrLn "** SURVIVED."
-       _     -> putStrLn "** UNDECIDED."
-
+    let qs = [ post_ q | q <- postconds ]
+    -- this function will be used to compare the resulting wlps
+    let comparePreC p1 p2 = let 
+                            f = PreNot (p1 ==* p2)
+                            (result,_) = unsafeIsSatisfiable (extendEnv typeEnv1 decls1 mname) decls1 f
+                            in
+                            result
+                            
+    ps1 <- sequence [ wlpMethod wlpConfiguretion typeEnv1 decls1 mname q | q <- qs ]
+    ps2 <- sequence [ wlpMethod wlpConfiguretion typeEnv2 decls2 mname q | q <- qs ]
+    putStrLn ("## Checking mutant " ++ mutantPath)
+    let z = zipWith comparePreC ps1 ps2
+    if any (== Sat) z        then return $ Just False -- the mutant is killed
+    else if all (== Unsat) z then return $ Just True  -- the mutant definitely survives
+    else return Nothing                          -- some of the wlps are undecidable
+    
+  
          
+checkAllMutants original mutantsRootDir methodName postconds = do   
+    mdirs <- getMutantsSubdirs mutantsRootDir
+    let mdirs_ = [ mutantsRootDir </> d | d <- mdirs ]
+    results <- sequence [ checkMutant original md methodName postconds | md <- mdirs_ ]
+    let nmutants = length results
+    let killed = length $ filter (== Just False) results
+    let undecided = length $ filter (== Nothing) results
+    putStrLn ("** Checking " ++ original ++ "." ++ methodName ++ " on " ++ show nmutants ++ " mutants.")
+    putStrLn ("** Killed=" ++ show killed ++ ", Survived=" ++ show (nmutants - killed)
+              ++ " (incl. " ++ show undecided ++ " undecided)" )
+    let survivors = [ (m,r) | (m,r) <- zip mdirs results, not(r == Just False) ]
+    sequence_ [ putStrLn ("** Unable to kill mutant " ++ m ++ ", " ++ show r) | (m,r) <- survivors ]
+    where
+    getMutantsSubdirs mutantsRootDir = do
+         fs <- listDirectory mutantsRootDir
+         let mdirs = [ name | name <- fs, not("." `isPrefixOf` name) 
+                                          && unsafePerformIO (doesDirectoryExist (mutantsRootDir </> name))
+                      ]
+         return mdirs
     
\ No newline at end of file
diff --git a/experiments/wermer2/mutation.mml b/experiments/wermer2/mutation.mml
index a27f80856b905bce59dc2defb46050f04ecf4493..8894557441c0009961e71d13a3a1557e78995925 100644
--- a/experiments/wermer2/mutation.mml
+++ b/experiments/wermer2/mutation.mml
@@ -1,12 +1,15 @@
 // A simple mml file to generate all mutants
 
 list_aor={+,-,*,/,%};
+list_aorPM={+,-};
 list_lor={&,|,^};
 list_sor={<<,>>,>>>};
 list_oru={+,-,~};
 
-BIN(+)->list_aor;
-BIN(-)->list_aor;
+//BIN(+)->list_aor;
+//BIN(-)->list_aor;
+BIN(+)->list_aorPM;
+BIN(-)->list_aorPM;
 BIN(*)->list_aor;
 BIN(/)->list_aor;
 BIN(%)->list_aor;