diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml
index d09cc1d02f..71a937fdd6 100644
--- a/src/bin/common/parse_command.ml
+++ b/src/bin/common/parse_command.ml
@@ -884,25 +884,19 @@ let parse_output_opt =
 
 
     let frontend =
-      let doc = "Select the parsing and typing frontend." in
+      let doc =
+        "Select the parsing and typing frontend. Support for non-default \
+         frontends is deprecated and will be removed in the next release."
+      in
       let docv = "FTD" in
-      Arg.(value & opt (some string) None &
-           info ["frontend"] ~docv ~docs:s_execution ~doc)
-    in
-
-    (* Use the dolmen frontend by default with --produce-models *)
-    let mk_frontend frontend produce_models =
-      match frontend with
-      | None ->
-        if produce_models then
-          "dolmen"
-        else
-          get_frontend ()
-      | Some frontend -> frontend
+      let deprecated =
+        "this option is deprecated and will be ignored in the \
+         next version"
+      in
+      Arg.(value & opt string "dolmen" &
+           info ["frontend"] ~docv ~docs:s_execution ~doc ~deprecated)
     in
 
-    let frontend = Term.(const mk_frontend $ frontend $ produce_models) in
-
     let dump_models =
       let doc =
         "Display a model each time the result is unknown (implies \
diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml
index 8895a8809e..f238ae6413 100644
--- a/src/lib/util/options.ml
+++ b/src/lib/util/options.ml
@@ -259,7 +259,7 @@ let output_with_colors = ref false
 let output_with_headers = ref true
 let output_with_formatting = ref true
 let output_with_forced_flush = ref true
-let frontend = ref "legacy"
+let frontend = ref "dolmen"
 let input_format = ref Native
 let infer_input_format = ref true
 let parse_only = ref false
diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t
index 187dc2748c..ff932c9595 100644
--- a/tests/cram.t/run.t
+++ b/tests/cram.t/run.t
@@ -6,7 +6,7 @@ Now we will have some tests for the models. Note that it is okay if the format
 changes slightly, you should be concerned with ensuring the semantic is
 appropriate here.
 
-  $ alt-ergo --frontend dolmen --produce-models model555.smt2 --no-forced-flush-in-output 2>/dev/null
+  $ alt-ergo --produce-models model555.smt2 --no-forced-flush-in-output 2>/dev/null
   
   unknown
   (
@@ -17,14 +17,7 @@ appropriate here.
 
 Now we will test some semantic triggers.
 
-  $ alt-ergo --frontend legacy -o smtlib2 semantic_triggers.ae 2>/dev/null
-  
-  unknown
-  
-  unsat
-  
-  unsat
-  $ alt-ergo --frontend dolmen -o smtlib2 semantic_triggers.ae 2>/dev/null
+  $ alt-ergo -o smtlib2 semantic_triggers.ae 2>/dev/null
   
   unknown
   
@@ -34,7 +27,7 @@ Now we will test some semantic triggers.
 
 And some SMT2 action.
 
-  $ alt-ergo --frontend dolmen -o smtlib2 --prelude prelude.ae postlude.smt2 2>/dev/null
+  $ alt-ergo -o smtlib2 --prelude prelude.ae postlude.smt2 2>/dev/null
   
   unknown
   
@@ -50,37 +43,37 @@ combinations of produce-models et al.
 First, if model generation is not enabled, we should error out when a
 `(get-model)` statement is issued:
 
-  $ echo '(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2
+  $ echo '(get-model)' | alt-ergo -i smtlib2 -o smtlib2
   (error "Model generation disabled (try --produce-models)")
 
 This should be the case Tableaux solver as well:
 
-  $ echo '(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2
+  $ echo '(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2
   (error "Model generation disabled (try --produce-models)")
 
 The messages above mention `--produce-models`, but we can also use
 `set-option`.
 
-  $ echo '(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2
+  $ echo '(get-model)' | alt-ergo --produce-models -i smtlib2 -o smtlib2
   (error "No model produced.")
 
-  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2
+  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2
   (error "No model produced.")
 
 And now some cases where it should work (using either `--produce-models` or `set-option`):
 
-  $ echo '(check-sat)(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2 2>/dev/null
+  $ echo '(check-sat)(get-model)' | alt-ergo --produce-models -i smtlib2 -o smtlib2 2>/dev/null
   
   unknown
   (
   )
 
-  $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2 2>/dev/null
+  $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo -i smtlib2 -o smtlib2 2>/dev/null
   
   unknown
   (
   )
-  $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2 2>/dev/null
+  $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2 2>/dev/null
   
   unknown
   (