diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile
index 4735583b0b0..ea2a100d6d3 100644
--- a/jbmc/src/java_bytecode/Makefile
+++ b/jbmc/src/java_bytecode/Makefile
@@ -26,6 +26,7 @@ SRC = bytecode_info.cpp \
       java_entry_point.cpp \
       java_local_variable_table.cpp \
       java_object_factory.cpp \
+      java_object_factory_parameters.cpp \
       java_pointer_casts.cpp \
       java_qualifiers.cpp \
       java_root_class.cpp \
@@ -35,7 +36,6 @@ SRC = bytecode_info.cpp \
       java_types.cpp \
       java_utils.cpp \
       load_method_by_regex.cpp \
-      object_factory_parameters.cpp \
       mz_zip_archive.cpp \
       remove_exceptions.cpp \
       remove_instanceof.cpp \
diff --git a/jbmc/src/java_bytecode/convert_java_nondet.cpp b/jbmc/src/java_bytecode/convert_java_nondet.cpp
index c9c35cad5b3..d945ed6d41d 100644
--- a/jbmc/src/java_bytecode/convert_java_nondet.cpp
+++ b/jbmc/src/java_bytecode/convert_java_nondet.cpp
@@ -44,7 +44,7 @@ static goto_programt get_gen_nondet_init_instructions(
   const source_locationt &source_loc,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const irep_idt &mode)
 {
   code_blockt gen_nondet_init_code;
@@ -82,7 +82,7 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
   const goto_programt::targett &target,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  object_factory_parameterst object_factory_parameters,
+  java_object_factory_parameterst object_factory_parameters,
   const irep_idt &mode)
 {
   const auto next_instr = std::next(target);
@@ -172,7 +172,7 @@ void convert_nondet(
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const irep_idt &mode)
 {
   bool changed = false;
@@ -200,10 +200,10 @@ void convert_nondet(
 void convert_nondet(
   goto_model_functiont &function,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const irep_idt &mode)
 {
-  object_factory_parameterst parameters = object_factory_parameters;
+  java_object_factory_parameterst parameters = object_factory_parameters;
   parameters.function_id = function.get_function_id();
   convert_nondet(
     function.get_goto_function().body,
@@ -219,7 +219,7 @@ void convert_nondet(
   goto_functionst &goto_functions,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters)
+  const java_object_factory_parameterst &object_factory_parameters)
 {
   const namespacet ns(symbol_table);
 
@@ -229,7 +229,7 @@ void convert_nondet(
 
     if(symbol.mode==ID_java)
     {
-      object_factory_parameterst parameters = object_factory_parameters;
+      java_object_factory_parameterst parameters = object_factory_parameters;
       parameters.function_id = f_it.first;
       convert_nondet(
         f_it.second.body,
@@ -248,7 +248,7 @@ void convert_nondet(
 void convert_nondet(
   goto_modelt &goto_model,
   message_handlert &message_handler,
-  const object_factory_parameterst& object_factory_parameters)
+  const java_object_factory_parameterst &object_factory_parameters)
 {
   convert_nondet(
     goto_model.goto_functions,
diff --git a/jbmc/src/java_bytecode/convert_java_nondet.h b/jbmc/src/java_bytecode/convert_java_nondet.h
index d5e415e01c9..871bd068c7e 100644
--- a/jbmc/src/java_bytecode/convert_java_nondet.h
+++ b/jbmc/src/java_bytecode/convert_java_nondet.h
@@ -20,7 +20,7 @@ class symbol_table_baset;
 class goto_modelt;
 class goto_model_functiont;
 class message_handlert;
-struct object_factory_parameterst;
+struct java_object_factory_parameterst;
 
 /// Converts side_effect_exprt_nondett expressions using java_object_factory.
 /// For example, NONDET(SomeClass *) may become a nondet choice between a null
@@ -40,12 +40,12 @@ void convert_nondet(
   goto_functionst &goto_functions,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters);
+  const java_object_factory_parameterst &object_factory_parameters);
 
 void convert_nondet(
   goto_modelt &,
   message_handlert &,
-  const object_factory_parameterst &object_factory_parameters);
+  const java_object_factory_parameterst &object_factory_parameters);
 
 /// Converts side_effect_exprt_nondett expressions using java_object_factory.
 /// For example, NONDET(SomeClass *) may become a nondet choice between a null
@@ -64,7 +64,7 @@ void convert_nondet(
 void convert_nondet(
   goto_model_functiont &function,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const irep_idt &mode);
 
 #endif // CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h
index 08980a1c70c..3a3011eda1c 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.h
+++ b/jbmc/src/java_bytecode/java_bytecode_language.h
@@ -13,9 +13,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ci_lazy_methods.h"
 #include "ci_lazy_methods_needed.h"
 #include "java_class_loader.h"
+#include "java_object_factory_parameters.h"
 #include "java_static_initializers.h"
 #include "java_string_library_preprocess.h"
-#include "object_factory_parameters.h"
 #include "select_pointer_type.h"
 #include "synthetic_methods_map.h"
 
@@ -179,7 +179,7 @@ class java_bytecode_languaget:public languaget
   java_class_loadert java_class_loader;
   bool threading_support;
   bool assume_inputs_non_null;      // assume inputs variables to be non-null
-  object_factory_parameterst object_factory_parameters;
+  java_object_factory_parameterst object_factory_parameters;
   size_t max_user_array_length;     // max size for user code created arrays
   method_bytecodet method_bytecode;
   lazy_methods_modet lazy_methods_mode;
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index b4af4eeac59..2626562568c 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -122,7 +122,7 @@ static void java_static_lifetime_init(
   symbol_table_baset &symbol_table,
   const source_locationt &source_location,
   bool assume_init_pointers_not_null,
-  object_factory_parameterst object_factory_parameters,
+  java_object_factory_parameterst object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   bool string_refinement_enabled,
   message_handlert &message_handler)
@@ -218,7 +218,7 @@ static void java_static_lifetime_init(
                                     is_non_null_library_global(sym.name) ||
                                     assume_init_pointers_not_null;
 
-        object_factory_parameterst parameters = object_factory_parameters;
+        java_object_factory_parameterst parameters = object_factory_parameters;
         if(not_allow_null && !is_class_model)
           parameters.min_null_tree_depth = 1;
 
@@ -278,7 +278,7 @@ exprt::operandst java_build_arguments(
   code_blockt &init_code,
   symbol_table_baset &symbol_table,
   bool assume_init_pointers_not_null,
-  object_factory_parameterst object_factory_parameters,
+  java_object_factory_parameterst object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   const java_method_typet::parameterst &parameters =
@@ -307,7 +307,7 @@ exprt::operandst java_build_arguments(
     // be null
     bool is_this=(param_number==0) && parameters[param_number].get_this();
 
-    object_factory_parameterst parameters = object_factory_parameters;
+    java_object_factory_parameterst parameters = object_factory_parameters;
     // only pointer must be non-null
     if(assume_init_pointers_not_null || is_this)
       parameters.min_null_tree_depth = 1;
@@ -598,7 +598,7 @@ bool java_entry_point(
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   bool assert_uncaught_exceptions,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   bool string_refinement_enabled)
 {
@@ -654,7 +654,7 @@ bool generate_java_start_function(
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   bool assert_uncaught_exceptions,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   messaget message(message_handler);
diff --git a/jbmc/src/java_bytecode/java_entry_point.h b/jbmc/src/java_bytecode/java_entry_point.h
index dd0b1fca004..1946c4b6dbe 100644
--- a/jbmc/src/java_bytecode/java_entry_point.h
+++ b/jbmc/src/java_bytecode/java_entry_point.h
@@ -25,7 +25,7 @@ bool java_entry_point(
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   bool assert_uncaught_exceptions,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   bool string_refinement_enabled);
 
@@ -76,7 +76,7 @@ bool generate_java_start_function(
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
   bool assert_uncaught_exceptions,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index e7e9217d4ed..98bf4839714 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -30,7 +30,7 @@ class java_object_factoryt
   /// methods in this class.
   const source_locationt &loc;
 
-  const object_factory_parameterst object_factory_parameters;
+  const java_object_factory_parameterst object_factory_parameters;
 
   /// This is employed in conjunction with the depth above. Every time the
   /// non-det generator visits a type, the type is added to this set. We forbid
@@ -83,7 +83,7 @@ class java_object_factoryt
   java_object_factoryt(
     std::vector<const symbolt *> &_symbols_created,
     const source_locationt &loc,
-    const object_factory_parameterst _object_factory_parameters,
+    const java_object_factory_parameterst _object_factory_parameters,
     symbol_table_baset &_symbol_table,
     const select_pointer_typet &pointer_type_selector)
     : symbols_created(_symbols_created),
@@ -1212,7 +1212,7 @@ void java_object_factoryt::gen_nondet_init(
   {
     // types different from pointer or structure:
     // bool, int, float, byte, char, ...
-    exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type)
+    exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, loc)
                                        : side_effect_expr_nondett(type, loc);
     code_assignt assign(expr, rhs);
     assign.add_source_location()=loc;
@@ -1536,7 +1536,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   symbol_table_baset &symbol_table,
-  object_factory_parameterst parameters,
+  java_object_factory_parameterst parameters,
   allocation_typet alloc_type,
   const source_locationt &loc,
   const select_pointer_typet &pointer_type_selector)
@@ -1629,7 +1629,7 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   update_in_placet update_in_place)
 {
@@ -1666,7 +1666,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   symbol_tablet &symbol_table,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   allocation_typet alloc_type,
   const source_locationt &location)
 {
@@ -1690,7 +1690,7 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   update_in_placet update_in_place)
 {
   select_pointer_typet pointer_type_selector;
diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h
index acde2f165fe..66f8506ae8f 100644
--- a/jbmc/src/java_bytecode/java_object_factory.h
+++ b/jbmc/src/java_bytecode/java_object_factory.h
@@ -94,7 +94,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   symbol_table_baset &symbol_table,
-  object_factory_parameterst parameters,
+  java_object_factory_parameterst parameters,
   allocation_typet alloc_type,
   const source_locationt &location,
   const select_pointer_typet &pointer_type_selector);
@@ -104,7 +104,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   symbol_tablet &symbol_table,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   allocation_typet alloc_type,
   const source_locationt &location);
 
@@ -122,7 +122,7 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   update_in_placet update_in_place);
 
@@ -133,7 +133,7 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   update_in_placet update_in_place);
 
 exprt allocate_dynamic_object(
diff --git a/jbmc/src/java_bytecode/java_object_factory_parameters.cpp b/jbmc/src/java_bytecode/java_object_factory_parameters.cpp
new file mode 100644
index 00000000000..7ff5bd89578
--- /dev/null
+++ b/jbmc/src/java_bytecode/java_object_factory_parameters.cpp
@@ -0,0 +1,16 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#include "java_object_factory_parameters.h"
+
+void parse_java_object_factory_options(
+  const cmdlinet &cmdline,
+  optionst &options)
+{
+  parse_object_factory_options(cmdline, options);
+}
diff --git a/jbmc/src/java_bytecode/java_object_factory_parameters.h b/jbmc/src/java_bytecode/java_object_factory_parameters.h
new file mode 100644
index 00000000000..e01b7175f1c
--- /dev/null
+++ b/jbmc/src/java_bytecode/java_object_factory_parameters.h
@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_PARAMETERS_H
+#define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_PARAMETERS_H
+
+#include <util/object_factory_parameters.h>
+
+struct java_object_factory_parameterst final : public object_factory_parameterst
+{
+  java_object_factory_parameterst()
+  {
+  }
+
+  explicit java_object_factory_parameterst(const optionst &options)
+    : object_factory_parameterst(options)
+  {
+  }
+};
+
+/// Parse the java object factory parameters from a given command line
+/// \param cmdline Command line
+/// \param [out] options The options object that will be updated
+void parse_java_object_factory_options(
+  const cmdlinet &cmdline,
+  optionst &options);
+
+#endif
diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
index 7c5ac727d88..bb15d6107a2 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.cpp
+++ b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -197,7 +197,7 @@ static void clinit_wrapper_do_recursive_calls(
   const irep_idt &class_name,
   code_blockt &init_body,
   const bool nondet_static,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
@@ -226,7 +226,7 @@ static void clinit_wrapper_do_recursive_calls(
   // used in get_stub_initializer_body and java_static_lifetime_init.
   if(nondet_static)
   {
-    object_factory_parameterst parameters = object_factory_parameters;
+    java_object_factory_parameterst parameters = object_factory_parameters;
     parameters.function_id = clinit_wrapper_name(class_name);
 
     std::vector<irep_idt> nondet_ids;
@@ -449,7 +449,7 @@ code_blockt get_thread_safe_clinit_wrapper_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   const bool nondet_static,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
@@ -645,7 +645,7 @@ code_ifthenelset get_clinit_wrapper_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   const bool nondet_static,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   // Assume that class C extends class C' and implements interfaces
@@ -843,7 +843,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
 code_blockt stub_global_initializer_factoryt::get_stub_initializer_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   const symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id);
@@ -862,7 +862,7 @@ code_blockt stub_global_initializer_factoryt::get_stub_initializer_body(
     class_globals.first != class_globals.second,
     "class with synthetic clinit should have at least one global to init");
 
-  object_factory_parameterst parameters = object_factory_parameters;
+  java_object_factory_parameterst parameters = object_factory_parameters;
   parameters.function_id = function_id;
 
   for(auto it = class_globals.first; it != class_globals.second; ++it)
diff --git a/jbmc/src/java_bytecode/java_static_initializers.h b/jbmc/src/java_bytecode/java_static_initializers.h
index 687bb48dead..9b6206cc70d 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.h
+++ b/jbmc/src/java_bytecode/java_static_initializers.h
@@ -9,7 +9,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H
 #define CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H
 
-#include "object_factory_parameters.h"
+#include "java_object_factory_parameters.h"
 #include "select_pointer_type.h"
 #include "synthetic_methods_map.h"
 
@@ -31,14 +31,14 @@ code_blockt get_thread_safe_clinit_wrapper_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   const bool nondet_static,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector);
 
 code_ifthenelset get_clinit_wrapper_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   const bool nondet_static,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector);
 
 class stub_global_initializer_factoryt
@@ -56,14 +56,14 @@ class stub_global_initializer_factoryt
   code_blockt get_stub_initializer_body(
     const irep_idt &function_id,
     symbol_table_baset &symbol_table,
-    const object_factory_parameterst &object_factory_parameters,
+    const java_object_factory_parameterst &object_factory_parameters,
     const select_pointer_typet &pointer_type_selector);
 };
 
 void create_stub_global_initializers(
   symbol_tablet &symbol_table,
   const std::unordered_set<irep_idt> &stub_globals_set,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector);
 
 #endif
diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
index d73486656ee..7b68aba3d1d 100644
--- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp
+++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
@@ -26,7 +26,7 @@ class java_simple_method_stubst
   java_simple_method_stubst(
     symbol_table_baset &_symbol_table,
     bool _assume_non_null,
-    const object_factory_parameterst &_object_factory_parameters,
+    const java_object_factory_parameterst &_object_factory_parameters,
     message_handlert &_message_handler)
     : symbol_table(_symbol_table),
       assume_non_null(_assume_non_null),
@@ -52,7 +52,7 @@ class java_simple_method_stubst
 protected:
   symbol_table_baset &symbol_table;
   bool assume_non_null;
-  const object_factory_parameterst &object_factory_parameters;
+  const java_object_factory_parameterst &object_factory_parameters;
   message_handlert &message_handler;
 };
 
@@ -110,7 +110,7 @@ void java_simple_method_stubst::create_method_stub_at(
   if(is_constructor)
     to_init = dereference_exprt(to_init, expected_base);
 
-  object_factory_parameterst parameters = object_factory_parameters;
+  java_object_factory_parameterst parameters = object_factory_parameters;
   if(assume_non_null)
     parameters.min_null_tree_depth = 1;
 
@@ -198,7 +198,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
       const exprt &to_return = to_return_symbol.symbol_expr();
       if(to_return_symbol.type.id() != ID_pointer)
       {
-        object_factory_parameterst parameters = object_factory_parameters;
+        java_object_factory_parameterst parameters = object_factory_parameters;
         if(assume_non_null)
           parameters.min_null_tree_depth = 1;
 
@@ -255,7 +255,7 @@ void java_generate_simple_method_stub(
   const irep_idt &function_name,
   symbol_table_baset &symbol_table,
   bool assume_non_null,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   message_handlert &message_handler)
 {
   java_simple_method_stubst stub_generator(
@@ -276,7 +276,7 @@ void java_generate_simple_method_stub(
 void java_generate_simple_method_stubs(
   symbol_table_baset &symbol_table,
   bool assume_non_null,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   message_handlert &message_handler)
 {
   // The intent here is to apply stub_generator.check_method_stub() to
diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.h b/jbmc/src/java_bytecode/simple_method_stubbing.h
index d12ede725ae..165d26835e7 100644
--- a/jbmc/src/java_bytecode/simple_method_stubbing.h
+++ b/jbmc/src/java_bytecode/simple_method_stubbing.h
@@ -15,20 +15,20 @@ Author: Diffblue Ltd.
 #include <util/irep.h>
 
 class message_handlert;
-struct object_factory_parameterst;
+struct java_object_factory_parameterst;
 class symbol_table_baset;
 
 void java_generate_simple_method_stub(
   const irep_idt &function_name,
   symbol_table_baset &symbol_table,
   bool assume_non_null,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   message_handlert &message_handler);
 
 void java_generate_simple_method_stubs(
   symbol_table_baset &symbol_table,
   bool assume_non_null,
-  const object_factory_parameterst &object_factory_parameters,
+  const java_object_factory_parameterst &object_factory_parameters,
   message_handlert &message_handler);
 
 #endif
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 3f59c93e2a4..ac6487e3dea 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -109,7 +109,7 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
 
   jbmc_parse_optionst::set_default_options(options);
   parse_java_language_options(cmdline, options);
-  parse_object_factory_options(cmdline, options);
+  parse_java_object_factory_options(cmdline, options);
 
   if(cmdline.isset("show-symex-strategies"))
   {
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
index a605d4b2440..2988c002a90 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.h
+++ b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -120,7 +120,7 @@ class jbmc_parse_optionst:
 protected:
   ui_message_handlert ui_message_handler;
   path_strategy_choosert path_strategy_chooser;
-  object_factory_parameterst object_factory_params;
+  java_object_factory_parameterst object_factory_params;
   bool stub_objects_are_not_null;
 
   std::unique_ptr<class_hierarchyt> class_hierarchy;
diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
index d224e36c65b..3c39c5a078e 100644
--- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
+++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
@@ -46,7 +46,7 @@ SCENARIO(
     symbol_typet java_string_type("java::java.lang.String");
     symbol_exprt expr("arg", java_string_type);
 
-    object_factory_parameterst object_factory_parameters;
+    java_object_factory_parameterst object_factory_parameters;
     object_factory_parameters.max_nondet_string_length = 20;
     object_factory_parameters.function_id = "test";
 
diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
index 46eb0c6749b..0fe9c6011f6 100644
--- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
+++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
@@ -16,7 +16,7 @@
 #include <goto-programs/remove_returns.h>
 
 #include <java_bytecode/convert_java_nondet.h>
-#include <java_bytecode/object_factory_parameters.h>
+#include <java_bytecode/java_object_factory_parameters.h>
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/replace_java_nondet.h>
 
@@ -166,7 +166,7 @@ void load_and_test_method(
     validate_nondet_method_removed(goto_function.body.instructions);
   }
 
-  object_factory_parameterst params{};
+  java_object_factory_parameterst params{};
 
   THEN(
     "Replace and convert nondet should work after remove returns has been "
diff --git a/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/main.c b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/main.c
new file mode 100644
index 00000000000..d4efed079c1
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/main.c
@@ -0,0 +1,29 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st1
+{
+  struct st2 *to_st2;
+  int data;
+} st1_t;
+
+typedef struct st2
+{
+  struct st1 *to_st1;
+  int data;
+} st2_t;
+
+st1_t dummy1;
+st2_t dummy2;
+
+void func(st1_t *p)
+{
+  assert(p != NULL);
+  assert(p->to_st2 != NULL);
+  assert(p->to_st2->to_st1 != NULL);
+  assert(p->to_st2->to_st1->to_st2 == NULL);
+
+  assert(p != &dummy1);
+  assert(p->to_st2 != &dummy2);
+  assert(p->to_st2->to_st1 != &dummy1);
+}
diff --git a/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc
new file mode 100644
index 00000000000..7b82cc87646
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
diff --git a/regression/cbmc/pointer-function-parameters-struct-non-recursive/main.c b/regression/cbmc/pointer-function-parameters-struct-non-recursive/main.c
new file mode 100644
index 00000000000..ab46298f592
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters-struct-non-recursive/main.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  int data;
+} st_t;
+
+st_t dummy;
+
+void func(st_t *p)
+{
+  assert(p != NULL);
+  assert(p != &dummy);
+  assert(p->data >= 4854549);
+  assert(p->data < 4854549);
+}
diff --git a/regression/cbmc/pointer-function-parameters-struct-non-recursive/test.desc b/regression/cbmc/pointer-function-parameters-struct-non-recursive/test.desc
new file mode 100644
index 00000000000..a90929db40c
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters-struct-non-recursive/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--function func --min-null-tree-depth 10
+^EXIT=10$
+^SIGNAL=0$
+\[func.assertion.1\] line [0-9]+ assertion p != .*((NULL)|0).*: SUCCESS
+\[func.assertion.2\] line [0-9]+ assertion p != &dummy: SUCCESS
+\[func.assertion.3\] line [0-9]+ assertion p->data >= 4854549: FAILURE
+\[func.assertion.4\] line [0-9]+ assertion p->data < 4854549: FAILURE
+--
+^warning: ignoring
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/main.c b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/main.c
new file mode 100644
index 00000000000..3d25cbdb9a1
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/main.c
@@ -0,0 +1,28 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  struct st *next;
+  struct st *prev;
+  int data;
+} st_t;
+
+st_t dummy;
+
+void func(st_t *p)
+{
+  assert(p != NULL);
+  assert(p != &dummy);
+
+  assert(p->prev != NULL);
+  assert(p->prev != &dummy);
+
+  assert(p->next != NULL);
+  assert(p->next != &dummy);
+
+  assert(p->prev->prev == NULL);
+  assert(p->prev->next == NULL);
+  assert(p->next->prev == NULL);
+  assert(p->next->next == NULL);
+}
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc
new file mode 100644
index 00000000000..716670ff6f7
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 2 --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-3/main.c b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-3/main.c
new file mode 100644
index 00000000000..b6e2caceca2
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-3/main.c
@@ -0,0 +1,36 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  struct st *next;
+  int data;
+} st_t;
+
+st_t dummy;
+
+void func(st_t *p)
+{
+  if(p != NULL)
+  {
+    if(p->next != NULL)
+    {
+      if(p->next->next != NULL)
+      {
+        // covered
+      }
+      else
+      {
+        // covered
+      }
+    }
+    else
+    {
+      // not covered
+    }
+  }
+  else
+  {
+    // not covered
+  }
+}
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-3/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-3/test.desc
new file mode 100644
index 00000000000..de61e8009ea
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-3/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--function func --min-null-tree-depth 2 --max-nondet-tree-depth 10 --cover branch
+^EXIT=0$
+^SIGNAL=0$
+\[func.coverage.2\] file main.c line .* function func block 1 branch false: SATISFIED
+\[func.coverage.3\] file main.c line .* function func block 1 branch true: FAILED
+\[func.coverage.4\] file main.c line .* function func block 2 branch false: SATISFIED
+\[func.coverage.5\] file main.c line .* function func block 2 branch true: FAILED
+\[func.coverage.6\] file main.c line .* function func block 3 branch false: SATISFIED
+\[func.coverage.7\] file main.c line .* function func block 3 branch true: SATISFIED
+--
+^warning: ignoring
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion/main.c b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/main.c
new file mode 100644
index 00000000000..70abdec5c77
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/main.c
@@ -0,0 +1,22 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  struct st *next;
+  int data;
+} st_t;
+
+st_t dummy;
+
+void func(st_t *p)
+{
+  assert(p != NULL);
+  assert(p->next != NULL);
+  assert(p->next->next != NULL);
+  assert(p->next->next->next == NULL);
+
+  assert(p != &dummy);
+  assert(p->next != &dummy);
+  assert(p->next->next != &dummy);
+}
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc
new file mode 100644
index 00000000000..7b82cc87646
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests
index 2fe8127538c..c47cd9128e7 100755
--- a/scripts/delete_failing_smt2_solver_tests
+++ b/scripts/delete_failing_smt2_solver_tests
@@ -156,6 +156,11 @@ rm no_nondet_static/test.desc
 rm null1/test.desc
 rm pointer-function-parameters/test.desc
 rm pointer-function-parameters-2/test.desc
+rm pointer-function-parameters-struct-mutual-recursion/test.desc
+rm pointer-function-parameters-struct-non-recursive/test.desc
+rm pointer-function-parameters-struct-simple-recursion/test.desc
+rm pointer-function-parameters-struct-simple-recursion-2/test.desc
+rm pointer-function-parameters-struct-simple-recursion-3/test.desc
 rm scanf1/test.desc
 rm simple_assert/test.desc
 rm stack-trace/test.desc
diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile
index d0ccdf84a3a..235c74bb578 100644
--- a/src/ansi-c/Makefile
+++ b/src/ansi-c/Makefile
@@ -13,6 +13,7 @@ SRC = anonymous_member.cpp \
       builtin_factory.cpp \
       c_misc.cpp \
       c_nondet_symbol_factory.cpp \
+      c_object_factory_parameters.cpp \
       c_preprocess.cpp \
       c_qualifiers.cpp \
       c_storage_spec.cpp \
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index 6b001e2e206..7db6cf7c1c1 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -22,7 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 exprt::operandst build_function_environment(
   const code_typet::parameterst &parameters,
   code_blockt &init_code,
-  symbol_tablet &symbol_table)
+  symbol_tablet &symbol_table,
+  const c_object_factory_parameterst &object_factory_parameters)
 {
   exprt::operandst main_arguments;
   main_arguments.resize(parameters.size());
@@ -35,14 +36,13 @@ exprt::operandst build_function_environment(
     const irep_idt base_name=p.get_base_name().empty()?
       ("argument#"+std::to_string(param_number)):p.get_base_name();
 
-    main_arguments[param_number]=
-      c_nondet_symbol_factory(
-        init_code,
-        symbol_table,
-        base_name,
-        p.type(),
-        p.source_location(),
-        true);
+    main_arguments[param_number] = c_nondet_symbol_factory(
+      init_code,
+      symbol_table,
+      base_name,
+      p.type(),
+      p.source_location(),
+      object_factory_parameters);
   }
 
   return main_arguments;
@@ -111,7 +111,8 @@ void record_function_outputs(
 
 bool ansi_c_entry_point(
   symbol_tablet &symbol_table,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const c_object_factory_parameterst &object_factory_parameters)
 {
   // check if entry point is already there
   if(symbol_table.symbols.find(goto_functionst::entry_point())!=
@@ -179,21 +180,24 @@ bool ansi_c_entry_point(
 
   static_lifetime_init(symbol_table, symbol.location);
 
-  return generate_ansi_c_start_function(symbol, symbol_table, message_handler);
+  return generate_ansi_c_start_function(
+    symbol, symbol_table, message_handler, object_factory_parameters);
 }
 
-
 /// Generate a _start function for a specific function
 /// \param symbol: The symbol for the function that should be
 ///   used as the entry point
 /// \param symbol_table: The symbol table for the program. The new _start
 ///   function symbol will be added to this table
 /// \param message_handler: The message handler
+/// \param object_factory_parameters configuration parameters for the object
+///   factory
 /// \return Returns false if the _start method was generated correctly
 bool generate_ansi_c_start_function(
   const symbolt &symbol,
   symbol_tablet &symbol_table,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const c_object_factory_parameterst &object_factory_parameters)
 {
   PRECONDITION(!symbol.value.is_nil());
   code_blockt init_code;
@@ -423,11 +427,8 @@ bool generate_ansi_c_start_function(
   else
   {
     // produce nondet arguments
-    call_main.arguments()=
-      build_function_environment(
-        parameters,
-        init_code,
-        symbol_table);
+    call_main.arguments() = build_function_environment(
+      parameters, init_code, symbol_table, object_factory_parameters);
   }
 
   init_code.add(std::move(call_main));
diff --git a/src/ansi-c/ansi_c_entry_point.h b/src/ansi-c/ansi_c_entry_point.h
index fe0ed04a2c1..9af2e68c71a 100644
--- a/src/ansi-c/ansi_c_entry_point.h
+++ b/src/ansi-c/ansi_c_entry_point.h
@@ -10,16 +10,19 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H
 #define CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H
 
-#include <util/symbol_table.h>
+#include <ansi-c/c_object_factory_parameters.h>
 #include <util/message.h>
+#include <util/symbol_table.h>
 
 bool ansi_c_entry_point(
   symbol_tablet &symbol_table,
-  message_handlert &message_handler);
+  message_handlert &message_handler,
+  const c_object_factory_parameterst &object_factory_parameters);
 
 bool generate_ansi_c_start_function(
   const symbolt &symbol,
   symbol_tablet &symbol_table,
-  message_handlert &message_handler);
+  message_handlert &message_handler,
+  const c_object_factory_parameterst &object_factory_parameters);
 
 #endif // CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index ae4c8f62f02..e6173c801c0 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -137,8 +137,10 @@ bool ansi_c_languaget::generate_support_functions(
   // function body parsing, or else generate-stubs moved to the
   // final phase.
   generate_opaque_method_stubs(symbol_table);
+
   // This creates __CPROVER_start and __CPROVER_initialize:
-  return ansi_c_entry_point(symbol_table, get_message_handler());
+  return ansi_c_entry_point(
+    symbol_table, get_message_handler(), object_factory_params);
 }
 
 void ansi_c_languaget::show_parse(std::ostream &out)
diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index b23bdad6469..d554dbb9d0c 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -17,10 +17,28 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language.h>
 
 #include "ansi_c_parse_tree.h"
+#include "c_object_factory_parameters.h"
+
+// clang-format off
+#define OPT_ANSI_C_LANGUAGE \
+  "(max-nondet-tree-depth):" \
+  "(min-null-tree-depth):"
+
+#define HELP_ANSI_C_LANGUAGE \
+  " --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */\
+  "                              at level N pointers are set to null\n" \
+  " --min-null-tree-depth N      minimum level at which a pointer can first be\n" /* NOLINT(*) */\
+  "                              NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */
+// clang-format on
 
 class ansi_c_languaget:public languaget
 {
 public:
+  void set_language_options(const optionst &options) override
+  {
+    object_factory_params.set(options);
+  }
+
   bool preprocess(
     std::istream &instream,
     const std::string &path,
@@ -75,6 +93,8 @@ class ansi_c_languaget:public languaget
 protected:
   ansi_c_parse_treet parse_tree;
   std::string parse_path;
+
+  c_object_factory_parameterst object_factory_params;
 };
 
 std::unique_ptr<languaget> new_ansi_c_language();
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 15e1a712f51..d07877054d9 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -11,65 +11,40 @@ Author: Diffblue Ltd.
 
 #include "c_nondet_symbol_factory.h"
 
+#include <ansi-c/c_object_factory_parameters.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
 #include <util/namespace.h>
+#include <util/nondet_bool.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
 
 #include <goto-programs/goto_functions.h>
 
-/// Create a new temporary static symbol
-/// \param symbol_table: The symbol table to create the symbol in
-/// \param loc: The location to assign to the symbol
-/// \param type: The type of symbol to create
-/// \param static_lifetime: Whether the symbol should have a static lifetime
-/// \param prefix: The prefix to use for the symbol's basename
-/// \return Returns a reference to the new symbol
-static const symbolt &c_new_tmp_symbol(
-  symbol_tablet &symbol_table,
-  const source_locationt &loc,
-  const typet &type,
-  const bool static_lifetime,
-  const std::string &prefix="tmp")
-{
-  symbolt &tmp_symbol = get_fresh_aux_symbol(
-    type, id2string(loc.get_function()), prefix, loc, ID_C, symbol_table);
-  tmp_symbol.is_static_lifetime=static_lifetime;
-
-  return tmp_symbol;
-}
-
-/// \param type: Desired type (C_bool or plain bool)
-/// \param loc: source location
-/// \return nondet expr of that type
-static exprt c_get_nondet_bool(const typet &type, const source_locationt &loc)
-{
-  // We force this to 0 and 1 and won't consider other values
-  return typecast_exprt(side_effect_expr_nondett(bool_typet(), loc), type);
-}
-
 class symbol_factoryt
 {
   std::vector<const symbolt *> &symbols_created;
   symbol_tablet &symbol_table;
   const source_locationt &loc;
-  const bool assume_non_null;
   namespacet ns;
+  const c_object_factory_parameterst &object_factory_params;
+
+  typedef std::set<irep_idt> recursion_sett;
 
 public:
   symbol_factoryt(
     std::vector<const symbolt *> &_symbols_created,
     symbol_tablet &_symbol_table,
     const source_locationt &loc,
-    const bool _assume_non_null):
-      symbols_created(_symbols_created),
+    const c_object_factory_parameterst &object_factory_params)
+    : symbols_created(_symbols_created),
       symbol_table(_symbol_table),
       loc(loc),
-      assume_non_null(_assume_non_null),
-      ns(_symbol_table)
+      ns(_symbol_table),
+      object_factory_params(object_factory_params)
   {}
 
   exprt allocate_object(
@@ -78,7 +53,11 @@ class symbol_factoryt
     const typet &allocate_type,
     const bool static_lifetime);
 
-  void gen_nondet_init(code_blockt &assignments, const exprt &expr);
+  void gen_nondet_init(
+    code_blockt &assignments,
+    const exprt &expr,
+    const std::size_t depth = 0,
+    recursion_sett recursion_set = recursion_sett());
 };
 
 /// Create a symbol for a pointer to point to
@@ -95,12 +74,14 @@ exprt symbol_factoryt::allocate_object(
   const typet &allocate_type,
   const bool static_lifetime)
 {
-  const symbolt &aux_symbol=
-    c_new_tmp_symbol(
-      symbol_table,
-      loc,
-      allocate_type,
-      static_lifetime);
+  symbolt &aux_symbol = get_fresh_aux_symbol(
+    allocate_type,
+    id2string(loc.get_function()),
+    "tmp",
+    loc,
+    ID_C,
+    symbol_table);
+  aux_symbol.is_static_lifetime = static_lifetime;
   symbols_created.push_back(&aux_symbol);
 
   const typet &allocate_type_resolved=ns.follow(allocate_type);
@@ -127,9 +108,13 @@ exprt symbol_factoryt::allocate_object(
 /// \param assignments: The code block to add code to
 /// \param expr: The expression which we are generating a non-determinate value
 ///   for
+/// \param depth number of pointers followed so far during initialisation
+/// \param recursion_set names of structs seen so far on current pointer chain
 void symbol_factoryt::gen_nondet_init(
   code_blockt &assignments,
-  const exprt &expr)
+  const exprt &expr,
+  const std::size_t depth,
+  recursion_sett recursion_set)
 {
   const typet &type=ns.follow(expr.type());
 
@@ -139,6 +124,22 @@ void symbol_factoryt::gen_nondet_init(
     const pointer_typet &pointer_type=to_pointer_type(type);
     const typet &subtype=ns.follow(pointer_type.subtype());
 
+    if(subtype.id() == ID_struct)
+    {
+      const struct_typet &struct_type = to_struct_type(subtype);
+      const irep_idt struct_tag = struct_type.get_tag();
+
+      if(
+        recursion_set.find(struct_tag) != recursion_set.end() &&
+        depth >= object_factory_params.max_nondet_tree_depth)
+      {
+        code_assignt c(expr, null_pointer_exprt(pointer_type));
+        assignments.add(std::move(c));
+
+        return;
+      }
+    }
+
     code_blockt non_null_inst;
 
     exprt allocated=allocate_object(non_null_inst, expr, subtype, false);
@@ -152,9 +153,9 @@ void symbol_factoryt::gen_nondet_init(
     {
       init_expr=dereference_exprt(allocated, allocated.type().subtype());
     }
-    gen_nondet_init(non_null_inst, init_expr);
+    gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set);
 
-    if(assume_non_null)
+    if(depth < object_factory_params.min_null_tree_depth)
     {
       // Add the following code to assignments:
       // <expr> = <aoe>;
@@ -181,14 +182,32 @@ void symbol_factoryt::gen_nondet_init(
       assignments.add(std::move(null_check));
     }
   }
-  // TODO(OJones): Add support for structs and arrays
+  else if(type.id() == ID_struct)
+  {
+    const struct_typet &struct_type = to_struct_type(type);
+
+    const irep_idt struct_tag = struct_type.get_tag();
+
+    recursion_set.insert(struct_tag);
+
+    for(const auto &component : struct_type.components())
+    {
+      const typet &component_type = component.type();
+      const irep_idt name = component.get_name();
+
+      member_exprt me(expr, name, component_type);
+      me.add_source_location() = loc;
+
+      gen_nondet_init(assignments, me, depth, recursion_set);
+    }
+  }
   else
   {
     // If type is a ID_c_bool then add the following code to assignments:
     //   <expr> = NONDET(_BOOL);
     // Else add the following code to assignments:
     //   <expr> = NONDET(type);
-    exprt rhs = type.id() == ID_c_bool ? c_get_nondet_bool(type, loc)
+    exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, loc)
                                        : side_effect_expr_nondett(type, loc);
     code_assignt assign(expr, rhs);
     assign.add_source_location()=loc;
@@ -205,7 +224,8 @@ void symbol_factoryt::gen_nondet_init(
 /// \param base_name: The name to use for the symbol created
 /// \param type: The type for the symbol created
 /// \param loc: The location to assign to generated code
-/// \param allow_null: Whether to allow a null value when type is a pointer
+/// \param object_factory_parameters configuration parameters for the object
+///   factory
 /// \return Returns the symbol_exprt for the symbol created
 symbol_exprt c_nondet_symbol_factory(
   code_blockt &init_code,
@@ -213,7 +233,7 @@ symbol_exprt c_nondet_symbol_factory(
   const irep_idt base_name,
   const typet &type,
   const source_locationt &loc,
-  bool allow_null)
+  const c_object_factory_parameterst &object_factory_parameters)
 {
   irep_idt identifier=id2string(goto_functionst::entry_point())+
     "::"+id2string(base_name);
@@ -236,10 +256,7 @@ symbol_exprt c_nondet_symbol_factory(
   symbols_created.push_back(main_symbol_ptr);
 
   symbol_factoryt state(
-    symbols_created,
-    symbol_table,
-    loc,
-    !allow_null);
+    symbols_created, symbol_table, loc, object_factory_parameters);
   code_blockt assignments;
   state.gen_nondet_init(assignments, main_symbol_expr);
 
diff --git a/src/ansi-c/c_nondet_symbol_factory.h b/src/ansi-c/c_nondet_symbol_factory.h
index c1e1d5efdd4..c4d74f6021f 100644
--- a/src/ansi-c/c_nondet_symbol_factory.h
+++ b/src/ansi-c/c_nondet_symbol_factory.h
@@ -12,6 +12,8 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
 #define CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
 
+#include "c_object_factory_parameters.h"
+
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
@@ -21,6 +23,6 @@ symbol_exprt c_nondet_symbol_factory(
   const irep_idt base_name,
   const typet &type,
   const source_locationt &,
-  bool allow_null);
+  const c_object_factory_parameterst &object_factory_parameters);
 
 #endif // CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
diff --git a/src/ansi-c/c_object_factory_parameters.cpp b/src/ansi-c/c_object_factory_parameters.cpp
new file mode 100644
index 00000000000..4634dc5aeee
--- /dev/null
+++ b/src/ansi-c/c_object_factory_parameters.cpp
@@ -0,0 +1,14 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#include "c_object_factory_parameters.h"
+
+void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
+{
+  parse_object_factory_options(cmdline, options);
+}
diff --git a/src/ansi-c/c_object_factory_parameters.h b/src/ansi-c/c_object_factory_parameters.h
new file mode 100644
index 00000000000..5a2460222b1
--- /dev/null
+++ b/src/ansi-c/c_object_factory_parameters.h
@@ -0,0 +1,31 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#ifndef CPROVER_ANSI_C_C_OBJECT_FACTORY_PARAMETERS_H
+#define CPROVER_ANSI_C_C_OBJECT_FACTORY_PARAMETERS_H
+
+#include <util/object_factory_parameters.h>
+
+struct c_object_factory_parameterst final : public object_factory_parameterst
+{
+  c_object_factory_parameterst()
+  {
+  }
+
+  explicit c_object_factory_parameterst(const optionst &options)
+    : object_factory_parameterst(options)
+  {
+  }
+};
+
+/// Parse the c object factory parameters from a given command line
+/// \param cmdline Command line
+/// \param [out] options The options object that will be updated
+void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options);
+
+#endif
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index f312832dcfc..4c51865ee6e 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -109,6 +109,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   }
 
   cbmc_parse_optionst::set_default_options(options);
+  parse_c_object_factory_options(cmdline, options);
 
   if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
   {
@@ -933,6 +934,7 @@ void cbmc_parse_optionst::help()
     " --round-to-plus-inf          rounding towards plus infinity\n"
     " --round-to-minus-inf         rounding towards minus infinity\n"
     " --round-to-zero              rounding towards zero\n"
+    HELP_ANSI_C_LANGUAGE
     HELP_FUNCTIONS
     "\n"
     "Program representations:\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index f6727890244..c1d947d1c87 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -12,6 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
 #define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
 
+#include <ansi-c/ansi_c_language.h>
+#include <ansi-c/c_object_factory_parameters.h>
+
 #include <util/parse_options.h>
 #include <util/timestamper.h>
 #include <util/ui_message.h>
@@ -75,6 +78,7 @@ class optionst;
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
   OPT_VALIDATE \
+  OPT_ANSI_C_LANGUAGE \
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 
diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp
index 4acd28a3e02..31729cb5689 100644
--- a/src/cpp/cpp_language.cpp
+++ b/src/cpp/cpp_language.cpp
@@ -137,7 +137,8 @@ bool cpp_languaget::typecheck(
 bool cpp_languaget::generate_support_functions(
   symbol_tablet &symbol_table)
 {
-  return ansi_c_entry_point(symbol_table, get_message_handler());
+  return ansi_c_entry_point(
+    symbol_table, get_message_handler(), object_factory_params);
 }
 
 void cpp_languaget::show_parse(std::ostream &out)
diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h
index 3f474005f15..00c06d73c1f 100644
--- a/src/cpp/cpp_language.h
+++ b/src/cpp/cpp_language.h
@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <memory>
 
+#include <ansi-c/c_object_factory_parameters.h>
+
 #include <util/make_unique.h> // unique_ptr
 
 #include <langapi/language.h>
@@ -23,6 +25,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 class cpp_languaget:public languaget
 {
 public:
+  void set_language_options(const optionst &options) override
+  {
+    object_factory_params.set(options);
+  }
+
   bool preprocess(
     std::istream &instream,
     const std::string &path,
@@ -88,6 +95,8 @@ class cpp_languaget:public languaget
   cpp_parse_treet cpp_parse_tree;
   std::string parse_path;
 
+  c_object_factory_parameterst object_factory_params;
+
   void show_parse(std::ostream &out, const cpp_itemt &item);
 
   std::string main_symbol()
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index aa4fd641681..0cc5ad2778d 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -368,7 +368,12 @@ bool compilet::link()
     goto_model.goto_functions.function_map.erase(
       goto_functionst::entry_point());
 
-    if(ansi_c_entry_point(goto_model.symbol_table, get_message_handler()))
+    const bool error = ansi_c_entry_point(
+      goto_model.symbol_table,
+      get_message_handler(),
+      c_object_factory_parameterst());
+
+    if(error)
       return true;
 
     // entry_point may (should) add some more functions.
diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp
index bd3fbed6ec2..dadf7d24998 100644
--- a/src/goto-programs/initialize_goto_model.cpp
+++ b/src/goto-programs/initialize_goto_model.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cmdline.h>
 #include <util/config.h>
 #include <util/message.h>
+#include <util/object_factory_parameters.h>
 #include <util/unicode.h>
 
 #include <langapi/mode.h>
diff --git a/src/langapi/language_file.cpp b/src/langapi/language_file.cpp
index b9500d7d1a3..6f301604269 100644
--- a/src/langapi/language_file.cpp
+++ b/src/langapi/language_file.cpp
@@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <fstream>
 
+#include <util/object_factory_parameters.h>
+
 #include "language.h"
 
 language_filet::language_filet(const language_filet &rhs):
diff --git a/src/util/Makefile b/src/util/Makefile
index 6734fe7e701..52ce754b1e5 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -48,6 +48,7 @@ SRC = arith_tools.cpp \
       mp_arith.cpp \
       namespace.cpp \
       nondet.cpp \
+      object_factory_parameters.cpp \
       options.cpp \
       parse_options.cpp \
       parser.cpp \
diff --git a/src/util/nondet_bool.h b/src/util/nondet_bool.h
index 7d39b21bd4c..8827d83ead2 100644
--- a/src/util/nondet_bool.h
+++ b/src/util/nondet_bool.h
@@ -15,14 +15,16 @@ Author: Chris Smowton, chris@smowton.net
 #include "std_expr.h"
 #include "std_types.h"
 
-/// \par parameters: Desired type (C_bool or plain bool)
+/// \param type desired type (C_bool or plain bool)
+/// \param source_location source location
 /// \return nondet expr of that type
-inline exprt get_nondet_bool(const typet &type)
+inline exprt
+get_nondet_bool(const typet &type, const source_locationt &source_location)
 {
   // We force this to 0 and 1 and won't consider
   // other values.
   return typecast_exprt(
-    side_effect_expr_nondett(bool_typet(), source_locationt()), type);
+    side_effect_expr_nondett(bool_typet(), source_location), type);
 }
 
 #endif // CPROVER_UTIL_NONDET_BOOL_H
diff --git a/jbmc/src/java_bytecode/object_factory_parameters.cpp b/src/util/object_factory_parameters.cpp
similarity index 86%
rename from jbmc/src/java_bytecode/object_factory_parameters.cpp
rename to src/util/object_factory_parameters.cpp
index 85d7dce4887..93f136df32b 100644
--- a/jbmc/src/java_bytecode/object_factory_parameters.cpp
+++ b/src/util/object_factory_parameters.cpp
@@ -1,6 +1,6 @@
 /*******************************************************************\
 
-Module: Java Object Factory
+Module: Object Factory
 
 Author: Diffblue Ltd
 
@@ -23,6 +23,11 @@ void object_factory_parameterst::set(const optionst &options)
     max_nondet_tree_depth =
       options.get_unsigned_int_option("max-nondet-tree-depth");
   }
+  if(options.is_set("min-null-tree-depth"))
+  {
+    min_null_tree_depth =
+      options.get_unsigned_int_option("min-null-tree-depth");
+  }
   if(options.is_set("max-nondet-string-length"))
   {
     max_nondet_string_length =
@@ -54,6 +59,11 @@ void parse_object_factory_options(const cmdlinet &cmdline, optionst &options)
     options.set_option(
       "max-nondet-tree-depth", cmdline.get_value("max-nondet-tree-depth"));
   }
+  if(cmdline.isset("min-null-tree-depth"))
+  {
+    options.set_option(
+      "min-null-tree-depth", cmdline.get_value("min-null-tree-depth"));
+  }
   if(cmdline.isset("max-nondet-string-length"))
   {
     options.set_option(
diff --git a/jbmc/src/java_bytecode/object_factory_parameters.h b/src/util/object_factory_parameters.h
similarity index 53%
rename from jbmc/src/java_bytecode/object_factory_parameters.h
rename to src/util/object_factory_parameters.h
index 3bbf4c5f3d3..37e084811a4 100644
--- a/jbmc/src/java_bytecode/object_factory_parameters.h
+++ b/src/util/object_factory_parameters.h
@@ -6,8 +6,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#ifndef CPROVER_JAVA_BYTECODE_OBJECT_FACTORY_PARAMETERS_H
-#define CPROVER_JAVA_BYTECODE_OBJECT_FACTORY_PARAMETERS_H
+#ifndef CPROVER_UTIL_OBJECT_FACTORY_PARAMETERS_H
+#define CPROVER_UTIL_OBJECT_FACTORY_PARAMETERS_H
 
 #include <cstdint>
 #include <limits>
@@ -17,30 +17,42 @@ Author: Daniel Kroening, kroening@kroening.com
 class cmdlinet;
 class optionst;
 
-#define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
-#define MAX_NONDET_STRING_LENGTH \
-  static_cast<std::size_t>(std::numeric_limits<std::int32_t>::max())
-#define MAX_NONDET_TREE_DEPTH 5
-#define MIN_NULL_TREE_DEPTH 0
-
-struct object_factory_parameterst final
+struct object_factory_parameterst
 {
+  object_factory_parameterst()
+  {
+  }
+
+  explicit object_factory_parameterst(const optionst &options)
+  {
+    set(options);
+  }
+
+  virtual ~object_factory_parameterst() = default;
+
   /// Maximum value for the non-deterministically-chosen length of an array.
-  size_t max_nondet_array_length=MAX_NONDET_ARRAY_LENGTH_DEFAULT;
+  size_t max_nondet_array_length = 5;
 
   /// Maximum value for the non-deterministically-chosen length of a string.
-  size_t max_nondet_string_length=MAX_NONDET_STRING_LENGTH;
+  size_t max_nondet_string_length =
+    static_cast<std::size_t>(std::numeric_limits<std::int32_t>::max());
 
   /// Minimum value for the non-deterministically-chosen length of a string.
   size_t min_nondet_string_length = 0;
 
-  /// Maximum depth for object hierarchy on input.
-  /// Used to prevent object factory to loop infinitely during the
-  /// generation of code that allocates/initializes data structures of recursive
-  /// data types or unbounded depth. We bound the maximum number of times we
-  /// dereference a pointer using a 'depth counter'. We set a pointer to null if
-  /// such depth becomes >= than this maximum value.
-  size_t max_nondet_tree_depth=MAX_NONDET_TREE_DEPTH;
+  /// Maximum depth of pointer chains (that contain recursion) in the nondet
+  /// generated input objects.
+  ///
+  /// Used to prevent the object factory from looping infinitely during the
+  /// generation of code that allocates/initializes recursive data structures
+  /// (such as a linked list). The object factory tracks the number of times a
+  /// pointer has been dereferenced in a 'depth' counter variable. If a pointer
+  /// to be initialized points to an object of a type that already occured on
+  /// the current pointer chain, and if 'depth' is larger than
+  /// 'max_nondet_tree_depth`, then the pointer is set to null. The parameter
+  /// does not affect non-recursive data structures, which are always
+  /// initialized to their full depth.
+  size_t max_nondet_tree_depth = 5;
 
   /// To force a certain depth of non-null objects.
   /// The default is that objects are 'maybe null' up to the nondet tree depth.
@@ -52,7 +64,7 @@ struct object_factory_parameterst final
   /// * max_nondet_tree_depth=n >=m, min_null_tree_depth=m
   ///   pointer and children up to depth m initialized to non-null,
   ///   children up to n maybe-null, beyond n null
-  size_t min_null_tree_depth = MIN_NULL_TREE_DEPTH;
+  size_t min_null_tree_depth = 0;
 
   /// Force string content to be ASCII printable characters when set to true.
   bool string_printable = false;