diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala index 83fa2d6083cecfe76b9d999029ba9eea87887357..d0e0fed699dc2683190dae45cad26c0f7782590b 100644 --- a/src/funcheck/CodeExtraction.scala +++ b/src/funcheck/CodeExtraction.scala @@ -211,7 +211,7 @@ trait CodeExtraction extends Extractors { realBody match { case ExEnsuredExpression(body2, resSym, contract) => { - varSubsts(resSym) = (() => ResultVariable()) + varSubsts(resSym) = (() => ResultVariable().setType(funDef.returnType)) val c1 = s2ps(contract) // varSubsts.remove(resSym) realBody = body2 diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala index 2e067cb53c5cc88e770d469e3b5b836764ddb99e..7701dca51155c32ee8340c5037f3f3a982c82c6b 100644 --- a/src/purescala/Analysis.scala +++ b/src/purescala/Analysis.scala @@ -93,6 +93,12 @@ class Analysis(val program: Program) { } } + def rewritePatternMatching(expr: Expr) : Expr = { + + + expr + } + def replaceInExpr(substs: Map[Expr,Expr], expr: Expr) : Expr = { def rec(ex: Expr) : Expr = ex match { case _ if (substs.get(ex).isDefined) => substs(ex)