executability test: bugfix

ECase(ghost e1,[branch]) and constructor application with ghost parameters
were handled incorrectly.

src/whyml/mlw_exec.ml

@@ -56,6 +56,13 @@ let rec is_exec_term ctx t = match t.t_node with
       true
   | Tconst c ->
       is_exec_const c
+  | Tapp (ls, tl) when ls.ls_constr > 0 ->
+      begin match try Some (Mlw_expr.restore_pl ls) with Not_found -> None with
+      | Some pl ->
+          let test fd arg = fd.Mlw_expr.fd_ghost || is_exec_term ctx arg in
+          List.for_all2 test pl.Mlw_expr.pl_args tl
+      | None -> List.for_all (is_exec_term ctx) tl
+      end
   | Tapp (ls, tl) ->
       is_exec_lsymbol ctx ls && List.for_all (is_exec_term ctx) tl
   | Tif (t1, t2, t3) ->
@@ -148,6 +155,8 @@ let rec is_exec_expr ctx e =
         let aux f = is_exec_expr ctx f.fun_lambda.l_expr in
         List.for_all aux fdl &&
         is_exec_expr ctx e1
+    | Ecase (e1, [_, e2]) when e1.e_ghost ->
+        is_exec_expr ctx e2
     | Ecase (e1, bl) ->
         let aux (_, e) = is_exec_expr ctx e in
         is_exec_expr ctx e1 &&