diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala index 94e94a8580f4540a6efc06452b2e0e13fea34209..f6d53576741a6dd12da4a05344559d5ecc95d471 100644 --- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala +++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala @@ -6,6 +6,8 @@ package xlang import leon.purescala.Definitions._ import leon.verification._ +import leon.utils._ + object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] { val name = "xlang analysis" @@ -23,6 +25,11 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] { val (pgm1, wasLoop) = ImperativeCodeElimination.run(ctx)(pgm) val pgm2 = purescala.FunctionClosure.run(ctx)(pgm1) + if (ctx.reporter.isDebugEnabled(DebugSectionTrees)) { + PrintTreePhase("Program after xlang transformations").run(ctx)(pgm2) + } + + def functionWasLoop(fd: FunDef): Boolean = fd.orig match { case Some(nested) => // could have been a LetDef originally wasLoop.contains(nested)