diff --git a/colibri2/theories/quantifier/definitions.ml b/colibri2/theories/quantifier/definitions.ml
index 76c4ea6d21a92af0aa920b3144d007b1846386c5..b34f825b3dee6f0a5f46bc02e2e8f911438a02d9 100644
--- a/colibri2/theories/quantifier/definitions.ml
+++ b/colibri2/theories/quantifier/definitions.ml
@@ -21,9 +21,22 @@
 open Colibri2_core
 open Colibri2_popop_lib
 
+let criteria d (_sym : Expr.Term.Const.t) _tyl _tvl (body : Expr.term) =
+  (* The definition should not start with a builtin symbol. The rational is that
+     builtin symbols are hard to match efficiently: substitution not found often
+     but takes a lot of time since there is a lot of term (e.g. boolean operators)
+  *)
+  match body.term_descr with
+  | Expr.Var _ -> false
+  | Expr.Cst _ -> false
+  | Expr.App ({ term_descr = Expr.Cst s; _ }, _, _) ->
+      not (Info.Builtin_skipped_for_trigger.skipped d s.builtin)
+  | Expr.App (_, _, _) -> false
+  | Expr.Binder (_, _) -> false
+  | Expr.Match (_, _) -> false
+
 let handler d (sym : Expr.Term.Const.t) tyl tvl body =
-  (* Check that it don't start with a builtin (can be changed) *)
-  if not (Info.Builtin_skipped_for_trigger.skipped d sym.builtin) then
+  if criteria d sym tyl tvl body then
     let tys, tvs =
       Expr.Term.free_vars (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty) body
     in