diff --git a/CHANGES.md b/CHANGES.md
index 03525f62fca4491151c92b65c7c2d315a6c4e912..8206a7aa3598b90b080eaa010073de7cef068ecc 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,8 @@
+# Unreleased
+
+- Add `--define` (or `--def`) to define the value of a declared constant from
+  the command line.
+
 # 0.2 (19-06-2023)
 
 - [prover] Integration of the [nnenum](https://github.com/stanleybak/nnenum)
diff --git a/src/interpretation.ml b/src/interpretation.ml
index f7901c003c85f8663cf340d7d436c3cd4c8806a9..a5850f2a0906f53d3e523b30de9eee02271cd815 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -378,7 +378,58 @@ let declare_language_lsymbols caisar_env task =
       else task)
     caisar_env.caisar_op_of_ls task
 
-let interpret_task ~cwd env task =
+let builtin_of_constant known_map (name, value) =
+  let decls =
+    Ident.Mid.fold_left
+      (fun acc id ls ->
+        if String.equal id.Ident.id_string name then ls :: acc else acc)
+      [] known_map
+  in
+  match decls with
+  | [] ->
+    Logging.user_error (fun m ->
+      m "'%s' is not a declared toplevel constant" name)
+  | _ :: _ :: _ ->
+    Logging.user_error (fun m ->
+      m "'%s' corresponds to multiple declared toplevel constants" name)
+  | [ { Decl.d_node = Dparam ls; _ } ] ->
+    let cst =
+      match ls.Term.ls_value with
+      | None -> (
+        match value with
+        | "true" -> Term.t_true
+        | "false" -> Term.t_false
+        | _ ->
+          Logging.user_error (fun m ->
+            m "'%s' expects 'true' or 'false', got '%s' instead" name value))
+      | Some ty when Ty.ty_equal ty Ty.ty_int || Ty.ty_equal ty Ty.ty_real ->
+        let lb = Lexing.from_string value in
+        Loc.set_file (Fmt.str "constant '%s' to be bound to '%s'" value name) lb;
+        let parsed = Lexer.parse_term lb in
+        let cst =
+          match parsed.term_desc with
+          | Ptree.Tconst cst -> cst
+          | _ ->
+            Logging.user_error (fun m ->
+              m "'%s' expects a numerical constant, got '%s' instead" name value)
+        in
+        Term.t_const cst ty
+      | Some ty when Ty.ty_equal ty Ty.ty_str ->
+        let cst = Constant.ConstStr value in
+        Term.t_const cst ty
+      | Some ty ->
+        Logging.not_implemented_yet (fun m ->
+          m
+            "'%s' has type '%a' but only toplevel constants of type bool, int, \
+             real and string can be defined"
+            name Pretty.print_ty ty)
+    in
+    (ls, fun _ _ _ _ -> CRE.Eval cst)
+  | _ ->
+    Logging.user_error (fun m ->
+      m "'%s' does not appear to be a declared toplevel constant" name)
+
+let interpret_task ~cwd ?(def_constants = []) env task =
   let known_map = Task.task_known task in
   let caisar_env = caisar_env env cwd in
   let params =
@@ -389,8 +440,10 @@ let interpret_task ~cwd env task =
       compute_max_quantifier_domain = Int.max_value;
     }
   in
+  let builtins = List.map ~f:(builtin_of_constant known_map) def_constants in
   let engine =
-    CRE.create ~bounded_quant params env known_map caisar_env caisar_builtins
+    CRE.create ~bounded_quant ~builtins params env known_map caisar_env
+      caisar_builtins
   in
   let g, f = (Task.task_goal task, Task.task_goal_fmla task) in
   let f = CRE.normalize ~limit:Int.max_value engine Term.Mvs.empty f in
diff --git a/src/interpretation.mli b/src/interpretation.mli
index 7804381528b17e3a450ad74b22f309f1e1a3706c..bb5c94f5c94a6838b5eb95709e9fb871cd62c651 100644
--- a/src/interpretation.mli
+++ b/src/interpretation.mli
@@ -22,4 +22,9 @@
 
 open Why3
 
-val interpret_task : cwd:string -> Env.env -> Task.task -> Task.task
+val interpret_task :
+  cwd:string ->
+  ?def_constants:(string * string) list ->
+  Env.env ->
+  Task.task ->
+  Task.task
diff --git a/src/logging.ml b/src/logging.ml
index 7318b5b8a4d2167bba85c17596b7de1ed3ef9d8a..78b3cfd9a8f5a9e2f8f6f12525da604e07d07368 100644
--- a/src/logging.ml
+++ b/src/logging.ml
@@ -68,3 +68,47 @@ let setup style_renderer level srcs =
   List.iter (fun src -> Logs.Src.set_level src (Some Debug)) srcs;
   Fmt_tty.setup_std_outputs ?style_renderer ();
   Logs.set_reporter reporter
