diff --git a/regression/cbmc/pointer-function-parameters-2/main.c b/regression/cbmc/pointer-function-parameters-2/main.c
new file mode 100644
index 00000000000..08428dde9cc
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters-2/main.c
@@ -0,0 +1,16 @@
+int fun(int **a)
+{
+  if(!a)
+  {
+    return 0;
+  }
+  if(!*a)
+  {
+    return 1;
+  }
+  if(**a==4)
+  {
+    return 2;
+  }
+  return 3;
+}
diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/cbmc/pointer-function-parameters-2/test.desc
new file mode 100644
index 00000000000..c67211d7387
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters-2/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--function fun --cover branch
+^\*\* 7 of 7 covered \(100.0%\)$
+^\*\* Used 4 iterations$
+^Test suite:$
+^a=\(\(signed int \*\*\)NULL\), tmp\$1=[^,]*, tmp\$2=[^,]*$
+^a=&tmp\$1!0, tmp\$1=\(\(signed int \*\)NULL\), tmp\$2=[^,]*$
+^a=&tmp\$1!0, tmp\$1=&tmp\$2!0, tmp\$2=([012356789][0-9]*|4[0-9]+)$
+^a=&tmp\$1!0, tmp\$1=&tmp\$2!0, tmp\$2=4$
+--
+^warning: ignoring
diff --git a/regression/cbmc/pointer-function-parameters/main.c b/regression/cbmc/pointer-function-parameters/main.c
new file mode 100644
index 00000000000..c6804d2f977
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters/main.c
@@ -0,0 +1,12 @@
+int fun(int *a)
+{
+  if(!a)
+  {
+    return 0;
+  }
+  if(*a==4)
+  {
+    return 1;
+  }
+  return 2;
+}
diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/cbmc/pointer-function-parameters/test.desc
new file mode 100644
index 00000000000..b9aa6240dea
--- /dev/null
+++ b/regression/cbmc/pointer-function-parameters/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--function fun --cover branch
+^\*\* 5 of 5 covered \(100\.0%\)$
+^\*\* Used 3 iterations$
+^Test suite:$
+^a=\(\(signed int \*\)NULL\), tmp\$1=[^,]*$
+^a=&tmp\$1!0, tmp\$1=4$
+^a=&tmp\$1!0, tmp\$1=([012356789][0-9]*|4[0-9]+)$
+--
+^warning: ignoring
diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile
index ac509c591dd..cfee8e68f07 100644
--- a/src/ansi-c/Makefile
+++ b/src/ansi-c/Makefile
@@ -11,6 +11,7 @@ SRC = anonymous_member.cpp \
       ansi_c_typecheck.cpp \
       ansi_c_y.tab.cpp \
       c_misc.cpp \
+      c_nondet_symbol_factory.cpp \
       c_preprocess.cpp \
       c_qualifiers.cpp \
       c_sizeof.cpp \
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index bfb3f8663b1..ecb2dcc73cd 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <linking/static_lifetime_init.h>
 
 #include "ansi_c_entry_point.h"
