diff --git a/regression/strings-smoke-tests/java_append_char/test.desc b/regression/strings-smoke-tests/java_append_char/test.desc
index 88d1cbf2114..7fdd9f47961 100644
--- a/regression/strings-smoke-tests/java_append_char/test.desc
+++ b/regression/strings-smoke-tests/java_append_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_append_char.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_case/test.desc b/regression/strings-smoke-tests/java_case/test.desc
index d2508fa3489..2889787e47a 100644
--- a/regression/strings-smoke-tests/java_case/test.desc
+++ b/regression/strings-smoke-tests/java_case/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_case.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_case.java line 10 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_insert_char/test.desc b/regression/strings-smoke-tests/java_insert_char/test.desc
index 0e9a06d5afb..88200524d70 100644
--- a/regression/strings-smoke-tests/java_insert_char/test.desc
+++ b/regression/strings-smoke-tests/java_insert_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char.class
---refine-strings
+--refine-strings  --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_insert_char_array/test.desc b/regression/strings-smoke-tests/java_insert_char_array/test.desc
index 082771dd2db..6fc7a12f439 100644
--- a/regression/strings-smoke-tests/java_insert_char_array/test.desc
+++ b/regression/strings-smoke-tests/java_insert_char_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char_array.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_insert_int/test.desc b/regression/strings-smoke-tests/java_insert_int/test.desc
index dc039fedbea..488e2bc8766 100644
--- a/regression/strings-smoke-tests/java_insert_int/test.desc
+++ b/regression/strings-smoke-tests/java_insert_int/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test_insert_int.class
---refine-strings
+--refine-strings  --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_insert_multiple/test.desc b/regression/strings-smoke-tests/java_insert_multiple/test.desc
index bb9a23f1b5c..d3236ab78ee 100644
--- a/regression/strings-smoke-tests/java_insert_multiple/test.desc
+++ b/regression/strings-smoke-tests/java_insert_multiple/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_multiple.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_insert_string/test.desc b/regression/strings-smoke-tests/java_insert_string/test.desc
index 44bf9f268d9..2b91905e17e 100644
--- a/regression/strings-smoke-tests/java_insert_string/test.desc
+++ b/regression/strings-smoke-tests/java_insert_string/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_string.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_int_to_string/test3.desc b/regression/strings-smoke-tests/java_int_to_string/test3.desc
index 5b48152f26e..97565815465 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test3.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test3.desc
@@ -1,6 +1,6 @@
 CORE
 Test3.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string/test5.desc b/regression/strings-smoke-tests/java_int_to_string/test5.desc
index 08531bc36e0..524a176db3f 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test5.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test5.desc
@@ -1,6 +1,6 @@
 CORE
 Test5.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc
