From a473c8f2317a98a5e26138c514353c8d26ef3068 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 11 May 2012 16:02:50 +0200
Subject: [PATCH] get returned expr with branches of match expression

---
 src/main/scala/leon/plugin/CodeExtraction.scala | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 4d3dab3d0..ae7d8c0e5 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -1065,6 +1065,10 @@ trait CodeExtraction extends Extractors {
     case LetVar(_, _, rest) => getReturnedExpr(rest)
     case PBlock(_, rest) => getReturnedExpr(rest)
     case IfExpr(_, then, elze) => getReturnedExpr(then) ++ getReturnedExpr(elze)
+    case MatchExpr(_, cses) => cses.flatMap{
+      case SimpleCase(_, rhs) => getReturnedExpr(rhs)
+      case GuardedCase(_, _, rhs) => getReturnedExpr(rhs)
+    }
     case _ => Seq(expr)
   }
 
-- 
GitLab