diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index f55c5d548ac53884951e735d0eaf037b328a04e5..b98faa52f1e0ffd27bb43d53998d8f206c5a9e4c 100644 --- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala +++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala @@ -1009,8 +1009,13 @@ trait CodeExtraction extends ASTExtractors { val rc = cases.map(extractMatchCase(_)) val UnwrapTuple(ines) = ine - (oute +: ines) foreach { - case Variable(_) => { } + ines foreach { + case v : Variable if currentFunDef.params.map{ _.toVariable } contains v => + case LeonThis(_) => + case other => ctx.reporter.fatalError(other.getPos, "Only i/o variables are allowed in i/o examples") + } + oute match { + case Variable(_) => // FIXME: this is not strict enough, we need the bound variable of enclosing Ensuring case other => ctx.reporter.fatalError(other.getPos, "Only i/o variables are allowed in i/o examples") } passes(ine, oute, rc)