index 1f7de38eee8..20bd5377109 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary1.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc
index cb1dd600e34..370139d2c42 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary2.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc
index 4b691b9c528..48d705734ac 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex1.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc
index d21d067e620..89c4928e147 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex2.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc
index c9fbfae377e..0c5ff51b802 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_hex3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex3.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc
index 06520bcde35..aee4977a75f 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal2.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc
index 32f319a9876..b7a5ceb3ce1 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal3.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc
index 4b691b9c528..48d705734ac 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex1.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc
index c9fbfae377e..0c5ff51b802 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex3.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc
index 9afe7b06279..8188ebc0ee9 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal1.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc
index 06520bcde35..3884ae1fa9f 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal2.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc
index 32f319a9876..527357b801e 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal3.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_value_of_float/test.desc b/regression/strings-smoke-tests/java_value_of_float/test.desc
index d1cc84bd13a..4e3e8769be6 100644
--- a/regression/strings-smoke-tests/java_value_of_float/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_float/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --function test.check
+--refine-strings --function test.check --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_value_of_float_2/test.desc b/regression/strings-smoke-tests/java_value_of_float_2/test.desc
index 8a2a2bc6207..370b9327f58 100644
--- a/regression/strings-smoke-tests/java_value_of_float_2/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_float_2/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 test.class
---refine-strings --function test.check
+--refine-strings --function test.check --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 6 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_value_of_long/test.desc b/regression/strings-smoke-tests/java_value_of_long/test.desc
index f96a114f708..c7ea25ab2f8 100644
--- a/regression/strings-smoke-tests/java_value_of_long/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_long/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 9 .* SUCCESS$
diff --git a/regression/strings/StringStartEnd02/test.desc b/regression/strings/StringStartEnd02/test.desc
index a650aa0ebe9..deddbb5b902 100644
--- a/regression/strings/StringStartEnd02/test.desc
+++ b/regression/strings/StringStartEnd02/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringStartEnd02.class
---refine-strings --unwind 30
+--refine-strings --unwind 30 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 13 .* FAILURE$
diff --git a/regression/strings/java_append_char/test.desc b/regression/strings/java_append_char/test.desc
index e39f1d5ebe8..1c583f7be2d 100644
--- a/regression/strings/java_append_char/test.desc
+++ b/regression/strings/java_append_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_append_char.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/java_case/test.desc b/regression/strings/java_case/test.desc
index 1dee2b7dd3e..22d58ddb3ac 100644
--- a/regression/strings/java_case/test.desc
+++ b/regression/strings/java_case/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_case.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/regression/strings/java_char_array_init/test.desc b/regression/strings/java_char_array_init/test.desc
index 3efff6619b7..61a71f5034f 100644
--- a/regression/strings/java_char_array_init/test.desc
+++ b/regression/strings/java_char_array_init/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_init.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 14.* FAILURE$
diff --git a/regression/strings/java_insert_char/test.desc b/regression/strings/java_insert_char/test.desc
index 406a20e9c52..cdda3eeae95 100644
--- a/regression/strings/java_insert_char/test.desc
+++ b/regression/strings/java_insert_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/regression/strings/java_insert_char_array/test.desc b/regression/strings/java_insert_char_array/test.desc
index 49a3afbffce..648fec2fa7d 100644
--- a/regression/strings/java_insert_char_array/test.desc
+++ b/regression/strings/java_insert_char_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_char_array.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 12.* FAILURE$
diff --git a/regression/strings/java_insert_int/test.desc b/regression/strings/java_insert_int/test.desc
index aa1f5cacab2..bc25e9abf3c 100644
--- a/regression/strings/java_insert_int/test.desc
+++ b/regression/strings/java_insert_int/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_int.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/regression/strings/java_insert_string/test.desc b/regression/strings/java_insert_string/test.desc
index 7ed578bfca5..79fa2931c93 100644
--- a/regression/strings/java_insert_string/test.desc
+++ b/regression/strings/java_insert_string/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_string.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 6b8966c7d6f..04fb0fbdc3f 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -24,6 +24,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <stack>
 #include <ansi-c/string_constant.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_iterator.h>
 #include <util/replace_expr.h>
 #include <util/refined_string_type.h>
 #include <util/simplify_expr.h>
@@ -289,88 +290,79 @@ bool string_refinementt::add_axioms_for_string_assigns(
   return true;
 }
 
+/// Convert exprt to a specific type. Throw bad_cast if conversion
+/// cannot be performed
+/// Generic case doesn't exist, specialize for different types accordingly
+/// TODO: this should go to util
+template<typename T>
+T expr_cast(const exprt&);
+
+template<>
+std::size_t expr_cast<std::size_t>(const exprt& val_expr)
+{
+  mp_integer val_mb;
+  if(to_integer(val_expr, val_mb))
+    throw std::bad_cast();
+  if(!val_mb.is_long())
+    throw std::bad_cast();
+  if(val_mb<0)
+    throw std::bad_cast();
+  return val_mb.to_long();
+}
+
 /// If the expression is of type string, then adds constants to the index set to
 /// force the solver to pick concrete values for each character, and fill the
 /// maps `found_length` and `found_content`.
 ///
