let abstract_others sa others = (* let sa = SAtom.filter (function *) (* | Comp ((Elem (x, _) | Access (x,_,_)), _, _) -> *) (* let x = if is_prime (Hstring.view x) then unprime_h x else x in *) (* not (Smt.Typing.has_abstract_type x) *) (* | Ite _ -> false *) (* | _ -> true) sa in *) SAtom.filter (fun a -> not (List.exists (fun z -> atom_contains_arg z a) others)) sa