Fix @induct creating incorrect type-parametric VCs.

Improve debugging capabilities of Pretty/Scala printer w.r.t. types

src/main/scala/leon/purescala/PrettyPrinter.scala

@@ -69,11 +69,15 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
         }
 
       case Variable(id) =>
-        //sb.append("(")
-        pp(id, p)
-        //sb.append(": ")
-        //pp(id.getType, p)
-        //sb.append(")")
+        if (opts.printTypes) {
+          sb.append("(")
+          pp(id, p)
+          sb.append(": ")
+          pp(id.getType, p)
+          sb.append(")")
+        } else {
+          pp(id, p)
+        }
 
       case LetTuple(bs,d,e) =>
         sb.append("(let ")
@@ -483,7 +487,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
         pp(tp, p)
 
       case TypeParameter(id) =>
-        sb.append(id.uniqueName)
+        pp(id, p)
 
       case _ => sb.append("Tree? (" + tree.getClass + ")")
     }

src/main/scala/leon/purescala/PrinterOptions.scala

@@ -3,5 +3,6 @@ package leon.purescala
 case class PrinterOptions (
   baseIndent: Int = 0,
   printPositions: Boolean = false,
+  printTypes: Boolean = false,
   printUniqueIds: Boolean = false
 )

src/main/scala/leon/purescala/ScalaPrinter.scala

@@ -53,9 +53,6 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
     var printPos = opts.printPositions
 
     tree match {
-      case Variable(id) => 
-        pp(id, p)
-
       case LetTuple(ids,d,e) =>
         optBraces { implicit lvl =>
           sb.append("val (" )

src/main/scala/leon/solvers/z3/FairZ3Solver.scala

@@ -225,6 +225,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
       // define an activating boolean...
       val template = getTemplate(expr)
 
+
       val z3args = for (vd <- template.tfd.args) yield {
         variables.getZ3(Variable(vd.id)) match {
           case Some(ast) =>

src/main/scala/leon/verification/InductionTactic.scala

@@ -13,16 +13,10 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
   override val description = "Induction tactic for suitable functions"
   override val shortDescription = "induction"
 
-  private def firstAbsClassDef(args: Seq[VarDecl]) : Option[(AbstractClassDef, VarDecl)] = {
-    val filtered = args.filter(arg =>
-      arg.getType match {
-        case AbstractClassType(_, _) => true
-        case _ => false
-      })
-    if (filtered.size == 0) None else (filtered.head.getType match {
-      case AbstractClassType(classDef, _) => Some((classDef, filtered.head))
-      case _ => scala.sys.error("This should not happen.")
-    })
+  private def firstAbsClassDef(args: Seq[VarDecl]) : Option[(AbstractClassType, VarDecl)] = {
+    args.map(vd => (vd.getType, vd)).collect {
+      case (act: AbstractClassType, vd) => (act, vd)
+    }.headOption
   } 
 
   private def selectorsOfParentType(parentType: ClassType, cct: CaseClassType, expr: Expr) : Seq[Expr] = {
@@ -34,14 +28,13 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
 
   override def generatePostconditions(funDef: FunDef) : Seq[VerificationCondition] = {
     assert(funDef.body.isDefined)
-    val defaultPost = super.generatePostconditions(funDef)
     firstAbsClassDef(funDef.args) match {
-      case Some((classDef, arg)) =>
+      case Some((cct, arg)) =>
         val prec = funDef.precondition
         val optPost = funDef.postcondition
         val body = matchToIfThenElse(funDef.body.get)
         val argAsVar = arg.toVariable
-        val parentType = classDefToClassType(classDef)
+        val parentType = cct
 
         optPost match {
           case None =>
@@ -66,22 +59,22 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
                   })
                   Implies(And(inductiveHypothesis), withPrec)
                 }
-              new VerificationCondition(Implies(CaseClassInstanceOf(cct, argAsVar), conditionForChild), funDef, VCKind.Postcondition, this)
+              new VerificationCondition(Implies(CaseClassInstanceOf(cct, argAsVar), conditionForChild), funDef, VCKind.Postcondition, this).setPos(funDef)
             }
         }
 
       case None =>
-        reporter.warning("Induction tactic currently supports exactly one argument of abstract class type")
-        defaultPost
+        reporter.warning("Could not find abstract class type argument to induct on")
+        super.generatePostconditions(funDef)
     }
   }
 
   override def generatePreconditions(function: FunDef) : Seq[VerificationCondition] = {
     val defaultPrec = super.generatePreconditions(function)
     firstAbsClassDef(function.args) match {
-      case Some((classDef, arg)) => {
+      case Some((cct, arg)) => {
         val toRet = if(function.hasBody) {
-          val parentType = classDefToClassType(classDef)
+          val parentType = cct
           val cleanBody = expandLets(matchToIfThenElse(function.body.get))
 
           val allPathConds = collectWithPathCondition((t => t match {