-///          The way this is done is by looking for the length of the string,
-///          then for each `i` in the index set, look at the value found by
-///          the solver and put it in the `result` table.
-///          For indexes that are not present in the index set, we put the
-///          same value as the next index that is present in the index set.
-///          We do so by traversing the array backward, remembering the
-///          last value that has been initialized.
+/// The way this is done is by looking for the length of the string,
+/// then for each `i` in the index set, look at the value found by
+/// the solver and put it in the `result` table.
+/// For indexes that are not present in the index set, we put the
+/// same value as the next index that is present in the index set.
+/// We do so by traversing the array backward, remembering the
+/// last value that has been initialized.
 void string_refinementt::concretize_string(const exprt &expr)
 {
   if(is_refined_string_type(expr.type()))
   {
-    string_exprt str=to_string_expr(expr);
-    exprt length=get(str.length());
+    const string_exprt str=to_string_expr(expr);
+    const exprt length=get(str.length());
     exprt content=str.content();
     replace_expr(symbol_resolve, content);
     found_length[content]=length;
-    mp_integer found_length;
-    if(!to_integer(length, found_length))
-    {
-      INVARIANT(
-        found_length.is_long(),
-        string_refinement_invariantt("the length of a string should be a "
-          "long"));
-      INVARIANT(
-        found_length>=0,
-        string_refinement_invariantt("the length of a string should be >= 0"));
-      size_t concretize_limit=found_length.to_long();
-      INVARIANT(
-        concretize_limit<=generator.max_string_length,
-        string_refinement_invariantt("string length must be less than the max "
-          "length"));
-      exprt content_expr=str.content();
-      std::vector<exprt> result;
-
-      if(index_set[str.content()].empty())
-        return;
-
-      // Use the last index as the default character value
-      exprt last_concretized=simplify_expr(
-        get(str[minus_exprt(length, from_integer(1, length.type()))]), ns);
-      result.resize(concretize_limit, last_concretized);
+    const auto string_length=expr_cast<std::size_t>(length);
+    INVARIANT(
+      string_length<=generator.max_string_length,
+      string_refinement_invariantt("string length must be less than the max "
+        "length"));
+    if(index_set[str.content()].empty())
+      return;
 
-      // Keep track of the indexes for which we have actual values
-      std::set<size_t> initialized;
+    std::map<std::size_t, exprt> map;
 
-      for(const auto &i : index_set[str.content()])
+    for(const auto &i : index_set[str.content()])
+    {
+      const exprt simple_i=simplify_expr(get(i), ns);
+      mp_integer mpi_index;
+      bool conversion_failure=to_integer(simple_i, mpi_index);
+      if(!conversion_failure && mpi_index>=0 && mpi_index<string_length)
       {
-        mp_integer mp_index;
-        exprt simple_i=simplify_expr(get(i), ns);
-        if(to_integer(simple_i, mp_index) ||
-           mp_index<0 ||
-           mp_index>=concretize_limit)
-        {
-          debug() << "concretize_string: ignoring out of bound index: "
-                  << from_expr(ns, "", simple_i) << eom;
-        }
-        else
-        {
-          // Add an entry in the result vector
-          size_t index=mp_index.to_long();
-          exprt str_i=simplify_expr(str[simple_i], ns);
-          exprt value=simplify_expr(get(str_i), ns);
-          result[index]=value;
-          initialized.insert(index);
-        }
+        const exprt str_i=simplify_expr(str[simple_i], ns);
+        const exprt value=simplify_expr(get(str_i), ns);
+        std::size_t index=mpi_index.to_long();
+        map.emplace(index, value);
+      }
+      else
+      {
+        debug() << "concretize_string: ignoring out of bound index: "
+                << from_expr(ns, "", simple_i) << eom;
       }
-
-      // Pad the concretized values to the left to assign the uninitialized
-      // values of result. The indices greater than concretize_limit are
-      // already assigned to last_concretized.
-      pad_vector(result, initialized, last_concretized);
-
-      array_exprt arr(to_array_type(content.type()));
-      arr.operands()=result;
-      debug() << "Concretized " << from_expr(ns, "", content_expr)
-              << " = " << from_expr(ns, "", arr) << eom;
-      found_content[content]=arr;
     }
+    array_exprt arr(to_array_type(content.type()));
+    arr.operands()=fill_in_map_as_vector(map);
+    debug() << "Concretized " << from_expr(ns, "", str.content())
+            << " = " << from_expr(ns, "", arr) << eom;
+    found_content[content]=arr;
   }
 }
 
@@ -715,62 +707,38 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const
     return empty_ret;
   }
 
