diff --git a/bench/bench b/bench/bench
index 98b6ebfc3bb4a2bb336cee14a18391fe78588e77..a1efc5c8ec36dd5c2ea07e468b5810e225f31b96 100755
--- a/bench/bench
+++ b/bench/bench
@@ -107,12 +107,12 @@ replay () {
     pgm="bin/why3replay$suffix"
     for f in $1/*/; do
         printf "  $f... "
-        if $pgm $f > /dev/null; then
+        if $pgm $2 $f > /dev/null 2> /dev/null; then
             echo "ok"
         else
             echo "replay test failed!"
-            echo $pgm $f
-            $pgm $f
+            echo $pgm $2 $f
+            $pgm $2 $f
             exit 1
         fi
     done
@@ -236,6 +236,22 @@ echo ""
 
 echo "=== Checking replay (no prover) ==="
 replay bench/replay
+replay examples/bts --merging-only
+replay examples/tests --merging-only
+replay examples/tests-provers --merging-only
+replay examples/check-builtin --merging-only
+replay examples/logic --merging-only
+replay examples --merging-only
+replay examples/foveoos11-cm --merging-only
+replay examples/WP_revisited --merging-only
+replay examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps --merging-only"
+replay examples/bitvectors "-L examples/bitvectors --merging-only"
+replay examples/avl "-L examples/avl --merging-only"
+#replay examples/to_port/verifythis_2016_matrix_multiplication "-L examples/to_port/verifythis_2016_matrix_multiplication --merging-only"
+replay examples/double_wp "-L examples/double_wp --merging-only"
+replay examples/ring_decision "-L examples/ring_decision --merging-only"
+#replay examples/in_progress --merging-only
+#replay examples/in_progress/multiprecision "-L examples/in_progress/multiprecision --merging-only"
 echo ""
 
 echo "=== Checking valid goals ==="
diff --git a/src/tools/why3replay.ml b/src/tools/why3replay.ml
index be3cdeaf2ca2542b078c2439427ab3ce24bb34e7..28f6e8cdd559857557d4ce656afd29af5cfa98f0 100644
--- a/src/tools/why3replay.ml
+++ b/src/tools/why3replay.ml
@@ -36,6 +36,7 @@ let opt_stats = ref true
 let opt_force = ref false
 let opt_obsolete_only = ref false
 let opt_use_steps = ref false
+let opt_merging_only = ref false
 (*
 let opt_bench = ref false
 *)
@@ -78,7 +79,10 @@ let option_list = [
    " replay using recorded number of proof steps (when possible)");
   ("--obsolete-only",
    Arg.Set opt_obsolete_only,
-   " replay only if session is obsolete") ;
+   " replay only if session is obsolete");
+  ("--merging-only",
+   Arg.Set opt_merging_only,
+   " check merging of session");
   ("-P",
    Arg.String (fun s ->
      opt_provers := Whyconf.parse_filter_prover s :: !opt_provers),
@@ -376,6 +380,8 @@ let () =
  *)
     if found_obs then eprintf "[Warning] session is obsolete@.";
     if found_detached then eprintf "[Warning] found detached goals or theories or transformations@.";
+    if !opt_merging_only then
+      exit (if found_detached then 1 else 0);
     add_to_check_no_smoke found_detached found_obs cont;
     Debug.dprintf debug "[Replay] starting scheduler@.";
     Unix_scheduler.Unix_scheduler.main_loop ~prompt:"" (fun _ -> ());