diff --git a/Cadical/test.ml b/Cadical/test.ml
new file mode 100644
index 00000000..22e16a19
--- /dev/null
+++ b/Cadical/test.ml
@@ -0,0 +1,14 @@
+(* ========================================================================= *)
+(* Test the Cadical interface on a set of (relatively easy) tautologies.     *)
+(* ========================================================================= *)
+
+needs "Minisat/taut.ml";;
+
+let TEST_TAUT TAUTCHECKER p =
+  let th = time TAUTCHECKER p in
+  if hyp th = [] && concl th = p
+  then true else failwith "Wrong theorem";;
+
+map (fun (p,s) -> print_string("Attempting "^s); print_newline();
+                  s,TEST_TAUT CADICAL_PROVE p)
+        all_taut;;