diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 3f96d94887186aa5a1afdb995ecce21e49a8d5f0..40e3a61177d434915c01a0a36508d67f66d89152 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -327,7 +327,11 @@ trait CodeExtraction extends ASTExtractors {
     }
     
     private def extractPackageRef(refPath : RefTree) : PackageRef =       
-      getSelectChain(refPath.qualifier) :+ refPath.name.toString
+      (getSelectChain(refPath.qualifier) :+ refPath.name.toString) match {
+        // Make sure to drop "<empty>" package
+        case List("<empty>") => List()
+        case other => other
+      }
     
     private def extractImport(i : Import, current : UnitDef, units : List[UnitDef]) : Seq[ LeonImport ] = i match { case Import(expr, sels) => 
       import DefOps._
diff --git a/src/test/scala/leon/test/purescala/DefOpsTests.scala b/src/test/scala/leon/test/purescala/DefOpsTests.scala
index 605e5012b7bf8eecdd27bfe8473c0001efd36c25..f6a062f1652b762c0401ca13c5ade3a4b5b1cfdd 100644
--- a/src/test/scala/leon/test/purescala/DefOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/DefOpsTests.scala
@@ -72,7 +72,9 @@ private [purescala] object DefOpsHelper {
         
     """ |package foo.bar.baz.and.some.more
         |object InSubpackage {}
-        |""".stripMargin
+        |""".stripMargin,
+
+    """ object InEmpty { def arrayLookup(a : Array[Int], i : Int) = a(i) } """
   )
   val program = parseStrings(test1)
   val fooC = searchByFullName("foo.bar.baz.Foo.fooC",program)
@@ -91,6 +93,13 @@ class DefOpsTests extends LeonTestSuite {
       val fooClass = searchByFullName("foo.bar.baz.Foo.FooC",program)
       assert (fooClass.isDefined)
       assert(leastCommonAncestor(fooC.get, fooClass.get).id.name == "Foo")
+    } 
+
+    test("In empty package") { 
+      val name = "InEmpty.arrayLookup"
+      val df = searchByFullName(name,program)
+      assert(df.isDefined)
+      assert{fullName(df.get) == name } 
     }
     
     // Search by full name    
@@ -113,7 +122,8 @@ class DefOpsTests extends LeonTestSuite {
     
     mustFind("other.hello.world.Foo",     "Find a definition in another package")
     mustFind("and.some.more.InSubpackage","Find a definition in a subpackage")
-    
+    mustFind("InEmpty.arrayLookup",       "Find a definition in the empty package")
+
     mustFail("nonExistent",    "Don't find non-existent definition")
     mustFail("A",              "Don't find definition in another object")
     mustFail("InSubpackage",   "Don't find definition in another package")