diff --git a/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.class b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.class
new file mode 100644
index 00000000000..bf9694b3f36
Binary files /dev/null and b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.class differ
diff --git a/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.java b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.java
new file mode 100644
index 00000000000..6e04c6f345a
--- /dev/null
+++ b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Item.java
@@ -0,0 +1,5 @@
+package com.diffblue.javatest.nestedobjects.subpackage;
+
+public class Item {
+  public int cost;
+}
diff --git a/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class
new file mode 100644
index 00000000000..9c810453dec
Binary files /dev/null and b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.class differ
diff --git a/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.java b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.java
new file mode 100644
index 00000000000..012c3c7a355
--- /dev/null
+++ b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/Order.java
@@ -0,0 +1,25 @@
+package com.diffblue.javatest.nestedobjects.subpackage;
+
+public class Order {
+  public Item item;
+
+  /**
+   * Checks if this order has an item.
+   */
+  public boolean hasItem() {
+    if (item == null) {
+      return false;
+    } else {
+      return true;
+    }
+  }
+
+  /**
+   * Sets the item for this order.
+   */
+  public boolean setItem(Item item) {
+    boolean exists = hasItem();
+    this.item = item;
+    return exists;
+  }
+}
diff --git a/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/readme.txt b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/readme.txt
new file mode 100644
index 00000000000..2a237709812
--- /dev/null
+++ b/regression/cbmc-java/internal1/com/diffblue/javatest/nestedobjects/subpackage/readme.txt
@@ -0,0 +1,2 @@
+Source of benchmark:
+https://github.com/DiffBlue-benchmarks/java-test
\ No newline at end of file
diff --git a/regression/cbmc-java/internal1/test.desc b/regression/cbmc-java/internal1/test.desc
new file mode 100644
index 00000000000..09047367ca9
--- /dev/null
+++ b/regression/cbmc-java/internal1/test.desc
@@ -0,0 +1,13 @@
+CORE
+com/diffblue/javatest/nestedobjects/subpackage/Order.class
+--json-ui --function 'com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:(Lcom/diffblue/javatest/nestedobjects/subpackage/Item;)Z' --cover location --trace
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+"identifier": "__CPROVER_initialize",\n *"sourceLocation": [{][}]\n *[}],\n *"hidden": false,\n *"internal": true,\n *"stepType": "function-call",
+"internal": true,\n *"lhs": "tmp_object_factory[$][0-9]+",
+"internal": false,\n *"sourceLocation": [{]\n *"file": "com/diffblue/javatest/nestedobjects/subpackage/Order.java",\n *"function": "java::com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:[(]Lcom/diffblue/javatest/nestedobjects/subpackage/Item;[)]Z",\n *"line": "21"\n *[}],\n *"stepType": "function-call",
+"internal": false,\n *"lhs": "this",\n *"mode": "java",\n *"sourceLocation": [{]\n *"file": "com/diffblue/javatest/nestedobjects/subpackage/Order.java",\n *"function": "java::com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:[(]Lcom/diffblue/javatest/nestedobjects/subpackage/Item;[)]Z",
+"internal": false,\n *"lhs": "item",\n *"mode": "java",\n *"sourceLocation": [{]\n *"file": "com/diffblue/javatest/nestedobjects/subpackage/Order.java",\n *"function": "java::com.diffblue.javatest.nestedobjects.subpackage.Order.setItem:[(]Lcom/diffblue/javatest/nestedobjects/subpackage/Item;[)]Z",
+--
+^warning: ignoring
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 29ba8e30236..d5c7b62c60a 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -206,7 +206,11 @@ void update_internal_field(
   // set internal field to _start function-return step
   if(SSA_step.source.pc->function==goto_functionst::entry_point())
   {
-    goto_trace_step.internal=true;
+    // "__CPROVER_*" function calls in __CPROVER_start are already marked as
+    // internal. Don't mark any other function calls (i.e. "main"), function
+    // arguments or any other parts of a code_function_callt as internal.
+    if(SSA_step.source.pc->code.get_statement()!=ID_function_call)
+      goto_trace_step.internal=true;
   }
 }