diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp
index 8e5663b45e2..e0440f6ab17 100644
--- a/jbmc/src/java_bytecode/assignments_from_json.cpp
+++ b/jbmc/src/java_bytecode/assignments_from_json.cpp
@@ -99,7 +99,7 @@ has_enum_type(const exprt &expr, const symbol_table_baset &symbol_table)
 /// \param declaring_class_type: type of the class where \p expr is declared.
 /// \return `true` if \p expr has an enum type and is declared within the
 ///   definition of that same type, `false` otherwise.
-bool is_enum_with_type_equal_to_declaring_type(
+static bool is_enum_with_type_equal_to_declaring_type(
   const exprt &expr,
   const symbol_table_baset &symbol_table,
   const java_class_typet &declaring_class_type)
@@ -188,9 +188,8 @@ static bool has_nondet_length(const jsont &json)
   if(!json.is_object())
     return false;
   const auto &json_object = to_json_object(json);
-  if(json_object.find("@nondetLength") != json_object.end())
-    return (json["@nondetLength"].is_true());
-  return false;
+  auto nondet_it = json_object.find("@nondetLength");
+  return nondet_it != json_object.end() && nondet_it->second.is_true();
 }
 
 /// For typed versions of primitive, string or array types, looks up their
@@ -438,63 +437,82 @@ static void allocate_array(
   info.block.add(assign);
 }
 
+/// Declare a non-deterministic length expression
+/// \param[out] allocate: allocation functor
+/// \param[out] code: code block to which code will get appended
+/// \param loc: location for the created code
+/// \return the length expression that has been non-deterministically created
+static symbol_exprt nondet_length(
+  allocate_objectst &allocate,
+  code_blockt &code,
+  source_locationt loc)
+{
+  const symbol_exprt length_expr = allocate.allocate_automatic_local_object(
+    java_int_type(), "user_specified_array_length");
+  code.add(code_assignt{
+    length_expr, side_effect_expr_nondett{java_int_type(), std::move(loc)}});
+  code.add(code_assumet{binary_predicate_exprt{
+    length_expr, ID_ge, from_integer(0, java_int_type())}});
+  return length_expr;
+}
+
 /// One of the cases in the recursive algorithm: the case where \p expr
-/// represents an array.
-/// The length of the array is given by a symbol: \p given_length_expr if it is
-/// specified (this will be the case when there are two or more reference-equal
-/// arrays), or a fresh symbol otherwise.
-/// If \p given_length_expr is specified, we assume that an array with this
-/// symbol as its length has already been allocated and that \p expr has been
-/// assigned to it.
-/// Either way, the length symbol stores a nondet integer, and we add
-/// constraints on this: if "nondetLength" is specified in \p json, then the
-/// number of elements specified in \p json should be the minimum length of the
-/// array. Otherwise the number of elements should be the exact length of the
-/// array.
+/// represents an array which is not flagged with `@nondetLength`.
+/// The length of the array is given by symbol \p given_length_expr.
+/// We assume that an array with this symbol as its length has already been
+/// allocated and that \p expr has been assigned to it.
+/// We constraint the length of the array to be the number of elements, which
+/// is known and constant.
 /// For the assignment of the array elements, see
 /// \ref assign_array_data_component_from_json.
 /// For the overall algorithm, see \ref assign_from_json_rec.
