diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 908fdabf3669d502f7f7056c7b41491feb2490e2..423206003a73629cbbdc94e1a4fb66efccc6739f 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -30,14 +30,15 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
 
           while (result.isEmpty && i < maxTries && continue) {
             val phi = andJoin(p.pc +: p.phi +: predicates)
+            val notPhi = andJoin(p.pc +: not(p.phi) +: predicates)
             //println("SOLVING " + phi + " ...")
             solver.solveSAT(phi) match {
               case (Some(true), satModel) =>
 
-                val newPhi = valuateWithModelIn(phi, xss, satModel)
+                val newNotPhi = valuateWithModelIn(notPhi, xss, satModel)
 
-                //println("REFUTING " + Not(newPhi) + "...")
-                solver.solveSAT(Not(newPhi)) match {
+                //println("REFUTING " + Not(newNotPhi) + "...")
+                solver.solveSAT(newNotPhi) match {
                   case (Some(true), invalidModel) =>
                     // Found as such as the xs break, refine predicates
                     predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates