diff --git a/CHANGES.md b/CHANGES.md
index 8ef6907ddd670cffbdc2e8224088bf33ecde8641..736ba5e11597f5dc1d406eafb1dfdfd7cc111fa9 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,7 +1,7 @@
  ## Unreleased
 
-- Add --define (or --def) to define the value of a declared constant from
-  the command line.
+- Add command line option --define (or -D) to define the value of a declared
+  constant in any specification file to verify.
 
 # 0.2.1 (19-09-2023)
 
diff --git a/src/main.ml b/src/main.ml
index f41eb638ac6f26798c86f819785dacc5ef045a9b..29663b778a7f28e3a05c02bf68d9c98c231e75ab 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -261,8 +261,8 @@ let verify_cmd =
     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")
+      & opt_all (pair ~sep:':' string string) []
+      & info [ "D"; "define" ] ~doc ~docv:"name:value")
   in
   let files =
     let doc = "File(s) to verify." in
diff --git a/tests/define.t b/tests/define.t
index 058ca5b9cec6088769057c1b101780453f2f0ffb..0da98bda32fa10d16d7f2c6b2849b6284fc91279 100644
--- a/tests/define.t
+++ b/tests/define.t
@@ -14,13 +14,13 @@ Test interpretation of on-the-fly definition of toplevel constants
   > end
   > EOF
 
-  $ caisar verify --prover PyRAT file.mlw --def n:1 --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
+  $ caisar verify --prover PyRAT file.mlw -D 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
+  $ caisar verify --prover PyRAT file.mlw -Dn:2 2>&1 | ./filter_tmpdir.sh
   [ERROR] Invalid argument: No neural network model found in task
 
   $ cat > file.mlw <<EOF
@@ -33,13 +33,13 @@ Test interpretation of on-the-fly definition of toplevel constants
   > end
   > EOF
 
-  $ caisar verify --prover PyRAT file.mlw --def n:foo --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
+  $ caisar verify --prover PyRAT file.mlw -D 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
+  $ caisar verify --prover PyRAT file.mlw -D n:bar 2>&1 | ./filter_tmpdir.sh
   [ERROR] Invalid argument: No neural network model found in task
 
   $ cat > file.mlw <<EOF
@@ -50,13 +50,13 @@ Test interpretation of on-the-fly definition of toplevel constants
   > end
   > EOF
 
-  $ caisar verify --prover PyRAT file.mlw --def n:1.0 --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
+  $ caisar verify --prover PyRAT file.mlw -D 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
+  $ caisar verify --prover PyRAT file.mlw -D n:foo 2>&1 | ./filter_tmpdir.sh
   [ERROR] 'n' expects a numerical constant, got 'foo' instead
 
   $ cat > file.mlw <<EOF
@@ -67,11 +67,11 @@ Test interpretation of on-the-fly definition of toplevel constants
   > end
   > EOF
 
-  $ caisar verify --prover PyRAT file.mlw --def n:true --ltag=InterpretGoal 2>&1 | ./filter_tmpdir.sh
+  $ caisar verify --prover PyRAT file.mlw -D 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
+  $ caisar verify --prover PyRAT file.mlw -D n:false 2>&1 | ./filter_tmpdir.sh
   [ERROR] Invalid argument: No neural network model found in task