Termination works with a fresh duplicated program

The termination checker updates the functions it checks in place (it
removes and adds post-conditions). We duplicate the program here to
ensure that side-effects do not propagate to other parts (such as
synthesis in the web-interface)

src/main/scala/leon/termination/ComplexTerminationChecker.scala

@@ -8,7 +8,7 @@ import purescala.Expressions._
 
 import scala.collection.mutable.{Map => MutableMap}
 
-class ComplexTerminationChecker(context: LeonContext, program: Program) extends ProcessingPipeline(context, program) {
+class ComplexTerminationChecker(context: LeonContext, initProgram: Program) extends ProcessingPipeline(context, initProgram) {
 
   val name = "Complex Termination Checker"
   val description = "A modular termination checker with a few basic modules™"

src/main/scala/leon/termination/ProcessingPipeline.scala

@@ -32,7 +32,7 @@ case class Cleared(funDef: FunDef) extends Result(funDef)
 case class Broken(funDef: FunDef, args: Seq[Expr]) extends Result(funDef)
 case class MaybeBroken(funDef: FunDef, args: Seq[Expr]) extends Result(funDef)
 
-abstract class ProcessingPipeline(context: LeonContext, program: Program) extends TerminationChecker(context, program) {
+abstract class ProcessingPipeline(context: LeonContext, initProgram: Program) extends TerminationChecker(context, initProgram) {
   implicit val debugSection = utils.DebugSectionTermination
 
   import scala.collection.mutable.{PriorityQueue, Map => MutableMap, Set => MutableSet}

src/main/scala/leon/termination/TerminationChecker.scala

@@ -7,7 +7,12 @@ import purescala.Definitions._
 import purescala.Expressions._
 import purescala.DefOps._
 
-abstract class TerminationChecker(val context: LeonContext, val program: Program) extends LeonComponent {
+abstract class TerminationChecker(val context: LeonContext, initProgram: Program) extends LeonComponent {
+  val program = {
+    val (pgm, _) = replaceFunDefs(initProgram){ fd => Some(fd.duplicate) }
+
+    pgm
+  }
 
   val functions = visibleFunDefsFromMain(program)
 

src/main/scala/leon/termination/TerminationPhase.scala

@@ -24,7 +24,7 @@ object TerminationPhase extends LeonPhase[Program,TerminationReport] {
       filterInclusive(ctx.findOption(SharedOptions.optFunctions).map(fdMatcher), Some(excludeByDefault _))
     }
 
-    val toVerify = program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
+    val toVerify = tc.program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
 
     val results = toVerify.map { funDef =>
       funDef -> tc.terminates(funDef)