+#include "c_nondet_symbol_factory.h"
 
 /*******************************************************************\
 
@@ -40,66 +41,31 @@ Function: build_function_environment
 exprt::operandst build_function_environment(
   const code_typet::parameterst &parameters,
   code_blockt &init_code,
-  symbol_tablet &symbol_table)
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler)
 {
-  exprt::operandst result;
-  result.resize(parameters.size());
+  exprt::operandst main_arguments;
+  main_arguments.resize(parameters.size());
 
-  std::size_t i=0;
-
-  for(const auto &p : parameters)
+  for(std::size_t param_number=0;
+      param_number<parameters.size();
+      param_number++)
   {
-    irep_idt base_name=p.get_base_name().empty()?
-      ("argument#"+std::to_string(i)):p.get_base_name();
-    irep_idt identifier=id2string(goto_functionst::entry_point())+
-      "::"+id2string(base_name);
-
-    {
-      auxiliary_symbolt new_symbol;
-      new_symbol.mode=ID_C;
-      new_symbol.is_static_lifetime=false;
-      new_symbol.name=identifier;
-      new_symbol.base_name=base_name;
-      new_symbol.type=p.type();
-
-      symbol_table.move(new_symbol);
-    }
-
-    symbol_exprt symbol_expr(identifier, p.type());
-
-    code_declt decl;
-    decl.symbol()=symbol_expr;
-
-    init_code.add(decl);
-
-    // nondet init for _Bool
-    if(decl.symbol().type().id()==ID_c_bool)
-    {
-      code_assignt assign(
-        decl.symbol(),
-        typecast_exprt(
-          side_effect_expr_nondett(bool_typet()),
-          decl.symbol().type()));
-
-      init_code.move_to_operands(assign);
-    }
-
-    codet input(ID_input);
-    input.operands().resize(2);
-
-    // record as an input
-    input.op0()=address_of_exprt(
-      index_exprt(string_constantt(base_name), from_integer(0, index_type())));
-    input.op1()=symbol_expr;
-    input.add_source_location()=p.source_location();
-
-    init_code.move_to_operands(input);
-
-    result[i]=symbol_expr;
-    i++;
+    const code_typet::parametert &p=parameters[param_number];
+    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);
   }
 
-  return result;
+  return main_arguments;
 }
 
 /*******************************************************************\
@@ -506,7 +472,11 @@ bool ansi_c_entry_point(
   {
     // produce nondet arguments
     call_main.arguments()=
-      build_function_environment(parameters, init_code, symbol_table);
+      build_function_environment(
+        parameters,
+        init_code,
+        symbol_table,
+        message_handler);
   }
 
   init_code.move_to_operands(call_main);
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
new file mode 100644
index 00000000000..9149d6f8786
--- /dev/null
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -0,0 +1,327 @@
+/*******************************************************************\
+
+Module: C Nondet Symbol Factory
+
+Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <set>
+#include <sstream>
+
+#include <util/arith_tools.h>
+#include <util/fresh_symbol.h>
+#include <util/std_types.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/namespace.h>
+#include <util/pointer_offset_size.h>
+#include <util/prefix.h>
+
+#include <linking/zero_initializer.h>
+
+#include <ansi-c/c_types.h>
+#include <ansi-c/string_constant.h>
+
+#include <goto-programs/goto_functions.h>
+
+#include "c_nondet_symbol_factory.h"
+
+/*******************************************************************\
+
+Function: declare_new_tmp_symbol
+
+ Inputs:
+  symbol_table - The symbol table to create the symbol in
+  loc - The location to assign to the symbol
+  type - The type of symbol to create
+  static_lifetime - Whether the symbol should have a static lifetime
+  prefix - The prefix to use for the symbol's basename
+
+ Outputs: Returns a reference to the new symbol
+
+ Purpose: Create a new temporary static 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, "", prefix, loc, ID_C, symbol_table);
+  tmp_symbol.is_static_lifetime=static_lifetime;
+
+  return tmp_symbol;
+}
+
+/*******************************************************************\
+
+Function: c_get_nondet_bool
+
+ Inputs:
+  type - Desired type (C_bool or plain bool)
+
+ Outputs: nondet expr of that type
+
+ Purpose:
+
+\*******************************************************************/
+
+static exprt c_get_nondet_bool(const typet &type)
+{
+  // We force this to 0 and 1 and won't consider other values
+  return typecast_exprt(side_effect_expr_nondett(bool_typet()), type);
+}
+
+class symbol_factoryt
+{
+  std::vector<symbolt const *> &symbols_created;
+  symbol_tablet &symbol_table;
+  const source_locationt &loc;
+  const bool assume_non_null;
+  namespacet ns;
+
+public:
+  symbol_factoryt(
+    std::vector<symbolt const *> &_symbols_created,
+    symbol_tablet &_symbol_table,
+    const source_locationt &loc,
+    const bool _assume_non_null):
+      symbols_created(_symbols_created),
+      symbol_table(_symbol_table),
+      loc(loc),
+      assume_non_null(_assume_non_null),
+      ns(_symbol_table)
+  {}
+
+  exprt allocate_object(
+    code_blockt &assignments,
+    const exprt &target_expr,
+    const typet &allocate_type,
+    const bool static_lifetime);
+
+  void gen_nondet_init(code_blockt &assignments, const exprt &expr);
+};
+
+/*******************************************************************\
+
+Function: symbol_factoryt::allocate_object
+
+ Inputs:
+  assignments - The code block to add code to
+  target_expr - The expression which we are allocating a symbol for
+  allocate_type - The type to use for the symbol. If this doesn't match
+                  target_expr then a cast will be used for the assignment
+  static_lifetime - Whether the symbol created should have static lifetime
+
+ Outputs: Returns the address of the allocated symbol
+
+ Purpose: Create a symbol for a pointer to point to
+
+\*******************************************************************/
+
+exprt symbol_factoryt::allocate_object(
+  code_blockt &assignments,
+  const exprt &target_expr,
+  const typet &allocate_type,
+  const bool static_lifetime)
+{
+  const symbolt &aux_symbol=
+    c_new_tmp_symbol(
+      symbol_table,
+      loc,
+      allocate_type,
+      static_lifetime);
+  symbols_created.push_back(&aux_symbol);
+
+  const typet &allocate_type_resolved=ns.follow(allocate_type);
+  const typet &target_type=ns.follow(target_expr.type().subtype());
+  bool cast_needed=allocate_type_resolved!=target_type;
+
+  exprt aoe=address_of_exprt(aux_symbol.symbol_expr());
+  if(cast_needed)
+  {
+    aoe=typecast_exprt(aoe, target_expr.type());
+  }
+
+  // Add the following code to assignments:
+  //   <target_expr> = &tmp$<temporary_counter>
+  code_assignt assign(target_expr, aoe);
+  assign.add_source_location()=loc;
+  assignments.add(assign);
+
+  return aoe;
+}
+
+/*******************************************************************\
+
+Function: symbol_factoryt::gen_nondet_init
+
+ Inputs:
+  assignments - The code block to add code to
+  expr - The expression which we are generating a non-determinate value for
+
+ Outputs:
+
+ Purpose: Creates a nondet for expr, including calling itself recursively to
+          make appropriate symbols to point to if expr is a pointer.
+
+\*******************************************************************/
+
+void symbol_factoryt::gen_nondet_init(
+  code_blockt &assignments,
+  const exprt &expr)
+{
+  const typet &type=ns.follow(expr.type());
+
+  if(type.id()==ID_pointer)
+  {
+    // dereferenced type
+    const pointer_typet &pointer_type=to_pointer_type(type);
+    const typet &subtype=ns.follow(pointer_type.subtype());
+
+    code_blockt non_null_inst;
+
+    exprt allocated=allocate_object(non_null_inst, expr, subtype, false);
+
+    exprt init_expr;
+    if(allocated.id()==ID_address_of)
+    {
+      init_expr=allocated.op0();
+    }
+    else
+    {
+      init_expr=dereference_exprt(allocated, allocated.type().subtype());
+    }
+    gen_nondet_init(non_null_inst, init_expr);
+
+    if(assume_non_null)
+    {
+      // Add the following code to assignments:
+      // <expr> = <aoe>;
+      assignments.append(non_null_inst);
+    }
+    else
+    {
+      // Add the following code to assignments:
+      //           IF !(NONDET(_Bool) == FALSE) THEN GOTO <label1>
+      //           <expr> = <null pointer>
+      //           GOTO <label2>
+      // <label1>: <expr> = &tmp$<temporary_counter>;
+      //           <code from recursive call to gen_nondet_init() with
+      //             tmp$<temporary_counter>>
+      // And the next line is labelled label2
+      auto set_null_inst=code_assignt(expr, null_pointer_exprt(pointer_type));
+      set_null_inst.add_source_location()=loc;
+
+      code_ifthenelset null_check;
+      null_check.cond()=side_effect_expr_nondett(bool_typet());
+      null_check.then_case()=set_null_inst;
+      null_check.else_case()=non_null_inst;
+
+      assignments.add(null_check);
+    }
+  }
+  // TODO(OJones): Add support for structs and arrays
+  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):
+      side_effect_expr_nondett(type);
+    code_assignt assign(expr, rhs);
+    assign.add_source_location()=loc;
+
+    assignments.add(assign);
+  }
+}
+
+/*******************************************************************\
+
+Function: c_nondet_symbol_factory
+
+ Inputs:
+  init_code - The code block to add generated code to
+  symbol_table - The symbol table
+  base_name - The name to use for the symbol created
+  type - The type for the symbol created
+  loc - The location to assign to generated code
+  allow_null - Whether to allow a null value when type is a pointer
+
+ Outputs: Returns the symbol_exprt for the symbol created
+
+ Purpose: Creates a symbol and generates code so that it can vary
+          over all possible values for its type. For pointers this
+          involves allocating symbols which it can point to.
+
+\*******************************************************************/
+
+exprt c_nondet_symbol_factory(
+  code_blockt &init_code,
+  symbol_tablet &symbol_table,
+  const irep_idt base_name,
+  const typet &type,
+  const source_locationt &loc,
+  bool allow_null)
+{
+  irep_idt identifier=id2string(goto_functionst::entry_point())+
+    "::"+id2string(base_name);
+
+  auxiliary_symbolt main_symbol;
+  main_symbol.mode=ID_C;
+  main_symbol.is_static_lifetime=false;
+  main_symbol.name=identifier;
+  main_symbol.base_name=base_name;
+  main_symbol.type=type;
+
+  symbolt *main_symbol_ptr;
+  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
+  assert(!moving_symbol_failed);
+
+  std::vector<symbolt const *> symbols_created;
+  symbol_exprt main_symbol_expr=(*main_symbol_ptr).symbol_expr();
+  symbols_created.push_back(main_symbol_ptr);
+
+  symbol_factoryt state(
+    symbols_created,
+    symbol_table,
+    loc,
+    !allow_null);
+  code_blockt assignments;
+  state.gen_nondet_init(assignments, main_symbol_expr);
+
+  // Add the following code to init_code for each symbol that's been created:
+  //   <type> <identifier>;
+  for(symbolt const *symbol_ptr : symbols_created)
+  {
+    code_declt decl(symbol_ptr->symbol_expr());
+    decl.add_source_location()=loc;
+    init_code.add(decl);
+  }
+
+  init_code.append(assignments);
+
+  // Add the following code to init_code for each symbol that's been created:
+  //   INPUT("<identifier>", <identifier>);
+  for(symbolt const *symbol_ptr : symbols_created)
+  {
+    codet input_code(ID_input);
+    input_code.operands().resize(2);
+    input_code.op0()=
+      address_of_exprt(index_exprt(
+        string_constantt(symbol_ptr->base_name),
+        from_integer(0, index_type())));
+    input_code.op1()=symbol_ptr->symbol_expr();
+    input_code.add_source_location()=loc;
+    init_code.add(input_code);
+  }
+
+  return main_symbol_expr;
+}
diff --git a/src/ansi-c/c_nondet_symbol_factory.h b/src/ansi-c/c_nondet_symbol_factory.h
new file mode 100644
index 00000000000..8760de6ac55
--- /dev/null
+++ b/src/ansi-c/c_nondet_symbol_factory.h
@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: C Nondet Symbol Factory
+
+Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#ifndef CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
+#define CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
+
+#include <util/std_code.h>
+#include <util/symbol_table.h>
+
+exprt c_nondet_symbol_factory(
+  code_blockt &init_code,
+  symbol_tablet &symbol_table,
+  const irep_idt base_name,
+  const typet &type,
+  const source_locationt &,
+  bool allow_null);
+
+#endif // CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index 60678dadfa1..1de7a09f227 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -38,7 +38,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 Function: create_initialize
 
