diff --git a/src/main/scala/leon/termination/ComplexTerminationChecker.scala b/src/main/scala/leon/termination/ComplexTerminationChecker.scala index 024792e2383f5deca56e4e4aad5a5d9686edf7ea..eef8ddaac7d2f99d47e3f713b6f71925826202ab 100644 --- a/src/main/scala/leon/termination/ComplexTerminationChecker.scala +++ b/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™" diff --git a/src/main/scala/leon/termination/ProcessingPipeline.scala b/src/main/scala/leon/termination/ProcessingPipeline.scala index 3b7a36c0a3127e95a524a95a296bd1fb5295521f..0dbdb9bd0523d5eaeb8831bbf9fc62d7cb3a7359 100644 --- a/src/main/scala/leon/termination/ProcessingPipeline.scala +++ b/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} diff --git a/src/main/scala/leon/termination/TerminationChecker.scala b/src/main/scala/leon/termination/TerminationChecker.scala index 9b12460d2c77834b6685c5050dc7d2367e2d5b32..fb881892221fb477c1e19f5b193ba2316711d5b6 100644 --- a/src/main/scala/leon/termination/TerminationChecker.scala +++ b/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) diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala index 12af96737f81912654b09421200f9aee4fe4e878..a2bd46d9077ca0834e9cac1ba6f6ffcff68d2c78 100644 --- a/src/main/scala/leon/termination/TerminationPhase.scala +++ b/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)