diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 744029ee3aa6c567b0cbb8fb91570e1bd82069af..3cc97f4f5d39c9c512800162371c3b6eaac173f1 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -199,8 +199,10 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
             case None =>
               true
           }
-
-          (for {
+          
+          if(cs.optGuard == Some(BooleanLiteral(false))) {
+            Nil
+          } else (for {
             inst <- instantiations.toSeq
             inR = replaceFromIDs(inst, pattExpr)
             outR = replaceFromIDs(inst, doSubstitute(ieMap, cs.rhs))
diff --git a/testcases/stringrender/DoubleListRender.scala b/testcases/stringrender/DoubleListRender.scala
index ed28a264bea40ccd1e0655531f818d01f6a43983..284760380abde82b5d9f317e3a390a5353c283a3 100644
--- a/testcases/stringrender/DoubleListRender.scala
+++ b/testcases/stringrender/DoubleListRender.scala
@@ -24,12 +24,30 @@ object DoubleListRender {
     a == b || a == c || b == c
   } holds
 
-  def AtoString(a : A): String =  {
+  def mutual_lists(a : A): String =  {
     ???
   } ensuring {
     (res : String) => (a, res) passes {
-      case B(BB(N(), BB(B(NN(), B(NN(), N())), NN())), N()) =>
-        "[([], [(), ()])]"
+      case N() =>
+        "[]"
+      case B(NN(), N()) =>
+        "[()]"
+      case B(NN(), B(NN(), N())) =>
+        "[(), ()]"
+      case B(BB(N(), NN()), N()) =>
+        "[([])]"
+      case B(NN(), B(NN(), B(NN(), N()))) =>
+        "[(), (), ()]"
+      case B(BB(N(), BB(N(), NN())), N()) =>
+        "[([], [])]"
+      case B(NN(), B(BB(N(), NN()), N())) =>
+        "[(), ([])]"
+      case B(BB(N(), NN()), B(NN(), N())) =>
+        "[([]), ()]"
+      case B(BB(B(NN(), N()), NN()), N()) =>
+        "[([()])]"
+      case B(BB(N(), BB(N(), BB(N(), NN()))), N()) =>
+        "[([], [], [])]"
     }
   }
 }
\ No newline at end of file