From 5e4507b3eb330f67848b65cc4e27f920e1be83dc Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Sat, 20 May 2017 16:01:15 +0200 Subject: [PATCH] Expr: be less zealous on term-to-fmla conversion --- src/mlw/expr.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/mlw/expr.ml b/src/mlw/expr.ml index 40693f0a7..bf6f5071d 100644 --- a/src/mlw/expr.ml +++ b/src/mlw/expr.ml @@ -571,15 +571,13 @@ let rec raw_of_expr prop e = match e.e_node with pure_of_expr prop e | Eif (e0,e1,e2) when is_e_false e1 && is_e_true e2 -> t_not (pure_of_expr true e0) - | Eif (e0,e1,e2) when is_e_false e2 -> + | Eif (e0,e1,e2) when prop && is_e_false e2 -> t_and (pure_of_expr true e0) (pure_of_expr true e1) - | Eif (e0,e1,e2) when is_e_true e1 -> + | Eif (e0,e1,e2) when prop && is_e_true e1 -> t_or (pure_of_expr true e0) (pure_of_expr true e2) | Eif (e0,e1,e2) -> - let prop = prop || ity_equal e.e_ity ity_bool in t_if (pure_of_expr true e0) (pure_of_expr prop e1) (pure_of_expr prop e2) | Ecase (d,bl) -> - let prop = prop || ity_equal e.e_ity ity_bool in let conv (p,e) = t_close_branch p.pp_pat (pure_of_expr prop e) in t_case (pure_of_expr false d) (List.map conv bl) | Etry _ | Eraise _ | Eabsurd -> raise Exit -- GitLab