Fixed app encoding in unrolling solver

src/main/scala/leon/solvers/unrolling/DatatypeManager.scala

@@ -189,17 +189,19 @@ class DatatypeManager[T](encoder: TemplateEncoder[T]) extends TemplateManager(en
           case (cct: CaseClassType) => Seq(cct)
         }
 
-        MatchExpr(expr, matchers.map { cct =>
+        val cases = matchers.map { cct =>
           val pattern = CaseClassPattern(None, cct, cct.fields.map(vd => WildcardPattern(Some(vd.id))))
           val expr = andJoin(cct.fields.map(vd => typeUnroller(Variable(vd.id))))
           MatchCase(pattern, None, expr)
-        })
+        }
+
+        if (cases.forall(_.rhs == BooleanLiteral(true))) None else Some(MatchExpr(expr, cases))
       } else {
         val fd = classTypeUnroller(ct.root)
-        FunctionInvocation(fd.typed, Seq(expr))
+        Some(FunctionInvocation(fd.typed, Seq(expr)))
       }
 
-      andJoin(inv ++ subtype :+ induct)
+      andJoin(inv ++ subtype ++ induct)
 
     case TupleType(tpes) =>
       andJoin(tpes.zipWithIndex.map(p => typeUnroller(TupleSelect(expr, p._2 + 1))))

src/main/scala/leon/solvers/unrolling/LambdaManager.scala

@@ -22,6 +22,11 @@ import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
 
 case class App[T](caller: T, tpe: FunctionType, args: Seq[Arg[T]], encoded: T) {
   override def toString = "(" + caller + " : " + tpe + ")" + args.map(_.encoded).mkString("(", ",", ")")
+  def substitute(substituter: T => T, msubst: Map[T, Matcher[T]]): App[T] = copy(
+    caller = substituter(caller),
+    args = args.map(_.substitute(substituter, msubst)),
+    encoded = substituter(encoded)
+  )
 }
 
 object LambdaTemplate {

src/main/scala/leon/solvers/unrolling/TemplateManager.scala

@@ -377,8 +377,7 @@ object Template {
     manager match {
       case lmanager: LambdaManager[T] =>
         for ((b,apps) <- applications; bp = substituter(b); app <- apps) {
-          val newApp = app.copy(caller = substituter(app.caller), args = app.args.map(_.substitute(substituter, msubst)))
-          instantiation ++= lmanager.instantiateApp(bp, newApp)
+          instantiation ++= lmanager.instantiateApp(bp, app.substitute(substituter, msubst))
         }
 
       case _ =>

src/test/resources/regression/verification/purescala/valid/ADTInvariants1.scala

+
+object ADTInvariants1 {
+
+  case class Positive(i: BigInt) {
+    require(i > 0)
+  }
+  
+  def theorem(f: Positive => Positive) = {
+    f(Positive(1))
+  } ensuring(res => res.i > 0)
+}

src/test/resources/regression/verification/purescala/valid/ADTInvariants2.scala

+import leon.lang._
+
+object ADTInvariants2 {
+  case class Pos(i: BigInt) {
+    require(i > 0)
+  }
+
+  def test(p: Pos): Boolean = {
+    Pos(p.i + 1).i > 0
+  }.holds
+
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case class Nil() extends List
+
+  case class C(l: Cons)
+
+  def test3(c: C): Boolean = {
+    c.l.isInstanceOf[Cons]
+  }.holds
+}