+
+exception Code_error
+
+let code_error ?src f =
+  Logs.err ?src f;
+  Logs.err ?src (fun fmt ->
+    fmt
+      "Unrecoverable error:@ please report@ the issue at@ \
+       https://git.frama-c.com/pub/caisar/issues");
+  raise Code_error
+
+exception User_error
+
+let user_error ?src f =
+  Logs.err ?src f;
+  raise User_error
+
+exception Not_implemented_yet
+
+let not_implemented_yet ?src f =
+  Logs.err ?src f;
+  Logs.err ?src (fun fmt ->
+    fmt
+      "Unimplemented feature:@ you may send a@ feature request at@ \
+       https://git.frama-c.com/pub/caisar/issues");
+  raise Not_implemented_yet
+
+let protect_main f =
+  try f () with
+  | (User_error | Code_error | Not_implemented_yet)
+    when not (is_debug_level src_stack_trace) ->
+    ()
+  | exn when not (is_debug_level src_stack_trace) ->
+    Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)
+
+let () =
+  (* We register custom printers for a selection of exceptions otherwise Why3
+     will print the related messages as "anomaly: <exception with message>". *)
+  Why3.Exn_printer.register (fun fmt exn ->
+    match exn with
+    | Invalid_argument msg -> Fmt.pf fmt "Invalid argument: %s" msg
+    | Failure msg -> Fmt.pf fmt "Failure: %s" msg
+    | Sys_error msg -> Fmt.pf fmt "%s" msg
+    | _ -> raise exn)
diff --git a/src/logging.mli b/src/logging.mli
index 8b03ff2d74b3d06d63f643c83eade57fa0216e64..7ebf4c3c0d2b0059b19927df38b52ec064779db6 100644
--- a/src/logging.mli
+++ b/src/logging.mli
@@ -33,7 +33,18 @@ val all_srcs : unit -> Logs.src list
 
 (** {2 Logs} *)
 
-val is_debug_level : Logs.src -> bool
-
 val setup :
   Fmt.style_renderer option -> Logs.level option -> Logs.src list -> unit
+
+val is_debug_level : Logs.src -> bool
+
+val code_error : ?src:Logs.src -> (_, unit) Logs.msgf -> 'b
+(** Terminate execution with a [code error] message. *)
+
+val user_error : ?src:Logs.src -> (_, unit) Logs.msgf -> 'b
+(** Terminate execution with a [user error] message. *)
+
+val not_implemented_yet : ?src:Logs.src -> (_, unit) Logs.msgf -> 'b
+(** Terminate execution with a [not implemented yet] message. *)
+
+val protect_main : (unit -> unit) -> unit
diff --git a/src/main.ml b/src/main.ml
index fdd445b4b57006bba20f40e158802a8eec01a564..61f910b127874f4787ce94af33560448779ac2cc 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -124,14 +124,14 @@ let log_theory_answer =
           additional_info)))
 
 let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
-  files =
+  ?def_constants files =
   let memlimit = Option.map memlimit ~f:memlimit_of_string in
   let timelimit = Option.map timelimit ~f:timelimit_of_string in
   let theory_answers =
     List.map files
       ~f:
         (Verification.verify ?format ~loadpath ?memlimit ?timelimit ?dataset
-           prover ?prover_altern)
+           prover ?prover_altern ?def_constants)
   in
   List.iter theory_answers ~f:log_theory_answer;
   theory_answers
@@ -182,7 +182,7 @@ let verify_json ?memlimit ?timelimit ?outfile json =
   let infile = Result.ok_or_failwith (Verification.File.of_json_input jin) in
   let verification_results =
     verify ~loadpath:[] ?memlimit ?timelimit ~dataset:jin.property.dataset
-      jin.prover [ infile ]
+      jin.prover ~def_constants:[] [ infile ]
   in
   match verification_results with
   | [] -> assert false (* We always build one theory from the provided JSON. *)
@@ -233,6 +233,13 @@ let config_cmd =
   in
   Cmd.v info term
 
+let define_constants =
+  let doc = "Define a declared constant with the given value." in
+  Arg.(
+    value
+    & opt_all (Arg.pair ~sep:':' string string) []
+    & info [ "define"; "def" ] ~doc ~docv:"name:value")
+
 let memlimit =
   let doc =
     "Memory limit. $(docv) is intended in megabytes (MB) by default, but \
@@ -305,15 +312,16 @@ let verify_cmd =
           prover
           prover_altern
           dataset
+          def_constants
           files
           _
         ->
         exec_cmd cmdname (fun () ->
           ignore
             (verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover
-               ?prover_altern files)))
+               ?prover_altern ~def_constants files)))
       $ format $ loadpath $ memlimit $ timelimit $ prover $ prover_altern
