diff --git a/doc/extensions.md b/doc/extensions.md
new file mode 100644
index 000000000..e873edb38
--- /dev/null
+++ b/doc/extensions.md
@@ -0,0 +1,25 @@
+# User-defined builtins
+
+Dolmen supports extensions through the form of user-defined builtins; see the
+`abs_real` and `abs_real_split` plugins.
+
+User-defined builtins can be added to the extensible `Builtin` type in
+`Dolmen.Std.Builtin.t`.
+
+Builtins need to be registered with the typer using `Dolmen_loop.Typer.Ext`,
+and they optionally need to be registered with the model evaluation mechanism
+(if they are to be used with model verification) using `Dolmen_model.Env.Ext`.
+
+The `dolmen` command-line tool looks up user-defined extensions using the Dune
+plugin mechanism. A plugin named `plugin.typing` will be picked up when
+`--ext plugin` or `--ext plugin.typing` is provided on the command-line, and
+the plugin must register a typing extension named `"plugin"` using
+`Dolmen_loop.Typer.Ext.create`. A plugin named `plugin.model` will be picked up
+when `--ext plugin` or `--ext plugin.model` is provided on the command-line and
+the plugin must register a model extension named `"plugin"` using
+`Dolmen_model.Ext.create`. A plugin named `plugin` (without dots) will be
+picked up when either of the above command line flags is provided, and must
+provide both a typing and model extension.
+
+*Note*: Model extensions are only used (and their existence checked) if the
+user provides the `--check-model` flag.
diff --git a/dolmen_bin.opam b/dolmen_bin.opam
index 8a91c564b..06fedac2d 100644
--- a/dolmen_bin.opam
+++ b/dolmen_bin.opam
@@ -15,6 +15,7 @@ depends: [
   "dolmen_loop" {= version }
   "dolmen_model" {= version }
   "dune" { >= "3.0" }
+  "dune-site" { >= "3.0" }
   "fmt"
   "cmdliner" { >= "1.1.0" }
   "odoc" { with-doc }
diff --git a/dune b/dune
index 1bcb14139..fd459cbde 100644
--- a/dune
+++ b/dune
@@ -4,4 +4,3 @@
   ; Use -03 in release mode when the compiler has flambda enabled
   (release (ocamlopt_flags :standard -O3))
 )
-
diff --git a/dune-project b/dune-project
index 7a21df0b7..dbb474e7e 100644
--- a/dune-project
+++ b/dune-project
@@ -2,4 +2,24 @@
 (name dolmen)
 (using mdx 0.2)
 (using menhir 2.0)
+(using dune_site 0.1)
 (implicit_transitive_deps true)
