diff --git a/colibri2/theories/quantifier/trigger.ml b/colibri2/theories/quantifier/trigger.ml
index 84094540e8b15ad91a4303b41fa725368161c093..62eb03ac229f5ae8b2c9fbf7dd2b4753bd653594 100644
--- a/colibri2/theories/quantifier/trigger.ml
+++ b/colibri2/theories/quantifier/trigger.ml
@@ -336,13 +336,21 @@ let debug_new_instantiation =
   Debug.register_info_flag ~desc:"Handling of quantifiers"
     "quantifiers.instantiations"
 
+let mode_option =
+  Options.register ~pp:Fmt.bool "Quant.old"
+    Cmdliner.Arg.(
+      value & flag & info [ "quant-old" ] ~doc:"Use quant old heuristic")
+
 let instantiate_aux d tri subst =
   SubstTrie.set tri.substs subst Instantiated;
   let form = Ground.ClosedQuantifier.sem tri.form in
   Debug.incr nb_instantiation;
-  let subst = Ground.Subst.distinct_union subst form.subst in
-  let n = Ground.convert ~subst d form.body in
-  (* let n = Subst.convert ~subst_old:form.subst ~subst_new:subst d form.body in *)
+  let n =
+    if Options.get d mode_option then
+      let subst = Ground.Subst.distinct_union subst form.subst in
+      Ground.convert ~subst d form.body
+    else Subst.convert ~subst_old:form.subst ~subst_new:subst d None form.body
+  in
   if
     Colibri2_stdlib.Debug.test_flag Colibri2_stdlib.Debug.stats
     && not (Egraph.is_equal d n (Ground.ClosedQuantifier.node tri.form))
@@ -391,11 +399,6 @@ end
 
 let () = Events.register (module Delayed_instantiation)
 
-let mode_option =
-  Options.register ~pp:Fmt.bool "Quant.old"
-    Cmdliner.Arg.(
-      value & flag & info [ "quant-old" ] ~doc:"Use quant old heuristic")
-
 let no_eager_instantiation =
   Options.register ~pp:Fmt.bool "Quant.no_eager_instantiation"
     Cmdliner.Arg.(