Add crucial testcases for K*K

src/testsuite/cool-testsuite.ml

@@ -87,6 +87,12 @@ let kAndKd_testcases : testcase_section =
     ; unsat "i' => [pi2][R] (~i') |- i' & [pi2] [R] i'"
     ]
 
+let kAndK_testcases : testcase_section =
+    use_functor "K * K"
+    [ sat   "[pi1]<R>c0 | [pi1]<S>c1 | [pi2]<T>c3"
+    ; sat   "[pi1]<R>c0 | [pi1]<S>c1 | [pi2]<T>c3 | [pi1][U]c4"
+    ]
+
 let kOrKd = [| (CoAlgMisc.Choice, [1; 2]);
                (CoAlgMisc.MultiModalK, [0]);
                (CoAlgMisc.MultiModalKD, [0])
@@ -115,6 +121,7 @@ let testcases =
     ; c "KD" kd_testcases
     ; cl_testcases
     ; kAndKd_testcases
+    ; kAndK_testcases
     ; c "K+KD" kOrKd_testcases
     ; pml_testcases
     ; use_functor "PML + K"