diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 47f6f344198642802742c88555e6202dad5291e2..b37067de4ba1c87c37b5648a21aafbbfd267ca15 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -1195,7 +1195,7 @@ trait CodeGeneration {
         mkBranch(b, al, fl, ch, canDelegateToMkExpr = false)
         ch << Label(fl) << POP << Ldc(0) << Label(al)
 
-      case MutableExpr(e) =>
+      case synthesis.utils.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 5fba0109e58fe9c1b361144ac6f08c55fa374a9e..933781bfbfb5867a3c04964e34871a5f874467cc 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -831,7 +831,7 @@ 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) =>
+    case synthesis.utils.MutableExpr(ex) =>
       e(ex)
 
     case gl: GenericValue => gl
diff --git a/src/main/scala/leon/evaluators/StreamEvaluator.scala b/src/main/scala/leon/evaluators/StreamEvaluator.scala
index c49e3941b355aa28a516c0d32e790fb09543f9fe..8caf0c9f42aab088be91e79de65cf61317b75575 100644
--- a/src/main/scala/leon/evaluators/StreamEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StreamEvaluator.scala
@@ -287,7 +287,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
           Stream()
       }
 
-    case MutableExpr(ex) =>
+    case synthesis.utils.MutableExpr(ex) =>
       e(ex)
 
     case MatchExpr(scrut, cases) =>
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 7567132ea11e717ffec71cdfe203f758dba9a776..65fbfb0dc99411ace43fa47ff4d2a6956a574bf2 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -998,20 +998,6 @@ 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/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 77ed0a9c8a67dd27d64e3c398ac9a76ef0558088..b37ffacf8b348da16f656f509c0659ebf141d39c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -529,7 +529,7 @@ trait SMTLIBTarget extends Interruptible {
         val constructor = constructors.toB(tpe)
         FunctionApplication(constructor, Seq(toSMT(InfiniteIntegerLiteral(n))))
 
-      case MutableExpr(ex) =>
+      case synthesis.utils.MutableExpr(ex) =>
         toSMT(ex)
 
       /**
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 99567a865bc09b8c3b154ae220d48d7fad5898fd..0fef7e87a214dc3727d9114cc916b62d88ca9f42 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -552,7 +552,7 @@ trait AbstractZ3Solver extends Z3Solver {
         val constructor = constructors.toB(tp)
         constructor(rec(InfiniteIntegerLiteral(id)))
 
-      case MutableExpr(ex) =>
+      case synthesis.utils.MutableExpr(ex) =>
         rec(ex)
 
       case other =>
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index f7ab39d9de113642c5b8d20fe6ad104fe21d2fb6..a737d78a65c13a2e9bcf9070a3c45394307f4d0a 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -13,6 +13,7 @@ import purescala.TypeOps.depth
 import purescala.DefOps._
 import purescala.Constructors._
 
+import utils.MutableExpr
 import solvers._
 import leon.grammars._
 import leon.grammars.aspects._
diff --git a/src/main/scala/leon/synthesis/utils/MutableExpr.scala b/src/main/scala/leon/synthesis/utils/MutableExpr.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f30fd8104d60eee795988e0199b36082ee9e8a18
--- /dev/null
+++ b/src/main/scala/leon/synthesis/utils/MutableExpr.scala
@@ -0,0 +1,21 @@
+package leon
+package synthesis.utils
+
+import purescala.Expressions.Expr
+import purescala.Extractors.Extractable
+import purescala.{PrinterHelpers, PrinterContext, PrettyPrintable}
+
+/** A mutable expression box useful for CEGIS */
+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"
+  }
+}
\ No newline at end of file