diff --git a/src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala b/src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c650efe8863d1a86eedbe7e3bc0c35932e7a0b40
--- /dev/null
+++ b/src/test/scala/leon/test/solvers/z3/BugWithEmptySet.scala
@@ -0,0 +1,50 @@
+package leon.test.solvers.z3
+
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TreeOps._
+import leon.purescala.TypeTrees._
+
+import leon.SilentReporter
+
+import leon.solvers.Solver
+import leon.solvers.z3.UninterpretedZ3Solver
+
+import org.scalatest.FunSuite
+
+class BugWithEmptySet extends FunSuite {
+  private val emptyProgram = Program(FreshIdentifier("empty"), ObjectDef(FreshIdentifier("empty"), Nil, Nil))
+
+  test("No distinction between Set() and Set.empty") {
+    val tInt = Int32Type
+    val tIntSet = SetType(Int32Type)
+
+    val e1 = EmptySet(tInt).setType(tIntSet)
+    assert(e1.getType === tIntSet)
+
+    val e2 = FiniteSet(Nil).setType(tIntSet)
+    assert(e2.getType === tIntSet)
+
+    val s0 = FiniteSet(Seq(IntLiteral(0))).setType(tIntSet)
+
+    val f1 = Equals(e1, e2)
+
+    val silentReporter = new SilentReporter
+    val solver : Solver = new UninterpretedZ3Solver(silentReporter)
+    solver.setProgram(emptyProgram)
+
+    assert(solver.solve(f1) === Some(true),
+           "Z3 should prove the equivalence between Ø and {}.")
+
+    val f2 = Equals(e1, SetDifference(e1, s0))
+
+    assert(solver.solve(f2) === Some(true),
+           """Z3 should prove Ø = Ø \ {0}""")
+
+    val f3 = Equals(e2, SetDifference(e2, s0))
+
+    assert(solver.solve(f3) === Some(true),
+           """Z3 should prove {} = {} \ {0}""")
+  } 
+}
diff --git a/testcases/synthesis/BinaryTree.scala b/testcases/synthesis/BinaryTree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..02b4030fe4caa71f88260264e3376e7c04e9c417
--- /dev/null
+++ b/testcases/synthesis/BinaryTree.scala
@@ -0,0 +1,18 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+  sealed abstract class Tree
+  case class Node(left : Tree, value : Int, right : Tree) extends Tree
+  case class Leaf() extends Tree
+
+  def content(t : Tree): Set[Int] = t match {
+    case Leaf() => Set.empty[Int]
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def delete(in : Tree, v : Int) = choose { (out : Tree) =>
+    content(out) == (content(in) -- Set(v))
+  }
+}