diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 62f9ecbd13185e6cf8b161627cdf91b15b11fde8..0c65ed814e7c2c2f3b5bb2f30dbd4e15059a1391 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -65,6 +65,13 @@ object Definitions {
       out.write(ScalaPrinter(this))
       out.close
     }
+
+    def duplicate = {
+      copy(mainObject = mainObject.copy(defs = mainObject.defs.collect {
+        case fd: FunDef => fd.duplicate
+        case d => d
+      }))
+    }
   }
 
   object Program {
@@ -278,6 +285,16 @@ object Definitions {
     var parent: Option[FunDef] = None
     var orig: Option[FunDef] = None
 
+    def duplicate: FunDef = {
+      val fd = new FunDef(id, returnType, args)
+      fd.body = body
+      fd.precondition = precondition
+      fd.postcondition = postcondition
+      fd.parent = parent
+      fd.orig = orig
+      fd
+    }
+
     def hasImplementation : Boolean = body.isDefined
     def hasBody                     = hasImplementation
     def hasPrecondition : Boolean   = precondition.isDefined
diff --git a/src/main/scala/leon/termination/ComplexTerminationChecker.scala b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
index de9d00cc2967f64121766cd7fabb999c63bff213..8dcd43fb2f1163ed18ca2ab81a6462e6158087c7 100644
--- a/src/main/scala/leon/termination/ComplexTerminationChecker.scala
+++ b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
@@ -4,7 +4,8 @@ package termination
 import purescala.Definitions._
 import purescala.Trees._
 
-class ComplexTerminationChecker(context: LeonContext, program: Program) extends TerminationChecker(context, program) {
+class ComplexTerminationChecker(context: LeonContext, _program: Program) extends TerminationChecker(context, _program.duplicate) {
+
   import scala.collection.mutable.{Map => MutableMap}
 
   val name = "Complex Termination Checker"