refactor TestGen

src/main/scala/leon/CallGraph.scala → src/main/scala/leon/testgen/CallGraph.scala

-package leon
+package leon.testgen
 
 import leon.purescala.Definitions._
 import leon.purescala.Trees._
 import leon.purescala.TypeTrees._
 import leon.purescala.Common._
+import leon.FairZ3Solver
 
 class CallGraph(val program: Program) {
 

src/main/scala/leon/TestGeneration.scala → src/main/scala/leon/testgen/TestGeneration.scala

-package leon
-
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Trees._
-import purescala.TypeTrees._
-import purescala.ScalaPrinter
-import Extensions._
-import scala.collection.mutable.{Set => MutableSet}
+package leon.testgen
+
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.Trees._
+import leon.purescala.TypeTrees._
+import leon.purescala.ScalaPrinter
+import leon.Extensions._
+import leon.FairZ3Solver
+import leon.Reporter
 
+import scala.collection.mutable.{Set => MutableSet}
 
 class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
 

testcases/testgen/Abs.scala

 import leon.Utils._
+import leon.Annotations._
 
 object Abs {
 
+  @main
   def abs(x: Int): Int = {
-    waypoint(1, if(x < 0) -x else x) 
+    if(x < 0) -x else x
   } ensuring(_ >= 0)
 
 }