No commit message

No commit message

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

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)