diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 40f745a332bee265ffafc5de6336040fa9058e7e..47f6f344198642802742c88555e6202dad5291e2 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -1195,6 +1195,9 @@ trait CodeGeneration {
         mkBranch(b, al, fl, ch, canDelegateToMkExpr = false)
         ch << Label(fl) << POP << Ldc(0) << Label(al)
 
+      case MutableExpr(e) =>
+        mkExpr(e, ch)
+
       case _ => throw CompilationException("Unsupported expr " + e + " : " + e.getClass)
     }
   }
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index f5536ee98318c4b9a2005a2af3bd82b8d0b3d71e..5fba0109e58fe9c1b361144ac6f08c55fa374a9e 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -831,6 +831,9 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, val bank: Eva
           throw RuntimeError("MatchError: "+rscrut.asString+" did not match any of the cases:\n"+cases)
       }
 
+    case MutableExpr(ex) =>
+      e(ex)
+
     case gl: GenericValue => gl
     case fl : FractionalLiteral => normalizeFraction(fl)
     case l : Literal[_] => l
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index 7058c9ba1a42e9001d463e58ea63f6fe1cb2ed67..c49e3941b355aa28a516c0d32e790fb09543f9fe 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -287,6 +287,9 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
           Stream()
       }
 
+    case MutableExpr(ex) =>
+      e(ex)
+
     case MatchExpr(scrut, cases) =>
 
       def matchesCase(scrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Stream[(MatchCase, Map[Identifier, Expr])] = {
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 64b0479b3abeaa2134560b6a7a9496e26d597b8b..5da34c789a74a277827612a5a2fd43cbe65b9199 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -998,6 +998,19 @@ object Expressions {
     val getType = ArrayType(tpe).unveilUntyped
   }
 
+  case class MutableExpr(var underlying: Expr) extends Expr with Extractable with PrettyPrintable {
+    def getType = underlying.getType
+
+    def extract: Option[(Seq[Expr], (Seq[Expr]) => Expr)] = Some(
+      Seq(underlying),
+      { case Seq(e) => underlying = e; this }
+    )
+
+    override def printWith(implicit pctx: PrinterContext): Unit = {
+      import PrinterHelpers._
+      p"$underlying"
+    }
+  }
 
   /* Special trees for synthesis */
   /** $encodingof `choose(pred)`, the non-deterministic choice in Leon.
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 2ae80beacdfd6d4a9fb88a4b25b9543f461f0e47..a48da5298ee856fd84e95f192afd42b4d97dfeb2 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -11,7 +11,7 @@ import TypeOps._
 object Types {
 
   trait Typed extends Printable {
-    val getType: TypeTree
+    def getType: TypeTree
     def isTyped : Boolean = getType != Untyped
   }
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 87d7985281b49d82cda40aa7a493f6e00200584c..77ed0a9c8a67dd27d64e3c398ac9a76ef0558088 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -529,6 +529,9 @@ trait SMTLIBTarget extends Interruptible {
         val constructor = constructors.toB(tpe)
         FunctionApplication(constructor, Seq(toSMT(InfiniteIntegerLiteral(n))))
 
+      case MutableExpr(ex) =>
+        toSMT(ex)
+
       /**
        * ===== Everything else =====
        */
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 95460440e8245ee33cf6f7e21ab0e63714b948c3..0eff41ea6b9b270bc774ec19b3f5751ec75920fd 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -520,6 +520,9 @@ trait AbstractZ3Solver extends Z3Solver {
         val constructor = constructors.toB(tp)
         constructor(rec(InfiniteIntegerLiteral(id)))
 
+      case MutableExpr(ex) =>
+        rec(ex)
+
       case other =>
         unsupported(other)
     }