diff --git a/library/collection/List.scala b/library/collection/List.scala
index 74a0f0c66e3bc23780076e16acdc6f7035c6986b..8ee7c398aa09d684ebf6a6cfb1f51124d4451151 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -556,9 +556,11 @@ sealed abstract class List[T] {
 }
 
 @isabelle.constructor(name = "List.list.Cons")
+@library
 case class Cons[T](h: T, t: List[T]) extends List[T]
 
 @isabelle.constructor(name = "List.list.Nil")
+@library
 case class Nil[T]() extends List[T]
 
 object List {
diff --git a/library/lang/Option.scala b/library/lang/Option.scala
index a6f09db68f3fecc7ad8095506a49d21e4d8ac7ad..04412e51b7b8cf642d6cc1d237e76f5b2907c8cf 100644
--- a/library/lang/Option.scala
+++ b/library/lang/Option.scala
@@ -78,7 +78,9 @@ sealed abstract class Option[T] {
 }
 
 @isabelle.constructor(name = "Option.option.Some")
+@library
 case class Some[T](v: T) extends Option[T]
 
 @isabelle.constructor(name = "Option.option.None")
+@library
 case class None[T]() extends Option[T]
diff --git a/library/lang/package.scala b/library/lang/package.scala
index b19ec529bdb3975956de00a7da8e8ad39bcf34e4..679495565b674ce4d0869d9082cff1a3a2b3c764 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -8,6 +8,7 @@ import scala.language.implicitConversions
 package object lang {
 
   implicit class BooleanDecorations(val underlying: Boolean) {
+
     @inline
     def holds : Boolean = {
       underlying
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 67e5c4502ad1810b323616916e3edfab9c05a8ea..cb0c7f96f914c190954a3c896ef531efe127bb8f 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -453,7 +453,11 @@ trait ASTExtractors {
           } else if (!dd.symbol.isSynthetic) {
             Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
           } else {
-            None
+            if(name.toString == "copy" || name.toString.startsWith("copy$default$")) {
+              Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
+            } else {
+              None
+            }
           }
         case _ => None
       }
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 8fb753d23d35364059115f7032bef3310c492d82..40091637c3c9dfa019df83a1b502448b7b221881 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -351,6 +351,21 @@ object Definitions {
       CaseClassType(this, tps)
     }
     def typed: CaseClassType = typed(tparams.map(_.tp))
+
+    //TODO: the function works via a horrible hack, as it is not very clear where the
+    //      companion object will end up being defined.
+    //      This also return an Option as Leon compiles some non-case class (so without
+    //      copy) towards an internal case class.
+    //FIXME: it does not properly handle copy methods coming from multiple children
+    //       that got lifted to a single root class.
+    def copyDef(implicit pgm: Program): Option[FunDef] = {
+      val tryName1 = DefOps.fullName(this.root) + ".copy"
+      val tryName2 = this.root.id.name + ".copy" //generated companion object of case classes defined inside objects are currently lifted at the top level.
+      pgm.lookup(tryName1).collectFirst { case (fd: FunDef) => fd }.orElse(
+        pgm.lookup(tryName2).collectFirst { case (fd: FunDef) => fd }
+      )
+    }
+
   }
 
   /** Function/method definition.
diff --git a/src/test/resources/regression/verification/purescala/valid/Copy.scala b/src/test/resources/regression/verification/purescala/valid/Copy.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d30d403a0be0dc9257653f2c4b817c3c8e0d2016
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Copy.scala
@@ -0,0 +1,16 @@
+object Copy {
+
+  case class A(a: Int, b: Int)
+
+  def f(a: A): A = {
+    a.copy(b = 17)
+  } ensuring(res => res.a == a.a && res.b == 17)
+
+  def g(a: A): A = {
+    a.copy(b = 17)
+  } ensuring(res => res.a == a.a)
+
+  def h(a: A): A = {
+    a.copy(b = 17)
+  } ensuring(res => res.b == 17)
+}