diff --git a/regression/cbmc/String_Literal1/main.c b/regression/cbmc/String_Literal1/main.c
index 0185fdf91b2..6d7af0325bb 100644
--- a/regression/cbmc/String_Literal1/main.c
+++ b/regression/cbmc/String_Literal1/main.c
@@ -52,4 +52,6 @@ int main()
 
   // generic wide string, OS-dependent
   assert(sizeof(L""[0])==sizeof(wchar_t));
+
+  assert(0);
 }
diff --git a/regression/cbmc/String_Literal1/test.desc b/regression/cbmc/String_Literal1/test.desc
index 9efefbc7362..3ff5fed3f75 100644
--- a/regression/cbmc/String_Literal1/test.desc
+++ b/regression/cbmc/String_Literal1/test.desc
@@ -1,8 +1,15 @@
 CORE
 main.c
-
-^EXIT=0$
+--trace
+^State \d+ file main.c function main line 20 thread 0$
+^State \d+ file main.c function main line 36 thread 0$
+^State \d+ file main.c function main line 44 thread 0$
+^\*\* 1 of \d+ failed \(\d+ iterations\)$
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+^State \d+ (function main )?thread 0$
+--
+Each step in the trace must have a full source location, including line numbers.
diff --git a/src/util/expr.h b/src/util/expr.h
index ac9c21dfc6b..57457aa9c40 100644
--- a/src/util/expr.h
+++ b/src/util/expr.h
@@ -98,6 +98,30 @@ class exprt:public irept
   const operandst &operands() const
   { return (const operandst &)get_sub(); }
 
+  /// Add the source location from \p other, if it has any.
+  template <typename T>
+  T &with_source_location(const exprt &other) &
+  {
+    static_assert(
+      std::is_base_of<exprt, T>::value,
+      "The template argument T must be derived from exprt.");
+    if(other.source_location().is_not_nil())
+      add_source_location() = other.source_location();
+    return *static_cast<T *>(this);
+  }
+
+  /// Add the source location from \p other, if it has any.
+  template <typename T>
+  T &&with_source_location(const exprt &other) &&
+  {
+    static_assert(
+      std::is_base_of<exprt, T>::value,
+      "The template argument T must be derived from exprt.");
+    if(other.source_location().is_not_nil())
+      add_source_location() = other.source_location();
+    return std::move(*static_cast<T *>(this));
+  }
+
 protected:
   exprt &op0()
   { return operands().front(); }
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 95c7f93667c..098160b3040 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -1571,6 +1571,16 @@ class array_exprt : public multi_ary_exprt
   {
     return static_cast<array_typet &>(multi_ary_exprt::type());
   }
+
+  array_exprt &with_source_location(const exprt &other) &
+  {
+    return exprt::with_source_location<array_exprt>(other);
+  }
+
+  array_exprt &&with_source_location(const exprt &other) &&
+  {
+    return std::move(*this).exprt::with_source_location<array_exprt>(other);
+  }
 };
 
 template <>
diff --git a/src/util/string_constant.cpp b/src/util/string_constant.cpp
index 9d2fa2c614a..1c4ec36fa19 100644
--- a/src/util/string_constant.cpp
+++ b/src/util/string_constant.cpp
@@ -53,5 +53,5 @@ array_exprt string_constantt::to_array_expr() const
     *it = from_integer(ch, char_type);
   }
 
-  return dest;
+  return std::move(dest).with_source_location(*this);
 }
diff --git a/src/util/string_constant.h b/src/util/string_constant.h
index 30c86347efe..b70823b95db 100644
--- a/src/util/string_constant.h
+++ b/src/util/string_constant.h
@@ -24,7 +24,6 @@ class string_constantt : public nullary_exprt
   }
 
   array_exprt to_array_expr() const;
-  bool from_array_expr(const array_exprt &);
 };
 
 template <>