diff --git a/tests/plugin/kawaguchi/MiniBDD.scala b/tests/plugin/kawaguchi/MiniBDD.scala
index 0678bf4b206a98c14c03a54aadd02de49f119b72..26ed18d24b021561314ea9bd936ea0559dcceeec 100644
--- a/tests/plugin/kawaguchi/MiniBDD.scala
+++ b/tests/plugin/kawaguchi/MiniBDD.scala
@@ -67,8 +67,8 @@ object MiniBDD {
   def empty2 = Map.empty[(BDD,BDD),BDD]
   
   def mk_not(x: BDD): BDD = {
+    require(check(x))
     val cache = empty
-    assert(check(x))
     
     def mk_not_rec(cache: Map[BDD,BDD], x: BDD): (Map[BDD,BDD],BDD) = {
       cache.get(x) match {
@@ -92,9 +92,8 @@ object MiniBDD {
     }
     
     val (_,rv) = mk_not_rec(cache, x)
-    assert(check(rv))
     rv
-  }
+  } ensuring { res => check(res)}
   
   def apply_op(op: Op, b1: Boolean, b2: Boolean): Boolean = op match {
     case And() => b1 && b2
@@ -174,4 +173,9 @@ object MiniBDD {
     
     }
   }
+  
+  
+  def main(args: Array[String]) = {
+    
+  }
 }