-      $ dataset $ files $ setup_logs)
+      $ dataset $ define_constants $ files $ setup_logs)
   in
   Cmd.v info term
 
@@ -401,7 +409,7 @@ let default_info =
       `S "MORE HELP";
       `P "Use `$(mname) $(i,COMMAND) --help' for help on a single command.";
       `S Manpage.s_bugs;
-      `P "Email bug reports to <...>";
+      `P "Submit bug reports to https://git.frama-c.com/pub/caisar/issues";
     ]
   in
   let version = "0.2" in
@@ -411,19 +419,7 @@ let default_info =
 let default_cmd = Term.(ret (const (fun _ -> `Help (`Pager, None)) $ const ()))
 
 let () =
-  (* We register custom printers for a selection of exceptions otherwise Why3
-     will print the related messages as "anomaly: <exception with message>". *)
-  Why3.Exn_printer.register (fun fmt exn ->
-    match exn with
-    | Invalid_argument msg -> Fmt.pf fmt "Invalid argument: %s" msg
-    | Failure msg -> Fmt.pf fmt "Failure: %s" msg
-    | Sys_error msg -> Fmt.pf fmt "%s" msg
-    | _ -> raise exn)
-
-let () =
-  try
+  Logging.protect_main (fun () ->
     Cmd.group ~default:default_cmd default_info
       [ config_cmd; verify_cmd; verify_json_cmd; verify_xgboost_cmd ]
-    |> Cmd.eval ~catch:false |> Caml.exit
-  with exn when not Logging.(is_debug_level src_stack_trace) ->
-    Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)
+    |> Cmd.eval ~catch:false |> Caml.exit)
diff --git a/src/reduction_engine.ml b/src/reduction_engine.ml
index 89119d3d82960ed241fcf4cfc43990d760a0aa5d..23965c77d9428b874a2e33a7ec4139c19c0e7019 100644
--- a/src/reduction_engine.ml
+++ b/src/reduction_engine.ml
@@ -1391,8 +1391,8 @@ let normalize ?step_limit ~limit engine sigma t0 =
 
 (* the rewrite engine *)
 
-let create ?(bounded_quant = fun _ _ ~cond:_ -> None) p env km user_env
-  built_in_user =
+let create ?(bounded_quant = fun _ _ ~cond:_ -> None) ?(builtins = []) p env km
+  user_env built_in_user =
   let th = Env.read_theory env [ "int" ] "Int" in
   let ls_lt = Theory.ns_find_ls th.Theory.th_export [ Ident.op_infix "<" ] in
   let env =
@@ -1408,6 +1408,7 @@ let create ?(bounded_quant = fun _ _ ~cond:_ -> None) p env km user_env
     }
   in
   if p.compute_builtin then get_builtins env built_in_user;
+  List.iter (fun (ls, f) -> Hls.add env.builtins ls f) builtins;
   env
 
 exception NotARewriteRule of string
diff --git a/src/reduction_engine.mli b/src/reduction_engine.mli
index 0668f3e44105a7aeb4985cc98a44cb2fab6f9883..68bbefaef429f50c78270c1fe3c2dc871082bbe1 100644
--- a/src/reduction_engine.mli
+++ b/src/reduction_engine.mli
@@ -115,6 +115,7 @@ type 'a bounded_quant =
 
 val create :
   ?bounded_quant:'a bounded_quant ->
+  ?builtins:(Why3.Term.lsymbol * 'a builtin) list ->
   params ->
   Env.env ->
   Decl.decl Ident.Mid.t ->
diff --git a/src/verification.ml b/src/verification.ml
index 5b7a808c35423e8fa57972879c4b9901874553cf..a6c4682711f67a15f82333c7caa873edc3c211b8 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -270,8 +270,8 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
   let additional_info = Generic None in
   (prover_answer, additional_info)
 
-let call_prover ~cwd ~limit config env prover config_prover driver ?dataset task
-    =
+let call_prover ~cwd ~limit config env prover config_prover driver ?dataset
+  def_constants task =
   let prover_answer, additional_info =
     match prover with
     | Prover.Saver -> answer_saver limit config env config_prover dataset task
@@ -280,12 +280,12 @@ let call_prover ~cwd ~limit config env prover config_prover driver ?dataset task
       let dataset = Unix.realpath (Option.value_exn dataset) in
       answer_dataset limit config env prover config_prover driver dataset task
     | Marabou | Pyrat | Nnenum | ABCrown ->
-      let task = Interpretation.interpret_task ~cwd env task in
+      let task = Interpretation.interpret_task ~cwd env ~def_constants task in
       let proof_strategy = Proof_strategy.apply_native_nn_prover in
       answer_generic limit config prover config_prover driver ~proof_strategy
         task
     | CVC5 ->
-      let task = Interpretation.interpret_task ~cwd env task in
+      let task = Interpretation.interpret_task ~cwd env ~def_constants task in
       let proof_strategy = Proof_strategy.apply_classic_prover env in
       answer_generic limit config prover config_prover driver ~proof_strategy
         task
@@ -306,7 +306,7 @@ let open_file ?format env file =
     (Unix.getcwd () (* TODO *), Wstdlib.Mstr.singleton th.th_name.id_string th)
 
 let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
-  file =
+  ?(def_constants = []) file =
   let debug = Logging.(is_debug_level src_prover_call) in
   (if debug then Debug.(set_flag (lookup_flag "call_prover")));
   let env, config = create_env loadpath in
@@ -368,6 +368,7 @@ let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
       let tasks = Task.split_theory theory None None in
       List.map
         ~f:
-          (call_prover ~cwd ~limit main env prover config_prover driver ?dataset)
+          (call_prover ~cwd ~limit main env prover config_prover driver ?dataset
+             def_constants)
         tasks)
     mstr_theory
diff --git a/src/verification.mli b/src/verification.mli
index 06a39fa83af9597bb2a104420b33098f9a5f6566..bc46c5784d4dff1dcec391a0d5b081a79b23f151 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -54,6 +54,7 @@ val verify :
   ?dataset:string ->
   Prover.t ->
   ?prover_altern:string ->
+  ?def_constants:(string * string) list ->
   File.t ->
   verification_result
 (** [verify ?debug ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern file]
@@ -69,6 +70,7 @@ val verify :
       is the filepath of a dataset (eg, in CSV format) possibly appearing in
       [file].
     @param prover_altern is the alternative [prover] configuration.
+    @param def_constants is a key:value list defining toplevel constants.
     @return
       for each theory, an [answer] for each goal of the theory, respecting the
       order of appearance. *)
diff --git a/tests/define.t b/tests/define.t
new file mode 100644
index 0000000000000000000000000000000000000000..b698beb81e1d88d7926f59610d0a8cd501fdbe54
--- /dev/null
+++ b/tests/define.t
@@ -0,0 +1,80 @@
+Test interpretation of on-the-fly definition of toplevel constants
+
+  $ chmod u+x bin/pyrat.py
+
+  $ bin/pyrat.py --version
+  PyRAT 1.1
+
+  $ PATH=$(pwd)/bin:$PATH
+
+  $ cat > file.mlw <<EOF
+  > theory T
+  >   use int.Int
+  > 
+  >   constant n: int
+  > 
+  >   goal G: 1 = n
+  > end
+  > EOF
+
+  $ caisar verify --prover PyRAT file.mlw --def n:1 --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
+  [DEBUG]{InterpretGoal} Interpreted formula for goal 'G':
+  true
+  
+  [ERROR] Invalid argument: No neural network model found in task
+
+  $ caisar verify --prover PyRAT file.mlw --def n:2 2>&1 | ./filter_tmpdir.sh
+  [ERROR] Invalid argument: No neural network model found in task
+
+  $ cat > file.mlw <<EOF
+  > theory T
+  >   use int.Int
+  > 
+  >   constant n: string
+  > 
+  >   goal G: n = "foo"
+  > end
+  > EOF
+
+  $ caisar verify --prover PyRAT file.mlw --def n:foo --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
+  [DEBUG]{InterpretGoal} Interpreted formula for goal 'G':
+  true
+  
+  [ERROR] Invalid argument: No neural network model found in task
+
+  $ caisar verify --prover PyRAT file.mlw --def n:bar 2>&1 | ./filter_tmpdir.sh
+  [ERROR] Invalid argument: No neural network model found in task
+
+  $ cat > file.mlw <<EOF
+  > theory T
+  >   constant n: real
+  > 
+  >   goal G: n = 1.0
+  > end
+  > EOF
+
+  $ caisar verify --prover PyRAT file.mlw --def n:1.0 --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
+  [DEBUG]{InterpretGoal} Interpreted formula for goal 'G':
+  true
+  
+  [ERROR] Invalid argument: No neural network model found in task
+
+  $ caisar verify --prover PyRAT file.mlw --def n:foo 2>&1 | ./filter_tmpdir.sh
+  [ERROR] 'n' expects a numerical constant, got 'foo' instead
+
+  $ cat > file.mlw <<EOF
+  > theory T
+  >   predicate n
+  > 
+  >   goal G: n
+  > end
+  > EOF
+
+  $ caisar verify --prover PyRAT file.mlw --def n:true --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
+  [DEBUG]{InterpretGoal} Interpreted formula for goal 'G':
+  true
+  
+  [ERROR] Invalid argument: No neural network model found in task
+
+  $ caisar verify --prover PyRAT file.mlw --def n:false 2>&1 | ./filter_tmpdir.sh
+  [ERROR] Invalid argument: No neural network model found in task