diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml
index 80e053d43106dc8bf4d0b7a224623fa30b9f742e..63fb1fded518fa1efd43a78f8472d17e33e11034 100644
--- a/src/testsuite/Testsuite.ml
+++ b/src/testsuite/Testsuite.ml
@@ -58,12 +58,14 @@ let runSatCheckVerbose (sc:satCheck) =
     let (expectation,_,title) = sc in
     PF.printf "Is %s " (cs "1" (columnCreate 60 title));
     PF.printf "%s? → " (sotr expectation);
+    flush stdout;
     let res = runSatCheck sc in
     (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));
+    flush stdout;
     res
 
 
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index 682b0819c1d9a5cedae1fa39b337f577b4616fda..6a5d9ab2d54d7d85f40f9169d32f553dbc187e37 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -117,6 +117,10 @@ let testcases =
     ; kAndKd_testcases
     ; c "K+KD" kOrKd_testcases
     ; pml_testcases
+    ; use_functor "PML + K"
+        [ sat "(P4 + False)"
+        ; sat "(({>= 3/5} p0 & {>= 2/5} p1) + False)"
+        ]
     ]
 
 let main =
@@ -124,8 +128,10 @@ let main =
     let failed = ref 0 in
     foreach_l testcases (fun (name,table) ->
         Printf.printf "==== Testing %s ====\n" name;
+        (*
         let (_,sorts,_) = List.hd table in
         Printf.printf "sortTable = %s\n" (FP.stringFromSortTable sorts);
+        *)
         foreach_l table (fun sc ->
             let (expected,_,_) = sc in
             let actual = runSatCheckVerbose sc in
@@ -134,7 +140,7 @@ let main =
             then success := !success + 1
             else failed := !failed + 1
         );
-        Printf.printf "\n"
+        print_endline ""
     );
     let s n = if n = 1 then "testcase" else "testcases" in
     Printf.printf "=> %d %s succeeded, %d %s failed.\n"