inlining corrected

compiler/heptagon/main/hept_compiler.ml

@@ -30,9 +30,7 @@ let compile_program p =
   let p = pass "Completion" true Completion.program p pp in
 
   (* Inlining *)
-  let p =
-    let call_inline_pass = (List.length !inline > 0) || !flatten in
-    pass "Inlining" call_inline_pass Inline.program p pp in
+  let p = pass "Inlining" true Inline.program p pp in
 
   (* Automata *)
   let p = pass "Automata" true Automata.program p pp in

compiler/heptagon/parsing/hept_parser.mly

@@ -463,6 +463,7 @@ node_name:
 
 merge_handlers:
   | hs=nonempty_list(merge_handler) { hs }
+  | e1=simple_exp e2=simple_exp { [(Q Initial.ptrue, e1);(Q Initial.pfalse, e2)] }
 merge_handler:
   | LPAREN c=constructor_or_bool ARROW e=exp RPAREN { (c,e) }
 

compiler/heptagon/transformations/inline.ml

@@ -58,7 +58,9 @@ let exp funs (env, newvars, newequs) exp =
         (Hept_printer.iterator_to_string it) (fullname nn);
       (exp, (env, newvars, newequs))
 
-  | Eapp ({ a_op = (Enode nn | Efun nn); } as op, argl, rso) when to_be_inlined nn ->
+  | Eapp ({ a_op = (Enode nn | Efun nn);
+            a_unsafe = false; (* Unsafe can't be inlined *)
+            a_inlined = inlined } as op, argl, rso) when inlined || to_be_inlined nn ->
     begin try
       let add_reset eq = match rso with
         | None -> eq