From e53d2b4d45dfd7809f160ebfffd2ea959ee5c062 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Tue, 8 Jan 2019 16:16:24 +0000
Subject: [PATCH] fix for uninterpreted functions

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

Fixes #3561.
---
 regression/cbmc/uninterpreted_function/uf1.c    |  7 +++++++
 regression/cbmc/uninterpreted_function/uf1.desc | 10 ++++++++++
 scripts/delete_failing_smt2_solver_tests        |  1 +
 src/goto-symex/build_goto_trace.cpp             | 15 +++++++++------
 4 files changed, 27 insertions(+), 6 deletions(-)
 create mode 100644 regression/cbmc/uninterpreted_function/uf1.c
 create mode 100644 regression/cbmc/uninterpreted_function/uf1.desc

diff --git a/regression/cbmc/uninterpreted_function/uf1.c b/regression/cbmc/uninterpreted_function/uf1.c
new file mode 100644
index 0000000000..420c44a0c7
--- /dev/null
+++ b/regression/cbmc/uninterpreted_function/uf1.c
@@ -0,0 +1,7 @@
+_Bool __CPROVER_uninterpreted_f();
+
+main()
+{
+  _Bool a = __CPROVER_uninterpreted_f();
+  assert(0);
+}
diff --git a/regression/cbmc/uninterpreted_function/uf1.desc b/regression/cbmc/uninterpreted_function/uf1.desc
new file mode 100644
index 0000000000..879865e93e
--- /dev/null
+++ b/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.
diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests
index 94ac578586..a995a33249 100755
--- a/scripts/delete_failing_smt2_solver_tests
+++ b/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
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 33a613b34f..481af90a2e 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/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