fix for uninterpreted functions

CBMC supports uninterpreted functions; this feature had no test, and thus
got broken with 5081310.

Fixes #3561.

Author: kroening

regression/cbmc/uninterpreted_function/uf1.c

@@ -0,0 +1,7 @@
+_Bool __CPROVER_uninterpreted_f();
+
+main()
+{
+  _Bool a = __CPROVER_uninterpreted_f();
+  assert(0);
+}

regression/cbmc/uninterpreted_function/uf1.desc

@@ -0,0 +1,10 @@
+CORE
+uf1.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Basic test for an uninterpreted function; based on issue #3561.

scripts/delete_failing_smt2_solver_tests

@@ -74,6 +74,7 @@ rm struct6/test.desc
 rm struct7/test.desc
 rm trace-values/trace-values.desc
 rm trace_show_function_calls/test.desc
+rm uninterpreted_function/uf1.desc
 rm union12/test.desc
 rm union6/test.desc
 rm union7/test.desc

src/goto-symex/build_goto_trace.cpp

@@ -111,13 +111,16 @@ void set_internal_dynamic_object(
 {
   if(expr.id()==ID_symbol)
   {
-    const irep_idt &id=to_ssa_expr(expr).get_original_name();
-    const symbolt *symbol;
-    if(!ns.lookup(id, symbol))
+    if(expr.type().id() != ID_code)
     {
-      bool result = symbol->type.get_bool(ID_C_dynamic);
-      if(result)
-        goto_trace_step.internal=true;
+      const irep_idt &id = to_ssa_expr(expr).get_original_name();
+      const symbolt *symbol;
+      if(!ns.lookup(id, symbol))
+      {
+        bool result = symbol->type.get_bool(ID_C_dynamic);
+        if(result)
+          goto_trace_step.internal = true;
+      }
     }
   }
   else