-  std::vector<unsigned> concrete_array(n);
-
   if(arr_val.id()=="array-list")
   {
-    std::set<unsigned> initialized;
+    DATA_INVARIANT(
+      arr_val.operands().size()%2==0,
+      string_refinement_invariantt("and index expression must be on a symbol, "
+                                   "with, array_of, if, or array, and all "
+                                   "cases besides array are handled above"));
+    std::map<std::size_t, exprt> initial_map;
     for(size_t i=0; i<arr_val.operands().size()/2; i++)
     {
       exprt index=arr_val.operands()[i*2];
       unsigned idx;
-      if(!to_unsigned_integer(to_constant_expr(index), idx))
-      {
-        if(idx<n)
-        {
-          exprt value=arr_val.operands()[i*2+1];
-          to_unsigned_integer(to_constant_expr(value), concrete_array[idx]);
-          initialized.insert(idx);
-        }
-      }
+      if(!to_unsigned_integer(to_constant_expr(index), idx) && idx<n)
+        initial_map[idx]=arr_val.operands()[i*2+1];
     }
 
     // Pad the concretized values to the left to assign the uninitialized
     // values of result.
-    pad_vector(concrete_array, initialized, concrete_array[n-1]);
+    ret.operands()=fill_in_map_as_vector(initial_map);
+    return ret;
   }
   else if(arr_val.id()==ID_array)
   {
+    // copy the `n` first elements of `arr_val`
     for(size_t i=0; i<arr_val.operands().size() && i<n; i++)
-    {
-      unsigned c;
-      exprt op=arr_val.operands()[i];
-      if(op.id()==ID_constant)
-      {
-        to_unsigned_integer(to_constant_expr(op), c);
-        concrete_array[i]=c;
-      }
-    }
+      ret.move_to_operands(arr_val.operands()[i]);
+    return ret;
   }
-  else
-  {
-#if 0
-    debug() << "unable to get array-list value of " << from_expr(ns, "", arr)
-            << " of size " << n << eom;
-#endif
-    return array_of_exprt(from_integer(0, char_type), ret_type);
-  }
-
-  for(size_t i=0; i<n; i++)
-  {
-    exprt c_expr=from_integer(concrete_array[i], char_type);
-    ret.move_to_operands(c_expr);
-  }
-
-  return ret;
+  // default return value is an array of `0`s
+  return array_of_exprt(from_integer(0, char_type), ret_type);
 }
 
-
 /// get a model of an array of unknown size and infer the size if possible
 /// \par parameters: an expression representing an array
 /// \return an expression
@@ -881,6 +849,7 @@ exprt string_refinementt::substitute_array_with_expr(
     exprt else_expr=substitute_array_with_expr(with_expr.old(), index);
     const typet &type=then_expr.type();
     CHECK_RETURN(else_expr.type()==type);
+    CHECK_RETURN(index.type()==with_expr.where().type());
     return if_exprt(
       equal_exprt(index, with_expr.where()), then_expr, else_expr, type);
   }
@@ -895,6 +864,42 @@ exprt string_refinementt::substitute_array_with_expr(
   }
 }
 
+/// Fill an array represented by a list of with_expr by propagating values to
+/// the left. For instance `ARRAY_OF(12) WITH[2:=24] WITH[4:=42]` will give
+/// `{ 24, 24, 24, 42, 42 }`
+/// \param expr: an array expression in the form
+///   `ARRAY_OF(x) WITH [i0:=v0] ... WITH [iN:=vN]`
+/// \param string_max_length: bound on the length of strings
+/// \return an array expression with filled in values, or expr if it is simply
+///   an `ARRAY_OF(x)` expression
+exprt fill_in_array_with_expr(const exprt &expr, std::size_t string_max_length)
+{
+  PRECONDITION(expr.type().id()==ID_array);
+  PRECONDITION(expr.id()==ID_with || expr.id()==ID_array_of);
+
+  // Nothing to do for empty array
+  if(expr.id()==ID_array_of)
+    return expr;
+
+  // Map of the parts of the array that are initialized
+  std::map<std::size_t, exprt> initial_map;
+
+  for(exprt it=expr; it.id()==ID_with; it=to_with_expr(it).old())
+  {
+    // Add to `initial_map` all the pairs (index,value) contained in `WITH`
+    // statements
+    const with_exprt with_expr=to_with_expr(it);
+    const exprt &then_expr=with_expr.new_value();
+    const auto index=expr_cast<std::size_t>(with_expr.where());
+    if(index<string_max_length)
+      initial_map.emplace(index, then_expr);
+  }
+
+  array_exprt result(to_array_type(expr.type()));
+  result.operands()=fill_in_map_as_vector(initial_map);
+  return result;
+}
+
 /// create an equivalent expression where array accesses and 'with' expressions
 /// are replaced by 'if' expressions, in particular:
 ///  * for an array access `arr[x]`, where:
