diff --git a/src/it/resources/regression/tip/UNSAT/HigherOrderFunctionsMutableParams10.scala-2.tip b/src/it/resources/regression/tip/UNSAT/HigherOrderFunctionsMutableParams10.scala-2.tip
new file mode 100644
index 0000000000000000000000000000000000000000..5d789266216543e7f7997138b4e93e067fd0d9eb
--- /dev/null
+++ b/src/it/resources/regression/tip/UNSAT/HigherOrderFunctionsMutableParams10.scala-2.tip
@@ -0,0 +1,19 @@
+(declare-datatypes () ((A!59 (A!60 (x!539 (_ BitVec 32))))))
+
+(declare-datatypes (A1!0 R!21) ((fun1!11 (fun1!12 (f!40 (=> A1!0 R!21)) (pre!15 (=> A1!0 Bool))))))
+
+(declare-datatypes (A0!6 A1!22) ((tuple2!10 (tuple2!11 (_1!5 A0!6) (_2!5 A1!22)))))
+
+(declare-datatypes () ((FunctionWrapper!5 (FunctionWrapper!6 (f!39 (fun1!11 A!59 (tuple2!10 (_ BitVec 32) A!59)))))))
+
+(declare-datatypes () ((WrapWrapper!5 (WrapWrapper!6 (fw!4 FunctionWrapper!5)))))
+
+(define-fun fImpl!0 ((a!1 A!59)) (tuple2!10 (_ BitVec 32) A!59) (let ((a!26 (A!60 (bvadd (x!539 a!1) #b00000000000000000000000000000001)))) (tuple2!11 (x!539 a!26) a!26)))
+
+(define-fun app!0 ((ww!0 WrapWrapper!5) (a!0 A!59)) (tuple2!10 (_ BitVec 32) A!59) (assume (forall ((x!133 A!59)) (=> (@ (f!40 (fun1!12 (lambda ((x!132 A!59)) true) (lambda ((x!364 A!59)) true))) x!133) (@ (f!40 (fun1!12 (pre!15 (f!39 (fw!4 ww!0))) (lambda ((x!365 A!59)) true))) x!133))) (let ((t!53 (let ((res!38 (@ (f!40 (f!39 (fw!4 ww!0))) a!0))) (tuple2!11 (_1!5 res!38) (_2!5 res!38))))) (tuple2!11 (_1!5 t!53) (_2!5 t!53)))))
+
+(assert (not (let ((wrap!0 (WrapWrapper!6 (FunctionWrapper!6 (fun1!12 (lambda ((a!3 A!59)) (let ((res!40 (fImpl!0 a!3))) (tuple2!11 (_1!5 res!40) (_2!5 res!40)))) (lambda ((a!32 A!59)) true)))))) (let ((x$1!5 (x!539 (_2!5 (app!0 wrap!0 (_2!5 (app!0 wrap!0 (A!60 #b00000000000000000000000000000000)))))))) (= x$1!5 #b00000000000000000000000000000010)))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index bd30be6d9a807cf1258fe750f9e554acecf63c12..c83185e238327e3b04fe5f5a56f4f65de6861f28 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -1030,10 +1030,6 @@ trait SymbolOps { self: TypeOps =>
           val (br, bBindings) = rec(b)
           (br, vBindings merge ((i -> vr) +: bBindings))
 
-        case Forall(args, body) =>
-          val (recBody, bodyBindings) = rec(body)
-          (Forall(args, bodyBindings wrap recBody), Seq.empty)
-
         case Assume(pred, body) =>
           val (recPred, predBindings) = rec(pred)
           val (recBody, bodyBindings) = rec(body)
@@ -1066,6 +1062,13 @@ trait SymbolOps { self: TypeOps =>
           val (recRhs, rhsBindings) = rec(rhs)
           (Implies(recLhs, rhsBindings wrap recRhs), lhsBindings)
 
+        case v: Variable => (v, Seq.empty)
+
+        case ex @ VariableExtractor(vs) if vs.nonEmpty =>
+          val Operator(subs, recons) = ex
+          val recSubs = subs.map(rec)
+          (recons(recSubs.map { case (e, bindings) => bindings wrap e }), Seq.empty)
+
         case Operator(es, recons) =>
           val (recEs, esBindings) = es.map(rec).unzip
           (recons(recEs), esBindings.flatten.distinct)
diff --git a/src/main/scala/inox/tip/Printer.scala b/src/main/scala/inox/tip/Printer.scala
index 14b5cc3faa917bdb2da247494d313813f85be1e3..b113697dd6b23c8570b327dd285a979533c8d4b2 100644
--- a/src/main/scala/inox/tip/Printer.scala
+++ b/src/main/scala/inox/tip/Printer.scala
@@ -145,7 +145,7 @@ class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.S
 
     val (ours, externals) = adts.partition {
       case (adt: ADTType, _) => adt == adt.getADT.definition.typed.toType
-      case (tpe @ TupleType(tps), _) => tpe == tuples(tps.size)
+      case (tpe @ TupleType(tps), _) => Some(tpe) == tuples.get(tps.size)
       case _ => true
     }