diff --git a/src/main/scala/leon/datagen/DataGenerator.scala b/src/main/scala/leon/datagen/DataGenerator.scala
index 210385cd1378b51ad5e59f1f349ce747756c7871..e97321053accebe5ecbb14756e48f3bafaef3d77 100644
--- a/src/main/scala/leon/datagen/DataGenerator.scala
+++ b/src/main/scala/leon/datagen/DataGenerator.scala
@@ -10,6 +10,8 @@ import utils._
 import java.util.concurrent.atomic.AtomicBoolean
 
 trait DataGenerator extends Interruptible {
+  implicit val debugSection = DebugSectionDataGen
+
   def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]];
 
   protected val interrupted: AtomicBoolean = new AtomicBoolean(false)
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 87e1184bcf42c3c43992d0d333a0ff2f35ea81b2..284a050099bcf7137c17a54d2f635d28b90ac7de 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -109,6 +109,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
       Nil
   }
 
+  // Returns the pattern and whether it is fully precise
   private def valueToPattern(v: AnyRef, expType: TypeTree): (VPattern[Expr, TypeTree], Boolean) = (v, expType) match {
     case (i: Integer, Int32Type) =>
       (cPattern(intConstructor(i), List()), true)
@@ -143,7 +144,8 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
           (ConstructorPattern(c, elems.map(_._1)), elems.forall(_._2))
 
         case _ =>
-          sys.error("Could not retreive type for :"+cc.getClass.getName)
+          ctx.reporter.error("Could not retreive type for :"+cc.getClass.getName)
+          (AnyPattern[Expr, TypeTree](), false)
       }
 
     case (t: codegen.runtime.Tuple, tt @ TupleType(parts)) =>
@@ -165,7 +167,8 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
     case (gv: GenericValue, t: TypeParameter) =>
       (cPattern(getConstructors(t)(gv.id-1), List()), true)
     case (v, t) =>
-      sys.error("Unsupported value, can't paternify : "+v+" ("+v.getClass+") : "+t)
+      ctx.reporter.debug("Unsupported value, can't paternify : "+v+" ("+v.getClass+") : "+t)
+      (AnyPattern[Expr, TypeTree](), false)
   }
 
   type InstrumentedResult = (EvaluationResults.Result, Option[vanuatoo.Pattern[Expr, TypeTree]])
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
index 394df76cad819fd58c5fc044bf582c577867f2ab..902d3b4f651f89c321b9cdaa6865f0240061b8ca 100644
--- a/src/main/scala/leon/utils/DebugSections.scala
+++ b/src/main/scala/leon/utils/DebugSections.scala
@@ -16,6 +16,7 @@ case object DebugSectionVerification extends DebugSection("verification", 1 << 4
 case object DebugSectionTermination  extends DebugSection("termination",  1 << 5)
 case object DebugSectionTrees        extends DebugSection("trees",        1 << 6)
 case object DebugSectionPositions    extends DebugSection("positions",    1 << 7)
+case object DebugSectionDataGen      extends DebugSection("datagen",      1 << 8)
 
 object DebugSections {
   val all = Set[DebugSection](
@@ -26,6 +27,7 @@ object DebugSections {
     DebugSectionVerification,
     DebugSectionTermination,
     DebugSectionTrees,
-    DebugSectionPositions
+    DebugSectionPositions,
+    DebugSectionDataGen
   )
 }
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 204f498b485f9384f00bbd5b747004b666f5e323..4a23e63e18d1f2ce928ddba204a91176c9f810c3 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -35,7 +35,6 @@ class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: V
     case Some(s) => s.name
     case None => ""
   }
-
 }
 
 object VCKind extends Enumeration {
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 9827c72bdd262d847f75d1fa2539e616276aabde..01b129d77671ac572aaa8494b0d565e97d8bf442 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -6,12 +6,8 @@ package verification
 import purescala.Definitions.FunDef
 
 class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
-  val conditions : Seq[VerificationCondition] = fvcs.flatMap(_._2).toSeq.sortWith {
-      (vc1,vc2) =>
-        val id1 = vc1.funDef.id.name
-        val id2 = vc2.funDef.id.name
-        if(id1 != id2) id1 < id2 else vc1.getPos < vc2.getPos
-    }
+  import scala.math.Ordering.Implicits._
+  val conditions : Seq[VerificationCondition] = fvcs.flatMap(_._2).toSeq.sortBy(vc => (vc.funDef.id.name, vc.kind))
 
   lazy val totalConditions : Int = conditions.size