fixed an evaluation order problem in e_plapp

parent a4e508ff
......@@ -591,7 +591,8 @@ let e_plapp pls el ity =
mk_expr (Elogic t) (VTvalue ity) ghost eff syms
| [],_ | _,[] ->
raise (Term.BadArity (pls.pl_ls, List.length el))
| fd::fdl, ({ e_node = Elogic t } as e)::argl ->
| fd::fdl, ({ e_node = Elogic t } as e)::argl
when Spv.for_all (fun pv -> ity_immutable pv.pv_ity) e.e_syms.syms_pv ->
let t = match t.t_ty with
| Some _ -> t
| None -> t_if_simp t t_bool_true t_bool_false in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment