diff --git a/project/build/funcheck.scala b/project/build/funcheck.scala
index df1b11317bda68063d50a7d272f927d7f8c55cf1..d649b73b58147e2f806da2774bf0d645502243ec 100644
--- a/project/build/funcheck.scala
+++ b/project/build/funcheck.scala
@@ -5,9 +5,12 @@ class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileT
   override def dependencyPath      = "lib"
   override def shouldCheckOutputDirectories = false
 
-  lazy val purescala = project(".", "PureScala Definitions", new PureScalaProject(_))
-  lazy val plugin    = project(".", "FunCheck Plugin", new PluginProject(_), purescala)
-  lazy val multisets = project(".", "Multiset Solver", new MultisetsProject(_), plugin, purescala)
+  lazy val purescala  = project(".", "PureScala Definitions", new PureScalaProject(_))
+  lazy val plugin     = project(".", "FunCheck Plugin", new PluginProject(_), purescala)
+  lazy val multisets  = project(".", "Multiset Solver", new MultisetsProject(_), plugin, purescala)
+  lazy val orderedsets = project(".", "Ordered Sets Solver", new OrderedSetsProject(_), plugin, purescala)
+
+  lazy val extensionJars : List[Path] = multisets.jarPath :: orderedsets.jarPath :: Nil
 
   val scriptPath: Path = "." / "scalac-funcheck"
 
@@ -22,7 +25,20 @@ class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileT
       val nl = System.getProperty("line.separator")
       val f = scriptPath.asFile
       val fw = new java.io.FileWriter(f)
-      fw.write("#!/bin/sh" + nl)
+      fw.write("#!/bin/bash" + nl)
+      fw.write("FUNCHECKCLASSPATH=")
+      fw.write(buildLibraryJar.absolutePath + ":")
+      fw.write(buildCompilerJar.absolutePath + ":")
+      fw.write(purescala.jarPath.absolutePath + ":")
+      fw.write(plugin.jarPath.absolutePath + ":")
+      fw.write(("lib" / "z3.jar").absolutePath)
+      fw.write(nl + nl)
+      fw.write("for f in " + extensionJars.map(_.absolutePath).map(n => "\"" + n + "\"").mkString(" ") + "; do" + nl)
+      fw.write("  if [ -e ${f} ]" + nl)
+      fw.write("  then" + nl)
+      fw.write("    FUNCHECKCLASSPATH=${FUNCHECKCLASSPATH}:${f}" + nl)
+      fw.write("  fi" + nl)
+      fw.write("done" + nl + nl)
       fw.write("LD_LIBRARY_PATH=" + ("." / "lib-bin").absolutePath + " \\" + nl)
       fw.write("java \\" + nl)
 
@@ -30,12 +46,7 @@ class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileT
       val libStr = (buildLibraryJar.absolutePath).toString
       fw.write("    -Dscala.home=" + libStr.substring(0, libStr.length-21) + " \\" + nl)
 
-      fw.write("    -classpath \\" + nl)
-      fw.write("    " + buildLibraryJar.absolutePath + ":")
-      fw.write(buildCompilerJar.absolutePath + ":")
-      fw.write(purescala.jarPath.absolutePath + ":")
-      fw.write(plugin.jarPath.absolutePath + ":")
-      fw.write(("lib" / "z3.jar").absolutePath + " \\" + nl)
+      fw.write("    -classpath ${FUNCHECKCLASSPATH} \\" + nl)
       fw.write("  scala.tools.nsc.Main -Xplugin:" + plugin.jarPath.absolutePath + " $@" + nl)
       fw.close
       f.setExecutable(true)
@@ -73,5 +84,9 @@ class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileT
     override def mainScalaSourcePath = "src" / "multisets"
     override def unmanagedClasspath = super.unmanagedClasspath +++ purescala.jarPath
   }
-  
+  class OrderedSetsProject(info: ProjectInfo) extends PersonalizedProject(info) {
+    override def outputPath = "bin" / "orderedsets"
+    override def mainScalaSourcePath = "src" / "orderedsets"
+    override def unmanagedClasspath = super.unmanagedClasspath +++ purescala.jarPath
+  }
 }
diff --git a/src/orderedsets/Main.scala b/src/orderedsets/Main.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7cc8895a8d714d4528e0531f22baba5903f72f5a
--- /dev/null
+++ b/src/orderedsets/Main.scala
@@ -0,0 +1,14 @@
+package orderedsets
+
+import purescala.Reporter
+import purescala.Extensions._
+import purescala.Trees._
+
+class Main(reporter: Reporter) extends Solver(reporter) {
+  val description = "Solver for constraints on ordered sets"
+
+  def solve(expr: Expr) : Option[Boolean] = {
+    reporter.info(expr, "I have no idea how to solve this :(")
+    None
+  }
+}
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index 8d617a834b0eab57a5a4e871d2468335dfccc447..1306ed75e7a83a2fb2c25f16076a22cd09691580 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -139,6 +139,8 @@ object Trees {
   case class SetIntersection(set1: Expr, set2: Expr) extends Expr 
   case class SetUnion(set1: Expr, set2: Expr) extends Expr 
   case class SetDifference(set1: Expr, set2: Expr) extends Expr 
+  case class SetMin(set: Expr) extends Expr
+  case class SetMax(set: Expr) extends Expr
 
   /* Multiset expressions */
   // case class EmptyMultiset(baseType: TypeTree) extends Expr