diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 4f3d96502..98a7ad6f3 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -83,13 +83,12 @@ jobs:
           opam exec -- cygpath -m ${{ github.workspace }} | % {$_ -replace "^","workspace=" }  | Out-File -FilePath $Env:GITHUB_ENV -Encoding utf8 -Append
           opam exec -- cygpath -m "$Env:CYGWIN_ROOT" | % {$_ -replace "^","cygwin_root=" }  | Out-File -FilePath $Env:GITHUB_ENV -Encoding utf8 -Append
           opam exec -- sed -i ' ' tests/sources/*.elpi
-          & "$Env:CYGWIN_ROOT/setup-x86_64.exe" -q -P time
-          & "$Env:CYGWIN_ROOT/setup-x86_64.exe" -q -P which
-          & "$Env:CYGWIN_ROOT/setup-x86_64.exe" -q -P wdiff
-          opam exec -- which which
-          opam exec -- time which
-          opam exec -- which time
-          opam exec -- which wdiff
+          & "$Env:CYGWIN_ROOT/setup-x86_64.exe" -v -q -P time,which,wdiff
+
+#          opam exec -- which which
+#          opam exec -- time which
+#          opam exec -- which time
+#          opam exec -- which wdiff
 
 # Build ######################################################################
 #
diff --git a/.ocamlformat b/.ocamlformat
new file mode 100644
index 000000000..e69de29bb
diff --git a/CHANGES.md b/CHANGES.md
index 1bc8ac46d..9d8287c2f 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -3,6 +3,10 @@
 Library:
   - New `std.fold-right`
 
+Runtime:
+  - New clause retrieval through discrimination tree. This new index is enabled
+    whenever the `:index` directive selects only one argument  with a depth `> 1`.
+
 # v1.18.0 (October 2023)
 
 Requires Menhir 20211230 and OCaml 4.08 or above.
diff --git a/ELPI.md b/ELPI.md
index 5ba8b5054..a04d4a9b0 100644
--- a/ELPI.md
+++ b/ELPI.md
@@ -66,7 +66,7 @@ trivial-facts :-
 ```
 
 Side note: no solution is computed for goals like `_ = something`.
-On the contrary a problem like `DummyNameUsedOnlyOnce = somthing` demands the
+On the contrary a problem like `DummyNameUsedOnlyOnce = something` demands the
 computation of the solution (even if it is not used), and hence can *fail* if
 some variable occurring in something is out of scope for `DummyNameUsedOnlyOnce`.
 
@@ -308,8 +308,20 @@ If only one argument is indexed, and it is indexed at depth one, then Elpi uses
 a standard indexing technique based on a perfect (for depth 1) search tree. This
 means that no false positives are returned by the index.
 
-If more than one argument is indexed, or if some argument is indexed at depth
-greater than 1, then Elpi uses an index based on the idea of
+### Discrimination tree index
+
+If only one argument is indexed at depth greater than one, then Elpi uses
+a [discrimination tree](https://www.cs.cmu.edu/~fp/courses/99-atp/lectures/lecture28.html).
+Both the rule argument and the goal argument are
+indexed up to the given depth. The indexing is not perfect, false positives may
+be returned and ruled out by unification.
+
+Indexed terms are linearized into paths. Paths are inserted into a trie data
+structure sharing common prefixes.
+
+### Hash based index
+
+If more than one argument is indexed then Elpi uses an index based on the idea of
 [unification hashes](http://blog.ndrix.com/2013/03/prolog-unification-hashes.html).
 
 ```prolog
@@ -618,7 +630,7 @@ syntax `{{:name` .. `}}` where `name` is any non-space or `\n` character.
 Quotations are elaborated before run-time.
 
 The [coq-elpi](https://github.com/LPCIC/coq-elpi) software embeds elpi 
-in Coq and provides a quatation for its terms. For example
+in Coq and provides a quotation for its terms. For example
 ```prolog
 {{ nat -> bool }}
 ```
diff --git a/INCOMPATIBILITIES.md b/INCOMPATIBILITIES.md
index ce581d932..7af327595 100644
--- a/INCOMPATIBILITIES.md
+++ b/INCOMPATIBILITIES.md
@@ -1,7 +1,7 @@
 Known incompatibilities with Teyjus
 ===================================
 
-This file tries to summarise known incompatibilities between Elpi and Teyjus.
+This file tries to summarize known incompatibilities between Elpi and Teyjus.
 
 # Semantics
 
@@ -37,7 +37,7 @@ This file tries to summarise known incompatibilities between Elpi and Teyjus.
 - Module signatures are ignored.
 - Elpi accumulates each file once; Teyjus does it multiple times, that is
   always bad (all clauses are duplicated and tried multiple times, that is
-  rarely the expected behaviour).
+  rarely the expected behavior).
 - Elpi understands relative paths as in `accumulate "../foo"`: resolution
   of relative paths is done according to the path of the accumulating file
   first or, if it fails, according to the TJPATH.
diff --git a/README.md b/README.md
index 5152d2139..526e49484 100644
--- a/README.md
+++ b/README.md
@@ -134,7 +134,7 @@ The elaborator manipulates terms with binders and holes
 (unification variables) representing missing piece of 
 information.  Some of them have to be filled in order 
 to make the term well typed. Some others are filled in because 
-the user has programmed the eleborator to do so, e.g. ad-hoc polymorphism.
+the user has programmed the elaborator to do so, e.g. ad-hoc polymorphism.
 
 Such software component is characterized by an high complexity
 coming from the interplay of binders, reduction and unification,
diff --git a/src/compiler.ml b/src/compiler.ml
index e442f5651..c4184aaeb 100644
--- a/src/compiler.ml
+++ b/src/compiler.ml
@@ -1233,6 +1233,7 @@ let query_preterm_of_ast ~depth macros state (loc, t) =
          Loc.show (snd (C.Map.find name map)) ^ ")")
 
   let compile_mode (state, modes) { Ast.Mode.name; args; loc } =
+    let args = List.map to_mode args in
     let state, mname = funct_of_ast state name in
     check_duplicate_mode state mname (args,loc) modes;
     state, C.Map.add mname (args,loc) modes
@@ -1356,7 +1357,7 @@ let query_preterm_of_ast ~depth macros state (loc, t) =
       (state : State.t), lcs, active_macros,
       { Structured.types; type_abbrevs; modes; body; symbols }
 
-    and compile_body macros types type_abbrevs modes lcs defs state = function
+    and compile_body macros types type_abbrevs (modes : (mode * Loc.t) C.Map.t) lcs defs state = function
       | [] -> lcs, state, types, type_abbrevs, modes, defs, []
       | Locals (nlist, p) :: rest ->
           let orig_varmap = get_varmap state in
@@ -1673,11 +1674,11 @@ module Spill : sig
 
   
   val spill_clause :
-    State.t -> types:Structured.typ list C.Map.t -> modes:(constant -> bool list) ->
+    State.t -> types:Structured.typ list C.Map.t -> modes:(constant -> mode) ->
       (preterm, 'a) Ast.Clause.t -> (preterm, 'a) Ast.Clause.t
 
   val spill_chr :
-    State.t -> types:Structured.typ list C.Map.t -> modes:(constant -> bool list) ->
+    State.t -> types:Structured.typ list C.Map.t -> modes:(constant -> mode) ->
       (constant list * prechr_rule list) -> (constant list * prechr_rule list)
   
   (* Exported to compile the query *)
@@ -1727,7 +1728,7 @@ end = struct (* {{{ *)
       | `Arrow(arity,_),_ ->
           let missing = arity - nargs in
           let output_suffix =
-            let rec aux = function false :: l -> 1 + aux l | _ -> 0 in
+            let rec aux = function Output :: l -> 1 + aux l | _ -> 0 in
             aux (List.rev mode) in
           if missing > output_suffix then
             error ~loc Printf.(sprintf
@@ -2358,14 +2359,13 @@ let compile_clause modes initial_depth state
   state, cl
 
 let chose_indexing state predicate l =
-  let rec all_zero = function
-    | [] -> true
-    | 0 :: l -> all_zero l
-    | _ -> false in
-  let rec aux n = function
+  let all_zero = List.for_all ((=) 0) in
+  let rec aux argno = function
+    (* TODO: @FissoreD here we should raise an error if n > arity of the predicate? *)
     | [] -> error ("Wrong indexing for " ^ Symbols.show state predicate)
-    | 0 :: l -> aux (n+1) l
-    | 1 :: l when all_zero l -> MapOn n
+    | 0 :: l -> aux (argno+1) l
+    | 1 :: l when all_zero l -> MapOn argno
+    | path_depth :: l when all_zero l -> Trie { argno ; path_depth }
     | _ -> Hash l
   in
     aux 0 l
diff --git a/src/data.ml b/src/data.ml
index 5f10aa804..c72b8d6fe 100644
--- a/src/data.ml
+++ b/src/data.ml
@@ -53,6 +53,7 @@ module Constants : sig
   module Set : Set.S with type elt = constant
   val pp : Format.formatter -> t -> unit
   val show : t -> string
+  val compare : t -> t -> int
 end = struct
 
 module Self = struct
@@ -115,6 +116,25 @@ let uvar_isnt_a_blocker { uid_private } = uid_private > 0 [@@inline];;
 let uvar_set_blocker r   = r.uid_private <- -(uvar_id r) [@@inline];;
 let uvar_unset_blocker r = r.uid_private <-  (uvar_id r) [@@inline];;
 
+type arg_mode = Util.arg_mode = Input | Output [@@deriving show]
+
+type clause = {
+    depth : int;
+    args : term list;
+    hyps : term list;
+    vars : int;
+    mode : mode;        (* CACHE to avoid allocation in get_clauses *)
+    loc : Loc.t option; (* debug *)
+}
+and 
+mode = arg_mode list
+[@@deriving show]
+
+let to_mode = function true -> Input | false -> Output
+
+
+module DT = Discrimination_tree
+
 type stuck_goal = {
   mutable blockers : blockers;
   kind : unification_def stuck_goal_kind;
@@ -138,25 +158,23 @@ and second_lvl_idx =
 | TwoLevelIndex of {
     mode : mode;
     argno : int;
-    all_clauses : clause list;         (* when the query is flexible *)
-    flex_arg_clauses : clause list;       (* when the query is rigid but arg_id ha nothing *)
-    arg_idx : clause list Ptmap.t;   (* when the query is rigid (includes in each binding flex_arg_clauses) *)
+    all_clauses : clause list;        (* when the query is flexible *)
+    flex_arg_clauses : clause list;   (* when the query is rigid but arg_id ha nothing *)
+    arg_idx : clause list Ptmap.t;    (* when the query is rigid (includes in each binding flex_arg_clauses) *)
   }
 | BitHash of {
     mode : mode;
     args : int list;
-    time : int; (* time is used to recover the total order *)
+    time : int;                             (* time is used to recover the total order *)
     args_idx : (clause * int) list Ptmap.t; (* clause, insertion time *)
   }
-and clause = {
-    depth : int;
-    args : term list;
-    hyps : term list;
-    vars : int;
-    mode : mode; (* CACHE to avoid allocation in get_clauses *)
-    loc : Loc.t option; (* debug *)
+| IndexWithTrie of {
+    mode : mode;
+    argno : int;        (* position of argument on which the trie is built *)
+    path_depth : int;   (* depth bound at which the term is inspected *)
+    time : int;         (* time is used to recover the total order *)
+    args_idx : clause DT.t; 
 }
-and mode = bool list (* true=input, false=output *)
 [@@deriving show]
 
 type constraints = stuck_goal list
@@ -167,9 +185,19 @@ type suspended_goal = {
   goal : int * term
 }
 
+(** 
+  Used to index the parameters of a predicate P
+  - [MapOn N] -> N-th argument at depth 1 (head symbol only)
+  - [Hash L]  -> L is the list of depths given by the urer for the parameters of
+                 P. Indexing is done by hashing all the parameters with a non
+                 zero depth and comparing it with the hashing of the parameters
+                 of the query
+  - [IndexWithTrie N D] -> N-th argument at D depth
+*)
 type indexing =
   | MapOn of int
   | Hash of int list
+  | Trie of { argno : int; path_depth : int }
 [@@deriving show]
 
 let mkLam x = Lam x [@@inline]
diff --git a/src/discrimination_tree.ml b/src/discrimination_tree.ml
new file mode 100644
index 000000000..a884750f8
--- /dev/null
+++ b/src/discrimination_tree.ml
@@ -0,0 +1,227 @@
+(* elpi: embedded lambda prolog interpreter                                  *)
+(* license: GNU Lesser General Public License Version 2.1 or later           *)
+(* ------------------------------------------------------------------------- *)
+let arity_bits = 4
+let k_bits = 2
+
+(* 4 constructors encoded as: arg_value , arity, kno *)
+let kConstant = 0
+let kPrimitive = 1
+let kVariable = 2
+let kOther = 3
+
+let k_lshift = Sys.int_size - k_bits
+let ka_lshift = Sys.int_size - k_bits - arity_bits
+let k_mask = ((1 lsl k_bits) - 1) lsl k_lshift
+let arity_mask = (((1 lsl arity_bits) lsl k_bits) - 1) lsl ka_lshift
+let data_mask = (1 lsl ka_lshift) - 1
+let encode k c a = (k lsl k_lshift) lor (a lsl ka_lshift) lor (c land data_mask)
+let k_of n = (n land k_mask) lsr k_lshift
+
+let arity_of n =
+  let k = k_of n in
+  if k == kConstant then (n land arity_mask) lsr ka_lshift else 0
+
+let mkConstant ~safe c a =
+  let rc = encode kConstant c a in
+  if safe && (abs c > data_mask || a >= 1 lsl arity_bits) then
+    Elpi_util.Util.anomaly (Printf.sprintf "Indexing at depth > 1 is unsupported since constant %d/%d is too large or wide" c a);
+  rc
+let mkVariable = encode kVariable 0 0
+let mkOther = encode kOther 0 0
+let mkPrimitive c = encode kPrimitive (Elpi_util.Util.CData.hash c lsl k_bits) 0
+
+let () = assert(k_of (mkConstant ~safe:false ~-17 0) == kConstant)
+let () = assert(k_of mkVariable == kVariable)
+let () = assert(k_of mkOther == kOther)
+
+let isVariable x = k_of x == kVariable
+let isOther x = k_of x == kOther
+
+type cell = int
+let pp_cell fmt n =
+  let k = k_of n in
+  if k == kConstant then
+    let data = data_mask land n in
+    let arity = (arity_mask land n) lsr ka_lshift in
+    Format.fprintf fmt "Constant(%d,%d)" data arity
+  else if k == kVariable then Format.fprintf fmt "Variable"
+  else if k == kOther then Format.fprintf fmt "Other"
+  else if k == kPrimitive then Format.fprintf fmt "Primitive"
+  else Format.fprintf fmt "%o" k
+
+let show_cell n =
+  Format.asprintf "%a" pp_cell n
+
+module Trie = struct
+  (*
+   * Trie: maps over lists.
+   * Note: This code is a heavily modified version of the original code.
+   * Copyright (C) 2000 Jean-Christophe FILLIATRE
+   * 
+   * This software is free software; you can redistribute it and/or
+   * modify it under the terms of the GNU Library General Public
+   * License version 2, as published by the Free Software Foundation.
+   * 
+   * This software is distributed in the hope that it will be useful,
+   * but WITHOUT ANY WARRANTY; without even the implied warranty of
+   * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
+   * 
+   * See the GNU Library General Public License version 2 for more details
+   * (enclosed in the file LGPL).
+   *)
+
+  (*s A trie is a tree-like structure to implement dictionaries over
+      keys which have list-like structures. The idea is that each node
+      branches on an element of the list and stores the value associated
+      to the path from the root, if any. Therefore, a trie can be
+      defined as soon as a map over the elements of the list is
+      given. *)
+
+  (*s Then a trie is just a tree-like structure, where a possible
+      information is stored at the node (['a option]) and where the sons
+      are given by a map from type [key] to sub-tries, so of type
+      ['a t Ptmap.t]. The empty trie is just the empty map. *)
+
+  type key = int list
+
+  type 'a t =
+    | Node of { data : 'a list; other : 'a t option; map : 'a t Ptmap.t }
+
+  let empty = Node { data = []; other = None; map = Ptmap.empty }
+
+  (*s To find a mapping in a trie is easy: when all the elements of the
+      key have been read, we just inspect the optional info at the
+      current node; otherwise, we descend in the appropriate sub-trie
+      using [Ptmap.find]. *)
+
+  let rec find l t =
+    match (l, t) with
+    | [], Node { data = [] } -> raise Not_found
+    | [], Node { data } -> data
+    | x :: r, Node { map } -> find r (Ptmap.find x map)
+
+  let mem l t = try Fun.const true (find l t) with Not_found -> false
+
+  (*s Insertion is more subtle. When the final node is reached, we just
+      put the information ([Some v]). Otherwise, we have to insert the
+      binding in the appropriate sub-trie [t']. But it may not exists,
+      and in that case [t'] is bound to an empty trie. Then we get a new
+      sub-trie [t''] by a recursive insertion and we modify the
+      branching, so that it now points to [t''], with [Ptmap.add]. *)
+
+  let add l v t =
+    let rec ins = function
+      | [], Node ({ data } as t) -> Node { t with data = v :: data }
+      | x :: r, Node ({ other } as t) when isVariable x || isOther x ->
+          let t' = match other with None -> empty | Some x -> x in
+          let t'' = ins (r, t') in
+          Node { t with other = Some t'' }
+      | x :: r, Node ({ map } as t) ->
+          let t' = try Ptmap.find x map with Not_found -> empty in
+          let t'' = ins (r, t') in
+          Node { t with map = Ptmap.add x t'' map }
+    in
+    ins (l, t)
+
+  let rec pp (ppelem : Format.formatter -> 'a -> unit) (fmt : Format.formatter)
+      (Node { data; other; map } : 'a t) : unit =
+    Format.fprintf fmt "[values:{";
+    Elpi_util.Util.pplist ppelem "; " fmt data;
+    Format.fprintf fmt "} other:{";
+    (match other with None -> () | Some m -> pp ppelem fmt m);
+    Format.fprintf fmt "} key:{";
+    Ptmap.to_list map |> Elpi_util.Util.pplist (fun fmt (k,v) -> pp_cell fmt k; pp ppelem fmt v) "; " fmt;
+    Format.fprintf fmt "}]"
+
+  let show (fmt : Format.formatter -> 'a -> unit) (n : 'a t) : string =
+    let b = Buffer.create 22 in
+    Format.fprintf (Format.formatter_of_buffer b) "@[%a@]" (pp fmt) n;
+    Buffer.contents b
+end
+
+type path = cell list [@@deriving show]
+
+let compare x y = x - y
+
+let skip (path : path) : path =
+  let rec aux arity path =
+    if arity = 0 then path
+    else
+      match path with
+      | [] -> assert false
+      | m :: tl -> aux (arity - 1 + arity_of m) tl
+  in
+  match path with
+  | [] -> Elpi_util.Util.anomaly "Skipping empty path is not possible"
+  | hd :: tl -> aux (arity_of hd) tl
+
+type 'a t = ('a * int) Trie.t
+
+let pp pp_a fmt (t : 'a t) : unit = Trie.pp (fun fmt (a, _) -> pp_a fmt a) fmt t
+let show pp_a (t : 'a t) : string = Trie.show (fun fmt (a, _) -> pp_a fmt a) t
+let empty = Trie.empty
+let index tree ps info ~time = Trie.add ps (info, time) tree
+
+let in_index tree ps test =
+  try
+    let ps_set = Trie.find ps tree in
+    List.exists (fun (x, _) -> test x) ps_set
+  with Not_found -> false
+
+(* the equivalent of skip, but on the index, thus the list of trees
+    that are rooted just after the term represented by the tree root
+    are returned (we are skipping the root) *)
+let all_children other map =
+  let rec get n = function
+    | Trie.Node { other = None; map } as tree ->
+        if n = 0 then [ tree ]
+        else Ptmap.fold (fun k v res -> get (n - 1 + arity_of k) v @ res) map []
+    | Trie.Node { other = Some other; map } as tree ->
+        if n = 0 then [ tree; other ]
+        else
+          Ptmap.fold
+            (fun k v res -> get (n - 1 + arity_of k) v @ res)
+            map [ other ]
+  in
+
+  Ptmap.fold
+    (fun k v res -> get (arity_of k) v @ res)
+    map
+    (match other with Some x -> [ x ] | None -> [])
+
+(* NOTE: l1 and l2 are supposed to be sorted *)
+let rec merge (l1 : ('a * int) list) l2 =
+  match (l1, l2) with
+  | [], l | l, [] -> l
+  | ((_, tx) as x) :: xs, (_, ty) :: _ when tx > ty -> x :: merge xs l2
+  | _, y :: ys -> y :: merge l1 ys
+
+let get_all_children v mode = isOther v || (isVariable v && Elpi_util.Util.Output == mode)
+
+(* get_all_children returns if a key should be unified with all the values of
+   the current sub-tree. This key should be either K.to_unfy or K.variable.
+   In the latter case, the mode boolean to be true (we are in output mode). *)
+let rec retrieve_aux mode path = function
+  | [] -> []
+  | hd :: tl -> merge (retrieve mode path hd) (retrieve_aux mode path tl)
+
+and retrieve mode path tree =
+  match (tree, path) with
+  | Trie.Node { data }, [] -> data
+  | Trie.Node { other; map }, v :: path when get_all_children v mode ->
+      retrieve_aux mode path (all_children other map)
+  | Trie.Node { other = None; map }, node :: sub_path ->
+      if mode == Elpi_util.Util.Input && isVariable node then []
+      else
+        let subtree = try Ptmap.find node map with Not_found -> Trie.empty in
+        retrieve mode sub_path subtree
+  | Trie.Node { other = Some other; map }, (node :: sub_path as path) ->
+      merge
+        (if mode == Elpi_util.Util.Input && isVariable node then []
+        else
+          let subtree = try Ptmap.find node map with Not_found -> Trie.empty in
+          retrieve mode sub_path subtree)
+        (retrieve mode (skip path) other)
+
+let retrieve mode path index = retrieve mode path index |> List.map fst
diff --git a/src/dune b/src/dune
index dd67874c9..20a1b2aa0 100644
--- a/src/dune
+++ b/src/dune
@@ -1,7 +1,7 @@
 (library
   (public_name elpi)
   (preprocess (per_module
-    ((pps ppx_deriving.std) API data compiler)
+    ((pps ppx_deriving.std) API data compiler discrimination_tree)
     ((pps ppx_deriving.std elpi.trace.ppx -- --cookie "elpi_trace=\"true\"") runtime)
     ((pps ppx_deriving.std elpi.trace.ppx -- --cookie "elpi_trace=\"false\"") runtime_trace_off)
     ))
@@ -14,7 +14,7 @@
     ; ----- public API ---------------------------------
     elpi API builtin builtin_checker
     ; ----- internal stuff -----------------------------
-    compiler data ptmap runtime_trace_off runtime
+    compiler data ptmap discrimination_tree runtime_trace_off runtime
     builtin_stdlib builtin_map builtin_set
     legacy_parser_proxy)
   (private_modules
diff --git a/src/elpi-checker.elpi b/src/elpi-checker.elpi
index 0c6ef787c..43a11a297 100644
--- a/src/elpi-checker.elpi
+++ b/src/elpi-checker.elpi
@@ -175,27 +175,27 @@ refresh X X.
 safe-dest-app (app [X | A]) X A :- !.
 safe-dest-app X X [].
 
-collect-symbols-term N _ X X :- name N, !.
-collect-symbols-term (cdata _) _ X X :- !.
-collect-symbols-term (app []) _ X X :- !.
-collect-symbols-term (app [HD|L]) Known Acc Res :- !,
-  collect-symbols-term HD Known Acc Acc1,
-  collect-symbols-term (app L) Known Acc1 Res.
-collect-symbols-term (lam F) Known Acc Res :- !,
-  pi x\ collect-symbols-term (F x) Known Acc Res.
-collect-symbols-term (arg F) Known Acc Res :- !,
-  pi x\ collect-symbols-term (F x) Known Acc Res.
-collect-symbols-term (const S) Known Acc Res :- !,
-  if (std.string.set.mem S Known ; std.string.map.mem S Acc) (Res = Acc)
+collect-symbols-term N X X :- name N, !.
+collect-symbols-term (cdata _) X X :- !.
+collect-symbols-term (app []) X X :- !.
+collect-symbols-term (app [HD|L]) Acc Res :- !,
+  collect-symbols-term HD Acc Acc1,
+  collect-symbols-term (app L) Acc1 Res.
+collect-symbols-term (lam F) Acc Res :- !,
+  pi x\ collect-symbols-term (F x) Acc Res.
+collect-symbols-term (arg F) Acc Res :- !,
+  pi x\ collect-symbols-term (F x) Acc Res.
+collect-symbols-term (const S) Acc Res :- !,
+  if (std.string.map.mem S Acc) (Res = Acc)
      (checking Loc, std.string.map.add S Loc Acc Res).
 
-collect-symbols-clause (clause Loc _ C) Known Acc Res :-
-  checking Loc => collect-symbols-term C Known Acc Res.
+collect-symbols-clause (clause Loc _ C) Acc Res :-
+  checking Loc => collect-symbols-term C Acc Res.
 
-collect-symbols-program [ C | P ] Known Acc Res :-
-  collect-symbols-clause C Known Acc Acc1,
-  collect-symbols-program P Known Acc1 Res.
-collect-symbols-program [] _ X X.
+collect-symbols-program [ C | P ] Acc Res :-
+  collect-symbols-clause C Acc Acc1,
+  collect-symbols-program P Acc1 Res.
+collect-symbols-program [] X X.
 
 mode (under-env i i).
 
@@ -241,21 +241,27 @@ under-undecl-env [ pr X _ | XS ] P :-
   %print "Assume" X PT,
   (of (const X) Ty_ :- !) => under-undecl-env XS P.
 
-add-known (const N `: _) S S1 :- std.string.set.add N S S1.
+rm-known (const N `: _) S S1 :- std.string.map.remove N S S1.
 
 :if "TIME:CHECKER"
 timing S P :- !, std.time P Time, print S Time.
 timing _ P :- P.
 
+pred check-all-symbols i:std.string.map loc.
+:name "check-all-symbols:main"
+check-all-symbols _.
+
+:name "typecheck-program:main"
 typecheck-program P Q DeclaredTypes RC :-
   KnownTypes = [
     ((const "pi") `: forall x\ (arrow (arrow x prop) prop)),
     ((const "sigma") `: forall x\ (arrow (arrow x prop) prop)),
     ((const "discard") `: forall x\ x)|DeclaredTypes],
-  timing "known set" (std.fold KnownTypes {std.string.set.empty} add-known Known),
-  timing "collect prog" (collect-symbols-program P Known {std.string.map.empty} TMP),
-  collect-symbols-clause Q Known TMP TMP1,
-  std.string.map.bindings TMP1 Undeclared,
+  timing "collect prog" (collect-symbols-program P {std.string.map.empty} TMP),
+  collect-symbols-clause Q TMP AllSymbols,
+  check-all-symbols AllSymbols,
+  std.fold KnownTypes AllSymbols rm-known Unknown,
+  std.string.map.bindings Unknown Undeclared,
   forall_uto10 {std.rev Undeclared} 0 (warn-undeclared KnownTypes), !,
   timing "typecheck "
          (under-decl-env {std.rev KnownTypes}
@@ -310,6 +316,7 @@ check-non-linear [] (arg C) L :- pi x\
 check-non-linear _ C L :-
   count C L, report-linear L.
 
+:name "warn-linear:main"
 warn-linear [].
 warn-linear [ (clause Loc Names Clause) |CS] :-
   checking Loc =>  check-non-linear Names Clause [],
@@ -337,6 +344,7 @@ compile-type-abbreviations [(S `:= T)|TS] [Clause|Clauses] :-
   type->ppt-clause S [] T Clause,
   compile-type-abbreviations TS Clauses.
 
+:name "check:main"
 check P Q DeclaredTypes TypeAbbreviations :-
   compile-type-abbreviations TypeAbbreviations Abbrevs,
   Abbrevs => typecheck-program P Q DeclaredTypes RC, !,
diff --git a/src/runtime.ml b/src/runtime.ml
index 586e7a595..48849b68a 100644
--- a/src/runtime.ml
+++ b/src/runtime.ml
@@ -2286,18 +2286,20 @@ let ppclause f ~hd { depth; args = args; hyps = hyps } =
      (uppterm ~min_prec:(Elpi_parser.Parser_config.appl_precedence+1) depth [] ~argsdepth:0 empty_env) (C.mkAppL hd args)
      (pplist (uppterm ~min_prec:(Elpi_parser.Parser_config.appl_precedence+1) depth [] ~argsdepth:0 empty_env) ", ") hyps
 
+(** [tail_opt L] returns: [match L with [] -> [] | x :: xs -> xs] *)
 let tail_opt = function
   | [] -> []
   | _ :: xs -> xs
 
+(** [hd_opt L] returns false if L = [[]] otherwise L.(0)  *)
 let hd_opt = function
   | b :: _ -> b
-  | _ -> false
+  | _ -> Output
 
 type clause_arg_classification =
   | Variable
   | MustBeVariable
-  | Rigid of constant * bool (* matching *)
+  | Rigid of constant * arg_mode
 
 let rec classify_clause_arg ~depth matching t =
   match deref_head ~depth t with
@@ -2315,6 +2317,11 @@ let rec classify_clause_arg ~depth matching t =
      if hash > mustbevariablec then Rigid (hash,matching)
      else Rigid (hash+1,matching)
 
+(** 
+  [classify_clause_argno ~depth N mode L] where L is the arguments of the
+  clause. Returns the classification of the Nth element of L wrt to the Nth mode
+  for the TwoLevelIndex 
+*)
 let rec classify_clause_argno ~depth argno mode = function
   | [] -> Variable
   | x :: _ when argno == 0 -> classify_clause_arg ~depth (hd_opt mode) x
@@ -2331,7 +2338,11 @@ let dec_to_bin2 num =
 
 let hash_bits = Sys.int_size - 1 (* the sign *)
 
-let hash_arg_list goal hd ~depth args mode spec =
+(**
+  Hashing function for clause and queries depending on the boolean [is_goal].
+  This is done by hashing the parameters wrt to Sys.int_size - 1 (see [hash_bits])
+*)
+let hash_arg_list is_goal hd ~depth args mode spec =
   let nargs = List.(length (filter (fun x -> x > 0) spec)) in
   (* we partition equally, that may not be smart, but is simple ;-) *)
   let arg_size = hash_bits / nargs in
@@ -2351,10 +2362,10 @@ let hash_arg_list goal hd ~depth args mode spec =
     | x::xs, n::spec ->
          let h = aux_arg arg_size (hd_opt mode) n x in
          aux (off + arg_size) (acc lor (h lsl off)) xs (tail_opt mode) spec
-  and aux_arg size matching deep arg =
+  and aux_arg size mode deep arg =
     let h =
       match deref_head ~depth arg with
-      | App (k,a,_) when k == Global_symbols.asc -> aux_arg size matching deep a
+      | App (k,a,_) when k == Global_symbols.asc -> aux_arg size mode deep a
       | Const k when k == Global_symbols.uvarc ->
           hash size mustbevariablec
       | App(k,_,_) when k == Global_symbols.uvarc && deep = 1 ->
@@ -2363,19 +2374,19 @@ let hash_arg_list goal hd ~depth args mode spec =
       | App(k,_,_) when deep = 1 -> hash size k
       | App(k,x,xs) ->
           let size = size / (List.length xs + 2) in
-          let self = aux_arg size matching (deep-1) in
+          let self = aux_arg size mode (deep-1) in
           let shift = shift size in
           (hash size k) lor
           (shift 1 (self x)) lor
           List.(fold_left (lor) 0 (mapi (fun i x -> shift (i+2) (self x)) xs))
-      | (UVar _ | AppUVar _) when matching && goal -> hash size mustbevariablec
-      | (UVar _ | AppUVar _) when matching -> all_1 size
-      | (UVar _ | AppUVar _) -> if goal then all_0 size else all_1 size
+      | (UVar _ | AppUVar _) when mode == Input && is_goal -> hash size mustbevariablec
+      | (UVar _ | AppUVar _) when mode == Input -> all_1 size
+      | (UVar _ | AppUVar _) -> if is_goal then all_0 size else all_1 size
       | (Arg _ | AppArg _) -> all_1 size
       | Nil -> hash size Global_symbols.nilc
       | Cons (x,xs) ->
           let size = size / 2 in
-          let self = aux_arg size matching (deep-1) in
+          let self = aux_arg size mode (deep-1) in
           let shift = shift size in
           (hash size Global_symbols.consc) lor (shift 1 (self x))
       | CData s -> hash size (CData.hash s)
@@ -2383,14 +2394,14 @@ let hash_arg_list goal hd ~depth args mode spec =
       | Discard -> all_1 size
       | Builtin(k,xs) ->
           let size = size / (List.length xs + 1) in
-          let self = aux_arg size matching (deep-1) in
+          let self = aux_arg size mode (deep-1) in
           let shift = shift size in
           (hash size k) lor
           List.(fold_left (lor) 0 (mapi (fun i x -> shift (i+1) (self x)) xs))
     in
     [%spy "dev:index:subhash" ~rid (fun fmt () ->
        Fmt.fprintf fmt "%s: %d: %s: %a"
-         (if goal then "goal" else "clause")
+         (if is_goal then "goal" else "clause")
          size
          (dec_to_bin2 h)
          (uppterm depth [] ~argsdepth:0 empty_env) arg) ()];
@@ -2399,7 +2410,7 @@ let hash_arg_list goal hd ~depth args mode spec =
   let h = aux 0 0 args mode spec in
   [%spy "dev:index:hash" ~rid (fun fmt () ->
      Fmt.fprintf fmt "%s: %s: %a"
-       (if goal then "goal" else "clause")
+       (if is_goal then "goal" else "clause")
        (dec_to_bin2 h)
        (pplist ~boxed:true (uppterm depth [] ~argsdepth:0 empty_env) " ")
       (Const hd :: args)) ()];
@@ -2408,11 +2419,64 @@ let hash_arg_list goal hd ~depth args mode spec =
 let hash_clause_arg_list = hash_arg_list false
 let hash_goal_arg_list = hash_arg_list true
 
+(** 
+  [arg_to_trie_path_aux ~depth t_list path_depth]
+  Takes a list of terms and builds the path representing this list with
+  height limited to [depth].
+*)
+let rec arg_to_trie_path_aux ~safe ~depth t_list path_depth : Discrimination_tree.path = 
+  if path_depth = 0 then []
+  else 
+    match t_list with 
+    | [] -> []
+    | hd :: tl -> 
+        let hd_path = arg_to_trie_path ~safe ~depth hd path_depth in 
+        let tl_path = arg_to_trie_path_aux ~safe ~depth tl path_depth in 
+        hd_path @ tl_path
+(**
+  [arg_to_trie_path ~depth t path_depth]
+  Takes a [term] and returns it path representation with height bound by [path_depth]
+*)
+and arg_to_trie_path ~safe ~depth t path_depth : Discrimination_tree.path =
+  let open Discrimination_tree in
+  if path_depth = 0 then []
+  else 
+    let path_depth = path_depth - 1 in 
+    match deref_head ~depth t with 
+    | Const k when k == Global_symbols.uvarc -> [mkVariable]
+    | Const k when safe -> [mkConstant ~safe k 0]
+    | Const k -> [mkConstant ~safe k 0]
+    | CData d -> [mkPrimitive d]
+    | App (k,_,_) when k == Global_symbols.uvarc -> [mkVariable]
+    | App (k,a,_) when k == Global_symbols.asc -> arg_to_trie_path ~safe ~depth a (path_depth+1)
+    | Nil -> [mkConstant ~safe Global_symbols.nilc 0]
+    | Lam _ -> [mkOther] (* loose indexing to enable eta *)
+    | Arg _ | UVar _ | AppArg _ | AppUVar _ | Discard -> [mkVariable]
+    | Builtin (k,tl) ->
+      let path = arg_to_trie_path_aux ~safe ~depth tl path_depth in 
+      mkConstant ~safe k (if path_depth = 0 then 0 else List.length tl) :: path 
+    | App (k, x, xs) -> 
+      let arg_length = if path_depth = 0 then 0 else List.length xs + 1 in
+      let hd_path = arg_to_trie_path ~safe ~depth x path_depth in
+      let tl_path = arg_to_trie_path_aux ~safe ~depth xs path_depth in
+      mkConstant ~safe k arg_length :: hd_path @ tl_path
+    | Cons (x,xs) ->
+      let hd_path = arg_to_trie_path ~safe ~depth x path_depth in
+      let tl_path = arg_to_trie_path ~safe ~depth xs path_depth in
+      mkConstant ~safe Global_symbols.consc (if path_depth = 0 then 0 else 2) :: hd_path @ tl_path
+
+(** 
+  [arg_to_trie_path ~path_depth ~depth t]
+  Take a term and returns its path representation up to path_depth
+*)
+let arg_to_trie_path ~safe ~path_depth ~depth t = 
+  arg_to_trie_path ~safe ~depth t path_depth
+
 let add1clause ~depth m (predicate,clause) =
   match Ptmap.find predicate m with
   | TwoLevelIndex { all_clauses; argno; mode; flex_arg_clauses; arg_idx } ->
-      (* X matches both rigid and flexible terms *)
       begin match classify_clause_argno ~depth argno mode clause.args with
+      (* X: matches both rigid and flexible terms *)
       | Variable ->
         Ptmap.add predicate (TwoLevelIndex {
           argno; mode;
@@ -2421,7 +2485,7 @@ let add1clause ~depth m (predicate,clause) =
           arg_idx = Ptmap.map (fun l_rev -> clause :: l_rev) arg_idx;
         }) m
       | MustBeVariable ->
-      (* uvar matches only flexible terms (or itself at the meta level) *)
+      (* uvar: matches only flexible terms (or itself at the meta level) *)
         let l_rev =
           try Ptmap.find mustbevariablec arg_idx
           with Not_found -> flex_arg_clauses in
@@ -2431,13 +2495,13 @@ let add1clause ~depth m (predicate,clause) =
           flex_arg_clauses;
           arg_idx = Ptmap.add mustbevariablec (clause::l_rev) arg_idx;
         }) m
-      | Rigid (arg_hd,matching) ->
-      (* a rigid term matches flexible terms only in unification mode *)
+      | Rigid (arg_hd,arg_mode) ->
+      (* t: a rigid term matches flexible terms only in unification mode *)
         let l_rev =
           try Ptmap.find arg_hd arg_idx
           with Not_found -> flex_arg_clauses in
         let all_clauses =
-          if matching then all_clauses else clause :: all_clauses in
+          if arg_mode = Input then all_clauses else clause :: all_clauses in
         Ptmap.add predicate (TwoLevelIndex {
             argno; mode;
           all_clauses;
@@ -2455,6 +2519,14 @@ let add1clause ~depth m (predicate,clause) =
          time = time + 1;
          args_idx = Ptmap.add hash ((clause,time) :: clauses) args_idx
        }) m
+  | IndexWithTrie {mode; argno; args_idx; time; path_depth } ->
+      let path = arg_to_trie_path ~safe:true ~depth ~path_depth (match clause.args with [] -> Discard | l -> List.nth l argno) in 
+      let dt = DT.index args_idx path clause ~time in
+        Ptmap.add predicate (IndexWithTrie {
+          mode; argno; path_depth;
+          time = time+1;
+          args_idx = dt
+        }) m
   | exception Not_found ->
       match classify_clause_argno ~depth 0 [] clause.args with
       | Variable ->
@@ -2471,8 +2543,8 @@ let add1clause ~depth m (predicate,clause) =
         flex_arg_clauses = [];
         arg_idx = Ptmap.add mustbevariablec [clause] Ptmap.empty;
       }) m
-      | Rigid (arg_hd,matching) ->
-      let all_clauses = if matching then [] else [clause] in
+      | Rigid (arg_hd,arg_mode) ->
+      let all_clauses = if arg_mode == Input then [] else [clause] in
       Ptmap.add predicate (TwoLevelIndex {
         argno = 0;mode = [];
         all_clauses;
@@ -2486,22 +2558,28 @@ let add_clauses ~depth clauses p =
 
 let make_index ~depth ~indexing ~clauses_rev:p =
   let m = C.Map.fold (fun predicate (mode, indexing) m ->
-    match indexing with
-    | Hash args ->
-      Ptmap.add predicate (BitHash {
-        args;
-        mode;
-        time = min_int;
-        args_idx = Ptmap.empty;
-      }) m
-    | MapOn argno ->
-      Ptmap.add predicate (TwoLevelIndex {
-        argno;
-        mode;
-        all_clauses = [];
-        flex_arg_clauses = [];
-        arg_idx = Ptmap.empty;
-      }) m) indexing Ptmap.empty in
+    Ptmap.add predicate 
+    begin
+      match indexing with
+      | Hash args -> BitHash {
+          args;
+          mode;
+          time = min_int;
+          args_idx = Ptmap.empty;
+        }
+      | MapOn argno -> TwoLevelIndex {
+          argno;
+          mode;
+          all_clauses = [];
+          flex_arg_clauses = [];
+          arg_idx = Ptmap.empty;
+        }
+      | Trie { argno; path_depth } -> IndexWithTrie {
+          argno; path_depth; mode; 
+          args_idx = DT.empty;
+          time = min_int;
+        }
+    end m) indexing Ptmap.empty in
   { index = add_clauses ~depth p m; src = [] }
 
 let add_clauses ~depth clauses clauses_src { index; src } =
@@ -2539,12 +2617,27 @@ let classify_goal_argno ~depth argno = function
       classify_goal_arg ~depth x
   | _ -> assert false
 
-let hash_goal_args ~depth mode args goal =
-  match goal with
+let hash_goal_args ~depth mode args goal = match goal with
   | Const _ -> 0
   | App(k,x,xs) -> hash_goal_arg_list k ~depth (x::xs) mode args
   | _ -> assert false
 
+let rec nth_not_found l n = match l with 
+  | [] -> raise Not_found
+  | x :: _ when n = 0 -> x 
+  | _ :: l -> nth_not_found l (n-1)
+
+let rec nth_not_bool_default l n = match l with 
+  | [] -> Output
+  | x :: _ when n = 0 -> x 
+  | _ :: l -> nth_not_bool_default l (n - 1)
+
+let trie_goal_args goal argno : term = match goal with
+  | Const a when argno = 0 -> goal
+  | App(k, x, _) when argno = 0 -> x
+  | App (_, _, xs) -> nth_not_found xs (argno - 1)
+  | _ -> assert false
+
 let get_clauses ~depth predicate goal { index = m } =
  let rc =
    try
@@ -2560,9 +2653,21 @@ let get_clauses ~depth predicate goal { index = m } =
        let hash = hash_goal_args ~depth mode args goal in
        let cl = List.flatten (Ptmap.find_unifiables hash args_idx) in
        List.(map fst (sort (fun (_,cl1) (_,cl2) -> cl2 - cl1) cl))
+     | IndexWithTrie {argno; path_depth; mode; args_idx} -> 
+        let mode_arg = nth_not_bool_default mode argno in 
+        let path = arg_to_trie_path ~safe:false ~depth ~path_depth (trie_goal_args goal argno) in
+        [%spy "dev:disc-tree:path" ~rid 
+          Discrimination_tree.pp_path path
+          pp_int path_depth
+          (*Discrimination_tree.(pp pp_clause) args_idx*)];
+        let candidates = DT.retrieve mode_arg path args_idx in 
+          [%spy "dev:disc-tree:candidates" ~rid 
+            pp_int (List.length candidates)];
+        candidates
    with Not_found -> []
  in
  [%log "get_clauses" ~rid (C.show predicate) (List.length rc)];
+ [%spy "dev:get_clauses" ~rid C.pp predicate pp_int (List.length rc)];
  rc
 
 (* flatten_snd = List.flatten o (List.map ~~snd~~) *)
@@ -2777,6 +2882,7 @@ let clausify ~loc { index } ~depth t =
     match Ptmap.find x index with
     | TwoLevelIndex { mode } -> mode
     | BitHash { mode } -> mode
+    | IndexWithTrie { mode } -> mode
     | exception Not_found -> [] in
   let l = split_conj ~depth t in
   let clauses, program, lcs =
@@ -3633,7 +3739,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
           | x :: xs -> arg != C.dummy &&
              match c_mode with
              | [] -> unif ~argsdepth:depth ~matching:false (gid[@trace]) depth env c_depth arg x && for_all23 ~argsdepth:depth (unif (gid[@trace])) depth env c_depth args_of_g xs
-             | matching :: ms -> unif ~argsdepth:depth ~matching (gid[@trace]) depth env c_depth arg x && for_all3b3 ~argsdepth:depth (unif (gid[@trace])) depth env c_depth args_of_g xs ms false
+             | arg_mode :: ms -> unif ~argsdepth:depth ~matching:(arg_mode == Input) (gid[@trace]) depth env c_depth arg x && for_all3b3 ~argsdepth:depth (unif (gid[@trace])) depth env c_depth args_of_g xs ms false
         with
         | false ->
             T.undo old_trail (); [%tcall backchain depth p (k, arg, args_of_g, gs) (gid[@trace]) next alts cutto_alts cs]
diff --git a/src/utils/util.ml b/src/utils/util.ml
index 3a7d86106..f40e4074e 100644
--- a/src/utils/util.ml
+++ b/src/utils/util.ml
@@ -83,6 +83,13 @@ module Int = struct
   let compare x y = x - y
 end
 
+module Bool = struct
+  type t = bool
+  let pp fmt x = Format.pp_print_bool fmt x
+  let show x = Format.asprintf "@[%a@]" pp x
+  let compare = Bool.compare
+end
+
 module String = struct
   include String
   let pp fmt s = Format.fprintf fmt "%s" s
@@ -211,13 +218,16 @@ let rec for_all3b p l1 l2 bl b =
   | (a1::l1, a2::l2, b3::bl) -> p a1 a2 b3 && for_all3b p l1 l2 bl b
   | (_, _, _) -> false
 ;;
+
+type arg_mode = Input | Output
+
 let rec for_all3b3 ~argsdepth (p : argsdepth:int -> matching:bool -> 'a) x1 x2 x3 l1 l2 bl b =
   match (l1, l2, bl) with
   | ([], [], _) -> true
   | ([a1], [a2], []) -> p ~argsdepth x1 x2 x3 a1 a2 ~matching:b
-  | ([a1], [a2], b3::_) -> p ~argsdepth x1 x2 x3 a1 a2 ~matching:b3
+  | ([a1], [a2], b3::_) -> p ~argsdepth x1 x2 x3 a1 a2 ~matching:(b3 == Input)
   | (a1::l1, a2::l2, []) -> p ~argsdepth x1 x2 x3 a1 a2 ~matching:b && for_all3b3 ~argsdepth p x1 x2 x3 l1 l2 bl b
-  | (a1::l1, a2::l2, b3::bl) -> p ~argsdepth x1 x2 x3 a1 a2 ~matching:b3 && for_all3b3 ~argsdepth p x1 x2 x3 l1 l2 bl b
+  | (a1::l1, a2::l2, b3::bl) -> p ~argsdepth x1 x2 x3 a1 a2 ~matching:(b3 == Input) && for_all3b3 ~argsdepth p x1 x2 x3 l1 l2 bl b
   | (_, _, _) -> false
 ;;
 
diff --git a/src/utils/util.mli b/src/utils/util.mli
index 1a2ebed48..bf5c5ec5f 100644
--- a/src/utils/util.mli
+++ b/src/utils/util.mli
@@ -60,6 +60,12 @@ module Int : sig
   include Show with type t := int
 end
 
+module Bool : sig
+  type t = bool
+  val compare : t -> t -> int
+  include Show with type t := t
+end
+
 module String : sig
   include module type of String
   include Show with type t := string
@@ -106,7 +112,8 @@ val uniqq: 'a list -> 'a list
 val for_all2 : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
 val for_all23 :  argsdepth:int -> (argsdepth:int -> matching:bool -> 'x -> 'y -> 'z -> 'a -> 'a -> bool) -> 'x -> 'y -> 'z -> 'a list -> 'a list -> bool
 val for_all3b : ('a -> 'a -> bool -> bool) -> 'a list -> 'a list -> bool list -> bool -> bool
-val for_all3b3 : argsdepth:int -> (argsdepth:int -> matching:bool -> 'x -> 'y -> 'z -> 'a -> 'a -> bool) -> 'x -> 'y -> 'z -> 'a list -> 'a list -> bool list -> bool -> bool
+type arg_mode = Input | Output
+val for_all3b3 : argsdepth:int -> (argsdepth:int -> matching:bool -> 'x -> 'y -> 'z -> 'a -> 'a -> bool) -> 'x -> 'y -> 'z -> 'a list -> 'a list -> arg_mode list -> bool -> bool
 (*uses physical equality and calls anomaly if the element is not in the list*)
 val remove_from_list : 'a -> 'a list -> 'a list
 (* returns Some t where f x = Some t for the first x in the list s.t.
diff --git a/tests/sources/dt.elpi b/tests/sources/dt.elpi
new file mode 100644
index 000000000..47d775b00
--- /dev/null
+++ b/tests/sources/dt.elpi
@@ -0,0 +1,25 @@
+:index (12) % DT is on
+pred f i:list int. 
+
+pred mk-index i:int, i:(list int -> prop), o:list prop.
+mk-index 0 _ [].
+mk-index N P [C|CL] :- N > 0, N1 is N - 1, mk-clause P 10 [N] C, mk-index N1 P CL.
+
+pred mk-clause i:(list int -> prop), i:int, i:list int, o:prop.
+mk-clause P 0 X (P X).
+mk-clause P N ACC C :- N > 0, N1 is N - 1,
+  mk-clause P N1 [N|ACC] C.
+
+pred repeat i:int, i:prop.
+repeat 0 _.
+repeat N P :- N > 0, N1 is N - 1, P, !, repeat N1 P.
+
+main :-
+  mk-index 100 f CL1,
+  !,
+  CL1 => std.do! [
+    std.time (repeat 300000 (f [1,2,3,4,5,6,7,8,9,10,1])) TFast,
+    std.time (repeat 300000 (f [1,2,3,4,5,6,7,8,9,10,100])) TSlow,
+    print "DT=" TFast,
+    print "PT=" TSlow,
+  ].
diff --git a/tests/sources/dt_off.elpi b/tests/sources/dt_off.elpi
new file mode 100644
index 000000000..6492b733c
--- /dev/null
+++ b/tests/sources/dt_off.elpi
@@ -0,0 +1,25 @@
+:index (1) % DT is off
+pred f i:list int. 
+
+pred mk-index i:int, i:(list int -> prop), o:list prop.
+mk-index 0 _ [].
+mk-index N P [C|CL] :- N > 0, N1 is N - 1, mk-clause P 10 [N] C, mk-index N1 P CL.
+
+pred mk-clause i:(list int -> prop), i:int, i:list int, o:prop.
+mk-clause P 0 X (P X).
+mk-clause P N ACC C :- N > 0, N1 is N - 1,
+  mk-clause P N1 [N|ACC] C.
+
+pred repeat i:int, i:prop.
+repeat 0 _.
+repeat N P :- N > 0, N1 is N - 1, P, !, repeat N1 P.
+
+main :-
+  mk-index 100 f CL1,
+  !,
+  CL1 => std.do! [
+    std.time (repeat 300000 (f [1,2,3,4,5,6,7,8,9,10,1])) TFast,
+    std.time (repeat 300000 (f [1,2,3,4,5,6,7,8,9,10,100])) TSlow,
+    print "DT=" TFast,
+    print "PT=" TSlow,
+  ].
diff --git a/tests/sources/dt_var.elpi b/tests/sources/dt_var.elpi
new file mode 100644
index 000000000..6e8a9bf44
--- /dev/null
+++ b/tests/sources/dt_var.elpi
@@ -0,0 +1,8 @@
+:index(20)
+pred f i:int.
+f uvar :- print "uvar".
+f X :- var X, print "X".
+f 1 :- halt "bug".
+
+main :-
+  (f X, fail) ; true.
\ No newline at end of file
diff --git a/tests/sources/dt_var2.elpi b/tests/sources/dt_var2.elpi
new file mode 100644
index 000000000..9c93bc96d
--- /dev/null
+++ b/tests/sources/dt_var2.elpi
@@ -0,0 +1,8 @@
+:index(20)
+pred f o:int.
+f uvar :- print "uvar".
+f X :- var X, print "X".
+f 1 :- print "Y".
+
+main :-
+  (f X, fail) ; true.
\ No newline at end of file
diff --git a/tests/suite/correctness_FO.ml b/tests/suite/correctness_FO.ml
index 7bf18a8cc..e3c08ad4d 100644
--- a/tests/suite/correctness_FO.ml
+++ b/tests/suite/correctness_FO.ml
@@ -109,3 +109,20 @@ let () = declare "conj2_legacy"
   ~description:"parsing and evaluation of & (binary conj)"
   ~legacy_parser:true
   ()
+
+let () = declare "dt_var"
+  ~source_elpi:"dt_var.elpi"
+  ~description:"discrimination_tree indexing flex"
+  ~typecheck:false
+  ~trace:(On["tty";"stdout";"-trace-at";"1";"9999";"-trace-only";"dev:disc-tree:candidates"])
+  ~expectation:(SuccessOutput (Str.regexp "dev:disc-tree:candidates = 2"))
+  ()
+
+let () = declare "dt_var2"
+  ~source_elpi:"dt_var2.elpi"
+  ~description:"discrimination_tree indexing flex"
+  ~typecheck:false
+  ~trace:(On["tty";"stdout";"-trace-at";"1";"9999";"-trace-only";"dev:disc-tree:candidates"])
+  ~expectation:(SuccessOutput (Str.regexp "dev:disc-tree:candidates = 3"))
+  ()
+
diff --git a/tests/suite/performance_FO.ml b/tests/suite/performance_FO.ml
index f75686c63..1963cf106 100644
--- a/tests/suite/performance_FO.ml
+++ b/tests/suite/performance_FO.ml
@@ -79,3 +79,14 @@ let () = declare "set"
   ~source_elpi:"set.elpi"
   ~description:"stdlib set"
   ()
+
+let () = declare "dt"
+  ~source_elpi:"dt.elpi"
+  ~description:"discrimination_tree indexing"
+  ()
+
+let () = declare "dt_off"
+  ~source_elpi:"dt_off.elpi"
+  ~description:"(without) discrimination_tree indexing"
+  ()
+