diff --git a/testcases/synthesis/repair/PropLogic/PropLogic.scala b/testcases/synthesis/repair/PropLogic/PropLogic.scala
index c33b0500e4eed341e650d1fa51b4261d77f46d6a..718a36e89b1fb70e7eb1c4cfc0a35520f7f953c4 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic.scala
@@ -34,7 +34,9 @@ object SemanticsPreservation {
     case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
     case Or(lhs, rhs)  => Or(nnf(lhs), nnf(rhs))
     case other => other 
-  }} ensuring { isNNF(_) }
+  }} ensuring { res => 
+    isNNF(res)
+  }
 
   def isNNF(f : Formula) : Boolean = f match {
     case Not(Literal(_)) => true
@@ -44,23 +46,5 @@ object SemanticsPreservation {
     case _ => true
   }
 
-  def partEval(formula : Formula) : Formula = { formula match {
-    case And(Const(false), _ ) => Const(false)
-    case And(_, Const(false)) => Const(false)
-    case And(Const(true), e) => partEval(e)
-    case And(e, Const(true)) => partEval(e)
-    case Or(Const(true), _ ) => Const(true)
-    case Or(_, Const(true)) => Const(true)
-    case Or(Const(false), e) => partEval(e)
-    case Or(e, Const(false)) => partEval(e)
-    case Not(Const(c)) => Const(!c)
-    case other => other
-  }} ensuring { size(_) <= size(formula) }
-
-  
-  @induct
-  def partEvalSound (f : Formula, env : Set[Int]) = {
-    eval(partEval(f))(env) == eval(f)(env)
-  }.holds
-  
+    
 }
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic1.scala b/testcases/synthesis/repair/PropLogic/PropLogic1.scala
index 8ff0b9f158014010b928fb838a3e8e28a20c9a0f..47752be39082a9ab05e73030919f423131fad1c6 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic1.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic1.scala
@@ -34,7 +34,12 @@ object SemanticsPreservation {
     case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
     case Or(lhs, rhs)  => Or(nnf(lhs), nnf(rhs))
     case other => other
-  }} ensuring { isNNF(_) }
+  }} ensuring { res => 
+    isNNF(res) && ((formula, res) passes {
+      case Not(Not(Not( Const(a) ))) => Const(!a)
+    })
+  }
+
 
   def isNNF(f : Formula) : Boolean = f match {
     case Not(Literal(_)) => true
@@ -44,23 +49,5 @@ object SemanticsPreservation {
     case _ => true
   }
 
-  def partEval(formula : Formula) : Formula = { formula match {
-    case And(Const(false), _ ) => Const(false)
-    case And(_, Const(false)) => Const(false)
-    case And(Const(true), e) => partEval(e)
-    case And(e, Const(true)) => partEval(e)
-    case Or(Const(true), _ ) => Const(true)
-    case Or(_, Const(true)) => Const(true)
-    case Or(Const(false), e) => partEval(e)
-    case Or(e, Const(false)) => partEval(e)
-    case Not(Const(c)) => Const(!c)
-    case other => other
-  }} ensuring { size(_) <= size(formula) }
-
-  
-  @induct
-  def partEvalSound (f : Formula, env : Set[Int]) = {
-    eval(partEval(f))(env) == eval(f)(env)
-  }.holds
-  
+    
 }
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic3.scala b/testcases/synthesis/repair/PropLogic/PropLogic3.scala
index b905ed40fcc161bd4e6bbaebd6f45aec0075a9f3..600c59ed273b883838d2091bbfcc9c8844bf6417 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic3.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic3.scala
@@ -34,7 +34,12 @@ object SemanticsPreservation {
     case Or(lhs, rhs)  => Or(nnf(lhs), nnf(rhs))
     // FIXME: forgot to handle the Not(Not(_)) case 
     case other => other 
-  }} ensuring { isNNF(_) }
+  }} ensuring { res => 
+     isNNF(res) && ((formula, res) passes {
+       case Not(And(Const(a), Const(b))) => Or(Const(!a), Const(!b))
+       case x@And(Literal(_), Literal(_)) => x
+     })
+  }
 
   def isNNF(f : Formula) : Boolean = f match {
     case Not(Literal(_)) => true
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic4.scala b/testcases/synthesis/repair/PropLogic/PropLogic4.scala
index 549b91c457c7689384e9ab0d51fb272245ac672d..facbe08aaa9d461e83e4e6ac79c6ac0a724b6577 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic4.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic4.scala
@@ -34,7 +34,12 @@ object SemanticsPreservation {
     case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
     case Or(lhs, rhs)  => Or(nnf(lhs), nnf(rhs))
     case other => other 
-  }} ensuring { isNNF(_) }
+  }} ensuring { res => 
+      isNNF(res) && ((formula, res) passes {
+        case Not(And(Const(a), Const(b))) => Or(Const(!a), Const(!b))
+        case x@And(Literal(_), Literal(_)) => x
+      })
+  }
 
   def isNNF(f : Formula) : Boolean = f match {
     case Not(Literal(_)) => true
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic5.scala b/testcases/synthesis/repair/PropLogic/PropLogic5.scala
index 4b8a2149a82e985b65f42d4ca5f829cc30e99504..d86d184ed59a5304ba814fa44b444422bee0df6a 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic5.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic5.scala
@@ -34,7 +34,12 @@ object SemanticsPreservation {
     case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
     case Or(lhs, rhs)  => Or(nnf(lhs), nnf(rhs))
     case other => other 
-  }} ensuring { isNNF(_) }
+  }} ensuring { res => 
+       isNNF(res) && ((formula, res) passes {
+         case Not(And(Const(a), Const(b))) => Or(Const(!a), Const(!b))
+         case x@And(Literal(_), Literal(_)) => x
+       })
+  }
 
   def isNNF(f : Formula) : Boolean = f match {
     case Not(Literal(_)) => true
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic6.scala b/testcases/synthesis/repair/PropLogic/PropLogic6.scala
index 12791f753dd61634708742a1ecbefb736841b28c..4fee819e2adb59647e2da76985a94c2b25a4feef 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic6.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic6.scala
@@ -34,7 +34,12 @@ object SemanticsPreservation {
     case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
     case Or(lhs, rhs)  => Or(nnf(lhs), nnf(rhs))
     case other => other 
-  }} ensuring { isNNF(_) }
+  }} ensuring { res => 
+    isNNF(res) && ((formula, res) passes {
+      case Not(And(Const(a), Const(b))) => Or(Const(!a), Const(!b))
+      case x@And(Literal(_), Literal(_)) => x
+    })
+  }
 
   def isNNF(f : Formula) : Boolean = f match {
     case Not(Literal(_)) => true