diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index 8fdb15e22..68607e187 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/config.h>
 #include <util/exit_codes.h>
+#include <util/help_formatter.h>
 
 #ifdef HAVE_INTERPOLATION
 #include "interpolation/interpolation_expr.h"
@@ -245,58 +246,57 @@ void ebmc_parse_optionst::help()
     "* *                     Version " EBMC_VERSION "                         * *\n"
     "* *     University of Oxford, Computer Science Department   * *\n"
     "* *                  kroening@kroening.com                  * *\n"
-    "\n"
+    "\n";
+
+  std::cout << help_formatter(
     "Usage:                             Purpose:\n"
     "\n"
-    " ebmc [-?] [-h] [--help]           show help\n"
-    " ebmc file ...                     source file names\n"
+    " {bebmc} [{y-?}] [{y-h}] [{y--help}] \t show help\n"
+    " {bebmc} {ufile} {u...}         \t source file names\n"
     "\n"
     "Additonal options:\n"
-    " --bound <nr>                      set bound (default: 1)\n"
-    // " --max-bound <nr>                  set maximum bound\n"
-    " --module <module>                 set top module (deprecated)\n"
-    " --top <module>                    set top module\n"
-    " -p <expr>                         specify a property\n"
-    " --outfile <file name>             set output file name (default: stdout)\n"
-    " --trace                           generate a trace for failing properties\n"
-    " --vcd <file name>                 generate traces in VCD format\n"
-    " --show-properties                 list the properties in the model\n"
-    " --property <id>                   check the property with given ID\n"
-    " -I path                           set include path\n"
-    " --reset <expr>                    set up module reset\n"
+    " {y--bound} {unr}               \t set bound (default: 1)\n"
+    " {y--module} {umodule}          \t set top module (deprecated)\n"
+    " {y--top} {umodule}             \t set top module\n"
+    " {y-p} {uexpr}                  \t specify a property\n"
+    " {y--outfile} {ufile name}      \t set output file name (default: stdout)\n"
+    " {y--trace}                     \t generate a trace for failing properties\n"
+    " {y--vcd} {ufile name}          \t generate traces in VCD format\n"
+    " {y--show-properties}           \t list the properties in the model\n"
+    " {y--property} {uid}            \t check the property with given ID\n"
+    " {y-I} {upath}                  \t set include path\n"
+    " {y--reset} {uexpr}             \t set up module reset\n"
     "\n"
     "Methods:\n"
-    " --k-induction                     do k-induction with k=bound\n"
-    " --bdd                             use (unbounded) BDD engine\n"
-    " --ic3 [options]                   use IC3 engine with options described below\n"
-    "       --property <nm>                  check property named <nm>\n"
-    "       --constr                         use constraints specified in 'file.cnstr'\n"
-    "       --h                              print out help information\n"
-    "       --new-mode                       new mode is switched on\n"
-    "       --aiger                          print out the instance in aiger format\n"
+    " {y--k-induction}               \t do k-induction with k=bound\n"
+    " {y--bdd}                       \t use (unbounded) BDD engine\n"
+    " {y--ic3}                       \t use IC3 engine with options described below\n"
+    "       {y--constr}              \t use constraints specified in 'file.cnstr'\n"
+    "       {y--new-mode}            \t new mode is switched on\n"
+    "       {y--aiger}               \t print out the instance in aiger format\n"
     
-    //" --interpolation                   use bit-level interpolants\n"
-    //" --interpolation-word              use word-level interpolants\n"
-    //" --diameter                        perform recurrence diameter test\n"
+    //" --interpolation                \t use bit-level interpolants\n"
+    //" --interpolation-word           \t use word-level interpolants\n"
+    //" --diameter                     \t perform recurrence diameter test\n"
     "\n"
     "Solvers:\n"
-    " --aig                             bit-level SAT with AIGs\n"
-    " --dimacs                          output bit-level CNF in DIMACS format\n"
-    " --smt1                            output word-level SMT 1 formula\n"
-    " --smt2                            output word-level SMT 2 formula\n"
-    " --boolector                       use Boolector as solver\n"
-    " --cvc4                            use CVC4 as solver\n"
-    " --mathsat                         use MathSAT as solver\n"
-    " --yices                           use Yices as solver\n"
-    " --z3                              use Z3 as solver\n"
+    " {y--aig}                       \t bit-level SAT with AIGs\n"
+    " {y--dimacs}                    \t output bit-level CNF in DIMACS format\n"
+    " {y--smt1}                      \t output word-level SMT 1 formula\n"
+    " {y--smt2}                      \t output word-level SMT 2 formula\n"
+    " {y--boolector}                 \t use Boolector as solver\n"
+    " {y--cvc4}                      \t use CVC4 as solver\n"
+    " {y--mathsat}                   \t use MathSAT as solver\n"
+    " {y--yices}                     \t use Yices as solver\n"
+    " {y--z3}                        \t use Z3 as solver\n"
     "\n"
     "Debugging options:\n"
-    " --show-parse                      show parse trees\n"
-    " --show-varmap                     show variable map\n"
-    " --show-netlist                    show netlist\n"
-    " --show-ldg                        show latch dependencies\n"
-    " --smv-netlist                     show netlist in SMV format\n"
-    " --dot-netlist                     show netlist in DOT format\n"
-    " --show-trans                      show transition system\n"
-    "\n";
+    " {y--show-parse}                \t show parse trees\n"
+    " {y--show-varmap}               \t show variable map\n"
+    " {y--show-netlist}              \t show netlist\n"
+    " {y--show-ldg}                  \t show latch dependencies\n"
+    " {y--smv-netlist}               \t show netlist in SMV format\n"
+    " {y--dot-netlist}               \t show netlist in DOT format\n"
+    " {y--show-trans}                \t show transition system\n"
+    "\n");
 }