diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml
index 2b1dc921fb3bb15fc988e9a5ca52b74c6bf99b7e..0204bd9e4dde3f01dab2a7be856a62664db3016f 100644
--- a/src/testsuite/Testsuite.ml
+++ b/src/testsuite/Testsuite.ml
@@ -50,11 +50,11 @@ let runSatCheckVerbose (sc:satCheck) =
     PF.printf "Is %-50s " (cs "1" title);
     PF.printf "%s?… " (sotr expectation);
     let res = runSatCheck sc in
-    if (res = expectation)
+    (if (res = expectation)
     then PF.printf "%s\n" (cs "1;32" "Yes")
     else PF.printf "%s, it is %s\n"
                     (cs "1;31" "No")
-                    (sotr res)
-
+                    (sotr res));
+    res
 
 
diff --git a/src/testsuite/Testsuite.mli b/src/testsuite/Testsuite.mli
index 2276f95bceb154e2a54fc3f9dcb86c9457fafc7a..3b645f359d0532b655b047e8bf249478fcbc5a6a 100644
--- a/src/testsuite/Testsuite.mli
+++ b/src/testsuite/Testsuite.mli
@@ -12,5 +12,5 @@ type testResult = | Sat
 type satCheck = testResult * (CoAlgMisc.sortTable) * string (* expected * functors * formula *)
 
 val runSatCheck : satCheck -> testResult
-val runSatCheckVerbose : satCheck -> unit
+val runSatCheckVerbose : satCheck -> testResult
 
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index 649a26b637f8bf9df7cb574d049309a77e9e9e09..a093b05ca8eae69ab5bb85d27546a1131bbd643c 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -10,7 +10,6 @@ let kd  = [| (CM.MultiModalKD, [0]) |]
 let cl  = [| (CM.CoalitionLogic, [0]) |]
 let gml = [| (CM.GML, [0]) |]
 
-(* ============ multi modal K ============ *)
 let k_testcases: satCheck list =
     let c a b = (a,k,b) in
     [ c Sat   "True"
@@ -50,10 +49,24 @@ let testcases =
     ]
 
 let main =
+    let success = ref 0 in
+    let failed = ref 0 in
     foreach_l testcases (fun (name,table) ->
-        Printf.printf "\n==== Testing %s ====\n" name;
-        foreach_l table runSatCheckVerbose
-    )
+        Printf.printf "==== Testing %s ====\n" name;
+        foreach_l table (fun sc ->
+            let (expected,_,_) = sc in
+            let actual = runSatCheckVerbose sc in
+            (* compare the expected and the actual result *)
+            if actual = expected
+            then success := !success + 1
+            else failed := !failed + 1
+        );
+        Printf.printf "\n"
+    );
+    let s n = if n = 1 then "testcase" else "testcases" in
+    Printf.printf "=> %d %s succeeded, %d %s failed.\n"
+        !success (s !success)
+        !failed (s !failed)
 
 let _ = main