@@ -924,8 +929,7 @@ void string_refinementt::substitute_array_access(exprt &expr) const
 
     if(index_expr.array().id()==ID_with)
     {
-      expr=substitute_array_with_expr(
-        index_expr.array(), index_expr.index());
+      expr=substitute_array_with_expr(index_expr.array(), index_expr.index());
       return;
     }
 
@@ -1084,21 +1088,44 @@ static exprt negation_of_constraint(const string_constraintt &axiom)
   return negaxiom;
 }
 
+/// Result of the solver `supert` should not be interpreted literally for char
+/// arrays as not all indices are present in the index set.
+/// In the given expression, we populate arrays at the indices for which the
+/// solver has no constraint by copying values to the left.
+/// For example an expression `ARRAY_OF(0) WITH [1:=2] WITH [4:=3]` would
+/// be interpreted as `{ 2, 2, 3, 3, 3}`.
+/// \param expr: expression to interpret
+/// \param string_max_length: maximum size of arrays to consider
+/// \return the interpreted expression
+exprt concretize_arrays_in_expression(exprt expr, std::size_t string_max_length)
+{
+  auto it=expr.depth_begin();
+  const auto end=expr.depth_end();
+  while(it!=end)
+  {
+    if(it->id()==ID_with && it->type().id()==ID_array)
+    {
+      it.mutate()=fill_in_array_with_expr(*it, string_max_length);
+      it.next_sibling_or_parent();
+    }
+    else
+      ++it;
+  }
+  return expr;
+}
+
 /// return true if the current model satisfies all the axioms
 /// \return a Boolean
 bool string_refinementt::check_axioms()
 {
-  debug() << "string_refinementt::check_axioms: ==============="
-          << "===========================================" << eom;
-  debug() << "string_refinementt::check_axioms: build the"
-          << " interpretation from the model of the prop_solver" << eom;
+  debug() << "string_refinementt::check_axioms:" << eom;
   debug_model();
 
   // Maps from indexes of violated universal axiom to a witness of violation
   std::map<size_t, exprt> violated;
 
-  debug() << "there are " << universal_axioms.size()
-          << " universal axioms" << eom;
+  debug() << "string_refinement::check_axioms: " << universal_axioms.size()
+          << " universal axioms:" << eom;
   for(size_t i=0; i<universal_axioms.size(); i++)
   {
     const string_constraintt &axiom=universal_axioms[i];
@@ -1112,20 +1139,36 @@ bool string_refinementt::check_axioms()
       univ_var, get(bound_inf), get(bound_sup), get(prem), get(body));
 
     exprt negaxiom=negation_of_constraint(axiom_in_model);
-    debug() << "(string_refinementt::check_axioms) Adding negated constraint: "
-            << from_expr(ns, "", negaxiom) << eom;
-    substitute_array_access(negaxiom);
+
+    debug() << "  "<< i << ".\n"
+            << "    - axiom:\n"
+            << "       " << from_expr(ns, "", axiom) << eom;
+    debug() << "    - axiom_in_model:\n"
+            << "       " << from_expr(ns, "", axiom_in_model) << eom;
+    debug() << "    - negated_axiom:\n"
+            << "       " << from_expr(ns, "", negaxiom) << eom;
+
+    exprt with_concretized_arrays=concretize_arrays_in_expression(
+      negaxiom, generator.max_string_length);
+    debug() << "    - negated_axiom_with_concretized_array_access:\n"
+            << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
+
+    substitute_array_access(with_concretized_arrays);
+    debug() << "    - negated_axiom_without_array_access:\n"
+            << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
     exprt witness;
 
-    bool is_sat=is_axiom_sat(negaxiom, univ_var, witness);
+    bool is_sat=is_axiom_sat(with_concretized_arrays, univ_var, witness);
 
     if(is_sat)
     {
-      debug() << "string constraint can be violated for "
+      debug() << "  - violated_for: "
               << univ_var.get_identifier()
               << " = " << from_expr(ns, "", witness) << eom;
       violated[i]=witness;
     }
+    else
+      debug() << "  - correct" << eom;
   }
 
   // Maps from indexes of violated not_contains axiom to a witness of violation
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 8762472312e..0eec3e99a9a 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -146,11 +146,6 @@ class string_refinementt: public bv_refinementt
   bool is_valid_string_constraint(const string_constraintt &expr);
 
   exprt simplify_sum(const exprt &f) const;
