diff --git a/jbmc/regression/jbmc/nondet-array-size/TestClass.class b/jbmc/regression/jbmc/nondet-array-size/TestClass.class
new file mode 100644
index 00000000000..75f92d76b8e
Binary files /dev/null and b/jbmc/regression/jbmc/nondet-array-size/TestClass.class differ
diff --git a/jbmc/regression/jbmc/nondet-array-size/TestClass.java b/jbmc/regression/jbmc/nondet-array-size/TestClass.java
new file mode 100644
index 00000000000..2fd314083a5
--- /dev/null
+++ b/jbmc/regression/jbmc/nondet-array-size/TestClass.java
@@ -0,0 +1,11 @@
+import org.cprover.CProver;
+
+public class TestClass {
+
+    public static void minimalJbmc(Object[] a) {
+        CProver.assume(a != null && a.length > 1);
+        float[] assigned = new float[a.length];
+        assigned[0] = 1.0f;
+        assert(false);
+    }
+}
diff --git a/jbmc/regression/jbmc/nondet-array-size/test.desc b/jbmc/regression/jbmc/nondet-array-size/test.desc
new file mode 100644
index 00000000000..c4069a8a128
--- /dev/null
+++ b/jbmc/regression/jbmc/nondet-array-size/test.desc
@@ -0,0 +1,16 @@
+CORE
+TestClass.class
+--function "TestClass.minimalJbmc" --unwind 5 --max-nondet-string-length 10 --java-unwind-enum-static --trace --json-ui
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+--
+--
+Verify that when an array's size is determined by an array input, the resulting
+trace is valid.
+To compile this source file, use:
+
+```bash
+$ javac -g TestClass.java -cp ../../../lib/java-models-library/target/classes/:.
+```
+to have the cprover library on the class path.
diff --git a/regression/cbmc/enum-trace1/test_json.desc b/regression/cbmc/enum-trace1/test_json.desc
index 6619fc73eea..255c95b8c1c 100644
--- a/regression/cbmc/enum-trace1/test_json.desc
+++ b/regression/cbmc/enum-trace1/test_json.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --json-ui --function test --trace
 activate-multi-line-match
diff --git a/regression/cbmc/json1/test.desc b/regression/cbmc/json1/test.desc
index b9eb6a30118..bf66d83d928 100644
--- a/regression/cbmc/json1/test.desc
+++ b/regression/cbmc/json1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --json-ui --stop-on-fail
 activate-multi-line-match
diff --git a/regression/cbmc/trace_options_json_extended/extended.desc b/regression/cbmc/trace_options_json_extended/extended.desc
index beafa0649de..51bef1274d1 100644
--- a/regression/cbmc/trace_options_json_extended/extended.desc
+++ b/regression/cbmc/trace_options_json_extended/extended.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 test.c
 --trace --json-ui --trace-json-extended
 ^EXIT=10$
diff --git a/regression/cbmc/trace_options_json_extended/non-extended.desc b/regression/cbmc/trace_options_json_extended/non-extended.desc
index 5d03ca97bc1..c70b6540a9d 100644
--- a/regression/cbmc/trace_options_json_extended/non-extended.desc
+++ b/regression/cbmc/trace_options_json_extended/non-extended.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 test.c
 --trace --json-ui
 ^EXIT=10$
diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp
index 2e27f766b5d..02a6f0f128d 100644
--- a/src/goto-programs/json_goto_trace.cpp
+++ b/src/goto-programs/json_goto_trace.cpp
@@ -118,6 +118,10 @@ void convert_decl(
   const symbolt *symbol;
   irep_idt base_name, display_name;
 
+  DATA_INVARIANT(
+    step.full_lhs_value.is_not_nil(),
+    "full_lhs_value in assignment must not be nil");
+
   if(!ns.lookup(identifier, symbol))
   {
     base_name = symbol->base_name;
@@ -132,9 +136,6 @@ void convert_decl(
   }
   else
   {
-    DATA_INVARIANT(
-      step.full_lhs_value.is_not_nil(),
-      "full_lhs_value in assignment must not be nil");
     full_lhs_value = json(step.full_lhs_value, ns, ID_unknown);
   }