diff --git a/regression/verilog/initial1/test.desc b/regression/verilog/initial/initial1.desc
similarity index 86%
rename from regression/verilog/initial1/test.desc
rename to regression/verilog/initial/initial1.desc
index cfd3731f6..f6ffcc859 100644
--- a/regression/verilog/initial1/test.desc
+++ b/regression/verilog/initial/initial1.desc
@@ -1,5 +1,5 @@
 CORE
-main.v
+initial1.v
 --module main --bound 2
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/verilog/initial1/main.v b/regression/verilog/initial/initial1.v
similarity index 100%
rename from regression/verilog/initial1/main.v
rename to regression/verilog/initial/initial1.v
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index f561bca9a..5e01e3ca9 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -356,9 +356,6 @@ void ebmc_parse_optionst::help()
     " {y--numbered-trace}            \t give a trace with identifiers numbered by timeframe\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--systemverilog}             \t force SystemVerilog instead of Verilog\n"
-    " {y--reset} {uexpr}             \t set up module reset\n"
     " {y--liveness-to-safety}        \t translate liveness properties to safety properties\n"
     "\n"
     "Methods:\n"
@@ -398,6 +395,13 @@ void ebmc_parse_optionst::help()
     " {y--yices}                     \t use Yices as solver\n"
     " {y--z3}                        \t use Z3 as solver\n"
     "\n"
+    "Verilog options:\n"
+    " {y-I} {upath}                  \t set include path\n"
+    " {y-D} {uvar}[={uvalue}]        \t set preprocessor define\n"
+    " {y--systemverilog}             \t force SystemVerilog instead of Verilog\n"
+    " {y--reset} {uexpr}             \t set up module reset\n"
+    " {y--ignore-initial}            \t disregard initial blocks\n"
+    "\n"
     "Debugging options:\n"
     " {y--preprocess}                \t output the preprocessed source file\n"
     " {y--show-parse}                \t show parse trees\n"
diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h
index d6abed1e8..03bb8772b 100644
--- a/src/ebmc/ebmc_parse_options.h
+++ b/src/ebmc/ebmc_parse_options.h
@@ -35,7 +35,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(outfile):(xml-ui)(verbosity):(gui)"
         "(json-modules):(json-properties):(json-result):"
         "(neural-liveness)(neural-engine):"
-        "(reset):"
+        "(reset):(ignore-initial)"
         "(version)(verilog-rtl)(verilog-netlist)"
         "(compute-interpolant)(interpolation)(interpolation-vmcai)"
         "(ic3)(property):(constr)(h)(new-mode)(aiger)"
diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp
index 899255db3..b6772f410 100644
--- a/src/ebmc/transition_system.cpp
+++ b/src/ebmc/transition_system.cpp
@@ -170,6 +170,10 @@ static bool parse(
   if(cmdline.isset('D'))
     options.set_option("defines", cmdline.get_values('D'));
 
+  // do --ignore-initial
+  if(cmdline.isset("ignore-initial"))
+    options.set_option("ignore-initial", true);
+
   language.set_language_options(options, message_handler);
 
   message.status() << "Parsing " << filename << messaget::eom;
diff --git a/src/verilog/verilog_language.cpp b/src/verilog/verilog_language.cpp
index fc6b277c1..f4f4b633d 100644
--- a/src/verilog/verilog_language.cpp
+++ b/src/verilog/verilog_language.cpp
@@ -38,6 +38,7 @@ void verilog_languaget::set_language_options(
   vl2smv_extensions = options.get_bool_option("vl2smv-extensions");
   initial_defines = options.get_list_option("defines");
   warn_implicit_nets = options.get_bool_option("warn-implicit-nets");
+  ignore_initial = options.get_bool_option("ignore-initial");
 }
 
 /*******************************************************************\
@@ -190,8 +191,14 @@ bool verilog_languaget::typecheck(
   message.debug() << "Synthesis " << module << messaget::eom;
 
   if(verilog_synthesis(
-       symbol_table, module, parse_tree.standard, message_handler, optionst{}))
+       symbol_table,
+       module,
+       parse_tree.standard,
+       ignore_initial,
+       message_handler))
+  {
     return true;
+  }
 
   return false;
 }
diff --git a/src/verilog/verilog_language.h b/src/verilog/verilog_language.h
index 0f566e91e..f565f9f05 100644
--- a/src/verilog/verilog_language.h
+++ b/src/verilog/verilog_language.h
@@ -94,6 +94,7 @@ class verilog_languaget:public languaget
   bool force_systemverilog = false;
   bool vl2smv_extensions = false;
   bool warn_implicit_nets = false;
+  bool ignore_initial = false;
   std::list<std::string> initial_defines;
   verilog_parse_treet parse_tree;
 };
diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp
index ee12837dc..fb471e806 100644
--- a/src/verilog/verilog_synthesis.cpp
+++ b/src/verilog/verilog_synthesis.cpp
@@ -1459,7 +1459,11 @@ void verilog_synthesist::synth_module_instance(
 
   // make sure the module is synthesized already
   verilog_synthesis(
-    symbol_table, module_identifier, standard, get_message_handler(), options);
+    symbol_table,
+    module_identifier,
+    standard,
+    ignore_initial,
+    get_message_handler());
 
   for(auto &instance : statement.instances())
     expand_module_instance(module_symbol, instance, trans);
@@ -1782,6 +1786,9 @@ void verilog_synthesist::synth_initial(
       << "initial module item expected to have one operand";
   }
 
+  if(ignore_initial)
+    return;
+
   construct=constructt::INITIAL;
   event_guard=event_guardt::NONE;
 
@@ -3716,12 +3723,12 @@ bool verilog_synthesis(
   symbol_table_baset &symbol_table,
   const irep_idt &module,
   verilog_standardt standard,
-  message_handlert &message_handler,
-  const optionst &options)
+  bool ignore_initial,
+  message_handlert &message_handler)
 {
   const namespacet ns(symbol_table);
   verilog_synthesist verilog_synthesis(
-    standard, ns, symbol_table, module, options, message_handler);
+    standard, ignore_initial, ns, symbol_table, module, message_handler);
   return verilog_synthesis.typecheck_main();
 }
 
@@ -3744,14 +3751,13 @@ bool verilog_synthesis(
   message_handlert &message_handler,
   const namespacet &ns)
 {
-  optionst options;
   symbol_tablet symbol_table;
 
   const auto errors_before =
     message_handler.get_message_count(messaget::M_ERROR);
 
   verilog_synthesist verilog_synthesis(
-    standard, ns, symbol_table, module_identifier, options, message_handler);
+    standard, false, ns, symbol_table, module_identifier, message_handler);
 
   try
   {
diff --git a/src/verilog/verilog_synthesis.h b/src/verilog/verilog_synthesis.h
index f5730e905..58b48403e 100644
--- a/src/verilog/verilog_synthesis.h
+++ b/src/verilog/verilog_synthesis.h
@@ -19,8 +19,8 @@ bool verilog_synthesis(
   symbol_table_baset &,
   const irep_idt &module,
   verilog_standardt,
-  message_handlert &,
-  const optionst &);
+  bool ignore_initial,
+  message_handlert &);
 
 bool verilog_synthesis(
   exprt &,
diff --git a/src/verilog/verilog_synthesis_class.h b/src/verilog/verilog_synthesis_class.h
index 8d53fab07..4c8723c6b 100644
--- a/src/verilog/verilog_synthesis_class.h
+++ b/src/verilog/verilog_synthesis_class.h
@@ -42,14 +42,14 @@ class verilog_synthesist:
 public:
   verilog_synthesist(
     verilog_standardt _standard,
+    bool _ignore_initial,
     const namespacet &_ns,
     symbol_table_baset &_symbol_table,
     const irep_idt &_module,
-    const optionst &_options,
     message_handlert &_message_handler)
     : verilog_typecheck_baset(_standard, _ns, _message_handler),
       verilog_symbol_tablet(_symbol_table),
-      options(_options),
+      ignore_initial(_ignore_initial),
       value_map(NULL),
       module(_module),
       temporary_counter(0)
@@ -69,7 +69,7 @@ class verilog_synthesist:
   [[nodiscard]] exprt synth_expr(exprt expr, symbol_statet symbol_state);
 
 protected:
-  const optionst &options;
+  bool ignore_initial;
 
   [[nodiscard]] exprt synth_expr_rec(exprt expr, symbol_statet symbol_state);