Document the change

CHANGES.md

@@ -1,5 +1,7 @@
 ## unreleased
+
 ### Deprecated
+* make Dolmen the default and deprecate the legacy frontend (PR #857)
 * printing underscore instead of fresh value in model (PR #805)
 
 ### Build

docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md

@@ -141,8 +141,8 @@ logic real_of_int : int -> real
 
 `real_of_int` converts an integer into its representation as a real number.
 
-*Note*: When using the `dolmen` frontend, `real_of_int` is also available in
-the smtlib2 format as the `to_real` function from the `Reals_Ints` theory.
+*Note*: `real_of_int` is also available in the smtlib2 format as the `to_real`
+function from the `Reals_Ints` theory.
 
 ```alt-ergo
 logic int_floor : real -> int
@@ -156,9 +156,9 @@ greater than a real, respectively.
 
 `real_is_int` is true for reals that are exact integers, and false otherwise.
 
-*Note*: When using the Dolmen frontend, `int_floor` and `real_is_int` are
-also available in the smtlib2 format as the `to_int` and `is_int` functions
-from the `Reals_Ints` theory respectively.
+*Note*: `int_floor` and `real_is_int` are also available in the smtlib2 format
+as the `to_int` and `is_int` functions from the `Reals_Ints` theory
+respectively.
 
 ### Square root
 

docs/sphinx_docs/Input_file_formats/SMT-LIB2/index.md

@@ -6,16 +6,13 @@ standard](http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.p
 language from the SMT community.
 
 *Note*: As of version 2.5.0, enhanced support for the SMT-LIB language is
-provided by the new [Dolmen](http://gbury.github.io/dolmen/) frontend. To use
-it, pass the option `--frontend dolmen` to Alt-Ergo. This will become the
-default in a future release.
+provided by the new [Dolmen](http://gbury.github.io/dolmen/) frontend.
 
 ## Bit-vectors
 
 Since version 2.5.0, Alt-Ergo has partial support for the `FixedSizeBitVectors`
-theory and the `QF_BV` and `BV` logics when used with the Dolmen frontend. All
-the symbols from these logics are available, although reasoning using them is
-limited and incomplete for now.
+theory and the `QF_BV` and `BV` logics. All the symbols from these logics are
+available, although reasoning using them is limited and incomplete for now.
 
 The non-standard symbols `bv2nat` and `(_ int2bv n)` (where `n >
 0` is a natural number representing the target bit-vector size) for conversion

docs/sphinx_docs/Usage/index.md

@@ -27,12 +27,19 @@ See the [Input section] for more information about the format of the input files
 
 The `--frontend` option lets you select the frontend used to parse and type the input file. Since version 2.5.0,
 Alt-Ergo integrates two frontends:
-- The `legacy` frontend is the historical frontend of Alt-Ergo supporting the native language
-  and (partially) supporting the SMT-LIB language. The legacy frontend is currently the default.
-- The `dolmen` frontend is a new frontend using the [Dolmen library](https://github.com/Gbury/dolmen).
-  The native and SMT-LIB languages are both supported by this frontend.
-  You can select it with the `--frontend dolmen` option, which is planned to become the
-  default in a future release.
+- The `dolmen` frontend is the default frontend, powered by the
+  [Dolmen](https://github.com/Gbury/dolmen) library.  The native and SMT-LIB
+  languages are both supported by this frontend.
+- The `legacy` frontend is the historical frontend of Alt-Ergo supporting the
+  native language. You can select it with the `--frontend legacy` option. The
+  legacy frontend is deprecated, and will be removed in a future release.
+
+```{admonition} Note
+
+The `legacy` frontend has limited support for the SMT-LIB language, but many
+SMT-LIB features will not work with the `legacy` frontend. Use the (default)
+`dolmen` frontend for SMT-LIB inputs.
+```
 
 ### Generating models
 Alt-Ergo can generates best-effort models in the case it cannot conclude the unsatisfiability of
@@ -51,8 +58,7 @@ Model generation is disabled by default. There are two recommended ways to enabl
   on demand using the statement `(get-model)`.
 
   Alternatively, you can enable model generation using the statement
-  `(set-option :produce-models true)`. This currently requires using the option
-  `--frontend dolmen`.
+  `(set-option :produce-models true)`.
 
 #### Examples
 
@@ -142,7 +148,7 @@ Model generation is disabled by default. There are two recommended ways to enabl
    (get-model)
 
   ```
-  and the command `alt-ergo --frontend dolmen INPUT.smt2` produces
+  and the command `alt-ergo INPUT.smt2` produces
   the output model
   ```
   unknown
@@ -153,11 +159,6 @@ Model generation is disabled by default. There are two recommended ways to enabl
   )
   ```
 
-  ```{admonition} Note
-  You need to select the Dolmen frontend. The options `--dump-models` and
-  `--produce-models` select the right frontend for you.
-  ```
-
   - As a more didactic example, let us imagine while checking the loop invariant
   in the pseudocode below:
   ```
@@ -177,7 +178,7 @@ Model generation is disabled by default. There are two recommended ways to enabl
   ```
   Execute the command
   ```sh
-  alt-ergo --frontend dolmen --produce-models INPUT.smt2
+  alt-ergo --produce-models INPUT.smt2
   ```
   We got the output
   ```