diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala index 546f27acf17214d7e3908e0a51911eeb99f64603..6458079be4ef662a49bd25ea2f118f8df73ce56f 100644 --- a/src/main/scala/leon/Analysis.scala +++ b/src/main/scala/leon/Analysis.scala @@ -7,13 +7,9 @@ import purescala.TypeTrees._ import Extensions._ import scala.collection.mutable.{Set => MutableSet} -class Analysis(pgm : Program, val reporter: Reporter = Settings.reporter) { +class Analysis(val program : Program, val reporter: Reporter = Settings.reporter) { Extensions.loadAll(reporter) - println("Analysis on program:\n" + pgm) - val passManager = new PassManager(Seq(ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator)) - val program = passManager.run(pgm) - val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions val trivialSolver = new TrivialSolver(reporter) // This one you can't disable :D diff --git a/src/main/scala/leon/DefaultTactic.scala b/src/main/scala/leon/DefaultTactic.scala index afba6d6f65922e6dd8aa1348ebff14f20620abec..a01d025431c2ec3c704a1950410334fd322abae9 100644 --- a/src/main/scala/leon/DefaultTactic.scala +++ b/src/main/scala/leon/DefaultTactic.scala @@ -78,8 +78,6 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) { expr2 } } - println("generating post condtion with: " + functionDefinition.fromLoop) - println("for" + functionDefinition) if(functionDefinition.fromLoop) Seq(new VerificationCondition(theExpr, functionDefinition.parent.get, VCKind.InvariantPost, this.asInstanceOf[DefaultTactic]).setPosInfo(functionDefinition)) else diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala index aefcf528a0c83593f806374bdc21688c5d2a15bc..72623c96a2c732b4dac1995392545474c7f3f9c7 100644 --- a/src/main/scala/leon/Main.scala +++ b/src/main/scala/leon/Main.scala @@ -31,7 +31,9 @@ object Main { } private def defaultAction(program: Program, reporter: Reporter) : Unit = { - val analysis = new Analysis(program, reporter) + val passManager = new PassManager(Seq(ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator)) + val program2 = passManager.run(program) + val analysis = new Analysis(program2, reporter) analysis.analyse }