clean up the code

src/main/scala/leon/TestGeneration.scala

@@ -25,7 +25,6 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
       case Waypoint(1, _) => true
       case _ => false
     })).get
-    println("Top level function: " + topFunDef)
 
     val testFun = new FunDef(FreshIdentifier("test"), UnitType, Seq())
     val funInvocs = testcases.map(testcase => {
@@ -39,7 +38,6 @@ class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
       FunctionInvocation(topFunDef, args)
     }).toSeq
     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))

testcases/testgen/Diamond.scala

+import leon.Utils._
+
+object Diamond {
+
+  def foo(x: Int): Int = waypoint(1, if(x < 0) bar(x) else bar(x))
+
+  def bar(y: Int): Int = if(y > 5) y else -y
+
+}

testcases/testgen/MultiCall.scala

+import leon.Utils._
+
+object MultiCall {
+
+
+  def a(i: Int): Int = waypoint(1, if(i < 0) b(i) else c(i))
+
+  def b(j: Int): Int = if(j == -5) d(j) else e(j)
+  def c(k: Int): Int = if(k == 5) d(k) else e(k)
+
+  def d(l: Int): Int = l
+  def e(m: Int): Int = m
+
+}

testcases/testgen/Sum.scala

+import leon.Utils._
+
+object Sum {
+
+  def sum(n: Int): Int = {
+    waypoint(1, if(n <= 0) 0 else n + sum(n-1))
+  } ensuring(_ >= 0)
+
+}