diff --git a/testcases/SatFun.scala b/testcases/SatFun.scala
index da37a77fb8a474665d4f1f9427e5a6b060e199ea..e94804a7ed73fc2a5dd10503cf9edd536cd362fa 100644
--- a/testcases/SatFun.scala
+++ b/testcases/SatFun.scala
@@ -130,6 +130,10 @@ object SatFun {
     val dnfFormula = dnfNaive(formula)
     eval(formula, trueVars) == evalDnf(dnfFormula, trueVars)
   } ensuring(_ == true)
+  def property2(formula: Formula, trueVars: Set[Int]): Boolean = {
+    val cnfFormula = cnfNaive(formula)
+    eval(formula, trueVars) == evalCnf(cnfFormula, trueVars)
+  } ensuring(_ == true)
 
 
   def vars(formula: Formula): Set[Int] = formula match {