-  template <typename T1, typename T2>
-  void pad_vector(
-    std::vector<T1> &result,
-    std::set<T2> &initialized,
-    T1 last_concretized) const;
 
   void concretize_string(const exprt &expr);
   void concretize_results();
@@ -164,39 +159,36 @@ class string_refinementt: public bv_refinementt
 
 exprt substitute_array_lists(exprt expr, size_t string_max_length);
 
-/// Utility function for concretization of strings. Copies concretized values to
-/// the left to initialize the unconcretized indices of concrete_array.
-/// \param concrete_array: the vector to populate
-/// \param initialized: the vector containing the indices of the concretized
-///   values
-/// \param last_concretized: initial value of the last concretized index
-template <typename T1, typename T2>
-void string_refinementt::pad_vector(
-  std::vector<T1> &concrete_array,
-  std::set<T2> &initialized,
-  T1 last_concretized) const
+exprt concretize_arrays_in_expression(
+  exprt expr, std::size_t string_max_length);
+
+/// Convert index-value map to a vector of values. If a value for an
+/// index is not defined, set it to the value referenced by the next higher
+/// index. The length of the resulting vector is the key of the map's
+/// last element + 1
+/// \param index_value: map containing values of specific vector cells
+/// \return Vector containing values as described in the map
+template <typename T>
+std::vector<T> fill_in_map_as_vector(
+  const std::map<std::size_t, T> &index_value)
 {
-  // Pad the concretized values to the left to assign the uninitialized
-  // values of result. The indices greater than concretize_limit are
-  // already assigned to last_concretized.
-  for(auto j=initialized.rbegin(); j!=initialized.rend();)
+  std::vector<T> result;
+  if(!index_value.empty())
   {
-    size_t i=*j;
-    // The leftmost index to pad is the value + 1 of the next element in
-    // 'initialized'. Since we cannot use the binary '+' operator on set
-    // iterators, we must increment the iterator here instead of in the
-    // for loop.
-    j++;
-    size_t leftmost_index_to_pad=(j!=initialized.rend()?*(j)+1:0);
-    // pad until we reach the next initialized index (right to left)
-    while(i>leftmost_index_to_pad)
-      concrete_array[(i--)-1]=last_concretized;
-    INVARIANT(
-      i==leftmost_index_to_pad,
-      string_refinement_invariantt("Loop decrements i until it is not greater "
-        " than leftmost_index_to_pad"));
-    if(i>0)
-      last_concretized=concrete_array[i-1];
+    result.resize(index_value.rbegin()->first+1);
+    for(auto it=index_value.rbegin(); it!=index_value.rend(); ++it)
+    {
+      const std::size_t index=it->first;
+      const T value=it->second;
+      const auto next=std::next(it);
+      const std::size_t leftmost_index_to_pad=
+        next!=index_value.rend()
+        ? next->first+1
+        : 0;
+      for(std::size_t j=leftmost_index_to_pad; j<=index; j++)
+        result[j]=value;
+    }
   }
+  return result;
 }
 #endif
diff --git a/src/util/expr_iterator.h b/src/util/expr_iterator.h
index 7f6b83440f0..be228bcfba4 100644
--- a/src/util/expr_iterator.h
+++ b/src/util/expr_iterator.h
@@ -55,7 +55,6 @@ inline bool operator==(
   const depth_iterator_expr_statet &right)
 { return left.it==right.it && left.expr.get()==right.expr.get(); }
 
-
 /// Depth first search iterator base - iterates over supplied expression
 /// and all its operands recursively.
 /// Base class using CRTP
@@ -97,11 +96,19 @@ class depth_iterator_baset
     return this->downcast();
   }
 
