diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index 32e75bf1ffe9122f1798b62b8684bd6d1bc776b2..7f592aeb72a53e07f2edabac4776e1c118c9c5b4 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -160,12 +160,19 @@ trait CodeExtraction extends Extractors {
         case None => Variable(id)
       }
       case ExAnd(l, r) => And(rec(l), rec(r))
+      case ExOr(l, r) => Or(rec(l), rec(r))
+      case ExNot(e) => Not(rec(e))
+      case ExUMinus(e) => UMinus(rec(e))
       case ExPlus(l, r) => Plus(rec(l), rec(r))
+      case ExMinus(l, r) => Minus(rec(l), rec(r))
+      case ExTimes(l, r) => Times(rec(l), rec(r))
+      case ExDiv(l, r) => Division(rec(l), rec(r))
       case ExEquals(l, r) => Equals(rec(l), rec(r))
       case ExGreaterThan(l, r) => GreaterThan(rec(l), rec(r))
       case ExGreaterEqThan(l, r) => GreaterEquals(rec(l), rec(r))
       case ExLessThan(l, r) => LessThan(rec(l), rec(r))
       case ExLessEqThan(l, r) => LessEquals(rec(l), rec(r))
+      case ExIfThenElse(t1,t2,t3) => IfExpr(rec(t1), rec(t2), rec(t3))
   
       // default behaviour is to complain :)
       case _ => {
@@ -184,10 +191,13 @@ trait CodeExtraction extends Extractors {
     tree match {
       case tt: TypeTree if tt.tpe == IntClass.tpe => Int32Type
       case tt: TypeTree if tt.tpe == BooleanClass.tpe => BooleanType
+      case tt: TypeTree =>  tt.tpe match {
+        case TypeRef(_,sym,_) if sym == setTraitSym => XXXXXX
+      }
 
-      case _ => {
+      case tt => {
         if(!silent) {
-          unit.error(tree.pos, "Could not extract type as PureScala.")
+          unit.error(tree.pos, "Could not extract type as PureScala. [" + tt + "]")
         }
         throw ImpureCodeEncounteredException(tree)
       }
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index 81e17eaf196b5df21ccf9a5c4e487eb5dda63a26..ae48a4976db7b7f70a1dc9d26c561620fd19bde9 100644
--- a/src/funcheck/Extractors.scala
+++ b/src/funcheck/Extractors.scala
@@ -105,6 +105,13 @@ trait Extractors {
   }
 
   object ExpressionExtractors {
+    object ExIfThenElse {
+      def unapply(tree: Tree): Option[(Tree,Tree,Tree)] = tree match {
+        case If(t1,t2,t3) => Some((t1,t2,t3))
+        case _ => None
+      }
+    }
+
     object ExBooleanLiteral {
       def unapply(tree: Tree): Option[Boolean] = tree match {
         case Literal(Constant(true)) => Some(true)
@@ -199,12 +206,40 @@ trait Extractors {
       }
     }
 
+    object ExUMinus {
+      def unapply(tree: Tree): Option[Tree] = tree match {
+        case Select(t, n) if (n == nme.UNARY_-) => Some(t)
+        case _ => None
+      }
+    }
+
     object ExPlus {
       def unapply(tree: Tree): Option[(Tree,Tree)] = tree match {
         case Apply(Select(lhs, n), List(rhs)) if (n == nme.ADD) => Some((lhs,rhs))
         case _ => None
       }
     }
+
+    object ExMinus {
+      def unapply(tree: Tree): Option[(Tree,Tree)] = tree match {
+        case Apply(Select(lhs, n), List(rhs)) if (n == nme.SUB) => Some((lhs,rhs))
+        case _ => None
+      }
+    }
+
+    object ExTimes {
+      def unapply(tree: Tree): Option[(Tree,Tree)] = tree match {
+        case Apply(Select(lhs, n), List(rhs)) if (n == nme.MUL) => Some((lhs,rhs))
+        case _ => None
+      }
+    }
+
+    object ExDiv {
+      def unapply(tree: Tree): Option[(Tree,Tree)] = tree match {
+        case Apply(Select(lhs, n), List(rhs)) if (n == nme.DIV) => Some((lhs,rhs))
+        case _ => None
+      }
+    }
   }
 
   object TypeExtractors {
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index e2205cd6808e19a372c0bde87716813a12a3e206..4d8f89bff786a65ef2fe3ea8c780fb6ea139b0cb 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/src/purescala/PrettyPrinter.scala
@@ -67,6 +67,7 @@ object PrettyPrinter {
     case Or(exprs) => ppNary(sb, exprs, " \u2228 ")             // \lor
     case Not(Equals(l, r)) => ppBinary(sb, l, r, " \u2260 ")    // \neq
     case Not(expr) => ppUnary(sb, expr, "\u00AC")               // \neg
+    case UMinus(expr) => ppUnary(sb, expr, "-")
     case Equals(l,r) => ppBinary(sb, l, r, " == ")
     case IntLiteral(v) => sb.append(v)
     case BooleanLiteral(v) => sb.append(v)
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index b158d2babc3be3e16669a1c31f211e4b56859fe5..288c2eb73ceaf35ee3145a005ce73d6505c2b1a2 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -43,6 +43,15 @@ object Trees {
     }
   }
 
+  case object Or {
+    def apply(l: Expr, r: Expr): Expr = (l,r) match {
+      case (Or(exs1), Or(exs2)) => Or(exs1 ++ exs2)
+      case (Or(exs1), ex2) => Or(exs1 :+ ex2)
+      case (ex1, Or(exs2)) => Or(exs2 :+ ex1)
+      case (ex1, ex2) => Or(List(ex1, ex2))
+    }
+  }
+
   case class And(exprs: Seq[Expr]) extends Expr
   case class Or(exprs: Seq[Expr]) extends Expr
   case class Not(expr: Expr) extends Expr