diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 06d89326cebdac5064c2da3c36ccfe8b16f6e5f6..0707b3d53cc04a8a413a8b2e1db9a453478d11ee 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1048,6 +1048,8 @@ trait CodeExtraction extends ASTExtractors {
           (e, Some(last))
         case Block(e :: es, last) =>
           (e, Some(Block(es, last)))
+        case Block(Nil, last) =>
+          (last, None)
         case e =>
           (e, None)
       }
@@ -1753,6 +1755,7 @@ trait CodeExtraction extends ASTExtractors {
 
         // default behaviour is to complain :)
         case _ =>
+          println(tr.getClass)
           outOfSubsetError(tr, "Could not extract as PureScala")
       }
 
diff --git a/src/test/resources/regression/verification/purescala/valid/FoldAssociative.scala b/src/test/resources/regression/verification/purescala/valid/FoldAssociative.scala
new file mode 100644
index 0000000000000000000000000000000000000000..261d15c0fcd6419f5a2d024d2155257726ba8394
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/FoldAssociative.scala
@@ -0,0 +1,101 @@
+import leon._
+import leon.lang._
+
+object FoldAssociative {
+
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case class Nil() extends List
+
+  sealed abstract class Option
+  case class Some(x: Int) extends Option
+  case class None() extends Option
+
+  def foldRight[A](list: List, state: A, f: (Int, A) => A): A = list match {
+    case Cons(head, tail) =>
+      val tailState = foldRight(tail, state, f)
+      f(head, tailState)
+    case Nil() => state
+  }
+
+  def take(list: List, count: Int): List = {
+    require(count >= 0)
+    list match {
+      case Cons(head, tail) if count > 0 => Cons(head, take(tail, count - 1))
+      case _ => Nil()
+    }
+  }
+
+  def drop(list: List, count: Int): List = {
+    require(count >= 0)
+    list match {
+      case Cons(head, tail) if count > 0 => drop(tail, count - 1)
+      case _ => list
+    }
+  }
+
+  def append(l1: List, l2: List): List = {
+    l1 match {
+      case Cons(head, tail) => Cons(head, append(tail, l2))
+      case Nil() => l2
+    }
+  }
+
+  def lemma_split(list: List, x: Int): Boolean = {
+    require(x >= 0)
+    val f = (x: Int, s: Int) => x + s
+    val l1 = take(list, x)
+    val l2 = drop(list, x)
+    foldRight(list, 0, f) == foldRight(l1, foldRight(l2, 0, f), f)
+  }
+
+  def lemma_split_induct(list: List, x: Int): Boolean = {
+    require(x >= 0)
+    val f = (x: Int, s: Int) => x + s
+    val l1 = take(list, x)
+    val l2 = drop(list, x)
+    lemma_split(list, x) && (list match {
+      case Cons(head, tail) if x > 0 =>
+        lemma_split_induct(tail, x - 1)
+      case _ => true
+    })
+  }.holds
+
+  def lemma_reassociative(list: List, x: Int): Boolean = {
+    require(x >= 0)
+    val f = (x: Int, s: Int) => x + s
+    val l1 = take(list, x)
+    val l2 = drop(list, x)
+
+    foldRight(list, 0, f) == foldRight(l1, 0, f) + foldRight(l2, 0, f)
+  }
+
+  def lemma_reassociative_induct(list: List, x: Int): Boolean = {
+    require(x >= 0)
+    val f = (x: Int, s: Int) => x + s
+    val l1 = take(list, x)
+    val l2 = drop(list, x)
+    lemma_reassociative(list, x) && (list match {
+      case Cons(head, tail) if x > 0 =>
+        lemma_reassociative_induct(tail, x - 1)
+      case _ => true
+    })
+  }.holds
+
+  def lemma_reassociative_presplit(l1: List, l2: List): Boolean = {
+    val f = (x: Int, s: Int) => x + s
+    val list = append(l1, l2)
+    foldRight(list, 0, f) == foldRight(l1, 0, f) + foldRight(l2, 0, f)
+  }
+
+  def lemma_reassociative_presplit_induct(l1: List, l2: List): Boolean = {
+    val f = (x: Int, s: Int) => x + s
+    val list = append(l1, l2)
+    lemma_reassociative_presplit(l1, l2) && (l1 match {
+      case Cons(head, tail) =>
+        lemma_reassociative_presplit_induct(tail, l2)
+      case Nil() => true
+    })
+  }.holds
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/Lists6.scala b/src/test/resources/regression/verification/purescala/valid/Lists6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f70d523c7f9139cef806bb6549c06c14c057e6d1
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Lists6.scala
@@ -0,0 +1,22 @@
+import leon.lang._
+import leon.collection._
+
+object Lists6 {
+  def exists[T](list: List[T], f: T => Boolean): Boolean = {
+    list match {
+      case Cons(head, tail) => f(head) || exists(tail, f)
+      case Nil() => false
+    }
+  }
+
+  def associative_lemma[T](list: List[T], f: T => Boolean, g: T => Boolean): Boolean = {
+    exists(list, (x: T) => f(x) || g(x)) == (exists(list, f) || exists(list, g))
+  }
+
+  def associative_lemma_induct[T](list: List[T], f: T => Boolean, g: T => Boolean): Boolean = {
+    associative_lemma(list, f, g) && (list match {
+      case Cons(head, tail) => associative_lemma_induct(tail, f, g)
+      case Nil() => true
+    })
+  }.holds
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/Monads2.scala b/src/test/resources/regression/verification/purescala/valid/Monads2.scala
index 341c60379522981ce625818d08d316a079fa1fa8..f89b2b7f7b71d6b5260bc87b861cd1b3fef9355b 100644
--- a/src/test/resources/regression/verification/purescala/valid/Monads2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Monads2.scala
@@ -10,6 +10,11 @@ object Monads2 {
     case None() => None()
   }
 
+  def add[T](o1: Option[T], o2: Option[T]): Option[T] = o1 match {
+    case Some(x) => o1
+    case None() => o2
+  }
+
   def associative_law[T,U,V](opt: Option[T], f: T => Option[U], g: U => Option[V]): Boolean = {
     flatMap(flatMap(opt, f), g) == flatMap(opt, (x: T) => flatMap(f(x), g))
   }.holds
@@ -22,14 +27,21 @@ object Monads2 {
     flatMap(opt, (x: T) => Some(x)) == opt
   }.holds
 
-  /*
-  def associative_induct[T,U,V](opt: Option[T], f: T => Option[U], g: U => Option[V]): Boolean = {
-    opt match {
-      case Some(x) => associative(opt)
+  def flatMap_zero_law[T,U](none: None[T], f: T => Option[U]): Boolean = {
+    flatMap(none, f) == None[U]()
+  }.holds
 
-    }
-  }
-  */
+  def flatMap_to_zero_law[T,U](opt: Option[T]): Boolean = {
+    flatMap(opt, (x: T) => None[U]()) == None[U]()
+  }.holds
+
+  def add_zero_law[T](opt: Option[T]): Boolean = {
+    add(opt, None[T]()) == opt
+  }.holds
+
+  def zero_add_law[T](opt: Option[T]): Boolean = {
+    add(None[T](), opt) == opt
+  }.holds
 }
 
 // vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/valid/Monads3.scala b/src/test/resources/regression/verification/purescala/valid/Monads3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a2911c98793e1d487b5338bc2d07010b52170ace
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Monads3.scala
@@ -0,0 +1,77 @@
+import leon.lang._
+import leon.collection._
+
+object FlatMap {
+
+  def append[T](l1: List[T], l2: List[T]): List[T] = {
+    l1 match {
+      case Cons(head, tail) => Cons(head, append(tail, l2))
+      case Nil() => l2
+    }
+  } ensuring { res => (res == l1) || (l2 != Nil[T]()) }
+
+  def flatMap[T,U](list: List[T], f: T => List[U]): List[U] = list match {
+    case Cons(head, tail) => append(f(head), flatMap(tail, f))
+    case Nil() => Nil()
+  }
+
+  def associative_lemma[T,U,V](list: List[T], f: T => List[U], g: U => List[V]): Boolean = {
+    flatMap(flatMap(list, f), g) == flatMap(list, (x: T) => flatMap(f(x), g))
+  }
+
+  def associative_lemma_induct[T,U,V](list: List[T], flist: List[U], glist: List[V], f: T => List[U], g: U => List[V]): Boolean = {
+    associative_lemma(list, f, g) &&
+    append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) &&
+    (glist match {
+      case Cons(ghead, gtail) =>
+        associative_lemma_induct(list, flist, gtail, f, g)
+      case Nil() => flist match {
+        case Cons(fhead, ftail) =>
+          associative_lemma_induct(list, ftail, g(fhead), f, g)
+        case Nil() => list match {
+          case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
+          case Nil() => true
+        }
+      }
+    })
+  }.holds
+
+  def left_unit_law[T,U](x: T, f: T => List[U]): Boolean = {
+    flatMap(Cons(x, Nil()), f) == f(x)
+  }.holds
+
+  def right_unit_law[T](list: List[T]): Boolean = {
+    flatMap(list, (x: T) => Cons(x, Nil())) == list
+  }
+    
+  def right_unit_induct[T,U](list: List[T]): Boolean = {
+    right_unit_law(list) && (list match {
+      case Cons(head, tail) => right_unit_induct(tail)
+      case Nil() => true
+    })
+  }.holds
+
+  def flatMap_zero_law[T,U](f: T => List[U]): Boolean = {
+    flatMap(Nil[T](), f) == Nil[U]()
+  }.holds
+
+  def flatMap_to_zero_law[T](list: List[T]): Boolean = {
+    flatMap(list, (x: T) => Nil[T]()) == Nil[T]()
+  }
+    
+  def flatMap_to_zero_induct[T,U](list: List[T]): Boolean = {
+    flatMap_to_zero_law(list) && (list match {
+      case Cons(head, tail) => flatMap_to_zero_induct(tail)
+      case Nil() => true
+    })
+  }.holds
+
+  def add_zero_law[T](list: List[T]): Boolean = {
+    append(list, Nil()) == list
+  }.holds
+
+  def zero_add_law[T](list: List[T]): Boolean = {
+    append(Nil(), list) == list
+  }.holds
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/ParBalance.scala b/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6f054eaec6940a5f9fbfaeb0631319a4f67de491
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
@@ -0,0 +1,206 @@
+import leon._
+import leon.lang._
+
+object ParBalance {
+
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case class Nil() extends List
+
+  sealed abstract class Option
+  case class Some(x: Int) extends Option
+  case class None() extends Option
+
+  val openPar = 1
+  val closePar = 2
+
+  def balanced(list: List, counter: Int): Boolean = {
+    if (counter < 0) false else list match {
+      case Cons(head, tail) =>
+        val c = if (head == openPar) counter + 1
+          else if (head == closePar) counter - 1
+          else counter
+        balanced(tail, c)
+      case Nil() => counter == 0
+    }
+  }
+
+  def balanced_nonEarly(list: List, counter: Int): Boolean = {
+    list match {
+      case Cons(head, tail) =>
+        if (counter < 0) balanced_nonEarly(tail, counter) else {
+          val c = if (head == openPar) counter + 1
+            else if (head == closePar) counter - 1
+            else counter
+          balanced_nonEarly(tail, c)
+        }
+      case Nil() => counter == 0
+    }
+  } ensuring { res => res == balanced(list, counter) }
+
+  def balanced_withFailure(list: List, counter: Int, failed: Boolean): Boolean = {
+    require(counter >= 0 || failed)
+    list match {
+      case Cons(head, tail) =>
+        val c = if (head == openPar) counter + 1
+          else if (head == closePar) counter - 1
+          else counter
+        balanced_withFailure(tail, c, failed || c < 0)
+      case Nil() => !failed && counter == 0
+    }
+  } ensuring { res =>
+    if (failed) {
+      res == balanced_nonEarly(list, -1)
+    } else {
+      res == balanced_nonEarly(list, counter)
+    }
+  }
+
+  def balanced_withReduce(list: List, p: (Int, Int)): Boolean = {
+    require(p._1 >= 0 && p._2 >= 0)
+    list match {
+      case Cons(head, tail) =>
+        val p2 = reduce(p, parPair(head))
+        balanced_withReduce(tail, p2)
+      case Nil() =>
+        p._1 == 0 && p._2 == 0
+    }
+  } ensuring { res => res == balanced_withFailure(list, p._1 - p._2, p._2 > 0) }
+
+  def balanced_foldLeft_equivalence(list: List, p: (Int, Int)): Boolean = {
+    require(p._1 >= 0 && p._2 >= 0)
+    val f = (s: (Int, Int), x: Int) => reduce(s, parPair(x))
+    (foldLeft(list, p, f) == (0, 0)) == balanced_withReduce(list, p) && (list match {
+      case Cons(head, tail) =>
+        val p2 = f(p, head)
+        balanced_foldLeft_equivalence(tail, p2)
+      case Nil() => true
+    })
+  }.holds
+
+  def foldRight[A](list: List, state: A, f: (Int, A) => A): A = list match {
+    case Cons(head, tail) =>
+      val tailState = foldRight(tail, state, f)
+      f(head, tailState)
+    case Nil() => state
+  }
+
+  def foldLeft[A](list: List, state: A, f: (A, Int) => A): A = list match {
+    case Cons(head, tail) =>
+      val nextState = f(state, head)
+      foldLeft(tail, nextState, f)
+    case Nil() => state
+  }
+
+  def reduce(p1: (Int, Int), p2: (Int, Int)): (Int, Int) = {
+    if (p1._1 >= p2._2) {
+      (p1._1 - p2._2 + p2._1, p1._2)
+    } else {
+      (p2._1, p2._2 - p1._1 + p1._2)
+    }
+  }
+
+  def reduce_associative(p1: (Int, Int), p2: (Int, Int), p3: (Int, Int)): Boolean = {
+    reduce(p1, reduce(p2, p3)) == reduce(reduce(p1, p2), p3)
+  }.holds
+
+  def swap(p: (Int, Int)): (Int, Int) = (p._2, p._1)
+
+  def reduce_inverse(p1: (Int, Int), p2: (Int, Int)): Boolean = {
+    reduce(p1, p2) == swap(reduce(swap(p2), swap(p1)))
+  }.holds
+
+  def reduce_associative_inverse(p1: (Int, Int), p2: (Int, Int), p3: (Int, Int)): Boolean = {
+    reduce(p1, reduce(p2, p3)) == swap(reduce(reduce(swap(p3), swap(p2)), swap(p1)))
+  }.holds
+
+  def reduce_associative_inverse2(p1: (Int, Int), p2: (Int, Int), p3: (Int, Int)): Boolean = {
+    reduce(reduce(p1, p2), p3) == swap(reduce(swap(p3), reduce(swap(p2), swap(p1))))
+  }.holds
+
+  def parPair(x: Int): (Int, Int) = {
+    if (x == openPar) (1, 0) else if (x == closePar) (0, 1) else (0, 0)
+  }
+
+  def headOption(list: List): Option = list match {
+    case Cons(head, tail) => Some(head)
+    case Nil() => None()
+  }
+
+  def lastOption(list: List): Option = list match {
+    case Cons(head, Nil()) => Some(head)
+    case Cons(head, tail) => lastOption(tail)
+    case Nil() => None()
+  }
+
+  def init(list: List): List = list match {
+    case Cons(head, Nil()) => Nil()
+    case Cons(head, tail) => Cons(head, init(tail))
+    case Nil() => Nil()
+  }
+
+  def tail(list: List): List = list match {
+    case Cons(head, tail) => tail
+    case Nil() => Nil()
+  }
+
+  def addLast(list: List, x: Int): List = {
+    list match {
+      case Cons(head, tail) => Cons(head, addLast(tail, x))
+      case Nil() => Cons(x, Nil())
+    }
+  } ensuring { res => lastOption(res) == Some(x) && init(res) == list }
+
+  def reverse(list: List): List = {
+    list match {
+      case Cons(head, tail) => addLast(reverse(tail), head)
+      case Nil() => Nil()
+    }
+  } ensuring { res =>
+    lastOption(res) == headOption(list) &&
+    lastOption(list) == headOption(res)
+  }
+
+  def reverse_tail_equivalence(list: List): Boolean = {
+    reverse(tail(list)) == init(reverse(list))
+  }.holds
+
+  def reverse_init_equivalence(list: List): Boolean = {
+    reverse(init(list)) == tail(reverse(list)) && (list match {
+      case Cons(head, tail) => reverse_init_equivalence(tail)
+      case Nil() => true
+    })
+  }.holds
+
+  def reverse_equality_equivalence(l1: List, l2: List): Boolean = {
+    (l1 == l2) == (reverse(l1) == reverse(l2)) && ((l1, l2) match {
+      case (Cons(h1, t1), Cons(h2, t2)) => reverse_equality_equivalence(t1, t2)
+      case _ => true
+    })
+  }.holds
+
+  def reverse_reverse_equivalence(list: List): Boolean = {
+    reverse(reverse(list)) == list && ((list, reverse(list)) match {
+      case (Cons(h1, t1), Cons(h2, t2)) =>
+        reverse_reverse_equivalence(t1) && reverse_reverse_equivalence(t2)
+      case _ => true
+    })
+  }.holds
+
+  /*
+  def fold_equivalence(list: List): Boolean = {
+    val s = (0, 0)
+    val fl = (s: (Int, Int), x: Int) => reduce(s, parPair(x))
+    val fr = (x: Int, s: (Int, Int)) => reduce(parPair(x), s)
+
+    foldLeft(list, s, fl) == foldRight(list, s, fr)
+  }.holds
+
+  def lemma(list: List): Boolean = {
+    val f = (x: Int, s: (Int, Int)) => reduce(parPair(x), s)
+    fold_equivalence(list) && balanced_foldLeft_equivalence(list, (0, 0)) &&
+    (foldRight(list, (0, 0), f) == (0, 0)) == balanced(list, 0)
+  }.holds
+  */
+
+}