+  depth_iterator_t &next_sibling_or_parent()
+  {
+    PRECONDITION(!m_stack.empty());
+    m_stack.back().it=m_stack.back().end;
+    ++(*this);
+    return this->downcast();
+  }
+
   /// Post-increment operator
   /// Expensive copy. Avoid if possible
   depth_iterator_t operator++(int)
   {
-    depth_iterator_t tmp(*this);
+    depth_iterator_t tmp(this->downcast());
     this->operator++();
     return tmp;
   }
diff --git a/unit/Makefile b/unit/Makefile
index 8fae7e49ca1..b24eeeab1ad 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -24,6 +24,7 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \
        solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
        solvers/refinement/string_refinement/substitute_array_list.cpp \
+       solvers/refinement/string_refinement/concretize_array.cpp \
        catch_example.cpp \
        # Empty last line
 
diff --git a/unit/solvers/refinement/string_refinement/concretize_array.cpp b/unit/solvers/refinement/string_refinement/concretize_array.cpp
new file mode 100644
index 00000000000..ab4dc31ae5f
--- /dev/null
+++ b/unit/solvers/refinement/string_refinement/concretize_array.cpp
@@ -0,0 +1,56 @@
+/*******************************************************************\
+
+ Module: Unit tests for concretize_array_expression in
+   solvers/refinement/string_refinement.cpp
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <catch.hpp>
+
+#include <util/arith_tools.h>
+#include <util/std_types.h>
+#include <util/std_expr.h>
+#include <solvers/refinement/string_refinement.h>
+
+SCENARIO("concretize_array_expression",
+  "[core][solvers][refinement][string_refinement]")
+{
+  const typet char_type=unsignedbv_typet(16);
+  const typet int_type=signedbv_typet(32);
+  const exprt index1=from_integer(1, int_type);
+  const exprt charx=from_integer('x', char_type);
+  const exprt index4=from_integer(4, int_type);
+  const exprt chary=from_integer('y', char_type);
+  const exprt index100=from_integer(100, int_type);
+  const exprt char0=from_integer('0', char_type);
+  const exprt index2=from_integer(2, int_type);
+  array_typet array_type(char_type, infinity_exprt(int_type));
+
+  // input_expr is
+  // `'0' + (ARRAY_OF(0) WITH [1:=x] WITH [4:=y] WITH [100:=z])[2]`
+  const plus_exprt input_expr(
+    from_integer('0', char_type),
+    index_exprt(
+      with_exprt(
+        with_exprt(
+          with_exprt(
+            array_of_exprt(from_integer(0, char_type), array_type),
+            index1,
+            charx),
+          index4,
+          chary),
+        index100,
+        from_integer('z', char_type)),
+      index2));
+
+  // String max length is 50, so index 100 should get ignored.
+  const exprt concrete=concretize_arrays_in_expression(input_expr, 50);
+
+  // The expected result is `'0' + { 'x', 'x', 'y', 'y', 'y' }`
+  array_exprt array(array_type);
+  array.operands()={charx, charx, chary, chary, chary};
+  const plus_exprt expected(char0, index_exprt(array, index2));
+  REQUIRE(concrete==expected);
+}
diff --git a/unit/util/expr_iterator.cpp b/unit/util/expr_iterator.cpp
index 4b914b01551..b806448b5c9 100644
--- a/unit/util/expr_iterator.cpp
+++ b/unit/util/expr_iterator.cpp
@@ -133,3 +133,26 @@ TEST_CASE("Iterate over a 3-level tree, mutate - set all types to ID_symbol")
     REQUIRE(expr.get().id()==ID_symbol);
   }
 }
+
+TEST_CASE("next_sibling_or_parent, next sibling")
+{
+  std::vector<exprt> input(4);
+  input[1].operands()={ input[3] };
+  input[2].id(ID_int);
+  input[0].operands()={ input[1], input[2] };
+  auto it=input[0].depth_begin();
+  it++;
+  it.next_sibling_or_parent();
+  REQUIRE(*it==input[2]);
+}
+
+TEST_CASE("next_sibling_or_parent, next parent ")
+{
+  std::vector<exprt> input(3);
+  input[1].operands()={ input[2] };
+  input[0].operands()={ input[1] };
+  auto it=input[0].depth_begin();
+  it++;
+  it.next_sibling_or_parent();
+  REQUIRE(it==input[0].depth_end());
+}