diff --git a/core/src/main/scala/stainless/ast/SymbolIdentifier.scala b/core/src/main/scala/stainless/ast/SymbolIdentifier.scala
index a8725d99ee..e64a919905 100644
--- a/core/src/main/scala/stainless/ast/SymbolIdentifier.scala
+++ b/core/src/main/scala/stainless/ast/SymbolIdentifier.scala
@@ -25,7 +25,9 @@ object Symbol {
 }
 
 class SymbolIdentifier private[stainless](id: Identifier, val symbol: Symbol)
-  extends Identifier(id.name, id.globalId, id.id, alwaysShowUniqueID = false)
+  extends Identifier(id.name, id.globalId, id.id, alwaysShowUniqueID = false) {
+  override def freshen: SymbolIdentifier = new SymbolIdentifier(id.freshen, symbol)
+}
 
 object SymbolIdentifier {
   def apply(name: String): SymbolIdentifier = {
diff --git a/core/src/main/scala/stainless/genc/ir/Referentiator.scala b/core/src/main/scala/stainless/genc/ir/Referentiator.scala
index 4bcc5a1654..bdc2688ad3 100644
--- a/core/src/main/scala/stainless/genc/ir/Referentiator.scala
+++ b/core/src/main/scala/stainless/genc/ir/Referentiator.scala
@@ -247,10 +247,6 @@ final class Referentiator(val ctx: inox.Context) extends Transformer(LIR, RIR) {
     case _: to.Binding | _: to.FieldAccess | _: to.ArrayAccess | _: to.AsA => to.Ref(e)
     case to.Deref(e) => e
 
-    // NOTE Reference can be built on Constructor, but we have to make sure we
-    //      don't take the reference of a temporary result for a too long period.
-    case ctor @ to.Construct(_, _) if shortLived => to.Ref(ctor)
-
     case _ => ctx.reporter.fatalError(s"Making reference on an unsupported expression: $e")
   }
 
diff --git a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala
index 5a9bde4ee5..bc216a5574 100644
--- a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala
+++ b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala
@@ -244,8 +244,15 @@ private class S2IRImpl(override val s: tt.type,
   //     of Extending Safe C Support In Leon.
   private def checkConstructArgs(args: Seq[(CIR.Expr, Position)]): Unit = {
     // Reject arguments that have mutable type (but allow var, and arrays)
+
+    def isVdMutable(vd: CIR.ValDef): Boolean = vd.getType.isMutable && !vd.getType.isArray
+
     def isRefToMutableVar(arg: (CIR.Expr, Position)): Boolean = arg._1 match {
-      case CIR.Binding(vd) => vd.getType.isMutable && !vd.getType.isArray
+      case CIR.Binding(vd) => isVdMutable(vd)
+      case CIR.Block(exprs :+ CIR.Binding(vd)) => isVdMutable(vd) && !exprs.exists {
+        case CIR.Decl(`vd`, Some(e)) => !isRefToMutableVar((e, arg._2))
+        case _ => false
+      }
       case _ => false
     }
 
@@ -479,7 +486,7 @@ private class S2IRImpl(override val s: tt.type,
   // Try first to fetch the function from cache to handle recursive funcitons.
   private def rec(fa: FunAbstraction, tps: Seq[Type])(using tm0: TypeMapping, env: Env): CIR.FunDef = {
     val cacheKey = (fa, tps, tm0)
-    funResults get cacheKey getOrElse {
+    funResults getOrElse(cacheKey, {
 
     val id = buildId(fa, tps)(using tm0)
 
@@ -568,7 +575,7 @@ private class S2IRImpl(override val s: tt.type,
     fun.body = body
 
     fun
-  }}
+  })}
 
   // We need a type mapping only when converting context argument to remove the remaining generics.
   private def rec(typ: Type)(using tm: TypeMapping): CIR.Type = typ match {
@@ -685,6 +692,45 @@ private class S2IRImpl(override val s: tt.type,
     })
   }
 
+  private def recArgs(args: Seq[Expr])(using env: Env, tm0: TypeMapping): Seq[CIR.Expr] = {
+    def exprNeedsBinding(e: Expr): Boolean = e match {
+      case _: Variable => false
+      case ClassSelector(recv, _) => exprNeedsBinding(recv)
+      case TupleSelect(recv, _) => exprNeedsBinding(recv)
+      case ArraySelect(array, _) => exprNeedsBinding(array)
+      case _ => true
+    }
+
+    args.map { e =>
+      val tpe = e.getType
+      val irTpe = rec(tpe)
+      // Arguments that are mutable (and not an array) gets transformed to Reference by the Referentiator later on.
+      // To simplify its task, expressions that are (more or less) non-lvalues get bound to a fresh variable
+      // so we can take their address.
+      // For example, given:
+      //   case class Ref(var x: Int)
+      //
+      //   def f(v: Int): Unit = {
+      //      g(Ref(v + 42))
+      //   }
+      //   def g(r: Ref): Unit = ()
+      //
+      // We would introduce a `val tmp = Ref(v)` and have that passed to g instead.
+      // The resulting C code would be:
+      //   void f(int32_t v) {
+      //     int32_t tmp = v + 42; // `tmp` introduced here
+      //     int32_t *norm = &tmp; // `norm` introduced by the normalisation phase
+      //     g(norm);
+      //   }
+      if (!irTpe.isArray && irTpe.isMutable && exprNeedsBinding(e)) {
+        val vd = ValDef(FreshIdentifier("tmp"), tpe)
+        buildLet(vd, e, vd.toVariable, false)
+      } else {
+        rec(e)
+      }
+    }
+  }
+
   private def rec(e: Expr)(using env: Env, tm0: TypeMapping): CIR.Expr = e match {
 
     case Annotated(body, _) => rec(body)
@@ -772,7 +818,7 @@ private class S2IRImpl(override val s: tt.type,
         val filteredArgs = args.zip(fd.params).filter {
           case (arg, vd) => !isGlobal(vd.tpe)
         }.map(_._1)
-        val newArgs = filteredArgs map { a0 => rec(a0) }
+        val newArgs = recArgs(filteredArgs)
         CIR.App(fun.toVal, Seq(), newArgs)
       }
 
@@ -783,7 +829,7 @@ private class S2IRImpl(override val s: tt.type,
       locally {
         given tm1: TypeMapping = tm0 ++ tpSubst
         val extra = ctxDB(lfd) map { c => convertVarInfoToParam(c) }
-        val args2 = args map { a0 => rec(a0) }
+        val args2 = recArgs(args)
         CIR.App(fun.toVal, extra, args2)
       }
 
@@ -794,7 +840,7 @@ private class S2IRImpl(override val s: tt.type,
         case e if e.getType.isInstanceOf[CIR.FunType] => CIR.FunRef(e)
         case e => reporter.fatalError(fun0.getPos, s"Expected a binding but got $e of type ${e.getClass}.")
       }
-      val args = args0 map rec
+      val args = recArgs(args0)
 
       CIR.App(fun, Nil, args)
 
@@ -827,7 +873,7 @@ private class S2IRImpl(override val s: tt.type,
     case ClassConstructor(ct, args) =>
       val cd = syms.getClass(ct.id)
       val ct2 = rec(ct)
-      val args2 = args map rec
+      val args2 = recArgs(args)
       val positions = args map { _.getPos }
 
       checkConstructArgs(args2 zip positions)
@@ -849,7 +895,7 @@ private class S2IRImpl(override val s: tt.type,
 
     case tuple @ Tuple(args0) =>
       val clazz = tuple2Class(tuple.getType)
-      val args = args0 map rec
+      val args = recArgs(args0)
       val poss = args0 map { _.getPos }
 
       checkConstructArgs(args zip poss)
diff --git a/frontends/benchmarks/genc/invalid/InvalidReference1.scala b/frontends/benchmarks/genc/invalid/InvalidReference1.scala
new file mode 100644
index 0000000000..ea3f9d9c58
--- /dev/null
+++ b/frontends/benchmarks/genc/invalid/InvalidReference1.scala
@@ -0,0 +1,14 @@
+import stainless._
+import stainless.annotation._
+
+object InvalidReference1 {
+  case class Ref[T](var x: T)
+  case class Container[T](ref: Ref[T])
+
+  @cCode.`export`
+  def test1(v: Int): Unit = {
+    val rf = Ref(v)
+    // Invalid reference: cannot construct an object from a mutable variable.
+    val cont = Container(rf)
+  }
+}
diff --git a/frontends/benchmarks/genc/invalid/InvalidReference2.scala b/frontends/benchmarks/genc/invalid/InvalidReference2.scala
new file mode 100644
index 0000000000..1360159979
--- /dev/null
+++ b/frontends/benchmarks/genc/invalid/InvalidReference2.scala
@@ -0,0 +1,14 @@
+import stainless._
+import stainless.annotation._
+
+object InvalidReference2 {
+  case class Ref[T](var x: T)
+  case class Container[T](ref: Ref[T])
+
+  @cCode.`export`
+  def test1(v: Int): Unit = {
+    val rf = Ref(v)
+    // Invalid reference: cannot construct an object from a mutable variable.
+    val cont = Container({val dummy = 3; rf})
+  }
+}
diff --git a/frontends/benchmarks/genc/invalid/InvalidReference3.scala b/frontends/benchmarks/genc/invalid/InvalidReference3.scala
new file mode 100644
index 0000000000..7962c3a5e0
--- /dev/null
+++ b/frontends/benchmarks/genc/invalid/InvalidReference3.scala
@@ -0,0 +1,14 @@
+import stainless._
+import stainless.annotation._
+
+object InvalidReference3 {
+  case class Ref[T](var x: T)
+  case class Container[T](ref: Ref[T])
+
+  @cCode.`export`
+  def test1(v: Int): Unit = {
+    val rf = Ref(v)
+    // Invalid reference: cannot construct an object from a mutable variable.
+    val cont = Container({val tmp = rf; tmp})
+  }
+}
diff --git a/frontends/benchmarks/genc/ArgumentsEffects.scala b/frontends/benchmarks/genc/valid/ArgumentsEffects.scala
similarity index 100%
rename from frontends/benchmarks/genc/ArgumentsEffects.scala
rename to frontends/benchmarks/genc/valid/ArgumentsEffects.scala
diff --git a/frontends/benchmarks/genc/FixedArray.scala b/frontends/benchmarks/genc/valid/FixedArray.scala
similarity index 100%
rename from frontends/benchmarks/genc/FixedArray.scala
rename to frontends/benchmarks/genc/valid/FixedArray.scala
diff --git a/frontends/benchmarks/genc/Global.scala b/frontends/benchmarks/genc/valid/Global.scala
similarity index 100%
rename from frontends/benchmarks/genc/Global.scala
rename to frontends/benchmarks/genc/valid/Global.scala
diff --git a/frontends/benchmarks/genc/GlobalUninitialized.scala b/frontends/benchmarks/genc/valid/GlobalUninitialized.scala
similarity index 100%
rename from frontends/benchmarks/genc/GlobalUninitialized.scala
rename to frontends/benchmarks/genc/valid/GlobalUninitialized.scala
diff --git a/frontends/benchmarks/genc/ImageProcessing.scala b/frontends/benchmarks/genc/valid/ImageProcessing.scala
similarity index 100%
rename from frontends/benchmarks/genc/ImageProcessing.scala
rename to frontends/benchmarks/genc/valid/ImageProcessing.scala
diff --git a/frontends/benchmarks/genc/valid/InPlaceRefFnCall1.scala b/frontends/benchmarks/genc/valid/InPlaceRefFnCall1.scala
new file mode 100644
index 0000000000..243bab06cf
--- /dev/null
+++ b/frontends/benchmarks/genc/valid/InPlaceRefFnCall1.scala
@@ -0,0 +1,23 @@
+import stainless._
+import stainless.annotation.cCode
+import stainless.math._
+
+object InPlaceRefFnCall1 {
+  case class Ref[T](var x: T)
+  case class Container[T](v: Ref[T])
+
+  @cCode.`export`
+  def f(v: Int): Unit = wrapping {
+    // The expression Container(Ref(v + 10)) will be converted to something like:
+    // int32_t tmp = v + 10;
+    // Container { .v = &tmp }
+    placeholder(Container(Ref(v + 10)))
+  }
+
+  def placeholder(r: Container[Int]): Unit = {
+    ()
+  }
+
+  @cCode.`export`
+  def main(): Unit = ()
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/genc/valid/InPlaceRefFnCall2.scala b/frontends/benchmarks/genc/valid/InPlaceRefFnCall2.scala
new file mode 100644
index 0000000000..348f0137ce
--- /dev/null
+++ b/frontends/benchmarks/genc/valid/InPlaceRefFnCall2.scala
@@ -0,0 +1,22 @@
+import stainless._
+import stainless.annotation.cCode
+import stainless.math._
+
+object InPlaceRefFnCall2 {
+  case class Ref[T](var x: T)
+
+  @cCode.`export`
+  def f(v: Int): Unit = wrapping {
+    // The expression (456, Ref(v + 10)) will be converted to something like:
+    // int32_t tmp = v + 10;
+    // Tuple2 { ._1 = 456, ._2 = &tmp }
+    placeholder((456, Ref(v + 10)))
+  }
+
+  def placeholder(r: (Int, Ref[Int])): Unit = {
+    ()
+  }
+
+  @cCode.`export`
+  def main(): Unit = ()
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/genc/LZWa.scala b/frontends/benchmarks/genc/valid/LZWa.scala
similarity index 100%
rename from frontends/benchmarks/genc/LZWa.scala
rename to frontends/benchmarks/genc/valid/LZWa.scala
diff --git a/frontends/benchmarks/genc/LZWb.scala b/frontends/benchmarks/genc/valid/LZWb.scala
similarity index 100%
rename from frontends/benchmarks/genc/LZWb.scala
rename to frontends/benchmarks/genc/valid/LZWb.scala
diff --git a/frontends/benchmarks/genc/Nested.scala b/frontends/benchmarks/genc/valid/Nested.scala
similarity index 100%
rename from frontends/benchmarks/genc/Nested.scala
rename to frontends/benchmarks/genc/valid/Nested.scala
diff --git a/frontends/benchmarks/genc/Normalisation.scala b/frontends/benchmarks/genc/valid/Normalisation.scala
similarity index 100%
rename from frontends/benchmarks/genc/Normalisation.scala
rename to frontends/benchmarks/genc/valid/Normalisation.scala
diff --git a/frontends/benchmarks/genc/Pointer.scala b/frontends/benchmarks/genc/valid/Pointer.scala
similarity index 100%
rename from frontends/benchmarks/genc/Pointer.scala
rename to frontends/benchmarks/genc/valid/Pointer.scala
diff --git a/frontends/benchmarks/genc/valid/Pointer2.scala b/frontends/benchmarks/genc/valid/Pointer2.scala
new file mode 100644
index 0000000000..ea9b0d91d6
--- /dev/null
+++ b/frontends/benchmarks/genc/valid/Pointer2.scala
@@ -0,0 +1,29 @@
+import stainless.annotation._
+import stainless.io._
+
+object Pointer2 {
+
+  case class Pointer[T](var x: T)
+
+  def inc(p: Pointer[Int]): Int = {
+    require(0 <= p.x && p.x <= 1000)
+    p.x += 1
+    p.x
+  }
+
+  def f(v: Int): Int = {
+    require(0 <= v && v <= 500)
+    inc(Pointer(v + 42))
+  }
+
+  @cCode.`export`
+  def main(): Unit = {
+    @ghost implicit val state = newState
+    val res1 = inc(Pointer(123))
+    assert(res1 == 124)
+    val res2 = f(400)
+    assert(res2 == 443)
+    StdOut.println(res1)
+    StdOut.println(res2)
+  }
+}
diff --git a/frontends/benchmarks/genc/valid/RefInCtor.scala b/frontends/benchmarks/genc/valid/RefInCtor.scala
new file mode 100644
index 0000000000..14d2cbe19e
--- /dev/null
+++ b/frontends/benchmarks/genc/valid/RefInCtor.scala
@@ -0,0 +1,25 @@
+import stainless._
+import stainless.annotation._
+
+object RefInCtor {
+
+  case class Ref[T](var x: T)
+
+  case class Container[T](ref: Ref[T])
+
+  @cCode.`export`
+  def test1(v: Int): Unit = {
+    val cont = Container(Ref(v))
+    // The above is fine, but the following is not (see invalid/InvalidReference1)
+    // val rf = Ref(v)
+    // val cont = Container(rf)
+  }
+
+  @cCode.`export`
+  def test2(v: Int): Unit = {
+    val cont = Container({val tmp = Ref(v); tmp}) // tmp is a ref. to a mutable variable, but is local to its block.
+  }
+
+  @cCode.`export`
+  def main(): Unit = ()
+}
diff --git a/frontends/benchmarks/genc/Return.scala b/frontends/benchmarks/genc/valid/Return.scala
similarity index 100%
rename from frontends/benchmarks/genc/Return.scala
rename to frontends/benchmarks/genc/valid/Return.scala
diff --git a/frontends/benchmarks/genc/StateTest.scala b/frontends/benchmarks/genc/valid/StateTest.scala
similarity index 100%
rename from frontends/benchmarks/genc/StateTest.scala
rename to frontends/benchmarks/genc/valid/StateTest.scala
diff --git a/frontends/benchmarks/genc/TwoOptions.scala b/frontends/benchmarks/genc/valid/TwoOptions.scala
similarity index 100%
rename from frontends/benchmarks/genc/TwoOptions.scala
rename to frontends/benchmarks/genc/valid/TwoOptions.scala
diff --git a/frontends/benchmarks/genc/Unsigned.scala b/frontends/benchmarks/genc/valid/Unsigned.scala
similarity index 100%
rename from frontends/benchmarks/genc/Unsigned.scala
rename to frontends/benchmarks/genc/valid/Unsigned.scala
diff --git a/frontends/benchmarks/genc/WhileInLet.scala b/frontends/benchmarks/genc/valid/WhileInLet.scala
similarity index 100%
rename from frontends/benchmarks/genc/WhileInLet.scala
rename to frontends/benchmarks/genc/valid/WhileInLet.scala
diff --git a/frontends/common/src/it/scala/stainless/GenCSuite.scala b/frontends/common/src/it/scala/stainless/GenCSuite.scala
index d58cd4908b..4bd4d9048a 100644
--- a/frontends/common/src/it/scala/stainless/GenCSuite.scala
+++ b/frontends/common/src/it/scala/stainless/GenCSuite.scala
@@ -5,6 +5,7 @@ package stainless
 import utils._
 
 import org.scalatest.funsuite.AnyFunSuite
+import org.scalatest.matchers.should.Matchers
 
 import java.nio.file.{Paths, Files}
 import java.io.File
@@ -12,8 +13,9 @@ import java.io.PrintWriter
 
 import Utils._
 
-class GenCSuite extends AnyFunSuite with inox.ResourceUtils with InputUtils {
-  val files = resourceFiles("genc", _.endsWith(".scala"), false).map(_.getPath).toSeq
+class GenCSuite extends AnyFunSuite with inox.ResourceUtils with InputUtils with Matchers {
+  val validFiles = resourceFiles("genc/valid", _.endsWith(".scala"), false).map(_.getPath)
+  val invalidFiles = resourceFiles("genc/invalid", _.endsWith(".scala"), false).map(_.getPath)
   val ctx = TestContext.empty
 
   // FIXME: fix verification for those files
@@ -26,7 +28,15 @@ class GenCSuite extends AnyFunSuite with inox.ResourceUtils with InputUtils {
     "ArgumentsEffects.scala", // https://github.com/epfl-lara/stainless/issues/1068
   )
 
-  for (file <- files if !ignoreVerification(new File(file).getName)) {
+  for (file <- invalidFiles) {
+    val cFile = file.replace(".scala", ".c")
+    val outFile = file.replace(".scala", ".out")
+    test(s"stainless --genc --genc-output=$cFile $file should fail") {
+      an [inox.FatalError] should be thrownBy runMainWithArgs(Array(file) :+ "--genc" :+ s"--genc-output=$cFile")
+    }
+  }
+
+  for (file <- validFiles if !ignoreVerification(new File(file).getName)) {
     test(s"stainless --batched $file") {
       val (localCtx, optReport) = runMainWithArgs(Array(file) :+ "--batched")
       assert(localCtx.reporter.errorCount == 0, "No errors")
@@ -35,7 +45,7 @@ class GenCSuite extends AnyFunSuite with inox.ResourceUtils with InputUtils {
     }
   }
 
-  for (file <- files) {
+  for (file <- validFiles) {
     val cFile = file.replace(".scala", ".c")
     val outFile = file.replace(".scala", ".out")
     test(s"stainless --genc --genc-output=$cFile $file") {
@@ -49,56 +59,49 @@ class GenCSuite extends AnyFunSuite with inox.ResourceUtils with InputUtils {
   }
 
   test("Checking that ArgumentsEffects outputs 113") {
-    val fileArgumentsEffects = files.find(_.toString.contains("ArgumentsEffects.scala")).get
-    val outFile = fileArgumentsEffects.replace(".scala", ".out")
-    ctx.reporter.info(s"Running: $outFile")
-    val (std, _) = runCommand(outFile)
-    val output = std.mkString
+    val output = runCHelper("ArgumentsEffects.scala")
     assert(output == "113", s"Output '$output' should be '113'")
   }
 
   test("Checking that Global outputs 5710120") {
-    val fileGlobal = files.find(_.toString.contains("Global.scala")).get
-    val outFile = fileGlobal.replace(".scala", ".out")
-    ctx.reporter.info(s"Running: $outFile")
-    val (std, _) = runCommand(outFile)
-    val output = std.mkString
+    val output = runCHelper("Global.scala")
     assert(output == "5710120", s"Output '$output' should be '5710120'")
   }
 
   test("Checking that GlobalUninitialized outputs 8410120") {
-    val fileGlobalUninitialized = files.find(_.toString.contains("GlobalUninitialized.scala")).get
-    val outFile = fileGlobalUninitialized.replace(".scala", ".out")
-    ctx.reporter.info(s"Running: $outFile")
-    val (std, _) = runCommand(outFile)
-    val output = std.mkString
+    val output = runCHelper("GlobalUninitialized.scala")
     assert(output == "8410120", s"Output '$output' should be '8410120'")
   }
 
   test("Checking that LZWa can encode and decode") {
-    val fileLZWa = files.find(_.toString.contains("LZWa.scala")).get
-    val outFile = fileLZWa.replace(".scala", ".out")
     val randomString = scala.util.Random.alphanumeric.take(1000).mkString
     new PrintWriter("input.txt") { try write(randomString) finally close() }
-    ctx.reporter.info(s"Running: $outFile")
-    val (std, _) = runCommand(outFile)
-    val output = std.mkString
+    val output = runCHelper("LZWa.scala")
     assert(output == "success", s"Output '$output' should be 'success'")
     val decoded = scala.io.Source.fromFile("decoded.txt").mkString
     assert(decoded == randomString, s"Decoded ($decoded) should be equal to $randomString")
   }
 
   test("Checking that LZWb can encode and decode") {
-    val fileLZWb = files.find(_.toString.contains("LZWb.scala")).get
-    val outFile = fileLZWb.replace(".scala", ".out")
     val randomString = scala.util.Random.alphanumeric.take(1000).mkString
     new PrintWriter("input.txt") { try write(randomString) finally close() }
-    ctx.reporter.info(s"Running: $outFile")
-    val (std, _) = runCommand(outFile)
-    val output = std.mkString
+    val output = runCHelper("LZWb.scala")
     assert(output == "success", s"Output '$output' should be 'success'")
     val decoded = scala.io.Source.fromFile("decoded.txt").mkString
     assert(decoded == randomString, s"Decoded ($decoded) should be equal to $randomString")
   }
 
+  test("Checking that Pointer2 outputs 124443") {
+    val output = runCHelper("Pointer2.scala")
+    assert(output == "124443", s"Output '$output' should be '124443'")
+  }
+
+  def runCHelper(filename: String): String = {
+    val file = validFiles.find(_.contains(filename)).get
+    val outFile = file.replace(".scala", ".out")
+    ctx.reporter.info(s"Running: $outFile")
+    val (std, _) = runCommand(outFile)
+    // Note: lines are concatenated without adding newlines between them
+    std.mkString
+  }
 }
diff --git a/frontends/common/src/it/scala/stainless/Utils.scala b/frontends/common/src/it/scala/stainless/Utils.scala
index 35c171e78b..b980340302 100644
--- a/frontends/common/src/it/scala/stainless/Utils.scala
+++ b/frontends/common/src/it/scala/stainless/Utils.scala
@@ -9,10 +9,10 @@ object Utils {
     (std.toList, exitCode)
   }
 
-  def runMainWithArgs(args: Array[String]) = {
+  def runMainWithArgs(args: Array[String]): (inox.Context, Option[AbstractReport[_]]) = {
     val ctx = Main.setup(args).copy(reporter = new inox.TestSilentReporter())
     val compilerArgs = args.toList filterNot { _.startsWith("--") }
-    var compiler = frontend.build(ctx, compilerArgs, stainless.Main.factory)
+    val compiler = frontend.build(ctx, compilerArgs, stainless.Main.factory)
     ctx.reporter.info(s"Running: stainless ${args.mkString(" ")}")
     compiler.run()
     compiler.join()