diff --git a/jbmc/regression/strings-smoke-tests/java_starts_with/test-no-simplify.desc b/jbmc/regression/strings-smoke-tests/java_starts_with/test-no-simplify.desc
new file mode 100644
index 00000000000..8ead656d962
--- /dev/null
+++ b/jbmc/regression/strings-smoke-tests/java_starts_with/test-no-simplify.desc
@@ -0,0 +1,14 @@
+CORE
+test_starts_with.class
+--verbosity 10 --max-nondet-string-length 1000 --function test_starts_with.main --unwind 1 --no-simplify
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* FAILURE$
+--
+non equal types
+--
+This test must also pass when not running simplification during goto-symex
+(--no-simplify). Prior to the changes in this commit the test would yield wrong
+results for either line 8, because the string solver was not able to identify
+the string object in a non-simplified expression.
diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp
index bd6894c62c8..7b37d2833bb 100644
--- a/src/solvers/strings/string_constraint_generator_main.cpp
+++ b/src/solvers/strings/string_constraint_generator_main.cpp
@@ -26,6 +26,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include <util/arith_tools.h>
 #include <util/deprecate.h>
 #include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 #include <util/string_constant.h>
 
@@ -180,7 +181,7 @@ exprt string_constraint_generatort::associate_array_to_pointer(
                                       : f.arguments()[0]);
 
   const exprt &pointer_expr = f.arguments()[1];
-  array_pool.insert(pointer_expr, array_expr);
+  array_pool.insert(simplify_expr(pointer_expr, ns), array_expr);
   // created_strings.emplace(to_array_string_expr(array_expr));
   return from_integer(0, f.type());
 }
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
index 140025194cf..8c6e227793d 100644
--- a/src/solvers/strings/string_refinement.cpp
+++ b/src/solvers/strings/string_refinement.cpp
@@ -339,7 +339,7 @@ static void add_equations_for_symbol_resolution(
 
     if(is_char_pointer_type(rhs.type()))
     {
-      symbol_solver.make_union(lhs, rhs);
+      symbol_solver.make_union(lhs, simplify_expr(rhs, ns));
     }
     else if(rhs.id() == ID_function_application)
     {
@@ -439,7 +439,7 @@ static void add_string_equation_to_symbol_resolution(
 {
   if(eq.rhs().type() == string_typet())
   {
-    symbol_resolve.make_union(eq.lhs(), eq.rhs());
+    symbol_resolve.make_union(eq.lhs(), simplify_expr(eq.rhs(), ns));
   }
   else if(has_subtype(eq.lhs().type(), ID_string, ns))
   {
@@ -646,7 +646,10 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   for(equal_exprt &eq : equations)
   {
     if(can_cast_expr<function_application_exprt>(eq.rhs()))
+    {
+      simplify(eq.rhs(), ns);
       string_id_symbol_resolve.replace_expr(eq.rhs());
+    }
   }
 
   // Generator is also used by get, so we have to use it as a class member