diff --git a/src/driver/autodetection.ml b/src/driver/autodetection.ml
index 319b0f7eec0a2d65a11a63d35e2ec28b21ae17f8..7aaac9978e88962a71b8b4bd367016b04de1c994 100644
--- a/src/driver/autodetection.ml
+++ b/src/driver/autodetection.ml
@@ -362,7 +362,7 @@ let generate_auto_strategies env =
      if b then print_info "  Prover %a will be used in Auto level >= %d@."
                        Whyconf.print_prover p lev) env.prover_auto_levels;
   (* Split VCs *)
-  let code = "t split_vc exit" in
+  let code = "t split_vc next\nnext: \nt trivial_true\n exit" in
   let split = {
       strategy_name = "Split_VC";
       strategy_desc = "Split@ the@ VC@ into@ subgoals";
diff --git a/src/transform/simplify_formula.ml b/src/transform/simplify_formula.ml
index eaa20dac622a948e6ecd956a68d4df88bc0a2260..2886e0e3a9d4681312839ad10f2e566e805ce372 100644
--- a/src/transform/simplify_formula.ml
+++ b/src/transform/simplify_formula.ml
@@ -243,3 +243,33 @@ let fmla_cond_subst filter f =
         fmla_unflatten conj f subf
     | _ -> t_map aux f in
   aux f
+
+let rec is_trivial fml =
+   (* Check wether the formula is trivial.  *)
+   match fml.t_node with
+   | Ttrue -> true
+   | Tquant (_,tq) ->
+         let _,_,t = t_open_quant tq in
+         is_trivial t
+   | Tlet (_,tb) ->
+         let _, t = t_open_bound tb in
+         is_trivial t
+   | Tbinop (Timplies,_,t2) ->
+         is_trivial t2
+   | Tcase (_,tbl) ->
+         List.for_all (fun b ->
+            let _, t = t_open_branch b in
+            is_trivial t) tbl
+   | _ -> false
+
+let is_trivial_trans =
+  Trans.goal_l (fun pr t ->
+      if is_trivial t then
+        [] (* Goal is proved *)
+      else
+        [[Decl.create_prop_decl Pgoal pr t]])
+
+
+let () = Trans.register_transform_l ~desc:"Prove goals whose positive part is just [true]"
+    "trivial_true"
+    is_trivial_trans