-  Inputs:
+ Inputs:
 
  Outputs:
 
@@ -90,7 +90,7 @@ static bool should_init_symbol(const symbolt &sym)
 
 Function: java_static_lifetime_init
 
-  Inputs:
+ Inputs:
 
  Outputs:
 
@@ -142,8 +142,7 @@ bool java_static_lifetime_init(
           allow_null,
           symbol_table,
           max_nondet_array_length,
-          source_location,
-          message_handler);
+          source_location);
         code_assignt assignment(sym.symbol_expr(), newsym);
         code_block.add(assignment);
       }
@@ -182,7 +181,7 @@ bool java_static_lifetime_init(
 
 Function: java_build_arguments
 
-  Inputs:
+ Inputs:
 
  Outputs:
 
@@ -234,8 +233,7 @@ exprt::operandst java_build_arguments(
         allow_null,
         symbol_table,
         max_nondet_array_length,
-        function.location,
-        message_handler);
+        function.location);
 
     const symbolt &p_symbol=
       symbol_table.lookup(parameters[param_number].get_identifier());
@@ -261,7 +259,7 @@ exprt::operandst java_build_arguments(
 
 Function: java_record_outputs
 
-  Inputs:
+ Inputs:
 
  Outputs:
 
@@ -520,10 +518,13 @@ main_function_resultt get_main_symbol(
 
 Function: java_entry_point
 
-  Inputs: symbol_table
-          main class
-          message_handler
-          allow pointers in initialization code to be null
+ Inputs:
+  symbol_table
+  main class
+  message_handler
+  assume_init_pointers_not_null - allow pointers in initialization code to be
+                                  null
+  max_nondet_array_length
 
  Outputs: true if error occurred on entry point search
 
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 166be7827c9..34f5495bb85 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -6,7 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <set>
+#include <unordered_set>
 #include <sstream>
 
 #include <util/arith_tools.h>
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
-#include <util/message.h>
 #include <util/namespace.h>
 #include <util/pointer_offset_size.h>
 #include <util/prefix.h>
@@ -25,14 +24,59 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_types.h"
 #include "java_utils.h"
 
-class java_object_factoryt:public messaget
+/*******************************************************************\
+
+Function: new_tmp_symbol
+
+ Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static symbolt &new_tmp_symbol(
+  symbol_tablet &symbol_table,
+  const source_locationt &loc,
+  const typet &type,
+  const std::string &prefix="tmp_object_factory")
+{
+  return get_fresh_aux_symbol(
+    type,
+    "",
+    prefix,
+    loc,
+    ID_java,
+    symbol_table);
+}
+
+/*******************************************************************\
+
+Function: get_nondet_bool
+
+ Inputs: Desired type (C_bool or plain bool)
+
+ Outputs: nondet expr of that type
+
+ Purpose:
+
+\*******************************************************************/
+
+static exprt get_nondet_bool(const typet &type)
+{
+  // We force this to 0 and 1 and won't consider
+  // other values.
+  return typecast_exprt(side_effect_expr_nondett(bool_typet()), type);
+}
+
+class java_object_factoryt
 {
   code_blockt &init_code;
-  std::set<irep_idt> recursion_set;
+  std::unordered_set<irep_idt, irep_id_hash> recursion_set;
   bool assume_non_null;
   size_t max_nondet_array_length;
   symbol_tablet &symbol_table;
-  message_handlert &message_handler;
   namespacet ns;
 
 public:
@@ -40,15 +84,13 @@ class java_object_factoryt:public messaget
     code_blockt &_init_code,
     bool _assume_non_null,
     size_t _max_nondet_array_length,
-    symbol_tablet &_symbol_table,
-    message_handlert &_message_handler):
-    init_code(_init_code),
-    assume_non_null(_assume_non_null),
-    max_nondet_array_length(_max_nondet_array_length),
-    symbol_table(_symbol_table),
-    message_handler(_message_handler),
-    ns(_symbol_table)
-    {}
+    symbol_tablet &_symbol_table):
+      init_code(_init_code),
+      assume_non_null(_assume_non_null),
+      max_nondet_array_length(_max_nondet_array_length),
+      symbol_table(_symbol_table),
+      ns(_symbol_table)
+  {}
 
   exprt allocate_object(
     const exprt &,
@@ -72,7 +114,7 @@ class java_object_factoryt:public messaget
 
 Function: java_object_factoryt::allocate_object
 
-  Inputs:
+ Inputs:
 
  Outputs:
 
@@ -152,17 +194,17 @@ exprt java_object_factoryt::allocate_object(
 
 Function: java_object_factoryt::gen_nondet_init
 
-  Inputs:
-   expr -
-   is_sub -
-   class_identifier -
-   loc -
-   create_dynamic_objects -
-   override - Ignore the LHS' real type. Used at the moment for
-              reference arrays, which are implemented as void*
-              arrays but should be init'd as their true type with
-              appropriate casts.
-   override_type - Type to use if ignoring the LHS' real type
+ Inputs:
+  expr -
+  is_sub -
+  class_identifier -
+  loc -
+  create_dynamic_objects -
+  override - Ignore the LHS' real type. Used at the moment for
+             reference arrays, which are implemented as void*
+             arrays but should be init'd as their true type with
+             appropriate casts.
+  override_type - Type to use if ignoring the LHS' real type
 
  Outputs:
 
@@ -209,26 +251,13 @@ void java_object_factoryt::gen_nondet_init(
     code_labelt set_null_label;
     code_labelt init_done_label;
 
-    static size_t synthetic_constructor_count=0;
-
     if(!assume_non_null)
     {
-      auto returns_null_sym=
-        new_tmp_symbol(
-          symbol_table,
-          loc,
-          c_bool_typet(1),
-          "opaque_returns_null");
-      auto returns_null=returns_null_sym.symbol_expr();
-      auto assign_returns_null=
-          code_assignt(returns_null, get_nondet_bool(returns_null_sym.type));
-      assign_returns_null.add_source_location()=loc;
-      init_code.move_to_operands(assign_returns_null);
-
       auto set_null_inst=
         code_assignt(expr, null_pointer_exprt(pointer_type));
       set_null_inst.add_source_location()=loc;
 
+      static size_t synthetic_constructor_count=0;
       std::string fresh_label=
         "post_synthetic_malloc_"+std::to_string(++synthetic_constructor_count);
       set_null_label=code_labelt(fresh_label, set_null_inst);
@@ -236,10 +265,9 @@ void java_object_factoryt::gen_nondet_init(
       init_done_label=code_labelt(fresh_label+"_init_done", code_skipt());
 
       code_ifthenelset null_check;
-      exprt null_return=
-        zero_initializer(returns_null_sym.type, loc, ns, message_handler);
+      exprt null_return=from_integer(0, c_bool_typet(1));
       null_check.cond()=
-        notequal_exprt(returns_null, null_return);
+        notequal_exprt(get_nondet_bool(c_bool_typet(1)), null_return);
       null_check.then_case()=code_gotot(fresh_label);
       init_code.move_to_operands(null_check);
     }
@@ -340,7 +368,7 @@ void java_object_factoryt::gen_nondet_init(
 
 Function: java_object_factoryt::gen_nondet_array_init
 
-  Inputs:
+ Inputs:
 
  Outputs:
 
@@ -471,55 +499,9 @@ void java_object_factoryt::gen_nondet_array_init(
 
 /*******************************************************************\
 
-Function: new_tmp_symbol
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-symbolt &new_tmp_symbol(
-  symbol_tablet &symbol_table,
-  const source_locationt &loc,
-  const typet &type,
-  const std::string &prefix)
-{
-  return get_fresh_aux_symbol(
-    type,
-    "",
-    prefix,
-    loc,
-    ID_java,
-    symbol_table);
-}
-
-/*******************************************************************\
-
-Function: get_nondet_bool
-
-  Inputs: Desired type (C_bool or plain bool)
-
- Outputs: nondet expr of that type
-
- Purpose:
-
-\*******************************************************************/
-
-exprt get_nondet_bool(const typet &type)
-{
-  // We force this to 0 and 1 and won't consider
-  // other values.
-  return typecast_exprt(side_effect_expr_nondett(bool_typet()), type);
-}
-
-/*******************************************************************\
-
 Function: object_factory
 
-  Inputs:
+ Inputs:
 
  Outputs:
 
@@ -533,8 +515,7 @@ exprt object_factory(
   bool allow_null,
   symbol_tablet &symbol_table,
   size_t max_nondet_array_length,
-  const source_locationt &loc,
-  message_handlert &message_handler)
+  const source_locationt &loc)
 {
   if(type.id()==ID_pointer)
   {
@@ -550,8 +531,7 @@ exprt object_factory(
       init_code,
       !allow_null,
       max_nondet_array_length,
-      symbol_table,
-      message_handler);
+      symbol_table);
     state.gen_nondet_init(
       object,
       false,
diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h
index 37ed40f0ec9..01e0205df71 100644
--- a/src/java_bytecode/java_object_factory.h
+++ b/src/java_bytecode/java_object_factory.h
@@ -19,15 +19,6 @@ exprt object_factory(
   bool allow_null,
   symbol_tablet &symbol_table,
   size_t max_nondet_array_length,
-  const source_locationt &,
-  message_handlert &message_handler);
-
-exprt get_nondet_bool(const typet &);
-
-symbolt &new_tmp_symbol(
-  symbol_tablet &symbol_table,
-  const source_locationt &,
-  const typet &,
-  const std::string &prefix="tmp_object_factory");
+  const source_locationt &);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp
index 8cc7979c4ac..d7a4f2aa0fd 100644
--- a/src/util/std_code.cpp
+++ b/src/util/std_code.cpp
@@ -177,3 +177,27 @@ const codet &codet::last_statement() const
 
   return *this;
 }
+
+/*******************************************************************\
+
+Function: code_blockt::append
+
+ Inputs:
+  extra_block - The input code_blockt
+
+ Outputs:
+
+ Purpose: Add all the codets from extra_block to the current
+          code_blockt
+
+\*******************************************************************/
+
+void code_blockt::append(const code_blockt &extra_block)
+{
+  operands().reserve(operands().size()+extra_block.operands().size());
+
+  for(const auto &operand : extra_block.operands())
+  {
+    add(to_code(operand));
+  }
+}
diff --git a/src/util/std_code.h b/src/util/std_code.h
index 17d038274a3..9768098b1b7 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -82,6 +82,8 @@ class code_blockt:public codet
     copy_to_operands(code);
   }
 
+  void append(const code_blockt &extra_block);
+
   // This is the closing '}' or 'END' at the end of a block
   source_locationt end_location() const
   {