diff --git a/src/main/scala/leon/xlang/EffectsChecking.scala b/src/main/scala/leon/xlang/EffectsChecking.scala index d7045af85..983a9fbc3 100644 --- a/src/main/scala/leon/xlang/EffectsChecking.scala +++ b/src/main/scala/leon/xlang/EffectsChecking.scala @@ -106,7 +106,7 @@ object EffectsChecking extends UnitPhase[Program] { getReturnedExpr(body).foreach{ case expr if effects.isMutableType(expr.getType) => findReferencedIds(expr).foreach(id => - if(bindings.contains(id)) + if(effects.isMutableType(id.getType) && bindings.contains(id)) ctx.reporter.fatalError(expr.getPos, "Cannot return a shared reference to a mutable object: " + expr) ) case _ => () diff --git a/src/test/resources/regression/xlang/passing/ReturnNoAliasing1.scala b/src/test/resources/regression/xlang/passing/ReturnNoAliasing1.scala new file mode 100644 index 000000000..985c2224e --- /dev/null +++ b/src/test/resources/regression/xlang/passing/ReturnNoAliasing1.scala @@ -0,0 +1,9 @@ +import leon.lang._ + +object ReturnNoAliasing1 { + + case class A(var x: Int) + + def f(y: Int): A = A(y) + +}