-static void assign_array_from_json(
+static void assign_det_length_array_from_json(
   const exprt &expr,
   const jsont &json,
-  const optionalt<symbol_exprt> &given_length_expr,
+  const exprt &given_length_expr,
   const optionalt<std::string> &type_from_array,
   object_creation_infot &info)
 {
   PRECONDITION(is_java_array_type(expr.type()));
   const auto &element_type =
     java_array_element_type(to_struct_tag_type(expr.type().subtype()));
+  const json_arrayt json_array = get_untyped_array(json, element_type);
+  const auto number_of_elements =
+    from_integer(json_array.size(), java_int_type());
+  info.block.add(
+    code_assumet{equal_exprt{given_length_expr, number_of_elements}});
+  assign_array_data_component_from_json(expr, json, type_from_array, info);
+}
 
-  exprt length_expr;
-  if(given_length_expr)
-    length_expr = *given_length_expr;
-  else
-  {
-    length_expr = info.allocate_objects.allocate_automatic_local_object(
-      java_int_type(), "user_specified_array_length");
-    info.block.add(code_assignt{
-      length_expr, side_effect_expr_nondett{java_int_type(), info.loc}});
-    info.block.add(code_assumet{binary_predicate_exprt{
-      length_expr, ID_ge, from_integer(0, java_int_type())}});
-    allocate_array(expr, length_expr, info);
-  }
+/// One of the cases in the recursive algorithm: the case where \p expr
+/// represents an array which is flagged with @nondetLength.
+/// The length of the array is given by symbol \p given_length_expr.
+/// We assume that an array with this symbol as its length has already been
+/// allocated and that \p expr has been assigned to it.
+/// We constrain the length of the array to be greater or equal to the number
+/// of elements specified in \p json.
+/// For the assignment of the array elements, see
+/// \ref assign_array_data_component_from_json.
+/// For the overall algorithm, see \ref assign_from_json_rec.
+static void assign_nondet_length_array_from_json(
+  const exprt &expr,
+  const jsont &json,
+  const exprt &given_length_expr,
+  const optionalt<std::string> &type_from_array,
+  object_creation_infot &info)
+{
+  PRECONDITION(is_java_array_type(expr.type()));
+  const auto &element_type =
+    java_array_element_type(to_struct_tag_type(expr.type().subtype()));
   const json_arrayt json_array = get_untyped_array(json, element_type);
   const auto number_of_elements =
     from_integer(json_array.size(), java_int_type());
-  info.block.add(code_assumet{
-    binary_predicate_exprt{length_expr, ID_ge, number_of_elements}});
-  if(has_nondet_length(json))
-  {
-    info.block.add(code_assumet{binary_predicate_exprt{
-      length_expr,
+  info.block.add(code_assumet{and_exprt{
+    binary_predicate_exprt{given_length_expr, ID_ge, number_of_elements},
+    binary_predicate_exprt{
+      given_length_expr,
       ID_le,
-      from_integer(info.max_user_array_length, java_int_type())}});
-  }
-  else
-  {
-    info.block.add(code_assumet{
-      binary_predicate_exprt{length_expr, ID_le, number_of_elements}});
-  }
+      from_integer(info.max_user_array_length, java_int_type())}}});
   assign_array_data_component_from_json(expr, json, type_from_array, info);
 }
 
@@ -771,8 +789,18 @@ static void assign_reference_from_json(
   {
     if(is_java_array_type(expr.type()))
     {
-      assign_array_from_json(
-        reference.expr, json, reference.array_length, type_from_array, info);
+      INVARIANT(
+        reference.array_length, "an array reference should store its length");
+      if(has_nondet_length(json))
+      {
+        assign_nondet_length_array_from_json(
+          reference.expr, json, *reference.array_length, type_from_array, info);
+      }
+      else
+      {
+        assign_det_length_array_from_json(
+          reference.expr, json, *reference.array_length, type_from_array, info);
+      }
     }
     else
       assign_struct_from_json(dereference_exprt(reference.expr), json, info);
@@ -810,7 +838,26 @@ void assign_from_json_rec(
       assign_reference_from_json(expr, json, type_from_array, info);
     }
     else if(is_java_array_type(expr.type()))
-      assign_array_from_json(expr, json, {}, type_from_array, info);
+    {
+      if(has_nondet_length(json))
+      {
+        const exprt length =
+          nondet_length(info.allocate_objects, info.block, info.loc);
+        allocate_array(expr, length, info);
+        assign_nondet_length_array_from_json(
+          expr, json, length, type_from_array, info);
+      }
+      else
+      {
+        PRECONDITION(is_java_array_type(expr.type()));
+        const auto &element_type =
+          java_array_element_type(to_struct_tag_type(expr.type().subtype()));
+        const std::size_t length = get_untyped_array(json, element_type).size();
+        allocate_array(expr, from_integer(length, java_int_type()), info);
+        assign_array_data_component_from_json(
+          expr, json, type_from_array, info);
+      }
+    }
     else if(
       const auto runtime_type =
         ::runtime_type(json, type_from_array, info.symbol_table))
diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile
index 5a9966ece15..f58793e1c59 100644
--- a/jbmc/unit/Makefile
+++ b/jbmc/unit/Makefile
@@ -48,6 +48,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
        java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
        java_bytecode/java_object_factory/struct_tag_types.cpp \
        java_bytecode/java_replace_nondet/replace_nondet.cpp \
+       java_bytecode/java_static_initializers/assignments_from_json.cpp \
        java_bytecode/java_static_initializers/java_static_initializers.cpp \
        java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
        java_bytecode/java_trace_validation/java_trace_validation.cpp \
diff --git a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp
new file mode 100644
index 00000000000..da4fa66278d
--- /dev/null
+++ b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp
@@ -0,0 +1,412 @@
+/*******************************************************************\
+
+Module: Unit tests for assign_from_json
+
+Author: Romain Brenguier, romain.brenguier@diffblue.com
+
+\*******************************************************************/
+
+#include <java_bytecode/assignments_from_json.h>
+
+#include <java_bytecode/ci_lazy_methods_needed.h>
+#include <java_bytecode/java_bytecode_convert_class.h>
+#include <java_bytecode/java_types.h>
+#include <java_bytecode/java_utils.h>
+#include <testing-utils/expr_query.h>
+#include <testing-utils/use_catch.h>
+#include <util/arith_tools.h>
+#include <util/json.h>
+#include <util/symbol_table.h>
+
+/// Add `clinit` function symbol to the table
+/// \return its identifier in the symbol table
+static irep_idt
+add_clinit(symbol_tablet &symbol_table, const std::string &class_name)
+{
+  symbolt clinit_symbol;
+  clinit_symbol.name = "java::" + class_name + ".<clinit>:()V";
+  set_declaring_class(clinit_symbol, "java::" + class_name);
+  symbol_table.insert(clinit_symbol);
+  return clinit_symbol.name;
+}
+
+static void add_class_with_components(
+  symbol_tablet &symbol_table,
+  const std::string &class_name,
+  const std::vector<std::pair<std::string, typet>> &components)
+{
+  symbolt test_class_symbol;
+  test_class_symbol.name = "java::" + class_name;
+  test_class_symbol.is_type = true;
+  test_class_symbol.type = [&] {
+    java_class_typet type;
+    // TODO java_class_typet constructors should ensure there is always a
+    // @class_identifier field, and that name is always set
+    type.set_name(test_class_symbol.name);
+    for(const auto &pair : components)
+      type.components().emplace_back(pair.first, pair.second);
+    return type;
+  }();
+  symbol_table.insert(test_class_symbol);
+}
+
+SCENARIO(
+  "assign_from_json",
+  "[core][java_static_initializers][assign_from_json]")
+{
+  symbol_tablet symbol_table;
+  const std::size_t max_user_array_length = 100;
+  std::unordered_map<std::string, object_creation_referencet> references;
+  std::unordered_multimap<irep_idt, symbolt> class_to_declared_symbols;
+
+  GIVEN("A class which has a static number in the provided JSON")
+  {
+    const json_objectt json = [] {
+      json_objectt entry{};
+      entry["field_name"] = [] {
+        json_objectt int_json;
+        int_json["value"] = json_numbert{"42"};
+        int_json["@type"] = json_stringt{"java.lang.Integer"};
+        return int_json;
+      }();
+      entry["@type"] = json_stringt{"TestClass"};
+      return entry;
+    }();
+    class_to_declared_symbols.emplace("java::TestClass", [] {
+      symbolt field_symbol;
+      field_symbol.base_name = "field_name";
+      field_symbol.name = "field_name_for_codet";
+      field_symbol.type = java_int_type();
+      field_symbol.is_static_lifetime = true;
+      return field_symbol;
+    }());
+    const irep_idt clinit_name = add_clinit(symbol_table, "TestClass");
+    add_class_with_components(
+      symbol_table,
+      "TestClass",
+      {std::pair<std::string, typet>("@class_identifier", string_typet{}),
+       std::pair<std::string, typet>("field_name", java_int_type())});
+
+    const reference_typet test_class_type =
+      reference_type(struct_tag_typet{"java::TestClass"});
+    code_blockt block;
+    optionalt<ci_lazy_methods_neededt> option{};
+    assign_from_json(
+      symbol_exprt{"symbol_to_assign", test_class_type},
+      json,
+      clinit_name,
+      block,
+      symbol_table,
+      option,
+      max_user_array_length,
+      references);
+    THEN("The instruction is the declaration of a symbol of TestClass* type")
+    {
+      const symbol_exprt declared_symbol =
+        make_query(block)[0].as<code_declt>()[0].as<symbol_exprt>().get();
+      REQUIRE(declared_symbol.type() == test_class_type);
+      THEN("The instruction allocates the symbol")
+      {
+        REQUIRE(
+          make_query(block)[1].as<code_assignt>()[0].as<symbol_exprt>().get() ==
+          declared_symbol);
+      }
+    }
+    THEN("The instruction assigns the symbol to `symbol_to_assign`")
+    {
+      REQUIRE(
+        make_query(block)[2]
+          .as<code_assignt>()[0]
+          .as<symbol_exprt>()
+          .get()
+          .get_identifier() == "symbol_to_assign");
+    }
+    THEN("The instruction zero-initializes the struct")
+    {
+      REQUIRE(
+        make_query(block)[3].as<code_assignt>()[1].get().type() ==
+        test_class_type.subtype());
+    }
+    THEN("The instruction assigns the field to 42")
+    {
+      REQUIRE(
+        make_query(block)[4]
+          .as<code_assignt>()[0]
+          .as<member_exprt>()
+          .get()
+          .get_component_name() == "field_name");
+      REQUIRE(
+        numeric_cast_v<mp_integer>(make_query(block)[4]
+                                     .as<code_assignt>()[1]
+                                     .as<constant_exprt>()
+                                     .get()) == 42);
+    }
+  }
+
+  GIVEN("A class with an array field")
+  {
+    const json_objectt json = [] {
+      json_objectt entry{};
+      entry["array_field"] = [] {
+        json_objectt array_json;
+        array_json["@items"] = json_arrayt{json_numbert{"42"}};
+        array_json["@type"] = json_stringt{"[I"};
+        return array_json;
+      }();
+      entry["@type"] = json_stringt{"TestClass"};
+      return entry;
+    }();
+    class_to_declared_symbols.emplace("java::TestClass", [] {
+      symbolt field_symbol;
+      field_symbol.base_name = "array_field";
+      field_symbol.name = "field_name_for_codet";
+      field_symbol.type = java_int_type();
+      field_symbol.is_static_lifetime = true;
+      return field_symbol;
+    }());
+    const irep_idt clinit_name = add_clinit(symbol_table, "TestClass");
+    add_class_with_components(
+      symbol_table,
+      "TestClass",
+      {std::pair<std::string, typet>("@class_identifier", string_typet{}),
+       std::pair<std::string, typet>("array_field", java_array_type('i'))});
+    // For array[int]
+    add_java_array_types(symbol_table);
+
+    const reference_typet test_class_type =
+      reference_type(struct_tag_typet{"java::TestClass"});
+    code_blockt block;
+    optionalt<ci_lazy_methods_neededt> option{};
+    assign_from_json(
+      symbol_exprt{"symbol_to_assign", test_class_type},
+      json,
+      clinit_name,
+      block,
+      symbol_table,
+      option,
+      max_user_array_length,
+      references);
+
+    THEN("The instruction is the declaration of a symbol of TestClass* type")
+    {
+      const symbol_exprt allocation_symbol =
+        make_query(block)[0].as<code_declt>()[0].as<symbol_exprt>().get();
+      REQUIRE(allocation_symbol.type() == test_class_type);
+      THEN("The instruction declares the array data")
+      {
+        REQUIRE(
+          make_query(block)[1]
+            .as<code_declt>()[0]
+            .as<symbol_exprt>()
+            .get()
+            .type() == java_reference_type(java_int_type()));
+      }
+      THEN("The instruction allocates the TestClass object")
+      {
+        REQUIRE(
+          make_query(block)[2].as<code_assignt>()[0].as<symbol_exprt>().get() ==
+          allocation_symbol);
+      }
+    }
+    THEN("The instruction assigns the symbol to \"symbol_to_assign\"")
+    {
+      REQUIRE(
+        make_query(block)[3]
+          .as<code_assignt>()[0]
+          .as<symbol_exprt>()
+          .get()
+          .get_identifier() == "symbol_to_assign");
+    }
+
+    THEN("The instruction zero-initializes the struct")
+    {
+      REQUIRE(
+        make_query(block)[4].as<code_assignt>()[0].get().type() ==
+        test_class_type.subtype());
+    }
+    THEN("The instruction allocates the array field, with a size of exactly 1")
+    {
+      REQUIRE(
+        make_query(block)[5]
+          .as<code_assignt>()[0]
+          .as<member_exprt>()
+          .get()
+          .get_component_name() == "array_field");
+      auto side_effect = make_query(block)[5]
+                           .as<code_assignt>()[1]
+                           .as<side_effect_exprt>()
+                           .get();
+      REQUIRE(side_effect.get_statement() == ID_java_new_array);
+      REQUIRE(
+        numeric_cast_v<mp_integer>(
+          make_query(side_effect)[0].as<constant_exprt>().get()) == 1);
+    }
+    THEN("The instruction copies the data to user_specified_array_data_init")
+    {
+      REQUIRE(
+        make_query(block)[6]
+          .as<code_assignt>()[0]
+          .as<symbol_exprt>()
+          .get()
+          .get_identifier() ==
+        "java::TestClass.<clinit>:()V::user_specified_array_data_init");
+    }
+    THEN("The instruction assigns the array cell to 42")
+    {
+      REQUIRE(
+        numeric_cast_v<mp_integer>(make_query(block)[7]
+                                     .as<code_assignt>()[1]
+                                     .as<constant_exprt>()
+                                     .get()) == 42);
+    }
+  }
+
+  GIVEN("A class with a nondet array field")
+  {
+    const json_objectt json = [] {
+      json_objectt entry{};
+      entry["array_field"] = [] {
+        json_objectt int_json;
+        int_json["@items"] = json_arrayt{json_numbert{"42"}};
+        int_json["@type"] = json_stringt{"[I"};
+        int_json["@nondetLength"] = json_truet{};
+        return int_json;
+      }();
+      entry["@type"] = json_stringt{"TestClass"};
+      return entry;
+    }();
+    class_to_declared_symbols.emplace("java::TestClass", [] {
+      symbolt field_symbol;
+      field_symbol.base_name = "array_field";
+      field_symbol.name = "field_name_for_codet";
+      field_symbol.type = java_int_type();
+      field_symbol.is_static_lifetime = true;
+      return field_symbol;
+    }());
+    const irep_idt clinit_name = add_clinit(symbol_table, "TestClass");
+    add_class_with_components(
+      symbol_table,
+      "TestClass",
+      {std::pair<std::string, typet>("@class_identifier", string_typet{}),
+       std::pair<std::string, typet>("array_field", java_array_type('i'))});
+    // For array[int]
+    add_java_array_types(symbol_table);
+
+    const reference_typet test_class_type =
+      reference_type(struct_tag_typet{"java::TestClass"});
+    code_blockt block;
+    optionalt<ci_lazy_methods_neededt> option{};
+    assign_from_json(
+      symbol_exprt{"symbol_to_assign", test_class_type},
+      json,
+      clinit_name,
+      block,
+      symbol_table,
+      option,
+      max_user_array_length,
+      references);
+
+    THEN("The instruction is the declaration of a symbol of TestClass* type")
+    {
+      const symbol_exprt allocation_symbol =
+        make_query(block)[0].as<code_declt>()[0].as<symbol_exprt>().get();
+      REQUIRE(allocation_symbol.type() == test_class_type);
+      THEN("The instruction declares a symbol for the length")
+      {
+        REQUIRE(
+          make_query(block)[1]
+            .as<code_declt>()[0]
+            .as<symbol_exprt>()
+            .get()
+            .type() == java_int_type());
+      }
+      THEN("The instruction declares the array data")
+      {
+        REQUIRE(
+          make_query(block)[2]
+            .as<code_declt>()[0]
+            .as<symbol_exprt>()
+            .get()
+            .type() == java_reference_type(java_int_type()));
+      }
+      THEN("The instruction allocates the struct")
+      {
+        REQUIRE(
+          make_query(block)[3].as<code_assignt>()[0].as<symbol_exprt>().get() ==
+          allocation_symbol);
+      }
+    }
+    THEN("The instruction assigns the symbol to \"symbol_to_assign\"")
+    {
+      REQUIRE(
+        make_query(block)[4]
+          .as<code_assignt>()[0]
+          .as<symbol_exprt>()
+          .get()
+          .get_identifier() == "symbol_to_assign");
+    }
+
+    THEN("The instruction zero-initializes the struct")
+    {
+      REQUIRE(
+        make_query(block)[5].as<code_assignt>()[0].get().type() ==
+        test_class_type.subtype());
+    }
+    THEN("The instruction makes the length nondet")
+    {
+      REQUIRE(
+        make_query(block)[6].as<code_assignt>()[0].get().type() ==
+        java_int_type());
+      auto side_effect = make_query(block)[6]
+                           .as<code_assignt>()[1]
+                           .as<side_effect_exprt>()
+                           .get();
+      REQUIRE(side_effect.get_statement() == ID_nondet);
+    }
+    THEN("The instruction adds assumption on the length")
+    {
+      REQUIRE(
+        make_query(block)[7].as<code_assumet>()[0].get().type() ==
+        bool_typet{});
+    }
+    THEN("The instruction allocates the array field, with the symbolic length")
+    {
+      REQUIRE(
+        make_query(block)[8]
+          .as<code_assignt>()[0]
+          .as<member_exprt>()
+          .get()
+          .get_component_name() == "array_field");
+      auto side_effect = make_query(block)[8]
+                           .as<code_assignt>()[1]
+                           .as<side_effect_exprt>()
+                           .get();
+      REQUIRE(side_effect.get_statement() == ID_java_new_array);
+      make_query(side_effect)[0].as<symbol_exprt>().get();
+    }
+    THEN("The instruction adds additional assumptions on the length")
+    {
+      REQUIRE(
+        make_query(block)[9].as<code_assumet>()[0].get().type() ==
+        bool_typet{});
+    }
+    THEN("The instruction copies the data to user_specified_array_data_init")
+    {
+      REQUIRE(
+        make_query(block)[10]
+          .as<code_assignt>()[0]
+          .as<symbol_exprt>()
+          .get()
+          .get_identifier() ==
+        "java::TestClass.<clinit>:()V::user_specified_array_data_init");
+    }
+    THEN("The instruction assigns the array cell to 42")
+    {
+      REQUIRE(
+        numeric_cast_v<mp_integer>(make_query(block)[11]
+                                     .as<code_assignt>()[1]
+                                     .as<constant_exprt>()
+                                     .get()) == 42);
+    }
+  }
+}