still some infinite loop on some unrollings (eg. pldi/InsertionSort:min), but...

still some infinite loop on some unrollings (eg. pldi/InsertionSort:min), but some examples are solved. yay.

pldi2011-testcases/RedBlackTree.scala

@@ -65,11 +65,11 @@ object RedBlackTree {
     makeBlack(ins(x, t))
   } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
   
-  def buggyAdd(x: Int, t: Tree): Tree = {
-    require(redNodesHaveBlackChildren(t))
-    // makeBlack(ins(x, t))
-    ins(x, t)
-  } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+//  def buggyAdd(x: Int, t: Tree): Tree = {
+//    require(redNodesHaveBlackChildren(t))
+//    // makeBlack(ins(x, t))
+//    ins(x, t)
+//  } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
   
   def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
     require(

project/build/funcheck.scala

@@ -48,7 +48,7 @@ class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileT
       fw.write(plugin.jarPath.absolutePath)
       fw.write("\"" + nl + nl)
       fw.write("LD_LIBRARY_PATH=" + ("." / "lib-bin").absolutePath + " \\" + nl)
-      fw.write("java \\" + nl)
+      fw.write("java -Xmx1024M \\" + nl)
 
       // This is a hack :(
       val libStr = (buildLibraryJar.absolutePath).toString

src/purescala/Trees.scala

@@ -654,6 +654,19 @@ object Trees {
     treeCatamorphism(convert, combine, compute, expr)
   }
 
+  def topLevelFunctionCallsOf(expr: Expr) : Set[FunctionInvocation] = {
+    def convert(t: Expr) : Set[FunctionInvocation] = t match {
+      case f @ FunctionInvocation(_, _) => Set(f)
+      case _ => Set.empty
+    }
+    def combine(s1: Set[FunctionInvocation], s2: Set[FunctionInvocation]) = s1 ++ s2
+    def compute(t: Expr, s: Set[FunctionInvocation]) = t match {
+      case f @ FunctionInvocation(_, _) => Set(f) // ++ s that's the difference with the one below
+      case _ => s
+    }
+    treeCatamorphism(convert, combine, compute, expr)
+  }
+
   def functionCallsOf(expr: Expr) : Set[FunctionInvocation] = {
     def convert(t: Expr) : Set[FunctionInvocation] = t match {
       case f @ FunctionInvocation(_, _) => Set(f)