diff --git a/src/main/scala/leon/TestGeneration.scala b/src/main/scala/leon/TestGeneration.scala index ede34a20b7397f5260f76c4db13e7f475eeb0887..5b2f86946294d80556ab1988c74b6c0918eae0e1 100644 --- a/src/main/scala/leon/TestGeneration.scala +++ b/src/main/scala/leon/TestGeneration.scala @@ -4,6 +4,7 @@ import purescala.Common._ import purescala.Definitions._ import purescala.Trees._ import purescala.TypeTrees._ +import purescala.ScalaPrinter import Extensions._ import scala.collection.mutable.{Set => MutableSet} @@ -37,9 +38,13 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) { } FunctionInvocation(topFunDef, args) }).toSeq - testFun.body = Some(Block(funInvocs.init, funInvocs.last)) + testFun.body = Some(Block(funInvocs, UnitLiteral)) println("The test function:\n" + testFun) + val Program(id, ObjectDef(objId, defs, invariants)) = program + val testProgram = Program(id, ObjectDef(objId, testFun +: defs , invariants)) + println("New program:\n" + ScalaPrinter(testProgram)) + reporter.info("Running from waypoint with the following testcases:\n") reporter.info(testcases.mkString("\n")) }