diff --git a/buddy/ChangeLog b/buddy/ChangeLog
index 20512128f..cfe5b9e3f 100644
--- a/buddy/ChangeLog
+++ b/buddy/ChangeLog
@@ -1,3 +1,7 @@
+2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	* src/kernel.h (CHECK, CHECKa, CHECKn): Disable if NDEBUG is set.
+
 2011-04-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Fix declaration of bddproduced.
diff --git a/buddy/src/kernel.h b/buddy/src/kernel.h
index 580311724..b024dcc9b 100644
--- a/buddy/src/kernel.h
+++ b/buddy/src/kernel.h
@@ -54,7 +54,11 @@
 #error The compiler does not support 4 byte integers!
 #endif
 
-
+#ifdef NDEBUG
+#define CHECK(r) (void)(r);
+#define CHECKa(r,a) (void)(r); (void)(a);
+#define CHECKn(r) (void)(r);
+#else
    /* Sanity check argument and return eventual error code */
 #define CHECK(r)\
    if (!bddrunning) return bdd_error(BDD_RUNNING);\
@@ -75,7 +79,7 @@
      { bdd_error(BDD_ILLBDD); return; }\
    else if (r >= 2 && LOW(r) == -1)\
      { bdd_error(BDD_ILLBDD); return; }
-
+#endif
 
 /*=== SEMI-INTERNAL TYPES ==============================================*/