+
+(package
+  (name dolmen)
+  (sites (lib plugins)))
+
+(package
+  (name dolmen_type))
+
+(package
+  (name dolmen_loop))
+
+(package
+  (name dolmen_model))
+
+(package
+  (name dolmen_bin))
+
+(package
+  (name dolmen_lsp))
diff --git a/examples/extensions/abs_real/README.md b/examples/extensions/abs_real/README.md
new file mode 100644
index 000000000..7162d9469
--- /dev/null
+++ b/examples/extensions/abs_real/README.md
@@ -0,0 +1,5 @@
+# `abs_real` plugin
+
+This is an example plugin adding support for an `abs_real` function. This
+plugin implements both the typing and model extensions for the `abs_real`
+function in the same Dune plugin.
diff --git a/examples/extensions/abs_real/abs_real.ml b/examples/extensions/abs_real/abs_real.ml
new file mode 100644
index 000000000..627e1376e
--- /dev/null
+++ b/examples/extensions/abs_real/abs_real.ml
@@ -0,0 +1,49 @@
+module Type = Dolmen_loop.Typer.T
+module Ty = Dolmen.Std.Expr.Ty
+module Term = Dolmen.Std.Expr.Term
+module Builtin = Dolmen.Std.Builtin
+module Base = Dolmen_type.Base
+
+type _ Builtin.t += Abs_real
+
+module Const = struct
+  let mk' ?pos ?name ?builtin ?tags cname vars args ret =
+    let ty = Ty.pi vars (Ty.arrow args ret) in
+    Dolmen.Std.Expr.Id.mk ?pos ?name ?builtin ?tags
+      (Dolmen.Std.Path.global cname) ty
+
+  module Real = struct
+    (* NB: Use [Dolmen.Std.Expr.with_cache] for parameterized builtins. *)
+    let abs =
+      mk' ~builtin:Abs_real "abs_real"
+        [] [Ty.real] Ty.real
+  end
+end
+
+let abs_real x = Term.apply_cst Const.Real.abs [] [x]
+
+let builtins _lang env s =
+  match s with
+  | Type.Id { ns = Term ; name = Simple "abs_real" } ->
+    Type.builtin_term (Base.term_app1 (module Type) env s abs_real)
+  | _ -> `Not_found
+
+let typing_ext =
+  Dolmen_loop.Typer.Ext.create ~name:"abs_real" ~builtins
+
+module B = Dolmen.Std.Builtin
+module Fun = Dolmen_model.Fun
+
+let real = Dolmen_model.Real.mk
+let of_real = Dolmen_model.Real.get
+
+let abs_real ~cst =
+  Some (Fun.mk_clos @@ Fun.fun_1 ~cst (fun x -> real (Q.abs (of_real x))))
+
+let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
+  match cst.builtin with
+  | Abs_real -> abs_real ~cst
+  | _ -> None
+
+let model_ext =
+  Dolmen_model.Ext.create ~name:"abs_real" ~builtins
\ No newline at end of file
diff --git a/examples/extensions/abs_real/dune b/examples/extensions/abs_real/dune
new file mode 100644
index 000000000..81d77e1b6
--- /dev/null
+++ b/examples/extensions/abs_real/dune
@@ -0,0 +1,10 @@
+(library
+  (public_name dolmen-extension-abs-real)
+  (name abs_real)
+  (modules abs_real)
+  (libraries dolmen_model))
+
+(plugin
+  (name abs_real)
+  (libraries dolmen-extension-abs-real)
+  (site (dolmen plugins)))
diff --git a/examples/extensions/abs_real/dune-project b/examples/extensions/abs_real/dune-project
new file mode 100644
index 000000000..e2b91884d
--- /dev/null
+++ b/examples/extensions/abs_real/dune-project
@@ -0,0 +1,8 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(generate_opam_files false)
+
+(package
+  (name dolmen-extension-abs-real)
+  (depends dolmen_type dolmen_loop dolmen_model))
diff --git a/examples/extensions/abs_real_split/README.md b/examples/extensions/abs_real_split/README.md
new file mode 100644
index 000000000..824414119
--- /dev/null
+++ b/examples/extensions/abs_real_split/README.md
@@ -0,0 +1,8 @@
+# `abs_real_split` plugin
+
+This is an example plugin adding support for an `abs_real` function. This
+plugin implements the typing and model extensions for the `abs_real` function
+in separate Dune plugins.
+
+This is more complex than implementing `abs_real` as a single plugin, but
+allows using the typing extension without a dependency on `dolmen_model`.
diff --git a/examples/extensions/abs_real_split/abs_real_model.ml b/examples/extensions/abs_real_split/abs_real_model.ml
new file mode 100644
index 000000000..9a9df7a43
--- /dev/null
+++ b/examples/extensions/abs_real_split/abs_real_model.ml
@@ -0,0 +1,16 @@
+module B = Dolmen.Std.Builtin
+module Fun = Dolmen_model.Fun
+
+let real = Dolmen_model.Real.mk
+let of_real = Dolmen_model.Real.get
+
+let abs_real ~cst =
+  Some (Fun.mk_clos @@ Fun.fun_1 ~cst (fun x -> real (Q.abs (of_real x))))
+
+let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
+  match cst.builtin with
+  | Abs_real_typing.Abs_real -> abs_real ~cst
+  | _ -> None
+
+let model_ext =
+  Dolmen_model.Ext.create ~name:"abs_real_split" ~builtins
\ No newline at end of file
diff --git a/examples/extensions/abs_real_split/abs_real_typing.ml b/examples/extensions/abs_real_split/abs_real_typing.ml
new file mode 100644
index 000000000..e68c48e12
--- /dev/null
+++ b/examples/extensions/abs_real_split/abs_real_typing.ml
@@ -0,0 +1,32 @@
+module Type = Dolmen_loop.Typer.T
+module Ty = Dolmen.Std.Expr.Ty
+module Term = Dolmen.Std.Expr.Term
+module Builtin = Dolmen.Std.Builtin
+module Base = Dolmen_type.Base
+
+type _ Builtin.t += Abs_real
+
+module Const = struct
+  let mk' ?pos ?name ?builtin ?tags cname vars args ret =
+    let ty = Ty.pi vars (Ty.arrow args ret) in
+    Dolmen.Std.Expr.Id.mk ?pos ?name ?builtin ?tags
+      (Dolmen.Std.Path.global cname) ty
+
+  module Real = struct
+    (* NB: Use [Dolmen.Std.Expr.with_cache] for parameterized builtins. *)
+    let abs =
+      mk' ~builtin:Abs_real "abs_real"
+        [] [Ty.real] Ty.real
+  end
+end
+
+let abs_real x = Term.apply_cst Const.Real.abs [] [x]
+
+let builtins _lang env s =
+  match s with
+  | Type.Id { ns = Term ; name = Simple "abs_real" } ->
+    Type.builtin_term (Base.term_app1 (module Type) env s abs_real)
+  | _ -> `Not_found
+
+let typing_ext =
+  Dolmen_loop.Typer.Ext.create ~name:"abs_real_split" ~builtins
\ No newline at end of file
diff --git a/examples/extensions/abs_real_split/dune b/examples/extensions/abs_real_split/dune
new file mode 100644
index 000000000..3fe7cae28
--- /dev/null
+++ b/examples/extensions/abs_real_split/dune
@@ -0,0 +1,23 @@
+(library
+  (public_name dolmen-typing-extension-abs-real-split)
+  (name abs_real_typing)
+  (modules abs_real_typing)
+  (libraries dolmen_loop))
+
+(library
+  (public_name dolmen-model-extension-abs-real-split)
+  (name abs_real_model)
+  (modules abs_real_model)
+  (libraries dolmen_model dolmen-typing-extension-abs-real-split))
+
+(plugin
+  (package dolmen-typing-extension-abs-real-split)
+  (name abs_real_split.typing)
+  (libraries dolmen-typing-extension-abs-real-split)
+  (site (dolmen plugins)))
+
+(plugin
+  (package dolmen-model-extension-abs-real-split)
+  (name abs_real_split.model)
+  (libraries dolmen-model-extension-abs-real-split)
+  (site (dolmen plugins)))
diff --git a/examples/extensions/abs_real_split/dune-project b/examples/extensions/abs_real_split/dune-project
new file mode 100644
index 000000000..82600c6c6
--- /dev/null
+++ b/examples/extensions/abs_real_split/dune-project
@@ -0,0 +1,12 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(generate_opam_files false)
+
+(package
+  (name dolmen-typing-extension-abs-real-split)
+  (depends dolmen_type dolmen_loop))
+
+(package
+  (name dolmen-model-extension-abs-real-split)
+  (depends dolmen-typing-extension-abs-real-split dolmen_model))
diff --git a/src/bin/dune b/src/bin/dune
index 3a5f51545..88435049c 100644
--- a/src/bin/dune
+++ b/src/bin/dune
@@ -1,4 +1,3 @@
-
 (executable
   (name           main)
   (public_name    dolmen)
diff --git a/src/bin/extensions.ml b/src/bin/extensions.ml
new file mode 100644
index 000000000..719f3afec
--- /dev/null
+++ b/src/bin/extensions.ml
@@ -0,0 +1,235 @@
+(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
+
+type 'a location =
+  | Builtin of 'a
+    (** A built-in extension. *)
+  | Unavailable
+    (** An unavailable extension. Cannot be loaded. *)
+  | Dune_plugin of string
+    (** An external extension to be loaded dune's plugin mechanism. Loading the
+        plugin should register an extension in the appropriate registry. *)
+(** The ['a location] type represents the location of an extension (either
+    built-in, or to be loaded from a specific dune plugin). *)
+
+let is_available = function
+  | Unavailable -> false
+  | Builtin _ | Dune_plugin _ -> true
+
+(* Merge two possible locations for the same plugin. Prefer builtin plugins. *)
+let merge_location p1 p2 =
+  match p1, p2 with
+  | Builtin _ as p, _ | _, (Builtin _ as p) -> p
+  | Dune_plugin _ as p, _ | _, (Dune_plugin _ as p) -> p
+  | Unavailable, Unavailable -> Unavailable
+
+type t = {
+  extension_name : string ;
+  (** Name of the extension (without dot). *)
+  typing_plugin : Dolmen_loop.Typer.Ext.t location ;
+  (** Name of the Dune plugin that provide typing extensions. *)
+  model_plugin : Dolmen_model.Ext.t location ;
+  (** Name of the Dune plugin that provide model extensions. *)
+}
+
+let has_typing_extension { typing_plugin; _ } = is_available typing_plugin
+
+let has_model_extension { model_plugin; _ } = is_available model_plugin
+
+let pp ppf e =
+  let variants =
+    (if has_typing_extension e then ["typing"] else []) @
+    (if has_model_extension e then ["model"] else [])
+  in
+  Fmt.pf ppf "%s@ %a" e.extension_name
+    Fmt.(parens @@ list ~sep:comma string) variants
+
+let name { extension_name ; _ } = extension_name
+
+type kind = Typing | Model
+
+let parse_ext_opt s : (string * kind option) option =
+  match String.rindex s '.' with
+  | exception Not_found -> Some (s, None)
+  | pos ->
+    let extension_name = String.sub s 0 pos in
+    let plugin_kind = String.sub s (pos + 1) (String.length s - pos - 1) in
+    match plugin_kind with
+    | "typing" -> Some (extension_name, Some Typing)
+    | "model" -> Some (extension_name, Some Model)
+    | _ -> None
+
+let merge_ext e1 e2 =
+  assert (e1.extension_name = e2.extension_name);
+  let typing_plugin = merge_location e1.typing_plugin e2.typing_plugin
+  and model_plugin = merge_location e1.model_plugin e2.model_plugin in
+  { extension_name = e1.extension_name
+  ; typing_plugin
+  ; model_plugin }
+
+let add_ext tbl ext =
+  let name = ext.extension_name in
+  match Hashtbl.find tbl name with
+  | ext' -> Hashtbl.replace tbl name (merge_ext ext ext')
+  | exception Not_found -> Hashtbl.replace tbl name ext
+
+let infos =
+  lazy (
+    let extensions = Hashtbl.create 17 in
+    (* Add builtin typing extensions. *)
+    List.iter (fun ext ->
+      add_ext extensions
+        { extension_name = Dolmen_loop.Typer.Ext.name ext
+        ; typing_plugin = Builtin ext
+        ; model_plugin = Unavailable }
+    ) [ Dolmen_loop.Typer.Ext.bvconv ];
+
+    (* Add builtin model extensions. *)
+    List.iter (fun ext ->
+      add_ext extensions
+        { extension_name = Dolmen_model.Ext.name ext
+        ; typing_plugin = Unavailable
+        ; model_plugin = Builtin ext }
+    ) [ Dolmen_model.Ext.bvconv ];
+
+    (* Add extensions from plugins. *)
+    let add_plugin invalid plugin = function
+      | None -> plugin :: invalid
+      | Some (extension_name, k) ->
+        let typing_plugin =
+          match k with
+          | None | Some Typing -> Dune_plugin plugin
+          | Some _ -> Unavailable
+        and model_plugin =
+          match k with
+          | None | Some Model -> Dune_plugin plugin
+          | Some _ -> Unavailable
+        in
+        add_ext extensions
+          { extension_name ; typing_plugin ; model_plugin };
+        invalid
+    in
+    let invalid =
+      List.fold_left (fun invalid e ->
+        add_plugin invalid e @@ parse_ext_opt e
+      ) [] (Dolmen.Sites.Plugins.Plugins.list ())
+    in
+    extensions, List.fast_sort String.compare invalid
+  )
+
+let invalid () = snd @@ Lazy.force infos
+
+let list () =
+  List.fast_sort
+    (fun e1 e2 -> String.compare (name e1) (name e2))
+    (Hashtbl.fold (fun _ e exts -> e :: exts) (fst @@ Lazy.force infos) [])
+
+let find_ext name =
+  let exts, _ = Lazy.force infos in
+  try Ok (Hashtbl.find exts name)
+  with Not_found ->
+    Fmt.error_msg
+      "@[<v>Could not find extension '%s'@ \
+      Available extensions:@;<1 2>@[<v>%a@]@]"
+      name
+      Fmt.(list (box pp)) (list ())
+
+let load_plugin_or_fail plugin =
+  try Ok (Dolmen.Sites.Plugins.Plugins.load plugin)
+  with Dynlink.Error err ->
+    Fmt.error_msg "while loading plugin %s: %s"
+      plugin (Dynlink.error_message err)
+
+let missing_extension =
+  Dolmen_loop.Report.Warning.mk ~mnemonic:"missing-extension"
+    ~message:(fun ppf (kind, ext, _) ->
+      Format.fprintf ppf "There is no %s extension named '%s'." kind ext)
+    ~hints:[fun (kind, _, plugin) ->
+      Some (Format.dprintf
+        "Expected plugin '%s' to register this %s extension." plugin kind)]
+    ~name:"Missing extension" ()
+
+let duplicate_extension =
+  Dolmen_loop.Report.Warning.mk ~mnemonic:"duplicate-extension"
+    ~message:(fun ppf (kind, name, _) ->
+      Format.fprintf ppf
+        "%s extension '%s' was registered multiple times."
+          (String.capitalize_ascii kind)
+          name)
+    ~hints:[
+      (fun (kind, name, _) ->
+        Some (
+          Format.dprintf "%a@ %s@ extension@ '%s'."
+            Fmt.words
+            "This is likely caused by multiple plugins trying to register the"
+            kind name));
+      (fun (kind, _, plugin) ->
+        Some (
+          Format.dprintf "Expected plugin '%s' to register this %s extension."
+            plugin kind))]
+    ~name:"Duplicate extension" ()
+
+let add_typing_extension ext st =
+  Loop.State.update Loop.Typer.extension_builtins (List.cons ext) st
+
+let load_typing_extension ext st =
+    match ext.typing_plugin with
+    | Unavailable ->
+      Fmt.error_msg
+        "No plugin provides the typing extension '%s'" ext.extension_name
+    | Builtin e ->
+      Ok (add_typing_extension e st)
+    | Dune_plugin plugin ->
+      Result.bind (load_plugin_or_fail plugin) @@ fun () ->
+      match Dolmen_loop.Typer.Ext.find_all ext.extension_name with
+      | [] ->
+        Ok (
+          Loop.State.warn st
+            missing_extension
+            ("typing", ext.extension_name, plugin)
+        )
+      | [ e ] ->
+        Ok (add_typing_extension e st)
+      | e :: _ ->
+        let st =
+          Loop.State.warn st
+            duplicate_extension
+            ("typing", ext.extension_name, plugin)
+        in
+        Ok (add_typing_extension e st)
+
+let add_model_extension b st =
+  Loop.State.update Loop.Check.builtins
+   (fun bs -> Dolmen_model.Eval.builtins [ Dolmen_model.Ext.builtins b ; bs ])
+   st
+
+let load_model_extension ext st =
+    match ext.model_plugin with
+    | Unavailable ->
+      Fmt.error_msg
+        "No plugin provides the model extension '%s'" ext.extension_name
+    | Builtin e ->
+      Ok (add_model_extension e st)
+    | Dune_plugin plugin ->
+      Result.bind (load_plugin_or_fail plugin) @@ fun () ->
+      match Dolmen_model.Ext.find_all ext.extension_name with
+      | [] ->
+        Ok (
+          Loop.State.warn st
+            missing_extension
+            ("model", ext.extension_name, plugin)
+        )
+      | [ e ] ->
+        Ok (add_model_extension e st)
+      | e :: _ ->
+        let st =
+          Loop.State.warn st
+            duplicate_extension
+            ("model", ext.extension_name, plugin)
+        in
+        Ok (add_model_extension e st)
+
+let parse s =
+  match parse_ext_opt s with
+  | None -> Fmt.error_msg "Invalid extension name '%s'" s
+  | Some (name, kind) ->
+    Result.map (fun ext -> (ext, kind)) (find_ext name)
\ No newline at end of file
diff --git a/src/bin/extensions.mli b/src/bin/extensions.mli
new file mode 100644
index 000000000..af1cbd910
--- /dev/null
+++ b/src/bin/extensions.mli
@@ -0,0 +1,40 @@
+type t
+
+val pp : Format.formatter -> t -> unit
+
+val name : t -> string
+(** Returns the name of the extension. *)
+
+val load_typing_extension :
+  t -> Loop.State.t -> (Loop.State.t, [> `Msg of string]) result
+(** [load_typing_extension e] loads and returns the typing extension associated
+    with [e].
+
+    Fails if an error occurs during loading of
+    an external typing extension. *)
+
+val load_model_extension :
+  t -> Loop.State.t -> (Loop.State.t, [> `Msg of string]) result
+(** [load_model_extension e] loads and returns the model extension associated
+    with [e].
+
+    Fails if [e] has no model extension, or an error occurs during loading of an
+    external model extension. *)
+
+val list : unit -> t list
+(** Lists the available extensions. *)
+
+val invalid : unit -> string list
+(** Lists the name of dune plugins registered as extensions but with an invalid
+    name. *)
+
+type kind = Typing | Model
+
+val parse :
+  string -> (t * kind option, [> `Msg of string ]) result
+(** Parses an extension name, with optional restriction prefix.
+
+    Returns a pair [(ext, kind)] where [kind] is [None] if both model and typing
+    extensions should be loaded, [Some Typing] if only the typing extension
+    should be loaded, and [Some Model] if only the model extension should be
+    loaded. *)
\ No newline at end of file
diff --git a/src/bin/main.ml b/src/bin/main.ml
index ad18fca89..631e7a807 100644
--- a/src/bin/main.ml
+++ b/src/bin/main.ml
@@ -118,6 +118,20 @@ let doc conf t =
     pp_status t
     (Report.T.doc t)
 
+(* Extensions list *)
+(* *************** *)
+
+let list_extensions () =
+  Format.printf "%a@."
+    Fmt.(vbox @@ list (box Extensions.pp)) (Extensions.list ());
+  match Extensions.invalid () with
+  | [] -> ()
+  | invalid ->
+    Format.printf "@[<v 2>%a@ %a@]@."
+      (Fmt.styled `Bold @@ Fmt.styled (`Fg (`Hi `Magenta)) @@ Fmt.string)
+      "The following plugins were found but are invalid:"
+      Fmt.(list string) invalid
+
 
 (* Main code *)
 (* ********* *)
@@ -146,3 +160,5 @@ let () =
     doc conf report
   | Ok (`Ok List_reports { conf; }) ->
     list conf
+  | Ok (`Ok List_extensions) ->
+    list_extensions ()
\ No newline at end of file
diff --git a/src/bin/options.ml b/src/bin/options.ml
index 53ab6d474..8986ffcd4 100644
--- a/src/bin/options.ml
+++ b/src/bin/options.ml
@@ -46,6 +46,7 @@ type cmd =
       report : Dolmen_loop.Report.T.t;
       conf : Dolmen_loop.Report.Conf.t;
     }
+  | List_extensions
 
 (* Color options *)
 (* ************************************************************************* *)
@@ -267,18 +268,12 @@ let report_style =
     "contextual", Loop.State.Contextual;
   ]
 
-
-(* Typing extensions *)
+(* Dolmen extensions *)
 (* ************************************************************************ *)
 
-let typing_extension_list =
-  List.map
-    (fun ext -> Loop.Typer.Ext.name ext, ext)
-    (Loop.Typer.Ext.list ())
-
-let typing_ext =
-  Arg.enum typing_extension_list
-
+let extension =
+  let print ppf (t, _) = Extensions.pp ppf t in
+  Cmdliner.Arg.conv (Extensions.parse, print)
 
 (* Smtlib2 logic and extensions *)
 (* ************************************************************************ *)
@@ -366,7 +361,7 @@ let mk_run_state
     flow_check
     header_check header_licenses header_lang_version
     smtlib2_forced_logic smtlib2_exts
-    type_check extension_builtins
+    type_check extensions
     check_model (* check_model_mode *)
     debug report_style max_warn reports syntax_error_ref
   =
@@ -384,26 +379,45 @@ let mk_run_state
   let () = if abort_on_bug then Dolmen_loop.Code.abort Dolmen_loop.Code.bug in
   let () = Hints.model ~check_model (* ~check_model_mode *) in
   (* State creation *)
-  Loop.State.empty
-  |> Loop.State.init
-    ~bt ~debug ~report_style ~reports
-    ~max_warn ~time_limit ~size_limit
-    ~response_file
-  |> Loop.Parser.init
-    ~syntax_error_ref
-    ~interactive_prompt:Loop.Parser.interactive_prompt_lang
-  |> Loop.Typer.init
-    ~smtlib2_forced_logic
-    ~extension_builtins
-  |> Loop.Typer_Pipe.init ~type_check
-  |> Loop.Check.init
-    ~check_model
-    (* ~check_model_mode *)
-  |> Loop.Flow.init ~flow_check
-  |> Loop.Header.init
-    ~header_check
-    ~header_licenses
-    ~header_lang_version
+  let st =
+    Loop.State.empty
+    |> Loop.State.init
+      ~bt ~debug ~report_style ~reports
+      ~max_warn ~time_limit ~size_limit
+      ~response_file
+    |> Loop.Parser.init
+      ~syntax_error_ref
+      ~interactive_prompt:Loop.Parser.interactive_prompt_lang
+    |> Loop.Typer.init
+      ~smtlib2_forced_logic
+    |> Loop.Typer_Pipe.init ~type_check
+    |> Loop.Check.init
+      ~check_model
+      (* ~check_model_mode *)
+    |> Loop.Flow.init ~flow_check
+    |> Loop.Header.init
+      ~header_check
+      ~header_licenses
+      ~header_lang_version
+  in
+  (* Extensions *)
+  let st =
+    List.fold_left (fun st (ext, kind) ->
+      match kind with
+      | None | Some Extensions.Typing ->
+        Result.bind st (Extensions.load_typing_extension ext)
+      | Some _ -> st
+    ) (Ok st) extensions
+  in
+  if check_model then
+    List.fold_left (fun st (ext, kind) ->
+      match kind with
+      | None | Some Extensions.Model ->
+        Result.bind st (Extensions.load_model_extension ext)
+      | Some _ -> st
+    ) st extensions
+  else
+    st
 
 (* Profiling *)
 (* ************************************************************************* *)
@@ -627,12 +641,12 @@ let state =
     Arg.(value & opt_all smtlib2_ext [] &
          info ["internal-smtlib2-extension"] ~docs:internal_section ~doc)
   in
-  let typing_ext =
+  let ext =
     let doc = Format.asprintf
-        "Enable typing extensions.
-         $(docv) must be %s" (Arg.doc_alts_enum typing_extension_list)
+        "Enable extensions. Use $(b,--list-extensions) to list available \
+        extensions."
     in
-    Arg.(value & opt_all typing_ext [] &
+    Arg.(value & opt_all extension [] &
          info ["ext"] ~docs ~doc)
   in
   let debug =
@@ -689,7 +703,8 @@ let state =
       in
       Arg.(value & opt bool false & info ["syntax-error-ref"] ~doc ~docs:error_section)
     in
-  Term.(const mk_run_state $ profiling_t $
+  Term.(term_result (
+    const mk_run_state $ profiling_t $
         gc $ gc_t $ bt $ colors $
         abort_on_bug $
         time $ size $
@@ -697,9 +712,9 @@ let state =
         flow_check $
         header_check $ header_licenses $ header_lang_version $
         force_smtlib2_logic $ smtlib2_extensions $
-        typing $ typing_ext $
+        typing $ ext $
         check_model $ (* check_model_mode $ *)
-        debug $ report_style $ max_warn $ reports $ syntax_error_ref)
+        debug $ report_style $ max_warn $ reports $ syntax_error_ref))
 
 
 (* List command term *)
@@ -707,19 +722,21 @@ let state =
 
 let cli =
   let docs = option_section in
-  let aux state preludes logic_file list doc =
-    match list, doc with
-    | false, None ->
+  let aux state preludes logic_file list doc list_extensions =
+    match list, doc, list_extensions with
+    | false, None, false ->
       `Ok (Run { state; logic_file; preludes })
-    | false, Some report ->
+    | false, Some report, false ->
       let conf = Loop.State.get Loop.State.reports state in
       `Ok (Doc { report; conf; })
-    | true, None ->
+    | true, None, false ->
       let conf = Loop.State.get Loop.State.reports state in
       `Ok (List_reports { conf; })
-    | true, Some _ ->
+    | false, None, true ->
+      `Ok List_extensions
+    | _ ->
       `Error (false,
-              "at most one of --list and --doc might be \
+              "at most one of --list, --doc and --list-extensions might be \
                present on the command line")
   in
   let list =
@@ -731,4 +748,11 @@ let cli =
     let doc = "The warning or error of which to show the documentation." in
     Arg.(value & opt (some mnemonic_conv) None & info ["doc"] ~doc ~docv:"mnemonic" ~docs)
   in
-  Term.(ret (const aux $ state $ preludes $ logic_file $ list $ doc))
+  let list_extensions =
+    let doc = "List all available extensions." in
+    Arg.(value & flag & info ["list-extensions"] ~doc ~docs)
+  in
+  Term.(ret (
+    const aux $ state $ preludes $ logic_file $ list $ doc
+    $ list_extensions
+  ))
diff --git a/src/dolmen.ml b/src/dolmen.ml
index 13a5f03ae..6828a95d3 100644
--- a/src/dolmen.ml
+++ b/src/dolmen.ml
@@ -15,3 +15,5 @@ module Zf = Dolmen_zf
 (* Classes *)
 module Class = Dolmen_class
 
+(* Extensions *)
+module Sites = Sites
diff --git a/src/dune b/src/dune
index cbb34af6a..8e4a56155 100644
--- a/src/dune
+++ b/src/dune
@@ -12,7 +12,12 @@
     dolmen_tptp dolmen_smtlib2 dolmen_zf
     ; Dolmen classes
     dolmen_class
+    ; extension support
+    dune-site dune-site.plugins
   )
-  (modules        Dolmen)
+  (modules        Dolmen Sites)
 )
 
+(generate_sites_module
+  (module Sites)
+  (plugins (dolmen plugins)))
diff --git a/src/loop/report.mli b/src/loop/report.mli
index a63254b48..10776c978 100644
--- a/src/loop/report.mli
+++ b/src/loop/report.mli
@@ -43,7 +43,6 @@ module T : sig
 
   val doc : [< t ] -> (Format.formatter -> unit)
   (** documentation for a report. *)
-
 end
 
 
diff --git a/src/loop/typer.ml b/src/loop/typer.ml
index e14e44e44..131dbdc2f 100644
--- a/src/loop/typer.ml
+++ b/src/loop/typer.ml
@@ -55,15 +55,15 @@ module Smtlib2_Arrays =
 module Smtlib2_Bitv =
   Dolmen_type.Bitv.Smtlib2.Tff(T)
     (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term.Bitv)
-module Smtlib2_Bvconv =
-  Dolmen_type.Bitv.Smtlib2.Bvconv(T)
-    (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term.Bitv)
 module Smtlib2_Float =
   Dolmen_type.Float.Smtlib2.Tff(T)
     (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term)
 module Smtlib2_String =
   Dolmen_type.Strings.Smtlib2.Tff(T)
     (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term)
+module Smtlib2_Bvconv =
+  Dolmen_type.Bitv.Smtlib2.Bvconv(T)
+    (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term.Bitv)
 
 (* Zf *)
 module Zf_Core =
@@ -73,6 +73,43 @@ module Zf_arith =
   Dolmen_type.Arith.Zf.Thf(T)
     (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term)
 
+(* Extensions builtins *)
+(* ************************************************************************ *)
+
+module Ext = struct
+
+  type t = {
+    name : string;
+    builtins : Typer_intf.lang -> T.builtin_symbols;
+  }
+
+  let name { name; _ } = name
+  let builtins { builtins; _ } = builtins
+
+  let registry = Hashtbl.create 17
+
+  let register ({ name; _ } as ext)  =
+    match Hashtbl.find registry name with
+    | exception Not_found -> Hashtbl.replace registry name [ ext ]
+    | exts -> Hashtbl.replace registry name (ext :: exts)
+
+  let find_all name =
+    try Hashtbl.find registry name with Not_found -> []
+
+  let create ~name ~builtins =
+    let t = { name ; builtins } in
+    register t;
+    t
+
+  let bvconv =
+    create ~name:"bvconv"
+      ~builtins:(function
+        | `Logic Logic.Smtlib2 version ->
+          Smtlib2_Bvconv.parse (`Script version)
+        | _ -> Dolmen_type.Base.noop)
+end
+
+
 (* Printing helpers *)
 (* ************************************************************************ *)
 
@@ -1075,40 +1112,7 @@ module Typer(State : State.S) = struct
   type error = T.error
   type warning = T.warning
   type builtin_symbols = T.builtin_symbols
-
-  type lang = [
-    | `Logic of Logic.language
-    | `Response of Response.language
-  ]
-
-  (* Extensions builtins *)
-  (* ************************************************************************ *)
-
-  module Ext = struct
-
-    type t = {
-      name : string;
-      builtins : lang -> T.builtin_symbols;
-    }
-
-    let all = ref []
-    let list () = !all
-    let name { name; _ } = name
-    let builtins { builtins; _ } = builtins
-
-    let create ~name ~builtins =
-      let t = { name; builtins; } in
-      all := t :: !all;
-      t
-
-    let bv2nat =
-      create ~name:"bvconv"
-        ~builtins:(function
-            | `Logic Logic.Smtlib2 version ->
-              Smtlib2_Bvconv.parse (`Script version)
-            | _ -> Dolmen_type.Base.noop)
-
-  end
+  type extension = Ext.t
 
   (* State setup *)
   (* ************************************************************************ *)
@@ -1122,7 +1126,8 @@ module Typer(State : State.S) = struct
     State.create_key ~pipe "smtlib2_forced_logic"
   let extension_builtins : Ext.t list State.key =
     State.create_key ~pipe "extensions_builtins"
-  let additional_builtins : (state -> lang -> T.builtin_symbols) State.key =
+  let additional_builtins :
+    (state -> Typer_intf.lang -> T.builtin_symbols) State.key =
     State.create_key ~pipe "additional_builtins"
 
   let init
@@ -1161,7 +1166,7 @@ module Typer(State : State.S) = struct
     | `Logic f -> f.loc
     | `Response f -> f.loc
 
-  let lang_of_input (input : input) : [ lang | `Missing ]=
+  let lang_of_input (input : input) : [ Typer_intf.lang | `Missing ] =
     match input with
     | `Logic f ->
       begin match f.lang with
@@ -1484,7 +1489,7 @@ module Typer(State : State.S) = struct
     (* Match the language to determine bultins and other options *)
     let lang =
       match lang_of_input input with
-      | #lang as lang -> lang
+      | #Typer_intf.lang as lang -> lang
       | `Missing ->
         let st =
           error st ~input ~loc:{ file; loc; } Report.Error.internal_error
diff --git a/src/loop/typer.mli b/src/loop/typer.mli
index aaf061eca..11836ca5d 100644
--- a/src/loop/typer.mli
+++ b/src/loop/typer.mli
@@ -40,6 +40,35 @@ val bad_arith_expr : (Dolmen_type.Arith.Smtlib2.config * string) Report.Warning.
 val unknown_logic : string Report.Warning.t
 (** Unknown logic warning *)
 
+module Ext : sig
+  (** Define typing extensions.
+
+      These extensions are typically extensions used by some community,
+      but not yet part of the standard.
+
+      @since 0.10 *)
+
+  type t
+  (** The type of typing extensions. *)
+
+  val name : t -> string
+  (** Extension name, sould be suitable for cli options. *)
+
+  val builtins : t -> Typer_intf.lang -> T.builtin_symbols
+  (** Reutnrs the typing builtins from an extension. *)
+
+  val create :
+    name:string -> builtins:(Typer_intf.lang -> T.builtin_symbols) -> t
+  (** Create a new extension. *)
+
+  val bvconv : t
+  (** Typing extension to add `bv2nat` and `int2bv`. *)
+
+  val find_all : string -> t list
+  (** Returns the extensions that have been registered with the given name.
+
+      @since 0.11 *)
+end
 
 (** {2 Typechecker Functor} *)
 
@@ -54,6 +83,7 @@ module Typer(State : State.S)
                 and type error = T.error
                 and type warning = T.warning
                 and type builtin_symbols = T.builtin_symbols
+                and type extension = Ext.t
 
 (** {2 Typechecker Pipe} *)
 
@@ -94,4 +124,3 @@ module Make
        and type term_var := Expr.term_var
        and type term_cst := Expr.term_cst
        and type formula := Expr.formula
-
diff --git a/src/loop/typer_intf.ml b/src/loop/typer_intf.ml
index 31074060f..5ac3c2979 100644
--- a/src/loop/typer_intf.ml
+++ b/src/loop/typer_intf.ml
@@ -1,4 +1,9 @@
-(* This file is free software, part of Archsat. See file "LICENSE" for more details. *)
+(* This file is free software, part of dolmen. See file "LICENSE" for more details. *)
+
+type lang = [
+  | `Logic of Logic.language
+  | `Response of Response.language
+]
 
 (* Small signature to define a number of types. *)
 module type Types = sig
@@ -31,11 +36,6 @@ module type Typer = sig
     | `Response of Response.language State.file
   ]
 
-  type lang = [
-    | `Logic of Logic.language
-    | `Response of Response.language
-  ]
-
   type decl = [
     | `Type_decl of ty_cst * ty_def option
     | `Term_decl of term_cst
@@ -129,6 +129,9 @@ module type Typer_Full = sig
   type builtin_symbols
   (** The type of builin symbols for the type-checker. *)
 
+  type extension
+  (** The type of extensions for the type-checker. *)
+
   include Typer
     with type env := env
      and type state := state
@@ -143,34 +146,6 @@ module type Typer_Full = sig
   (** This signature includes the requirements to instantiate the {Pipes.Make:
       functor*)
 
-  module Ext : sig
-    (** Define typing extensions.
-
-        These extensions are typically extensions used by some community,
-        but not yet part of the standard.
-
-        @since 0.10 *)
-
-    type t
-    (** The type of typing extensions. *)
-
-    val name : t -> string
-    (** Extension name, sould be suitable for cli options. *)
-
-    val builtins : t -> lang -> builtin_symbols
-    (** Reutnrs the typing builtins from an extension. *)
-
-    val create : name:string -> builtins:(lang -> builtin_symbols) -> t
-    (** Create a new extension. *)
-
-    val list : unit -> t list
-    (** The list of all extensions. *)
-
-    val bv2nat : t
-    (** Typing extension to add the `bv2nat` function. *)
-
-  end
-
   val ty_state : ty_state key
   (** Key to store the local typechecking state in the global pipeline state. *)
 
@@ -181,7 +156,7 @@ module type Typer_Full = sig
   (** Force the typechecker to use the given logic (instead of using the one declared
       in the `set-logic` statement). *)
 
-  val extension_builtins : Ext.t list key
+  val extension_builtins : extension list key
   (** Use typing extensions defined by the typechecker.
 
       @since 0.10 *)
@@ -197,7 +172,7 @@ module type Typer_Full = sig
   val init :
     ?ty_state:ty_state ->
     ?smtlib2_forced_logic:string option ->
-    ?extension_builtins:(Ext.t list) ->
+    ?extension_builtins:(extension list) ->
     ?additional_builtins:(state -> lang -> builtin_symbols) ->
     state -> state
 
diff --git a/src/model/bitv.ml b/src/model/bitv.ml
index 7ea4ca820..d6ef40298 100644
--- a/src/model/bitv.ml
+++ b/src/model/bitv.ml
@@ -29,8 +29,6 @@ let ops = Value.ops ~print ~compare ()
 (* Value helpers *)
 (* ************************************************************************* *)
 
-
-
 let is_unsigned_integer size z =
   Z.sign z >= 0 && Z.numbits z <= size
 
@@ -199,3 +197,15 @@ let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
   | B.Bitv_sge n -> cmp ~cst (fun a b -> Z.geq (sbitv n a) (sbitv n b))
   | _ -> None
 
+let bv2nat ~cst ~size =
+  Some (Fun.mk_clos @@ Fun.fun_1 ~cst (fun x -> Int.mk (ubitv size x)))
+
+let int2bv ~cst ~size =
+  Some (Fun.mk_clos @@ Fun.fun_1 ~cst (fun x ->
+    mk size (Z.extract (Value.extract_exn ~ops:Int.ops x) 0 size)))
+
+let bvconv_builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
+  match cst.builtin with
+  | B.Bitv_of_int { n } -> int2bv ~cst ~size:n
+  | B.Bitv_to_nat { n } -> bv2nat ~cst ~size:n
+  | _ -> None
diff --git a/src/model/bitv.mli b/src/model/bitv.mli
index ca538ab82..50bda2974 100644
--- a/src/model/bitv.mli
+++ b/src/model/bitv.mli
@@ -21,4 +21,5 @@ val ubitv : int -> Value.t -> Z.t
 val sbitv : int -> Value.t -> Z.t
 (** Extract the value as a signed integer *)
 
-
+val bvconv_builtins : Env.builtins
+(** builtins for conversions between bitvectors and integers *)
\ No newline at end of file
diff --git a/src/model/dune b/src/model/dune
index 466fabc98..5f105c1dd 100644
--- a/src/model/dune
+++ b/src/model/dune
@@ -20,7 +20,7 @@
   )
   (modules
     ; Model checking
-    Value Model Env Eval
+    Value Model Env Eval Ext
     ; Builtins
     Adt Array Bool Core Fun Int Rat Real Bitv Fp Coercion
     ; Loop Pipe
diff --git a/src/model/env.ml b/src/model/env.ml
index ebf308351..d8920f06b 100644
--- a/src/model/env.ml
+++ b/src/model/env.ml
@@ -26,6 +26,4 @@ let builtins t = t.builtins
 
 let model { model; _ } = model
 
-let update_model t f = { t with model = f t.model; }
-
-
+let update_model t f = { t with model = f t.model; }
\ No newline at end of file
diff --git a/src/model/env.mli b/src/model/env.mli
index ed9ef6d38..312166fb1 100644
--- a/src/model/env.mli
+++ b/src/model/env.mli
@@ -19,6 +19,4 @@ val builtins : t -> builtins
 
 val model : t -> Model.t
 
-val update_model : t -> (Model.t -> Model.t) -> t
-
-
+val update_model : t -> (Model.t -> Model.t) -> t
\ No newline at end of file
diff --git a/src/model/ext.ml b/src/model/ext.ml
new file mode 100644
index 000000000..c68357b89
--- /dev/null
+++ b/src/model/ext.ml
@@ -0,0 +1,30 @@
+(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
+
+(* Extensions builtins *)
+(* ************************************************************************ *)
+
+type t = {
+  name : string;
+  builtins : Env.builtins;
+}
+
+let name { name; _ } = name
+let builtins { builtins; _ } = builtins
+
+let registry = Hashtbl.create 17
+
+let register ({ name; _ } as ext)  =
+  match Hashtbl.find registry name with
+  | exception Not_found -> Hashtbl.replace registry name [ ext ]
+  | exts -> Hashtbl.replace registry name (ext :: exts)
+
+let find_all name =
+  try Hashtbl.find registry name with Not_found -> []
+
+let create ~name ~builtins =
+  let t = { name ; builtins } in
+  register t;
+  t
+
+let bvconv =
+  create ~name:"bvconv" ~builtins:Bitv.bvconv_builtins
\ No newline at end of file
diff --git a/src/model/ext.mli b/src/model/ext.mli
new file mode 100644
index 000000000..52c74faa3
--- /dev/null
+++ b/src/model/ext.mli
@@ -0,0 +1,26 @@
+
+
+(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
+
+(** Define model extensions.
+
+    @since 0.11 *)
+
+type t
+(** The type of evaluation extensions. *)
+
+val name : t -> string
+(** Extension name, should be suitable for cli options. *)
+
+val builtins : t -> Env.builtins
+(** Returns the evaluation builtins from an extension. *)
+
+val create :
+  name:string -> builtins:Env.builtins -> t
+(** Create a new extension. *)
+
+val bvconv : t
+(** Built-in extension for conversion between bit-vectors and integers *)
+
+val find_all : string -> t list
+(** Returns the extensions that have been registered with the given name. *)
\ No newline at end of file
diff --git a/src/model/loop.ml b/src/model/loop.ml
index 384905936..f6bf44693 100644
--- a/src/model/loop.ml
+++ b/src/model/loop.ml
@@ -141,6 +141,36 @@ let parsed_model =
                     "This is an internal error, plean report upstream, ^^")]
     ~name:"Parsed model" ()
 
+let missing_model_extension =
+  Dolmen_loop.Report.Warning.mk ~code ~mnemonic:"missing-model-extension"
+    ~message:(fun ppf name ->
+      Format.fprintf ppf "There is no model extension named '%s'." name)
+    ~hints:[fun name ->
+      Some (Format.dprintf
+        "This is likely due to the plugin for '%s' being broken." name)]
+    ~name:"Missing model extension" ()
+
+let duplicate_model_extension =
+  Dolmen_loop.Report.Warning.mk ~code ~mnemonic:"duplicate-model-extension"
+    ~message:(fun ppf name ->
+      Format.fprintf ppf
+        "Model extension '%s' was registered multiple times." name)
+    ~hints:[
+      (fun name ->
+        Some (
+          Format.dprintf "%a@ '%s'@ %a@ '%s'."
+            Fmt.words "This is likely caused by a plugin other than"
+            name
+            Fmt.words "trying to register the model extension"
+            name));
+      (fun _ ->
+        Some (
+          Format.dprintf "%a"
+            Fmt.words
+            "Plugins should not define model extensions with a name other than \
+             the name of the plugin itself. "))]
+    ~name:"Duplicate model extension" ()
+
 let error_in_response =
   Dolmen_loop.Report.Error.mk ~code ~mnemonic:"response-error"
     ~message:(fun fmt () ->
@@ -265,40 +295,46 @@ module Make
       and type formula := Dolmen.Std.Expr.formula)
 = struct
 
+  let core_builtins =
+    Eval.builtins [
+      Adt.builtins;
+      Bool.builtins;
+      Core.builtins;
+      Array.builtins;
+      Int.builtins;
+      Rat.builtins;
+      Real.builtins;
+      Bitv.builtins;
+      Fp.builtins;
+      Coercion.builtins;
+    ]
+
   let pipe = "Model"
   let check_model = Typer.check_model
   let check_state = State.create_key ~pipe "check_state"
+  let builtins = State.create_key ~pipe "builtins"
 
   let init
       ~check_model:check_model_value
+      ?(extension_builtins=[])
       st =
+    let rev_extension_builtins = List.rev_map Ext.builtins extension_builtins in
     st
     |> State.set check_model check_model_value
     |> State.set check_state empty
+    |> State.set builtins
+        (Eval.builtins @@
+          List.rev_append rev_extension_builtins [core_builtins])
 
 
   (* Evaluation and errors *)
   (* ************************************************************************ *)
 
-  let builtins =
-    Eval.builtins [
-      Adt.builtins;
-      Bool.builtins;
-      Core.builtins;
-      Array.builtins;
-      Int.builtins;
-      Rat.builtins;
-      Real.builtins;
-      Bitv.builtins;
-      Fp.builtins;
-      Coercion.builtins;
-    ]
-
   let eval ~reraise_for_delayed_eval ~file ~loc st model term =
     let _err err args =
       raise (State.Error (State.error st ~file ~loc err args))
     in
-    let env = Env.mk model ~builtins in
+    let env = Env.mk model ~builtins:(State.get builtins st) in
     try
       Eval.eval env term
     with
diff --git a/src/standard/extensions.ml b/src/standard/extensions.ml
index a469bf6de..967f43fc9 100644
--- a/src/standard/extensions.ml
+++ b/src/standard/extensions.ml
@@ -42,4 +42,3 @@ module Smtlib2 = struct
     then Some mk else None
 
 end
-
diff --git a/tests/model/bvconv/bv2nat.expected b/tests/model/bvconv/bv2nat.expected
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/model/bvconv/bv2nat.rsmt2 b/tests/model/bvconv/bv2nat.rsmt2
new file mode 100644
index 000000000..44aa72914
--- /dev/null
+++ b/tests/model/bvconv/bv2nat.rsmt2
@@ -0,0 +1,5 @@
+sat
+(
+  (define-fun b () (_ BitVec 5)
+    #b00101)
+)
diff --git a/tests/model/bvconv/bv2nat.smt2 b/tests/model/bvconv/bv2nat.smt2
new file mode 100644
index 000000000..7f23d729d
--- /dev/null
+++ b/tests/model/bvconv/bv2nat.smt2
@@ -0,0 +1,7 @@
+(set-logic BVLIA)
+(declare-const b (_ BitVec 5))
+(assert (= 5 (bv2nat b)))
+(check-sat)
+(get-model)
+(exit)
+
diff --git a/tests/model/bvconv/dune b/tests/model/bvconv/dune
new file mode 100644
index 000000000..b92fe23e6
--- /dev/null
+++ b/tests/model/bvconv/dune
@@ -0,0 +1,68 @@
+; File auto-generated by gentests.ml
+
+; Auto-generated part begin
+; Test for bv2nat.smt2
+; Incremental test
+
+(rule
+   (target  bv2nat.incremental)
+   (deps    (:response bv2nat.rsmt2) (:input bv2nat.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff bv2nat.expected bv2nat.incremental)))
+
+; Full mode test
+
+(rule
+   (target  bv2nat.full)
+   (deps    (:response bv2nat.rsmt2) (:input bv2nat.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff bv2nat.expected bv2nat.full)))
+
+
+; Test for int2bv.smt2
+; Incremental test
+
+(rule
+   (target  int2bv.incremental)
+   (deps    (:response int2bv.rsmt2) (:input int2bv.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff int2bv.expected int2bv.incremental)))
+
+; Full mode test
+
+(rule
+   (target  int2bv.full)
+   (deps    (:response int2bv.rsmt2) (:input int2bv.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff int2bv.expected int2bv.full)))
+
+
+; Auto-generated part end
diff --git a/tests/model/bvconv/flags.dune b/tests/model/bvconv/flags.dune
new file mode 100644
index 000000000..28abbcb40
--- /dev/null
+++ b/tests/model/bvconv/flags.dune
@@ -0,0 +1 @@
+--ext=bvconv
diff --git a/tests/model/bvconv/int2bv.expected b/tests/model/bvconv/int2bv.expected
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/model/bvconv/int2bv.rsmt2 b/tests/model/bvconv/int2bv.rsmt2
new file mode 100644
index 000000000..5495168e2
--- /dev/null
+++ b/tests/model/bvconv/int2bv.rsmt2
@@ -0,0 +1,6 @@
+sat
+(
+  (define-fun b () (_ BitVec 5)
+    #b01101)
+)
+
diff --git a/tests/model/bvconv/int2bv.smt2 b/tests/model/bvconv/int2bv.smt2
new file mode 100644
index 000000000..d24c23a31
--- /dev/null
+++ b/tests/model/bvconv/int2bv.smt2
@@ -0,0 +1,6 @@
+(set-logic BVLIA)
+(declare-const b (_ BitVec 5))
+(assert (= b ((_ int2bv 5) 13) ))
+(check-sat)
+(get-model)
+(exit)