Make vanuatoo more resilient to non-patternable Exprs

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)

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]])

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
   )
 }

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 {

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