Move invariant out of if

The full_lhs_value should have a non-nil value regardless of whether the
identifier exists in the namespace. This makes visible that the SMT
solver returns for an unbounded array as value

((|__CPROVER_threads_exited#1| |__CPROVER_threads_exited#1|))

which is self-referential and thus not usable.

Author: thk123

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

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

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$

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$

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);
   }