diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml index 1539cc634068710ca3f35c892be41aa267b45268..4697b7f2671b060c9aa199b2d6af8b657aa6d84b 100644 --- a/src/plugins/eva/engine/transfer_specification.ml +++ b/src/plugins/eva/engine/transfer_specification.ml @@ -46,7 +46,18 @@ let warn_empty_assigns () = (* Warn for assigns clauses without \from. *) let warn_empty_from list = - let no_from = List.filter (fun (_, from) -> from = FromAny) list in + let is_empty_set it = + match it with + | { it_content = { term_node = Tempty_set }} -> true + | _ -> false + in + let no_from = + List.filter + (fun (it, from) -> + (* Ignore assigns \empty with no \from. *) + not (is_empty_set it) && from = FromAny) + list + in match no_from with | [] -> () | (out, _) :: _ ->