diff --git a/cp-demo/FirstClassConstraints.scala b/cp-demo/FirstClassConstraints.scala
index 983154ea7053de883c0012d52c379eda73fd6f65..4fb908670012a43cd97409d56d959aade2f9e59d 100644
--- a/cp-demo/FirstClassConstraints.scala
+++ b/cp-demo/FirstClassConstraints.scala
@@ -40,9 +40,10 @@ object FirstClassConstraints {
     val f5 = ((x : Int, y : Int) => x + y) compose0 ((x : Int) => x + 42) compose1 ((x: Int) => x + 43)
     println("Composed f5: " + f5.expr)
 
-    // println("has size 3: " + hasSize(3).expr)
-
-    for (s <- hasSize(3).findAll)
-      println(s)
+    // println("has size 5: " + hasSize(5).expr)
+ 
+    println(hasSize(5).solve)
+    // for (s <- hasSize(3).findAll)
+    //   println(s)
   }
 }
diff --git a/cp-runner b/cp-runner
index aabc3c235a8293e5837f808faea9b53db6772c86..365392426fe8451ecda86335b5c4f23cbc636b72 100755
--- a/cp-runner
+++ b/cp-runner
@@ -1,4 +1,5 @@
 #!/bin/bash
 
 LD_LIBRARY_PATH=lib-bin \
+JAVA_OPTS="-Xmx512M -Xms512M -Xss256M" \
 scala -classpath bin/purescala/purescala-definitions_2.8.1-1.0.jar:lib/z3.jar:bin/cp/constraint-programming-plugin_2.8.1-1.0.jar:out ${@}
diff --git a/src/cp/CodeGeneration.scala b/src/cp/CodeGeneration.scala
index 3da20918272d0432b136c9227725b6c323229544..a94ffc9cd9ebbdb0c4a03b3a73a895699a475eb9 100644
--- a/src/cp/CodeGeneration.scala
+++ b/src/cp/CodeGeneration.scala
@@ -44,11 +44,6 @@ trait CodeGeneration {
   private lazy val skipCounterFunction            = definitions.getMember(runtimeMethodsModule, "skipCounter")
   private lazy val copySettingsFunction           = definitions.getMember(runtimeMethodsModule, "copySettings")
 
-  private lazy val termModules                    = List(
-                                                    definitions.getModule("cp.Terms.Term1"),
-                                                    definitions.getModule("cp.Terms.Term2")
-                                                    )
-
   private lazy val converterClass                 = definitions.getClass("cp.Converter")
 
   private lazy val serializationModule            = definitions.getModule("cp.Serialization")
@@ -79,6 +74,8 @@ trait CodeGeneration {
   private lazy val andClass                       = definitions.getClass("purescala.Trees.And")
   private lazy val equalsClass                    = definitions.getClass("purescala.Trees.Equals")
 
+  private def termModules(arity : Int)            = definitions.getModule("cp.Terms.Term" + arity)
+
   class CodeGenerator(unit : CompilationUnit, owner : Symbol, defaultPos : Position) {
 
     private def newSerialized(serialized : Serialized) : Tree = {
@@ -233,7 +230,7 @@ trait CodeGeneration {
     }
 
     def newBaseTerm(exprToScalaSym : Symbol, serializedProg : Serialized, serializedInputVarList : Serialized, serializedOutputVars : Serialized, serializedExpr : Serialized, inputVarValues : Tree, arity : Int) : Tree = {
-      termModules(arity-1) APPLY (
+      termModules(arity) APPLY (
         newConverter(exprToScalaSym),
         newSerialized(serializedProg),
         newSerialized(serializedInputVarList),
diff --git a/src/cp/Terms.scala b/src/cp/Terms.scala
index 4ba948c20d7ad0a735b87db5e9cf1445e537d495..3bcc32d94d737a5a3eea550d5665ba0b6f92a2a5 100644
--- a/src/cp/Terms.scala
+++ b/src/cp/Terms.scala
@@ -73,6 +73,21 @@ object Terms {
     def compose1[A](other : Term1[A, T2]) : Term2[T1,A,R] = compose_1_1_2(other, this)
   }
 
+  /** Terms with three arguments */
+  sealed trait Term3[T1,T2,T3,R] extends Term[(T1,T2,T3),R] {
+    val convertingFunction = converterOf(this).exprSeq2scala3[T1,T2,T3] _
+    type t2c = (Term3[T1,T2,T3,R]) => Term3[T1,T2,T3,Boolean]
+
+    def minimizing(minFunc : IntTerm3[T1,T2,T3])(implicit asConstraint: t2c) : MinConstraint3[T1,T2,T3] =
+      MinConstraint3[T1,T2,T3](asConstraint(this), minFunc)
+      
+    def ||(other : Constraint3[T1,T2,T3])(implicit asConstraint: t2c) : Constraint3[T1,T2,T3] = OrConstraint3[T1,T2,T3](this, other)
+
+    def &&(other : Constraint3[T1,T2,T3])(implicit asConstraint: t2c) : Constraint3[T1,T2,T3] = AndConstraint3[T1,T2,T3](this, other)
+
+    def unary_!(implicit asConstraint: t2c) : Constraint3[T1,T2,T3] = NotConstraint3[T1,T2,T3](this)
+  }
+
     /*  this is for Constraint2[A,B]
     def proj0 : Constraint1[A] = this.asInstanceOf[Constraint] match {
       case BaseTerm(conv,pr,ex,ts) => {
@@ -126,10 +141,21 @@ object Terms {
       new Term[(T1,T2),R](program, expr, types, converter) with Term2[T1,T2,R]
   }
 
+  object Term3 {
+    def apply[T1,T2,T3,R](conv : Converter, serializedProg : Serialized, serializedInputVars : Serialized, serializedOutputVars : Serialized, serializedExpr : Serialized, inputVarValues : Seq[Expr]) = {
+      val (converter, program, expr, types) = Term.processArgs(conv, serializedProg, serializedInputVars, serializedOutputVars, serializedExpr, inputVarValues)
+      new Term[(T1,T2,T3),R](program, expr, types, converter) with Term3[T1,T2,T3,R]
+    }
+
+    def apply[T1,T2,T3,R](program : Program, expr : Expr, types : Seq[TypeTree], converter : Converter) =
+      new Term[(T1,T2,T3),R](program, expr, types, converter) with Term3[T1,T2,T3,R]
+  }
+
   /** A constraint is just a term with Boolean range */
   type Constraint[T] = Term[T,Boolean]
   type Constraint1[T1] = Term1[T1,Boolean]
   type Constraint2[T1,T2] = Term2[T1,T2,Boolean]
+  type Constraint3[T1,T2,T3] = Term3[T1,T2,T3,Boolean]
 
   object OrConstraint1 {
     def apply[A](l : Constraint[A], r : Constraint[A]) : Constraint1[A] = (l, r) match {
@@ -151,6 +177,16 @@ object Terms {
     }
   }
 
+  object OrConstraint3 {
+    def apply[A,B,C](l : Constraint[(A,B,C)], r : Constraint[(A,B,C)]) : Constraint3[A,B,C] = (l, r) match {
+      case (Term(p1,ex1,ts1,conv1), Term(p2,ex2,ts2,conv2)) => Term3(p1,Or(ex1,ex2),ts1,conv1)
+    }
+
+    def apply[A,B,C](cs : Seq[Constraint[(A,B,C)]]) : Constraint3[A,B,C] = cs match {
+      case s @ Seq(Term(p,ex,ts,conv), _*) => Term3(p, Or(s.map(_.expr)), ts, conv)
+    }
+  }
+
   object AndConstraint1 {
     def apply[A](l : Constraint[A], r : Constraint[A]) : Constraint1[A] = (l, r) match {
       case (Term(p1,ex1,ts1,conv1), Term(p2,ex2,ts2,conv2)) => Term1(p1,And(ex1,ex2),ts1,conv1)
@@ -171,6 +207,16 @@ object Terms {
     }
   }
 
+  object AndConstraint3 {
+    def apply[A,B,C](l : Constraint[(A,B,C)], r : Constraint[(A,B,C)]) : Constraint3[A,B,C] = (l, r) match {
+      case (Term(p1,ex1,ts1,conv1), Term(p2,ex2,ts2,conv2)) => Term3(p1,And(ex1,ex2),ts1,conv1)
+    }
+
+    def apply[A,B,C](cs : Seq[Constraint[(A,B,C)]]) : Constraint3[A,B,C] = cs match {
+      case s @ Seq(Term(p,ex,ts,conv), _*) => Term3(p, And(s.map(_.expr)), ts, conv)
+    }
+  }
+
   object NotConstraint1 {
     def apply[A](c : Constraint[A]) : Constraint1[A] = c match {
       case Term(p,ex,ts,conv) => Term1(p,Not(ex),ts,conv)
@@ -183,9 +229,16 @@ object Terms {
     }
   }
 
+  object NotConstraint3 {
+    def apply[A,B,C](c : Constraint[(A,B,C)]) : Constraint3[A,B,C] = c match {
+      case Term(p,ex,ts,conv) => Term3(p,Not(ex),ts,conv)
+    }
+  }
+
   type IntTerm[T] = Term[T,Int]
   type IntTerm1[T1] = Term1[T1,Int]
   type IntTerm2[T1,T2] = Term2[T1,T2,Int]
+  type IntTerm3[T1,T2,T3] = Term3[T1,T2,T3,Int]
 
   /** This construct represents a constraint with an expression to minimize */
   abstract class MinConstraint[T](cons : Constraint[_], minFunc : IntTerm[_]) {
@@ -217,6 +270,10 @@ object Terms {
     val convertingFunction = converterOf(cons).exprSeq2scala2[T1,T2] _
   }
 
+  case class MinConstraint3[T1,T2,T3](cons : Constraint3[T1,T2,T3], minFunc : IntTerm3[T1,T2,T3]) extends MinConstraint[(T1,T2,T3)](cons, minFunc) {
+    val convertingFunction = converterOf(cons).exprSeq2scala3[T1,T2,T3] _
+  }
+
   /********** TERM METHODS **********/
   /** compose_i_j_k will compose f (of arity j) and g (of arity k) as "g∘f" by
    * inserting arguments of f in place of argument i of g */
@@ -224,19 +281,52 @@ object Terms {
     val (newExpr, newTypes) = compose(f, g, 0, 1, 1)
     Term1(f.program, newExpr, newTypes, f.converter)
   }
+
   private def compose_0_2_1[A1,A2,R1,R2](f : Term[(A1,A2),R1], g : Term[(R1),R2]) : Term2[A1,A2,R2] = {
     val (newExpr, newTypes) = compose(f, g, 0, 2, 1)
     Term2(f.program, newExpr, newTypes, f.converter)
   }
+
+  private def compose_0_3_1[A1,A2,A3,R1,R2](f : Term[(A1,A2,A3),R1], g : Term[(R1),R2]) : Term3[A1,A2,A3,R2] = {
+    val (newExpr, newTypes) = compose(f, g, 0, 3, 1)
+    Term3(f.program, newExpr, newTypes, f.converter)
+  }
+
   private def compose_0_1_2[A1,R1,B2,R2](f : Term[(A1),R1], g : Term[(R1,B2),R2]) : Term2[A1,B2,R2] = {
     val (newExpr, newTypes) = compose(f, g, 0, 1, 2)
     Term2(f.program, newExpr, newTypes, f.converter)
   }
+
   private def compose_1_1_2[A1,R1,B1,R2](f : Term[(A1),R1], g : Term[(B1,R1),R2]) : Term2[B1,A1,R2] = {
     val (newExpr, newTypes) = compose(f, g, 1, 1, 2)
     Term2(f.program, newExpr, newTypes, f.converter)
   }
 
+  private def compose_0_2_2[A1,A2,R1,B2,R2](f : Term[(A1,A2),R1], g : Term[(R1,B2),R2]) : Term3[A1,A2,B2,R2] = {
+    val (newExpr, newTypes) = compose(f, g, 0, 2, 2)
+    Term3(f.program, newExpr, newTypes, f.converter)
+  }
+
+  private def compose_1_2_2[A1,A2,R1,B1,R2](f : Term[(A1,A2),R1], g : Term[(B1,R1),R2]) : Term3[B1,A1,A2,R2] = {
+    val (newExpr, newTypes) = compose(f, g, 1, 2, 2)
+    Term3(f.program, newExpr, newTypes, f.converter)
+  }
+
+  private def compose_0_1_3[A1,R1,B2,B3,R2](f : Term[(A1),R1], g : Term[(R1,B2,B3),R2]) : Term3[A1,B2,B3,R2] = {
+    val (newExpr, newTypes) = compose(f, g, 0, 1, 3)
+    Term3(f.program, newExpr, newTypes, f.converter)
+  }
+
+  private def compose_1_1_3[A1,R1,B1,B3,R2](f : Term[(A1),R1], g : Term[(B1,R1,B3),R2]) : Term3[B1,A1,B3,R2] = {
+    val (newExpr, newTypes) = compose(f, g, 1, 1, 3)
+    Term3(f.program, newExpr, newTypes, f.converter)
+  }
+
+  private def compose_2_1_3[A1,R1,B1,B2,R2](f : Term[(A1),R1], g : Term[(B1,B2,R1),R2]) : Term3[B1,B2,A1,R2] = {
+    val (newExpr, newTypes) = compose(f, g, 2, 1, 3)
+    Term3(f.program, newExpr, newTypes, f.converter)
+  }
+
   /** Compute composed expression for g∘f */
   private def compose(f : Term[_,_], g : Term[_,_], index : Int, nf : Int, ng : Int) : (Expr, Seq[TypeTree]) = (f, g) match {
     case (Term(_,ef,tf,_),Term(_,eg,tg,_)) => {