diff --git a/jbmc/regression/jbmc/nondet-static/My$PInner.class b/jbmc/regression/jbmc/nondet-static/My$PInner.class
new file mode 100644
index 00000000000..58d8d6f41f8
Binary files /dev/null and b/jbmc/regression/jbmc/nondet-static/My$PInner.class differ
diff --git a/jbmc/regression/jbmc/nondet-static/My$PSInner.class b/jbmc/regression/jbmc/nondet-static/My$PSInner.class
new file mode 100644
index 00000000000..f3432fcb033
Binary files /dev/null and b/jbmc/regression/jbmc/nondet-static/My$PSInner.class differ
diff --git a/jbmc/regression/jbmc/nondet-static/My$PrInner.class b/jbmc/regression/jbmc/nondet-static/My$PrInner.class
new file mode 100644
index 00000000000..54c96ed1500
Binary files /dev/null and b/jbmc/regression/jbmc/nondet-static/My$PrInner.class differ
diff --git a/jbmc/regression/jbmc/nondet-static/My$PrSInner.class b/jbmc/regression/jbmc/nondet-static/My$PrSInner.class
new file mode 100644
index 00000000000..2c9413cd7c3
Binary files /dev/null and b/jbmc/regression/jbmc/nondet-static/My$PrSInner.class differ
diff --git a/jbmc/regression/jbmc/nondet-static/My.class b/jbmc/regression/jbmc/nondet-static/My.class
new file mode 100644
index 00000000000..df0cb67c701
Binary files /dev/null and b/jbmc/regression/jbmc/nondet-static/My.class differ
diff --git a/jbmc/regression/jbmc/nondet-static/My.java b/jbmc/regression/jbmc/nondet-static/My.java
new file mode 100644
index 00000000000..6e8d6d86eef
--- /dev/null
+++ b/jbmc/regression/jbmc/nondet-static/My.java
@@ -0,0 +1,238 @@
+public class My {
+  public static int val() { return 3; }
+
+  public static int p1;
+  public static int p2 = 1;
+  public static int p3;
+  static { p3 = 2; }
+  public static int p4 = val();
+  public static Integer p5 = new Integer(5);
+
+  public static final int pf1 = 1;
+  public static final int pf2;
+  static { pf2 = 2; }
+  public static final int pf3 = val();
+  public static final Integer pf4 = new Integer(4);
+
+  private static int pr1;
+  private static int pr2 = 1;
+  private static int pr3;
+  static { pr3 = 2; }
+  private static int pr4 = val();
+  private static Integer pr5 = new Integer(5);
+
+  private static final int prf1 = 1;
+  private static final int prf2;
+  static { prf2 = 2; }
+  private static final int prf3 = val();
+  private static final Integer prf4 = new Integer(4);
+
+  // for inner classes, the missing cases of the above fields do not compile
+  public class PInner {
+    public static final int pf1 = 1;
+
+    private static final int prf1 = 1;
+  }
+
+  public static class PSInner {
+    public static int p1;
+    public static int p2 = 1;
+    public static int p3;
+    static { p3 = 2; }
+    public static int p4 = val();
+    public static Integer p5 = new Integer(5);
+
+    public static final int pf1 = 1;
+    public static final int pf2;
+    static { pf2 = 2; }
+    public static final int pf3 = val();
+    public static final Integer pf4 = new Integer(4);
+
+    private static int pr1;
+    private static int pr2 = 1;
+    private static int pr3;
+    static { pr3 = 2; }
+    private static int pr4 = val();
+    private static Integer pr5 = new Integer(5);
+
+    private static final int prf1 = 1;
+    private static final int prf2;
+    static { prf2 = 2; }
+    private static final int prf3 = val();
+    private static final Integer prf4 = new Integer(4);
+  }
+
+  private class PrInner {
+    public static final int pf1 = 1;
+
+    private static final int prf1 = 1;
+  }
+
+  private static class PrSInner {
+    public static int p1;
+    public static int p2 = 1;
+    public static int p3;
+    static { p3 = 2; }
+    public static int p4 = val();
+    public static Integer p5 = new Integer(5);
+
+    public static final int pf1 = 1;
+    public static final int pf2;
+    static { pf2 = 2; }
+    public static final int pf3 = val();
+    public static final Integer pf4 = new Integer(4);
+
+    private static int pr1;
+    private static int pr2 = 1;
+    private static int pr3;
+    static { pr3 = 2; }
+    private static int pr4 = val();
+    private static Integer pr5 = new Integer(5);
+
+    private static final int prf1 = 1;
+    private static final int prf2;
+    static { prf2 = 2; }
+    private static final int prf3 = val();
+    private static final Integer prf4 = new Integer(4);
+  }
+
+  public int field;
+  public My(int i) {
+    String s = "bla";
+    field = i;
+    if (p1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (p2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (p3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (p4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!p5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (pf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (pf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!pf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (pr1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (pr2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (pr3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (pr4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!pr5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (prf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (prf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!prf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PInner.pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PInner.prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PSInner.p1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.p2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.p3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.p4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!PSInner.p5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (PSInner.pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PSInner.pf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PSInner.pf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!PSInner.pf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PSInner.pr1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.pr2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.pr3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.pr4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!PSInner.pr5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (PSInner.prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PSInner.prf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PSInner.prf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!PSInner.prf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PrInner.pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PrInner.prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PrSInner.p1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.p2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.p3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.p4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!PrSInner.p5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (PrSInner.pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PrSInner.pf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PrSInner.pf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!PrSInner.pf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PrSInner.pr1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.pr2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.pr3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.pr4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!PrSInner.pr5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (PrSInner.prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PrSInner.prf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PrSInner.prf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!PSInner.prf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (s != "bla")
+      field = 108; // this line cannot be covered even with nondet-static
+  }
+}
diff --git a/jbmc/regression/jbmc/nondet-static/test.desc b/jbmc/regression/jbmc/nondet-static/test.desc
new file mode 100644
index 00000000000..36b8fd59718
--- /dev/null
+++ b/jbmc/regression/jbmc/nondet-static/test.desc
@@ -0,0 +1,70 @@
+CORE symex-driven-lazy-loading-expected-failure
+My.class
+--function "My.<init>" --cover location --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+file My\.java line 104 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 106 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 108 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 110 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 112 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 117 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 119 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 121 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 124 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 126 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 128 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 130 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 132 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 137 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 139 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 141 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 150 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 152 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 154 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 156 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 158 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 163 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 165 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 167 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 170 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 172 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 174 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 176 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 178 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 183 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 185 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 187 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 196 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 198 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 200 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 202 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 204 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 209 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 211 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 213 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 216 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 218 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 220 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 222 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 224 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 229 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 231 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 233 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 236 function java::My\.\<init\>:\(I\)V.*FAILED$
+--
+file My\.java line 115 function java::My\.\<init\>:\(I\)V
+file My\.java line 135 function java::My\.\<init\>:\(I\)V
+file My\.java line 144 function java::My\.\<init\>:\(I\)V
+file My\.java line 147 function java::My\.\<init\>:\(I\)V
+file My\.java line 161 function java::My\.\<init\>:\(I\)V
+file My\.java line 181 function java::My\.\<init\>:\(I\)V
+file My\.java line 190 function java::My\.\<init\>:\(I\)V
+file My\.java line 193 function java::My\.\<init\>:\(I\)V
+file My\.java line 207 function java::My\.\<init\>:\(I\)V
+file My\.java line 227 function java::My\.\<init\>:\(I\)V
+--
+This tests nondet-static option
+
+This fails under symex-driven lazy loading because nondet-static cannot be used
+with it
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index e92d1906167..f8bc2e396bc 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -645,6 +645,8 @@ void java_bytecode_convert_classt::convert(
     // link matches the method used by java_bytecode_convert_method::convert
     // for methods.
     new_symbol.type.set(ID_C_class, class_symbol.name);
+    new_symbol.type.set(ID_C_field, f.name);
+    new_symbol.type.set(ID_C_constant, f.is_final);
     new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
       "."+id2string(f.name);
     new_symbol.mode=ID_java;
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index 8499e5913e6..c08a914bd88 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -157,6 +157,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   else
     java_cp_include_files=".*";
 
+  nondet_static = cmd.isset("nondet-static");
+
   language_options_initialized=true;
 }
 
@@ -1029,9 +1031,18 @@ bool java_bytecode_languaget::convert_single_method(
     case synthetic_method_typet::STATIC_INITIALIZER_WRAPPER:
       if(threading_support)
         symbol.value = get_thread_safe_clinit_wrapper_body(
-          function_id, symbol_table);
+          function_id,
+          symbol_table,
+          nondet_static,
+          object_factory_parameters,
+          get_pointer_type_selector());
       else
-        symbol.value = get_clinit_wrapper_body(function_id, symbol_table);
+        symbol.value = get_clinit_wrapper_body(
+          function_id,
+          symbol_table,
+          nondet_static,
+          object_factory_parameters,
+          get_pointer_type_selector());
       break;
     case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:
       symbol.value =
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h
index 20885ed689c..387ac57db04 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.h
+++ b/jbmc/src/java_bytecode/java_bytecode_language.h
@@ -192,6 +192,7 @@ class java_bytecode_languaget:public languaget
   bool throw_assertion_error;
   java_string_library_preprocesst string_preprocess;
   std::string java_cp_include_files;
+  bool nondet_static;
 
   // list of classes to force load even without reference from the entry point
   std::vector<irep_idt> java_load_classes;
diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
index b4daf706820..2c1d1c27346 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.cpp
+++ b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -180,14 +180,25 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 
 /// Generates codet that iterates through the base types of the class specified
 /// by class_name, C, and recursively adds calls to their clinit wrapper.
-/// Finally a call to the clinint wrapper of C is made.
+/// Finally a call to the clinit of C is made. If nondet-static option was
+/// given then all static variables that are not constants (i.e. final) are
+/// then re-assigned to a nondet value.
 /// \param symbol_table: symbol table
 /// \param class_name: name of the class to generate clinit wrapper calls for
 /// \param [out] init_body: appended with calls to clinit wrapper
+/// \param nondet_static: true if nondet-static option was given
+/// \param object_factory_parameters: object factory parameters used to populate
+///   nondet-initialized globals and objects reachable from them (only needed
+///   if nondet-static is true)
+/// \param pointer_type_selector: used to choose concrete types for abstract-
+///   typed globals and fields (only needed if nondet-static is true)
 static void clinit_wrapper_do_recursive_calls(
-  const symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   const irep_idt &class_name,
-  code_blockt &init_body)
+  code_blockt &init_body,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector)
 {
   const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
   for(const auto &base : to_class_type(class_symbol.type).bases())
@@ -210,6 +221,52 @@ static void clinit_wrapper_do_recursive_calls(
     call_real_init.function() = find_sym_it->second.symbol_expr();
     init_body.move_to_operands(call_real_init);
   }
+
+  // If nondet-static option is given, add a standard nondet initialization for
+  // each non-final static field of this class. Note this is the same invocation
+  // used in get_stub_initializer_body and java_static_lifetime_init.
+  if(nondet_static)
+  {
+    object_factory_parameterst parameters = object_factory_parameters;
+    parameters.function_id = clinit_wrapper_name(class_name);
+
+    std::vector<irep_idt> nondet_ids;
+    std::for_each(
+      symbol_table.symbols.begin(),
+      symbol_table.symbols.end(),
+      [&](const std::pair<irep_idt, symbolt> &symbol) {
+        if(
+          symbol.second.type.get(ID_C_class) == class_name &&
+          symbol.second.is_static_lifetime &&
+          !symbol.second.type.get_bool(ID_C_constant))
+        {
+          nondet_ids.push_back(symbol.first);
+        }
+      });
+
+    for(const auto &id : nondet_ids)
+    {
+      const symbol_exprt new_global_symbol =
+        symbol_table.lookup_ref(id).symbol_expr();
+
+      parameters.max_nonnull_tree_depth =
+        is_non_null_library_global(id)
+          ? std::max(
+              size_t(1), object_factory_parameters.max_nonnull_tree_depth)
+          : object_factory_parameters.max_nonnull_tree_depth;
+
+      gen_nondet_init(
+        new_global_symbol,
+        init_body,
+        symbol_table,
+        source_locationt(),
+        false,
+        allocation_typet::DYNAMIC,
+        parameters,
+        pointer_type_selector,
+        update_in_placet::NO_UPDATE_IN_PLACE);
+    }
+  }
 }
 
 /// Checks whether a static initializer wrapper is needed for a given class,
@@ -316,9 +373,9 @@ static void create_clinit_wrapper_symbols(
     "clinit wrapper");
 }
 
-/// Thread safe version of the static initialiser.
+/// Thread safe version of the static initializer.
 ///
-/// Produces the static initialiser wrapper body for the given function. This
+/// Produces the static initializer wrapper body for the given function. This
 /// static initializer implements (a simplification of) the algorithm defined
 /// in Section 5.5 of the JVM Specs. This function, or wrapper, checks whether
 /// static init has already taken place, calls the actual `<clinit>` method if
@@ -365,7 +422,8 @@ static void create_clinit_wrapper_symbols(
 ///   // ...
 ///   java::In::clinit_wrapper();
 ///
-///   java::C::<clinit>();
+///   java::C::<clinit>();  // or nondet-initialization of all static
+///                         // variables of C if nondet-static is true
 ///
 ///   // Setting this variable to INIT_COMPLETE will let other threads "cross"
 ///   // beyond the assume() statement above in this function.
@@ -382,10 +440,19 @@ static void create_clinit_wrapper_symbols(
 /// \param function_id: clinit wrapper function id (the wrapper_method_symbol
 ///   name created by `create_clinit_wrapper_symbols`)
 /// \param symbol_table: global symbol table
-/// \return the body of the static initialiser wrapper
+/// \param nondet_static: true if nondet-static option was given
+/// \param object_factory_parameters: object factory parameters used to populate
+///   nondet-initialized globals and objects reachable from them (only needed
+///   if nondet-static is true)
+/// \param pointer_type_selector: used to choose concrete types for abstract-
+///   typed globals and fields (only needed if nondet-static is true)
+/// \return the body of the static initializer wrapper
 codet get_thread_safe_clinit_wrapper_body(
   const irep_idt &function_id,
-  symbol_table_baset &symbol_table)
+  symbol_table_baset &symbol_table,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector)
 {
   const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
   irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
@@ -532,11 +599,18 @@ codet get_thread_safe_clinit_wrapper_body(
   //  // ...
   //  java::In::clinit_wrapper();
   //
-  //  java::C::<clinit>();
+  //  java::C::<clinit>(); // or nondet-initialization of all static
+  //                       // variables of C if nondet-static is true
   //
   {
     code_blockt init_body;
-    clinit_wrapper_do_recursive_calls(symbol_table, class_name, init_body);
+    clinit_wrapper_do_recursive_calls(
+      symbol_table,
+      class_name,
+      init_body,
+      nondet_static,
+      object_factory_parameters,
+      pointer_type_selector);
     function_body.append(init_body);
   }
 
@@ -557,15 +631,24 @@ codet get_thread_safe_clinit_wrapper_body(
   return function_body;
 }
 
-/// Produces the static initialiser wrapper body for the given function.
+/// Produces the static initializer wrapper body for the given function.
 /// Note: this version of the clinit wrapper is not thread safe.
 /// \param function_id: clinit wrapper function id (the wrapper_method_symbol
 ///   name created by `create_clinit_wrapper_symbols`)
 /// \param symbol_table: global symbol table
-/// \return the body of the static initialiser wrapper/
+/// \param nondet_static: true if nondet-static option was given
+/// \param object_factory_parameters: object factory parameters used to populate
+///   nondet-initialized globals and objects reachable from them (only needed
+///   if nondet-static is true)
+/// \param pointer_type_selector: used to choose concrete types for abstract-
+///   typed globals and fields (only needed if nondet-static is true)
+/// \return the body of the static initializer wrapper
 codet get_clinit_wrapper_body(
   const irep_idt &function_id,
-  symbol_table_baset &symbol_table)
+  symbol_table_baset &symbol_table,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector)
 {
   // Assume that class C extends class C' and implements interfaces
   // I1, ..., In. We now create the following function (possibly recursively
@@ -583,7 +666,8 @@ codet get_clinit_wrapper_body(
   //     // ...
   //     java::In::clinit_wrapper();
   //
-  //     java::C::<clinit>();
+  //     java::C::<clinit>(); // or nondet-initialization of all static
+  //                          // variables of C if nondet-static is true
   //   }
   // }
   const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
@@ -609,7 +693,13 @@ codet get_clinit_wrapper_body(
   code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
   init_body.move_to_operands(set_already_run);
 
-  clinit_wrapper_do_recursive_calls(symbol_table, class_name, init_body);
+  clinit_wrapper_do_recursive_calls(
+    symbol_table,
+    class_name,
+    init_body,
+    nondet_static,
+    object_factory_parameters,
+    pointer_type_selector);
 
   wrapper_body.then_case() = init_body;
 
diff --git a/jbmc/src/java_bytecode/java_static_initializers.h b/jbmc/src/java_bytecode/java_static_initializers.h
index f8daab5b0cd..471ce646a2a 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.h
+++ b/jbmc/src/java_bytecode/java_static_initializers.h
@@ -29,11 +29,17 @@ void create_static_initializer_wrappers(
 
 codet get_thread_safe_clinit_wrapper_body(
   const irep_idt &function_id,
-  symbol_table_baset &symbol_table);
+  symbol_table_baset &symbol_table,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector);
 
 codet get_clinit_wrapper_body(
   const irep_idt &function_id,
-  symbol_table_baset &symbol_table);
+  symbol_table_baset &symbol_table,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector);
 
 class stub_global_initializer_factoryt
 {
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index cdcb16b6062..abcfc87057b 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -124,6 +124,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("cover"))
     parse_cover_options(cmdline, options);
 
+  if(cmdline.isset("nondet-static"))
+    options.set_option("nondet-static", true);
+
   if(cmdline.isset("no-simplify"))
     options.set_option("simplify", false);
 
@@ -1095,6 +1098,10 @@ void jbmc_parse_optionst::help()
     "                              will be restricted to loaded methods in this case,\n" // NOLINT(*)
     "                              and only output after the symex phase.\n"
     "\n"
+    "Semantic transformations:\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --nondet-static              add nondeterministic initialization of variables with static lifetime\n"
+    "\n"
     "BMC options:\n"
     HELP_BMC
     "\n"
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
index b4fab93735c..d0c5ad3d094 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.h
+++ b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -67,6 +67,7 @@ class optionst;
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(verbosity):" \
+  "(nondet-static)" \
   "(version)" \
   "(cover):(symex-coverage-report):" \
   OPT_TIMESTAMP \
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 42a1d7c447f..321802c8abe 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -351,6 +351,7 @@ IREP_ID_TWO(power, **)
 IREP_ID_ONE(factorial_power)
 IREP_ID_ONE(pretty_name)
 IREP_ID_TWO(C_class, #class)
+IREP_ID_TWO(C_field, #field)
 IREP_ID_TWO(C_interface, #interface)
 IREP_ID_ONE(event)
 IREP_ID_ONE(designated_initializer)