diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index 8f33f9bb39f7fd9ad5a685e9d22556ec1bd138d5..5106ccfef797e31476a83fe3db8905bfa65af9b6 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -183,7 +183,8 @@ trait DatatypeTemplates { self: Templates =>
                 storeCond(pathVar, newBool)
 
                 for (vd <- tcons.fields) {
-                  rec(newBool, ADTSelector(AsInstanceOf(expr, tpe), vd.id), state.copy(recurseSort = false))
+                  val ex = if (adt != tpe) AsInstanceOf(expr, tpe) else expr
+                  rec(newBool, ADTSelector(ex, vd.id), state.copy(recurseSort = false))
                 }
 
                 val vars = tpes.keys.toSet ++ functions.keys ++
diff --git a/src/main/scala/inox/tip/Parser.scala b/src/main/scala/inox/tip/Parser.scala
index 52f8fa69d62ab197f4dc1aefc5da471ce3d3ffa2..0a5af026d2f7aff1d51a42403c4de5e27e1c65e6 100644
--- a/src/main/scala/inox/tip/Parser.scala
+++ b/src/main/scala/inox/tip/Parser.scala
@@ -13,7 +13,7 @@ import smtlib.theories.experimental._
 import smtlib.extensions.tip.Terms.{Lambda => SMTLambda, Application => SMTApplication, _}
 import smtlib.extensions.tip.Commands._
 
-import Terms.{Assume => SMTAssume}
+import Terms.{Assume => SMTAssume, Choose => SMTChoose}
 import Commands._
 
 import scala.collection.BitSet
@@ -407,6 +407,10 @@ class Parser(file: File) {
     case SMTAssume(pred, body) =>
       Assume(extractTerm(pred), extractTerm(body))
 
+    case SMTChoose(sym, sort, pred) =>
+      val vd = ValDef(FreshIdentifier(sym.name), extractSort(sort))
+      Choose(vd, extractTerm(pred)(locals.withVariable(sym, vd.toVariable)))
+
     case SMTLet(binding, bindings, term) =>
       var locs = locals
       val mapping = for (VarBinding(name, term) <- (binding +: bindings)) yield {
diff --git a/src/main/scala/inox/tip/Printer.scala b/src/main/scala/inox/tip/Printer.scala
index 5d76756b2612726c3ed4c976de998fb315308463..1761d5db3ab15f2b70603d0f56706e0f7a513ddb 100644
--- a/src/main/scala/inox/tip/Printer.scala
+++ b/src/main/scala/inox/tip/Printer.scala
@@ -11,7 +11,7 @@ import smtlib.extensions.tip.Terms.{Lambda => SMTLambda, Application => SMTAppli
 import smtlib.extensions.tip.Commands._
 import smtlib.Interpreter
 
-import Terms.{Assume => SMTAssume}
+import Terms.{Assume => SMTAssume, Choose => SMTChoose}
 import Commands._
 
 import java.io.Writer
@@ -356,6 +356,11 @@ class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.S
         Some(declareSort(fi.tfd.returnType))
       )
 
+    case Choose(vd, pred) =>
+      val sym = id2sym(vd.id)
+      val sort = declareSort(vd.tpe)
+      SMTChoose(sym, declareSort(vd.tpe), toSMT(pred)(bindings + (vd.id -> (sym: Term))))
+
     case _ => super.toSMT(e)
   }
 }
diff --git a/src/main/scala/inox/tip/TipExtensions.scala b/src/main/scala/inox/tip/TipExtensions.scala
index 0f22f3d8af7ab36e672d22dd7a8c90446cf8a9a9..48f942e3098487de17c535d45fbace30d32317c8 100644
--- a/src/main/scala/inox/tip/TipExtensions.scala
+++ b/src/main/scala/inox/tip/TipExtensions.scala
@@ -13,6 +13,7 @@ object Tokens {
   import LT.ReservedWord
 
   case object Assume extends ReservedWord
+  case object Choose extends ReservedWord
   case object DatatypeInvariant extends ReservedWord
 }
 
@@ -26,6 +27,18 @@ object Terms {
       ctx.print(")")
     }
   }
+
+  case class Choose(name: SSymbol, sort: Sort, pred: Term) extends TermExtension {
+    def print(ctx: PrintingContext): Unit = {
+      ctx.print("(choose ")
+      ctx.print(name)
+      ctx.print(" ")
+      ctx.print(sort)
+      ctx.print(" ")
+      ctx.print(pred)
+      ctx.print(")")
+    }
+  }
 }
 
 object Commands {
@@ -60,6 +73,7 @@ class TipLexer(reader: java.io.Reader) extends SMTLexer(reader) {
 
   override protected def toReserved(s: String): Option[Token] = s match {
     case "assume" => Some(Token(Tokens.Assume))
+    case "choose" => Some(Token(Tokens.Choose))
     case "datatype-invariant" => Some(Token(Tokens.DatatypeInvariant))
     case _ => super.toReserved(s)
   }
@@ -76,6 +90,13 @@ class TipParser(lexer: TipLexer) extends SMTParser(lexer) {
       val body = parseTerm
       Assume(pred, body)
 
+    case Tokens.Choose =>
+      eat(Tokens.Choose)
+      val name = parseSymbol
+      val sort = parseSort
+      val pred = parseTerm
+      Choose(name, sort, pred)
+
     case _ => super.parseTermWithoutParens
   }