From 07d49a0ccf39b7162065fc91e6207ddc5f286f5b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 27 Jun 2012 14:20:44 +0200
Subject: [PATCH] more properties on Sat

---
 testcases/SatFun.scala | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/testcases/SatFun.scala b/testcases/SatFun.scala
index e94804a7e..c1e47f9e8 100644
--- a/testcases/SatFun.scala
+++ b/testcases/SatFun.scala
@@ -1,3 +1,5 @@
+import leon.Utils._
+
 object SatFun {
 
   sealed abstract class Formula
@@ -129,11 +131,23 @@ object SatFun {
   def property1(formula: Formula, trueVars: Set[Int]): Boolean = {
     val dnfFormula = dnfNaive(formula)
     eval(formula, trueVars) == evalDnf(dnfFormula, trueVars)
-  } ensuring(_ == true)
+  } holds
+
   def property2(formula: Formula, trueVars: Set[Int]): Boolean = {
     val cnfFormula = cnfNaive(formula)
     eval(formula, trueVars) == evalCnf(cnfFormula, trueVars)
-  } ensuring(_ == true)
+  } holds
+
+  def propertyWrong1(formula: Formula, trueVars: Set[Int]): Boolean = {
+    val dnfFormula = dnfNaive(formula)
+    isSatDnf(dnfFormula)
+  } holds
+
+  def property3(formula: Formula, trueVars: Set[Int]): Boolean = {
+    val dnfFormula = dnfNaive(formula)
+    if(!isSatDnf(dnfFormula)) eval(formula, trueVars) else true
+  } holds
+
 
 
   def vars(formula: Formula): Set[Int] = formula match {
-- 
GitLab