From 2d2ff895bf360d4d48e1ea514d99a60816166ada Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 19 Feb 2018 15:43:15 +0000
Subject: [PATCH 01/22] Get rid of default axioms for strings

These default axioms where too strict and where applied even for strings
that may never be creted in the actual program.
This could for instance lead to problematic contradiction for a Java
object which could be casted either to a string or an int:
the axiom added there would apply both on the string and on the integer.
---
 .../refinement/string_constraint_generator.h  |  1 -
 .../string_constraint_generator_main.cpp      | 26 ++-----------------
 2 files changed, 2 insertions(+), 25 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index 74d341a24c9..fc2e951990d 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -108,7 +108,6 @@ class string_constraint_generatort final
   array_string_exprt
   char_array_of_pointer(const exprt &pointer, const exprt &length);
 
-  void add_default_axioms(const array_string_exprt &s);
   exprt axiom_for_is_positive_index(const exprt &x);
 
   void add_constraint_on_characters(
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index 1d623280dec..30b1edf02f8 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -181,7 +181,6 @@ array_string_exprt string_constraint_generatort::fresh_string(
   symbol_exprt content = fresh_symbol("string_content", array_type);
   array_string_exprt str = to_array_string_expr(content);
   created_strings.insert(str);
-  add_default_axioms(str);
   return str;
 }
 
@@ -249,7 +248,7 @@ string_constraint_generatort::associate_char_array_to_char_pointer(
   auto insert_result =
     arrays_of_pointers_.insert(std::make_pair(char_pointer, array_sym));
   array_string_exprt result = to_array_string_expr(insert_result.first->second);
-  add_default_axioms(result);
+  created_strings.insert(result);
   return result;
 }
 
@@ -287,7 +286,7 @@ exprt string_constraint_generatort::associate_array_to_pointer(
     arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr));
   INVARIANT(
     it_bool.second, "should not associate two arrays to the same pointer");
-  add_default_axioms(to_array_string_expr(array_expr));
+  created_strings.emplace(to_array_string_expr(array_expr));
   return from_integer(0, f.type());
 }
 
@@ -320,27 +319,6 @@ string_constraint_generatort::get_string_expr(const exprt &expr)
   return char_array_of_pointer(str.content(), str.length());
 }
 
-/// adds standard axioms about the length of the string and its content: * its
-/// length should be positive * it should not exceed max_string_length * if
-/// force_printable_characters is true then all characters should belong to the
-/// range of ASCII characters between ' ' and '~'
-/// \param s: a string expression
-/// \return a string expression that is linked to the argument through axioms
-///   that are added to the list
-void string_constraint_generatort::add_default_axioms(
-  const array_string_exprt &s)
-{
-  // If `s` was already added we do nothing.
-  if(!created_strings.insert(s).second)
-    return;
-
-  const exprt index_zero = from_integer(0, s.length().type());
-  lemmas.push_back(s.axiom_for_length_ge(index_zero));
-
-  if(max_string_length!=std::numeric_limits<size_t>::max())
-    lemmas.push_back(s.axiom_for_length_le(max_string_length));
-}
-
 /// Add constraint on characters of a string.
 ///
 /// This constraint is

From 163250a51738e2393b75db1acaf89ef74d49975f Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 19 Feb 2018 15:45:44 +0000
Subject: [PATCH 02/22] Get rid of string_max_length field

In constraint generator, this was used for adding default axioms but is
no longer used.
---
 src/cbmc/cbmc_solvers.cpp                     |  2 +-
 .../refinement/string_constraint_generator.h  | 10 +-----
 .../string_constraint_generator_main.cpp      |  7 ++---
 src/solvers/refinement/string_refinement.cpp  | 31 ++++++++++---------
 src/solvers/refinement/string_refinement.h    |  3 +-
 .../instantiate_not_contains.cpp              | 18 ++++-------
 6 files changed, 29 insertions(+), 42 deletions(-)

diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
index 557bf1ca3b7..ed5787af6d3 100644
--- a/src/cbmc/cbmc_solvers.cpp
+++ b/src/cbmc/cbmc_solvers.cpp
@@ -177,7 +177,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
   info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
   info.ui=ui;
   if(options.get_bool_option("string-max-length"))
-    info.string_max_length=options.get_signed_int_option("string-max-length");
+    info.max_string_length = options.get_signed_int_option("string-max-length");
   info.trace=options.get_bool_option("trace");
   if(options.get_bool_option("max-node-refinement"))
     info.max_node_refinement=
diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index fc2e951990d..0f0f4e5462d 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -37,14 +37,7 @@ class string_constraint_generatort final
   // Used by format function
   class format_specifiert;
 
-  /// Arguments pack for the string_constraint_generator constructor
-  struct infot
-  {
-    /// Max length of non-deterministic strings
-    size_t string_max_length=std::numeric_limits<size_t>::max();
-  };
-
-  string_constraint_generatort(const infot& info, const namespacet& ns);
+  explicit string_constraint_generatort(const namespacet &ns);
 
   /// Axioms are of three kinds: universally quantified string constraint,
   /// not contains string constraints and simple formulas.
@@ -343,7 +336,6 @@ class string_constraint_generatort final
 
   // MEMBERS
 public:
-  const size_t max_string_length;
   // Used to store information about witnesses for not_contains constraints
   std::map<string_not_contains_constraintt, symbol_exprt> witness;
 private:
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index 30b1edf02f8..6b4c4558541 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -28,11 +28,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include <util/ssa_expr.h>
 #include <util/string_constant.h>
 
-string_constraint_generatort::string_constraint_generatort(
-  const string_constraint_generatort::infot &info,
-  const namespacet &ns)
-  : max_string_length(info.string_max_length),
-    ns(ns)
+string_constraint_generatort::string_constraint_generatort(const namespacet &ns)
+  : ns(ns)
 {
 }
 
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 882b2b28e5d..65bf0ad1c36 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -167,11 +167,14 @@ static bool validate(const string_refinementt::infot &info)
   return true;
 }
 
-string_refinementt::string_refinementt(const infot &info, bool):
-  supert(info),
-  config_(info),
-  loop_bound_(info.refinement_bound),
-  generator(info, *info.ns) { }
+string_refinementt::string_refinementt(const infot &info, bool)
+  : supert(info),
+    config_(info),
+    loop_bound_(info.refinement_bound),
+    max_string_length(info.max_string_length),
+    generator(*info.ns)
+{
+}
 
 string_refinementt::string_refinementt(const infot &info):
   string_refinementt(info, validate(info)) { }
@@ -866,13 +869,13 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   {
     bool satisfied;
     std::vector<exprt> counter_examples;
-    std::tie(satisfied, counter_examples)=check_axioms(
+    std::tie(satisfied, counter_examples) = check_axioms(
       axioms,
       generator,
       get,
       debug(),
       ns,
-      generator.max_string_length,
+      max_string_length,
       config_.use_counter_example,
       supert::config_.ui,
       symbol_resolve);
@@ -914,13 +917,13 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     {
       bool satisfied;
       std::vector<exprt> counter_examples;
-      std::tie(satisfied, counter_examples)=check_axioms(
+      std::tie(satisfied, counter_examples) = check_axioms(
         axioms,
         generator,
         get,
         debug(),
         ns,
-        generator.max_string_length,
+        max_string_length,
         config_.use_counter_example,
         supert::config_.ui,
         symbol_resolve);
@@ -2428,13 +2431,13 @@ exprt string_refinementt::get(const exprt &expr) const
     array_string_exprt &arr = to_array_string_expr(ecopy);
     arr.length() = generator.get_length_of_string_array(arr);
     const auto arr_model_opt =
-      get_array(super_get, ns, generator.max_string_length, debug(), arr);
+      get_array(super_get, ns, max_string_length, debug(), arr);
     // \todo Refactor with get array in model
     if(arr_model_opt)
     {
       const exprt arr_model = simplify_expr(*arr_model_opt, ns);
-      const exprt concretized_array = concretize_arrays_in_expression(
-        arr_model, generator.max_string_length, ns);
+      const exprt concretized_array =
+        concretize_arrays_in_expression(arr_model, max_string_length, ns);
       return concretized_array;
     }
     else
@@ -2449,8 +2452,8 @@ exprt string_refinementt::get(const exprt &expr) const
             array_exprt(array_typet(arr.type().subtype(), length));
           for(size_t i = 0; i < *n; i++)
             arr_model.copy_to_operands(exprt(ID_unknown, arr.type().subtype()));
-          const exprt concretized_array = concretize_arrays_in_expression(
-            arr_model, generator.max_string_length, ns);
+          const exprt concretized_array =
+            concretize_arrays_in_expression(arr_model, max_string_length, ns);
           return concretized_array;
         }
       }
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index e3fdf335820..eba7e99aa9a 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -87,12 +87,12 @@ class string_refinementt final: public bv_refinementt
     /// Concretize strings after solver is finished
     bool trace=false;
     bool use_counter_example=true;
+    std::size_t max_string_length;
   };
 public:
   /// string_refinementt constructor arguments
   struct infot:
     public bv_refinementt::infot,
-    public string_constraint_generatort::infot,
     public configt { };
 
   explicit string_refinementt(const infot &);
@@ -112,6 +112,7 @@ class string_refinementt final: public bv_refinementt
 
   const configt config_;
   std::size_t loop_bound_;
+  std::size_t max_string_length;
   string_constraint_generatort generator;
 
   // Simple constraints that have been given to the solver
diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
index a5aa7eb4028..53aea7e4085 100644
--- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -188,8 +188,7 @@ SCENARIO("instantiate_not_contains",
     // Generating the corresponding axioms and simplifying, recording info
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
-    string_constraint_generatort::infot info;
-    string_constraint_generatort generator(info, ns);
+    string_constraint_generatort generator(ns);
     exprt res=generator.add_axioms_for_function_application(func);
     std::string axioms;
     std::vector<string_not_contains_constraintt> nc_axioms;
@@ -284,8 +283,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
-    string_constraint_generatort::infot info;
-    string_constraint_generatort generator(info, ns);
+    string_constraint_generatort generator(ns);
     generator.witness[vacuous]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -338,8 +336,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet ns(symtab);
-    string_constraint_generatort::infot info;
-    string_constraint_generatort generator(info, ns);
+    string_constraint_generatort generator(ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -393,8 +390,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
-    string_constraint_generatort::infot info;
-    string_constraint_generatort generator(info, ns);
+    string_constraint_generatort generator(ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -451,8 +447,7 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
 
-    string_constraint_generatort::infot info;
-    string_constraint_generatort generator(info, ns);
+    string_constraint_generatort generator(ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -506,8 +501,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     symbol_tablet symtab;
     const namespacet empty_ns(symtab);
-    string_constraint_generatort::infot info;
-    string_constraint_generatort generator(info, ns);
+    string_constraint_generatort generator(ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 

From c303197681e43434d77e9f5c76b6f3453e0f401e Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 7 Feb 2018 08:54:10 +0000
Subject: [PATCH 03/22] Use string-max-length as default max input-length

Having input string longer than string-max-length does not make sense as
the solver will not know how to analyse them.
So when string-max-input-length is not specified we can use
string-max-length instead.
---
 src/java_bytecode/java_bytecode_language.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index b10c7b93796..390a802637a 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -56,6 +56,10 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   if(cmd.isset("string-max-input-length"))
     object_factory_parameters.max_nondet_string_length=
       std::stoi(cmd.get_value("string-max-input-length"));
+  else if(cmd.isset("string-max-length"))
+    object_factory_parameters.max_nondet_string_length =
+      std::stoi(cmd.get_value("string-max-length"));
+
   object_factory_parameters.string_printable = cmd.isset("string-printable");
   if(cmd.isset("java-max-vla-length"))
     max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length"));

From b233d449d753713c9a693ac971015f7c63787a32 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 7 Feb 2018 09:01:00 +0000
Subject: [PATCH 04/22] Give indications in case of error in solver

---
 src/solvers/refinement/string_refinement.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 65bf0ad1c36..af89e758405 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -954,7 +954,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         if(axioms.not_contains.empty())
         {
           error() << "dec_solve: current index set is empty, "
-                  << "this should not happen" << eom;
+                  << "consider increasing the gap between string-max-length "
+                  << "and string-max-input-length" << eom;
           return resultt::D_ERROR;
         }
         else

From fcb3e4d32fa28bc46572bed92ca736fa0dcc3d29 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 19 Feb 2018 11:12:56 +0000
Subject: [PATCH 05/22] Improve debugging in string solver

We flush after every output on the output stream, so that if an
instruction abort the program we can see what axiom was being processed.
---
 src/solvers/refinement/string_refinement.cpp | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index af89e758405..05e7bfdb13a 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -1065,7 +1065,8 @@ static optionalt<exprt> get_array(
   auto n_opt = numeric_cast<std::size_t>(size_val);
   if(!n_opt)
   {
-    stream << "(sr::get_array) size is not valid" << eom;
+    stream << "(sr::get_array) size is not valid: "
+           << from_expr(ns, "", size_val) << eom;
     return {};
   }
   std::size_t n = *n_opt;
@@ -1075,7 +1076,8 @@ static optionalt<exprt> get_array(
 
   if(n>max_string_length)
   {
-    stream << "(sr::get_array) long string (size=" << n << ")" << eom;
+    stream << "(sr::get_array) long string (size=" << n << "):"
+           << from_expr(ns, "", arr_val) << eom;
     return {};
   }
 
@@ -1646,7 +1648,7 @@ static void debug_check_axioms_step(
 {
   static const std::string indent = "  ";
   static const std::string indent2 = "    ";
-  stream << indent2 << "- axiom:\n" << indent2 << indent;
+  stream << indent2 << "- axiom:" << messaget::eom << indent2 << indent;
 
   if(axiom.id() == ID_string_constraint)
     stream << from_expr(ns, "", to_string_constraint(axiom));
@@ -1654,7 +1656,9 @@ static void debug_check_axioms_step(
     stream << from_expr(ns, "", to_string_not_contains_constraint(axiom));
   else
     stream << from_expr(ns, "", axiom);
-  stream << '\n' << indent2 << "- axiom_in_model:\n" << indent2 << indent;
+  stream << '\n'
+         << indent2 << "- axiom_in_model:" << messaget::eom << indent2
+         << indent;
 
   if(axiom_in_model.id() == ID_string_constraint)
     stream << from_expr(ns, "", to_string_constraint(axiom_in_model));
@@ -1666,10 +1670,10 @@ static void debug_check_axioms_step(
 
   stream << '\n'
          << indent2 << "- negated_axiom:\n"
-         << indent2 << indent << from_expr(ns, "", negaxiom) << '\n';
+         << indent2 << indent << from_expr(ns, "", negaxiom) << messaget::eom;
   stream << indent2 << "- negated_axiom_with_concretized_arrays:\n"
          << indent2 << indent << from_expr(ns, "", with_concretized_arrays)
-         << '\n';
+         << messaget::eom;
 }
 
 /// \return true if the current model satisfies all the axioms
@@ -1790,7 +1794,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
     const exprt with_concrete_arrays =
       substitute_array_access(negaxiom, gen_symbol, true);
 
-    stream << indent << i << ".\n";
+    stream << indent << i << '.' << eom;
     debug_check_axioms_step(
       stream, ns, nc_axiom, nc_axiom_in_model, negaxiom, with_concrete_arrays);
 

From b817de565f38ac7dd9d46053e4c5f9eb8daf371c Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 21 Feb 2018 16:44:08 +0000
Subject: [PATCH 06/22] Add max_index to substitute array function params

This avoid substituing indexes that are past the length limit up to
which we want to refine string.
---
 src/solvers/refinement/string_refinement.cpp | 123 ++++++++++++-------
 src/solvers/refinement/string_refinement.h   |  12 +-
 2 files changed, 89 insertions(+), 46 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 05e7bfdb13a..120eb5192be 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -119,7 +119,7 @@ static std::vector<exprt> instantiate(
 static optionalt<exprt> get_array(
   const std::function<exprt(const exprt &)> &super_get,
   const namespacet &ns,
-  const std::size_t max_string_length,
+  std::size_t max_string_length,
   messaget::mstreamt &stream,
   const array_string_exprt &arr);
 
@@ -127,7 +127,8 @@ static exprt substitute_array_access(
   const index_exprt &index_expr,
   const std::function<symbol_exprt(const irep_idt &, const typet &)>
     &symbol_generator,
-  const bool left_propagate);
+  bool left_propagate,
+  std::size_t max_index);
 
 /// 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
@@ -1244,21 +1245,25 @@ sparse_arrayt::sparse_arrayt(const with_exprt &expr)
   default_value = expr_dynamic_cast<array_of_exprt>(ref.get()).what();
 }
 
-exprt sparse_arrayt::to_if_expression(const exprt &index) const
+exprt sparse_arrayt::to_if_expression(
+  const exprt &index,
+  const std::size_t max_index) const
 {
   return std::accumulate(
     entries.begin(),
     entries.end(),
     default_value,
-    [&](
-      const exprt if_expr,
-      const std::pair<std::size_t, exprt> &entry) { // NOLINT
-      const exprt entry_index = from_integer(entry.first, index.type());
-      const exprt &then_expr = entry.second;
-      CHECK_RETURN(then_expr.type() == if_expr.type());
-      const equal_exprt index_equal(index, entry_index);
-      return if_exprt(index_equal, then_expr, if_expr, if_expr.type());
-    });
+    [&](const exprt if_expr, const std::pair<std::size_t, exprt> &entry)
+      -> exprt { // NOLINT
+        if(entry.first > max_index)
+          return if_expr;
+
+        const exprt entry_index = from_integer(entry.first, index.type());
+        const exprt &then_expr = entry.second;
+        CHECK_RETURN(then_expr.type() == if_expr.type());
+        const equal_exprt index_equal(index, entry_index);
+        return if_exprt(index_equal, then_expr, if_expr, if_expr.type());
+      });
 }
 
 interval_sparse_arrayt::interval_sparse_arrayt(const with_exprt &expr)
@@ -1273,21 +1278,25 @@ interval_sparse_arrayt::interval_sparse_arrayt(const with_exprt &expr)
       const std::pair<std::size_t, exprt> &b) { return a.first < b.first; });
 }
 
-exprt interval_sparse_arrayt::to_if_expression(const exprt &index) const
+exprt interval_sparse_arrayt::to_if_expression(
+  const exprt &index,
+  const std::size_t max_index) const
 {
   return std::accumulate(
     entries.rbegin(),
     entries.rend(),
     default_value,
-    [&](
-      const exprt if_expr,
-      const std::pair<std::size_t, exprt> &entry) { // NOLINT
-      const exprt entry_index = from_integer(entry.first, index.type());
-      const exprt &then_expr = entry.second;
-      CHECK_RETURN(then_expr.type() == if_expr.type());
-      const binary_relation_exprt index_small_eq(index, ID_le, entry_index);
-      return if_exprt(index_small_eq, then_expr, if_expr, if_expr.type());
-    });
+    [&](const exprt if_expr, const std::pair<std::size_t, exprt> &entry)
+      -> exprt { // NOLINT
+        if(entry.first > max_index)
+          return if_expr;
+
+        const exprt entry_index = from_integer(entry.first, index.type());
+        const exprt &then_expr = entry.second;
+        CHECK_RETURN(then_expr.type() == if_expr.type());
+        const binary_relation_exprt index_small_eq(index, ID_le, entry_index);
+        return if_exprt(index_small_eq, then_expr, if_expr, if_expr.type());
+      });
 }
 
 /// Create a new expression where 'with' expressions on arrays are replaced by
@@ -1301,14 +1310,21 @@ exprt interval_sparse_arrayt::to_if_expression(const exprt &index) const
 ///   `with_expr(with_expr(...(array_of(...)))`. This is the form in which
 ///   array valuations coming from the underlying solver are given.
 /// \param index: An index with which to build the equality condition
+/// \param left_propagate: whether values of the array should be propagated to
+///        the left
+/// \param max_index: maximum index up to which we concretize, beyond this index
+///        the array will take the default value (given at the bottom of the
+///        with expression)
 /// \return An expression containing no 'with' expression
 static exprt substitute_array_access(
   const with_exprt &expr,
   const exprt &index,
-  const bool left_propagate)
+  const bool left_propagate,
+  const std::size_t max_index)
 {
-  return left_propagate ? interval_sparse_arrayt(expr).to_if_expression(index)
-                        : sparse_arrayt(expr).to_if_expression(index);
+  return left_propagate
+           ? interval_sparse_arrayt(expr).to_if_expression(index, max_index)
+           : sparse_arrayt(expr).to_if_expression(index, max_index);
 }
 
 /// Fill an array represented by a list of with_expr by propagating values to
@@ -1333,7 +1349,7 @@ fill_in_array_with_expr(const exprt &expr, const std::size_t string_max_length)
   const auto &array_size_opt = numeric_cast<std::size_t>(array_type.size());
   if(array_size_opt && *array_size_opt > 0)
     initial_map.emplace(
-      *array_size_opt - 1,
+      std::min(*array_size_opt - 1, string_max_length),
       from_integer(CHARACTER_FOR_UNKNOWN, array_type.subtype()));
 
   for(exprt it=expr; it.id()==ID_with; it=to_with_expr(it).old())
@@ -1394,14 +1410,15 @@ static exprt substitute_array_access(
   const array_exprt &array_expr,
   const exprt &index,
   const std::function<symbol_exprt(const irep_idt &, const typet &)>
-    &symbol_generator)
+    &symbol_generator,
+  const std::size_t max_index)
 {
   const typet &char_type = array_expr.type().subtype();
   const std::vector<exprt> &operands = array_expr.operands();
 
   exprt result = symbol_generator("out_of_bound_access", char_type);
 
-  for(std::size_t i = 0; i < operands.size(); ++i)
+  for(std::size_t i = 0; i < operands.size() && i < max_index; ++i)
   {
     // Go in reverse order so that smaller indexes appear first in the result
     const std::size_t pos = operands.size() - 1 - i;
@@ -1426,13 +1443,20 @@ static exprt substitute_array_access(
   const exprt &index,
   const std::function<symbol_exprt(const irep_idt &, const typet &)>
     &symbol_generator,
-  const bool left_propagate)
+  const bool left_propagate,
+  const std::size_t max_index)
 {
   // Substitute recursively in branches of conditional expressions
   const exprt true_case = substitute_array_access(
-    index_exprt(if_expr.true_case(), index), symbol_generator, left_propagate);
+    index_exprt(if_expr.true_case(), index),
+    symbol_generator,
+    left_propagate,
+    max_index);
   const exprt false_case = substitute_array_access(
-    index_exprt(if_expr.false_case(), index), symbol_generator, left_propagate);
+    index_exprt(if_expr.false_case(), index),
+    symbol_generator,
+    left_propagate,
+    max_index);
 
   return if_exprt(if_expr.cond(), true_case, false_case);
 }
@@ -1441,23 +1465,32 @@ static exprt substitute_array_access(
   const index_exprt &index_expr,
   const std::function<symbol_exprt(const irep_idt &, const typet &)>
     &symbol_generator,
-  const bool left_propagate)
+  const bool left_propagate,
+  const std::size_t max_index)
 {
   const exprt &array = index_expr.array();
 
   if(array.id() == ID_symbol)
     return index_expr;
+
   if(auto array_of = expr_try_dynamic_cast<array_of_exprt>(array))
     return array_of->op();
+
   if(auto array_with = expr_try_dynamic_cast<with_exprt>(array))
     return substitute_array_access(
-      *array_with, index_expr.index(), left_propagate);
+      *array_with, index_expr.index(), left_propagate, max_index);
+
   if(auto array_expr = expr_try_dynamic_cast<array_exprt>(array))
     return substitute_array_access(
-      *array_expr, index_expr.index(), symbol_generator);
+      *array_expr, index_expr.index(), symbol_generator, max_index);
+
   if(auto if_expr = expr_try_dynamic_cast<if_exprt>(array))
     return substitute_array_access(
-      *if_expr, index_expr.index(), symbol_generator, left_propagate);
+      *if_expr,
+      index_expr.index(),
+      symbol_generator,
+      left_propagate,
+      max_index);
 
   UNREACHABLE;
 }
@@ -1469,16 +1502,18 @@ static void substitute_array_access_in_place(
   exprt &expr,
   const std::function<symbol_exprt(const irep_idt &, const typet &)>
     &symbol_generator,
-  const bool left_propagate)
+  const bool left_propagate,
+  const std::size_t max_index)
 {
   if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
   {
-    expr =
-      substitute_array_access(*index_expr, symbol_generator, left_propagate);
+    expr = substitute_array_access(
+      *index_expr, symbol_generator, left_propagate, max_index);
   }
 
   for(auto &op : expr.operands())
-    substitute_array_access_in_place(op, symbol_generator, left_propagate);
+    substitute_array_access_in_place(
+      op, symbol_generator, left_propagate, max_index);
 }
 
 /// Create an equivalent expression where array accesses and 'with' expressions
@@ -1505,9 +1540,11 @@ exprt substitute_array_access(
   exprt expr,
   const std::function<symbol_exprt(const irep_idt &, const typet &)>
     &symbol_generator,
-  const bool left_propagate)
+  const bool left_propagate,
+  const std::size_t max_index)
 {
-  substitute_array_access_in_place(expr, symbol_generator, left_propagate);
+  substitute_array_access_in_place(
+    expr, symbol_generator, left_propagate, max_index);
   return expr;
 }
 
@@ -1740,7 +1777,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
 
     stream << indent << i << ".\n";
     const exprt with_concretized_arrays =
-      substitute_array_access(negaxiom, gen_symbol, true);
+      substitute_array_access(negaxiom, gen_symbol, true, max_string_length);
     debug_check_axioms_step(
       stream, ns, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
 
@@ -1792,7 +1829,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
 
     negaxiom = simplify_expr(negaxiom, ns);
     const exprt with_concrete_arrays =
-      substitute_array_access(negaxiom, gen_symbol, true);
+      substitute_array_access(negaxiom, gen_symbol, true, max_string_length);
 
     stream << indent << i << '.' << eom;
     debug_check_axioms_step(
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index eba7e99aa9a..7444d006f72 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -56,7 +56,9 @@ class sparse_arrayt
 
   /// Creates an if_expr corresponding to the result of accessing the array
   /// at the given index
-  virtual exprt to_if_expression(const exprt &index) const;
+  virtual exprt to_if_expression(
+    const exprt &index,
+    std::size_t max_index = std::numeric_limits<std::size_t>::max()) const;
 
 protected:
   exprt default_value;
@@ -75,7 +77,10 @@ class interval_sparse_arrayt final : public sparse_arrayt
   /// `arr[k]` is `a`, for all index between `i` (exclusive) and `j` it is `b`
   /// and for the others it is `x`.
   explicit interval_sparse_arrayt(const with_exprt &expr);
-  exprt to_if_expression(const exprt &index) const override;
+  exprt to_if_expression(
+    const exprt &index,
+    std::size_t max_index =
+      std::numeric_limits<std::size_t>::max()) const override;
 };
 
 class string_refinementt final: public bv_refinementt
@@ -157,6 +162,7 @@ exprt substitute_array_access(
   exprt expr,
   const std::function<symbol_exprt(const irep_idt &, const typet &)>
     &symbol_generator,
-  const bool left_propagate);
+  bool left_propagate,
+  std::size_t max_index);
 
 #endif

From 57140f1a8b22590614641e0add744a9577bcd3b0 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 21 Feb 2018 16:55:20 +0000
Subject: [PATCH 07/22] Initialize interval_sparse_array from array_exprt

We can use this to minimize the size of generated formulas when the
array_exprt as repetitive values.
---
 src/solvers/refinement/string_refinement.cpp | 46 ++++++++++----------
 src/solvers/refinement/string_refinement.h   |  2 +
 2 files changed, 26 insertions(+), 22 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 120eb5192be..55d79f7bf45 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -1278,6 +1278,25 @@ interval_sparse_arrayt::interval_sparse_arrayt(const with_exprt &expr)
       const std::pair<std::size_t, exprt> &b) { return a.first < b.first; });
 }
 
+interval_sparse_arrayt::interval_sparse_arrayt(
+  const array_exprt &expr,
+  const exprt &extra_value)
+{
+  default_value = extra_value;
+  if(expr.operands().empty())
+    return;
+
+  entries.emplace_back(0, expr.operands()[0]);
+
+  for(std::size_t i = 1; i < expr.operands().size(); ++i)
+  {
+    if(entries.back().second == expr.operands()[i])
+      entries.back().first = i;
+    else
+      entries.emplace_back(i, expr.operands()[i]);
+  }
+}
+
 exprt interval_sparse_arrayt::to_if_expression(
   const exprt &index,
   const std::size_t max_index) const
@@ -1406,6 +1425,8 @@ exprt fill_in_array_expr(const array_exprt &expr, std::size_t string_max_length)
 /// expressions: for instance in array access `arr[index]`, where:
 /// `arr := {12, 24, 48}` the constructed expression will be:
 ///    `index==0 ? 12 : index==1 ? 24 : 48`
+/// Avoids repetition so `arr := {12, 12, 24, 48}` will give
+///    `index<=1 ? 12 : index==1 ? 24 : 48`
 static exprt substitute_array_access(
   const array_exprt &array_expr,
   const exprt &index,
@@ -1414,28 +1435,9 @@ static exprt substitute_array_access(
   const std::size_t max_index)
 {
   const typet &char_type = array_expr.type().subtype();
-  const std::vector<exprt> &operands = array_expr.operands();
-
-  exprt result = symbol_generator("out_of_bound_access", char_type);
-
-  for(std::size_t i = 0; i < operands.size() && i < max_index; ++i)
-  {
-    // Go in reverse order so that smaller indexes appear first in the result
-    const std::size_t pos = operands.size() - 1 - i;
-    const equal_exprt equals(index, from_integer(pos, java_int_type()));
-    if(operands[pos].type() != char_type)
-    {
-      INVARIANT(
-        operands[pos].id() == ID_unknown,
-        string_refinement_invariantt(
-          "elements can only have type char or "
-          "unknown, and it is not char type"));
-      result = if_exprt(equals, exprt(ID_unknown, char_type), result);
-    }
-    else
-      result = if_exprt(equals, operands[pos], result);
-  }
-  return result;
+  const exprt default_val = symbol_generator("out_of_bound_access", char_type);
+  const interval_sparse_arrayt sparse_array(array_expr, default_val);
+  return sparse_array.to_if_expression(index, max_index);
 }
 
 static exprt substitute_array_access(
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 7444d006f72..e2f614d72c8 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -63,6 +63,7 @@ class sparse_arrayt
 protected:
   exprt default_value;
   std::vector<std::pair<std::size_t, exprt>> entries;
+  sparse_arrayt() = default;
 };
 
 /// Represents arrays by the indexes up to which the value remains the same.
@@ -77,6 +78,7 @@ class interval_sparse_arrayt final : public sparse_arrayt
   /// `arr[k]` is `a`, for all index between `i` (exclusive) and `j` it is `b`
   /// and for the others it is `x`.
   explicit interval_sparse_arrayt(const with_exprt &expr);
+  interval_sparse_arrayt(const array_exprt &expr, const exprt &default_value);
   exprt to_if_expression(
     const exprt &index,
     std::size_t max_index =

From 2323da224ae7291a443d6590dd32fbc464bb05c2 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 22 Feb 2018 10:16:10 +0000
Subject: [PATCH 08/22] Ensure counter-example is smaller than max-length

When check axioms ask for counter examples, we don't want counter
examples that exceeds string-max-length, since these will always be
intrepreted as a non-deterministic character.
---
 src/solvers/refinement/string_refinement.cpp | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 55d79f7bf45..08ea8b8f216 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -1783,8 +1783,13 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
     debug_check_axioms_step(
       stream, ns, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
 
-    if(const auto &witness=
-       find_counter_example(ns, ui, with_concretized_arrays, univ_var))
+    const binary_relation_exprt bound_counter_example(
+      univ_var, ID_le, from_integer(max_string_length, univ_var.type()));
+    const and_exprt negated_with_univ_bound(
+      with_concretized_arrays, bound_counter_example);
+    if(
+      const auto &witness =
+        find_counter_example(ns, ui, negated_with_univ_bound, univ_var))
     {
       stream << indent2 << "- violated_for: " << univ_var.get_identifier()
              << "=" << from_expr(ns, "", *witness) << eom;
@@ -1837,7 +1842,14 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
     debug_check_axioms_step(
       stream, ns, nc_axiom, nc_axiom_in_model, negaxiom, with_concrete_arrays);
 
-    if(const auto witness = find_counter_example(ns, ui, negaxiom, univ_var))
+    const binary_relation_exprt bound_counter_example(
+      univ_var, ID_le, from_integer(max_string_length, univ_var.type()));
+    const and_exprt negated_with_univ_bound(
+      with_concrete_arrays, bound_counter_example);
+
+    if(
+      const auto witness =
+        find_counter_example(ns, ui, negated_with_univ_bound, univ_var))
     {
       stream << indent2 << "- violated_for: " << univ_var.get_identifier()
              << "=" << from_expr(ns, "", *witness) << eom;

From 715837b01ffa7102a543df9ba09611ed0bddd26c Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 22 Feb 2018 11:59:17 +0000
Subject: [PATCH 09/22] Add guard to array access in instanciated formulas

This is so that any access past the bound of string_max_length is
interpreted as a constant.
This avoids the underlying solver attempting to assing values to very
big indexes in arrays.
---
 src/solvers/refinement/string_refinement.cpp | 66 +++++++++++++++-----
 1 file changed, 52 insertions(+), 14 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 08ea8b8f216..966f18388be 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -689,6 +689,44 @@ void output_equations(
            << " == " << from_expr(ns, "", equations[i].rhs()) << std::endl;
 }
 
+/// Make character array accesses at index greater than max_index return
+/// CHARACTER_FOR_UNKNOWN.
+///
+/// For an index_expr `s[i]` we return `(0 <= i <= max_index ? s[i] : '?')`
+/// \param index_expr : an access expression in an array of characters
+/// \param max_index : maximal index up to which array access is meaningful
+/// \return index_expr with the added guard
+static exprt add_guard_to_array_accesses(
+  const index_exprt &index_expr,
+  const std::size_t max_index)
+{
+  PRECONDITION(index_expr.type().id() == ID_unsignedbv);
+  const exprt &index = index_expr.index();
+  // The guard is `0 <= index && index <= max_index`
+  const and_exprt guard(
+    binary_relation_exprt(index, ID_ge, from_integer(0, index.type())),
+    binary_relation_exprt(index, ID_le, from_integer(max_index, index.type())));
+  const exprt unknown = from_integer(CHARACTER_FOR_UNKNOWN, index_expr.type());
+  return if_exprt(guard, index_expr, unknown);
+}
+
+// NOLINTNEXTLINE
+/// \copybrief add_guard_to_array_accesses(index_exprt &index_expr, const std::size_t max_index)
+/// For instance `s[i] == 'a'` would be replaced by
+/// `(i <= max_index ? s[i] : '?') == 'a'`
+/// \param [out] expr : expression in which we replace the accesses
+/// \param max_index : maximal index up to which array access is meaningful
+static void
+add_guard_to_array_accesses(exprt &expr, const std::size_t max_index)
+{
+  for(exprt &op : expr.operands())
+    add_guard_to_array_accesses(op, max_index);
+
+  const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr);
+  if(index_expr && is_char_type(index_expr->type()))
+    expr = add_guard_to_array_accesses(*index_expr, max_index);
+}
+
 /// Main decision procedure of the solver. Looks for a valuation of variables
 /// compatible with the constraints that have been given to `set_to` so far.
 ///
@@ -901,14 +939,14 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   initial_index_set(index_sets, ns, axioms);
   update_index_set(index_sets, ns, current_constraints);
   current_constraints.clear();
-  for(const auto &instance :
-        generate_instantiations(
-          debug(),
-          ns,
-          generator,
-          index_sets,
-          axioms))
+
+  std::vector<exprt> instances =
+    generate_instantiations(debug(), ns, generator, index_sets, axioms);
+  for(auto &instance : instances)
+  {
+    add_guard_to_array_accesses(instance, max_string_length);
     add_lemma(instance);
+  }
 
   while((loop_bound_--)>0)
   {
@@ -963,14 +1001,14 @@ decision_proceduret::resultt string_refinementt::dec_solve()
           debug() << "dec_solve: current index set is empty" << eom;
       }
       current_constraints.clear();
-      for(const auto &instance :
-        generate_instantiations(
-          debug(),
-          ns,
-          generator,
-          index_sets,
-          axioms))
+
+      std::vector<exprt> instances =
+        generate_instantiations(debug(), ns, generator, index_sets, axioms);
+      for(auto &instance : instances)
+      {
+        add_guard_to_array_accesses(instance, max_string_length);
         add_lemma(instance);
+      }
     }
     else
     {

From 4299659b7262cbfe6286bae3b14b58bfff58437b Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 22 Feb 2018 12:02:37 +0000
Subject: [PATCH 10/22] Small refactoring in string_refinement instantiate

---
 src/solvers/refinement/string_refinement.cpp | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 966f18388be..bfcb7871f5c 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -2397,18 +2397,17 @@ static exprt instantiate(
   const exprt &str,
   const exprt &val)
 {
-  exprt idx=find_index(axiom.body(), str, axiom.univ_var());
+  const exprt idx = find_index(axiom.body(), str, axiom.univ_var());
   if(idx.is_nil())
     return true_exprt();
 
-  exprt r=compute_inverse_function(stream, axiom.univ_var(), val, idx);
+  const exprt r = compute_inverse_function(stream, axiom.univ_var(), val, idx);
   implies_exprt instance(axiom.premise(), axiom.body());
   replace_expr(axiom.univ_var(), r, instance);
   // We are not sure the index set contains only positive numbers
-  exprt bounds=and_exprt(
+  and_exprt bounds(
     axiom.univ_within_bounds(),
-    binary_relation_exprt(
-      from_integer(0, val.type()), ID_le, val));
+    binary_relation_exprt(from_integer(0, val.type()), ID_le, val));
   replace_expr(axiom.univ_var(), r, bounds);
   return implies_exprt(bounds, instance);
 }

From 93a3f20e3dbf0d00ede44fe5e1d44ea50368462b Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 22 Feb 2018 15:42:31 +0000
Subject: [PATCH 11/22] Define a sensible default for string-max-length

We set the value of 2^30 as a default value for string-max-length.
It is largely enough for most programs and having a default avoids
possible problems with overflows, and running out of memory because of a
string that is too large.
---
 src/cbmc/cbmc_solvers.cpp                  | 6 ++++--
 src/solvers/refinement/string_refinement.h | 5 +++++
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
index ed5787af6d3..08e4bc3911c 100644
--- a/src/cbmc/cbmc_solvers.cpp
+++ b/src/cbmc/cbmc_solvers.cpp
@@ -176,8 +176,10 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
   info.prop=prop.get();
   info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
   info.ui=ui;
-  if(options.get_bool_option("string-max-length"))
-    info.max_string_length = options.get_signed_int_option("string-max-length");
+  info.max_string_length =
+    options.get_bool_option("string-max-length")
+      ? options.get_unsigned_int_option("string-max-length")
+      : DEFAULT_MAX_STRING_LENGTH;
   info.trace=options.get_bool_option("trace");
   if(options.get_bool_option("max-node-refinement"))
     info.max_node_refinement=
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index e2f614d72c8..b8ded0acc28 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -31,6 +31,11 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
 #define CHARACTER_FOR_UNKNOWN '?'
 
+// The following default for max string length is largely enough for most
+// programs and avoids potential problems with overflows, and running out
+// of memory because of a string that is too large.
+#define DEFAULT_MAX_STRING_LENGTH (1 << 30)
+
 struct index_set_pairt
 {
   std::map<exprt, std::set<exprt>> cumulative;

From 6fa3c616d92e625397a2bd62038918ee46e31002 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 14 Feb 2018 10:49:35 +0000
Subject: [PATCH 12/22] Correct string-max-input-length tests

Remove test from max_input_length

This remove test which was using the way max-input-length was limiting
the size of strings, even constant one.
The solver is now more permisives and the long strings would just get
troncated instead of leading to a solver contradiction.

For MemberTest, we add a new test.
We now have two tests with different values of the option, which should
give different results.
---
 .../max_input_length/MemberTest.class           | Bin 712 -> 728 bytes
 .../max_input_length/MemberTest.desc            |   6 +++---
 .../max_input_length/MemberTest.java            |  14 +++++++++++---
 .../max_input_length/MemberTest2.desc           |   8 ++++++++
 .../max_input_length/Test.class                 | Bin 644 -> 651 bytes
 .../max_input_length/Test.java                  |   6 +++---
 .../max_input_length/test.desc                  |   8 --------
 7 files changed, 25 insertions(+), 17 deletions(-)
 create mode 100644 regression/strings-smoke-tests/max_input_length/MemberTest2.desc
 delete mode 100644 regression/strings-smoke-tests/max_input_length/test.desc

diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.class b/regression/strings-smoke-tests/max_input_length/MemberTest.class
index cbb5dcfdbbd4bfb5916f4bd046d9421035deeb40..1ffb198b86d6a1e2390db748c209fa69057536c3 100644
GIT binary patch
delta 265
zcmYL@Jx;?w5QV>8XT9sq0wzNIBwz?h2$)0&i82ME<^n0{Xy`ZqSFqgCaRY)PA`yv{
zAWlHXMG#_4L-R)SerDdg`81=CpO;tQjG-scO7Lu3b{v@}Vz+|5ifmi<J&u;8<LT0~
z92BG5NW8`4i3u#RTzp;B`+-A_0xP8DsmkL#aLk~*Qj42wxuxaTFrT8|s7>ZX<3??U
zxvZFH;xv0;^$B}VeU2N?NEQ<bXx0Rq#DWGZ(@CR-^v&eYfRuGn614lKW7!aSv%J&o
WzWq<fDDkL2r$L8vCCipjn&vO9q#|7a

delta 247
zcmYL@O-=$q6okKS?CF`dg$W_zAESVP3?yt=vM{c_0CD5OBX|%evt#EGR04@4vNMDe
zcmpqCh;Q7ush6sJ^-^DEV<y|(`v)*)=<u9aPD9Qdnnr{pDdfDc7nY_YEQpq)&84N2
zO&+tiQTBZkcRdwi&jDpmkE?vF(xC528RQRYeSb$ue!y^ro>ogs_HJJ>Gm>;p@JXdO
z3v8S`v%eyoE{WDJ!fR@xWobhoQ!E47a40T9|IoH*D?vSf(#@XvZv-e|)E{Zk{#uDS
Il1Ov>3wPNe1poj5

diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.desc b/regression/strings-smoke-tests/max_input_length/MemberTest.desc
index 2a62caa2eda..4603a102472 100644
--- a/regression/strings-smoke-tests/max_input_length/MemberTest.desc
+++ b/regression/strings-smoke-tests/max_input_length/MemberTest.desc
@@ -1,8 +1,8 @@
 CORE
 MemberTest.class
---refine-strings --verbosity 10 --string-max-length 29 --java-assume-inputs-non-null --function MemberTest.main
-^EXIT=0$
+--refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 31 --function MemberTest.main
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 --
 non equal types
diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.java b/regression/strings-smoke-tests/max_input_length/MemberTest.java
index cf88d8d8f83..9dd3e67a50b 100644
--- a/regression/strings-smoke-tests/max_input_length/MemberTest.java
+++ b/regression/strings-smoke-tests/max_input_length/MemberTest.java
@@ -1,9 +1,17 @@
 public class MemberTest {
     String foo;
+
     public void main() {
-        // Causes this function to be ignored if string-max-length is
-        // less than 40
+        if (foo == null)
+          return;
+
+        // This would prevent anything from happening if we were to add a
+        // constraints on strings being smaller than 40
         String t = new String("0123456789012345678901234567890123456789");
-        assert foo != null && foo.length() < 30;
+
+        if (foo.length() >= 30)
+            // This should not happen when string-max-input length is smaller
+            // than 30
+            assert false;
     }
 }
diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest2.desc b/regression/strings-smoke-tests/max_input_length/MemberTest2.desc
new file mode 100644
index 00000000000..b4e7b2322e4
--- /dev/null
+++ b/regression/strings-smoke-tests/max_input_length/MemberTest2.desc
@@ -0,0 +1,8 @@
+CORE
+MemberTest.class
+--refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 20 --function MemberTest.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+non equal types
diff --git a/regression/strings-smoke-tests/max_input_length/Test.class b/regression/strings-smoke-tests/max_input_length/Test.class
index d01720ffa38de67cc43d1af484757e4e9fcfda97..37d68870ec961e859c4aefbab310cfa3ae28ac2a 100644
GIT binary patch
delta 202
zcmW-aJ8r^I6hx1oKhJ(R5;#8~!N!gupE{D8EFc9XjT@GL#2(V6vfQOXbZL_UBrK6W
zYeI+%&C%%2%$*PS(=GlF+a2)Av!O*#)AzYEDDF=f1O&vI#Gp^+(2$a89;#wtOSbx+
z`#GbKkc&FDa&H{+$W#4pEz2pke1NP$m65%{nY^rV+wqFdFWwie23>CO|9&K;=m;Ym
ip^L%eQl?W;S90;O_N1C?Q8)FQN-eLRsYKtNo82RRGaAnT

delta 194
zcmW-ayAA<S07TDT?%s7RLDu`Z-cd_@fRaL^@Bvzhf6%F9JB_GS6eJ|{zDdMg&15Ds
zC$p6sIeLHZPhd!26Q`gkI+Qema*P<2&{Y*RjS9=Urh%_$?ndj~Y2~;iTw1gP-)h?(
zmoB|vVjbo)A_j!!1F^_NZbYXS<Q{Ku#ZJ|Z#2=`|4d-<>D?!?5(l8*=*!bqoGs(gF
Vgnz=gY%mtSC4;4?tK6T;{{Z2%8gKvr

diff --git a/regression/strings-smoke-tests/max_input_length/Test.java b/regression/strings-smoke-tests/max_input_length/Test.java
index 0616daa4053..9c6e8839f58 100644
--- a/regression/strings-smoke-tests/max_input_length/Test.java
+++ b/regression/strings-smoke-tests/max_input_length/Test.java
@@ -1,8 +1,8 @@
 public class Test {
     public static void main(String s) {
-	// This prevent anything from happening if string-max-length is smaller
-	// than 40
-	String t = new String("0123456789012345678901234567890123456789");
+        // This prevent anything from happening if we were to add a constraints on strings
+        // being smaller than 40
+        String t = new String("0123456789012345678901234567890123456789");
 	if (s.length() >= 30)
 	    // This should not happen when string-max-input length is smaller
 	    // than 30
diff --git a/regression/strings-smoke-tests/max_input_length/test.desc b/regression/strings-smoke-tests/max_input_length/test.desc
deleted file mode 100644
index fb57067e0d7..00000000000
--- a/regression/strings-smoke-tests/max_input_length/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-CORE
-Test.class
---refine-strings --verbosity 10 --string-max-length 30
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-non equal types

From fccdff1663c0eeebc555bae31cc74e045602382b Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 22 Feb 2018 12:13:48 +0000
Subject: [PATCH 13/22] Add test for generics array and strings

This adds an int greater than string-max-length in a generic array.
This is to check that TG-2138 is fixed.
Before the issue was solved setting the array to 101 was in
contradiction with default axioms added by the string solver.
---
 .../IntegerTests.class                        | Bin 0 -> 834 bytes
 .../IntegerTests.java                         |  44 ++++++++++++++++++
 .../max-length-generic-array/MyGenSet.class   | Bin 0 -> 501 bytes
 .../max-length-generic-array/MySet.class      | Bin 0 -> 446 bytes
 .../max-length-generic-array/test.desc        |  19 ++++++++
 .../max-length-generic-array/test_gen.desc    |  20 ++++++++
 6 files changed, 83 insertions(+)
 create mode 100644 regression/jbmc-strings/max-length-generic-array/IntegerTests.class
 create mode 100644 regression/jbmc-strings/max-length-generic-array/IntegerTests.java
 create mode 100644 regression/jbmc-strings/max-length-generic-array/MyGenSet.class
 create mode 100644 regression/jbmc-strings/max-length-generic-array/MySet.class
 create mode 100644 regression/jbmc-strings/max-length-generic-array/test.desc
 create mode 100644 regression/jbmc-strings/max-length-generic-array/test_gen.desc

diff --git a/regression/jbmc-strings/max-length-generic-array/IntegerTests.class b/regression/jbmc-strings/max-length-generic-array/IntegerTests.class
new file mode 100644
index 0000000000000000000000000000000000000000..6120bff5bb6f256912ddb4120be2d604bb633a6e
GIT binary patch
literal 834
zcmaKq&2G~`6ot=?V^3_{Hlb~x^p6%=>;w}2c10{e0#!=rB2}e^)g(+SmtZ5usgy_I
zEsBI_1rlP1#4{npozx~~gBLS*?s(33&z<@C`^z@~kMYRCES3dU92Br@^ROzg=3pH+
zb!NlCCT<Dbc3|sm8(TWs7Puqe5v(Uc7$i>#hUXs;iqE4riZIs-LiK9&uBYOC*&A@i
zP1G=Hk6)^=qY{GWwNB)zYz}02+}sTlb*$nYKbLzJMFS<n9l}f}k^Q%A`F^6rg%a#b
zF;?Qj2u>#&#eMZ6(4b1Hw$Hp_LqlB5p-d=cbQeBqgoW2RTvmcW-NjwpbJ0Lk;J#iw
zAeikj!}P&5z4MU$<S~Tu)XiS+MD^LCDdSj<3G;c*<tDqTOb?_=1aT?{Bei!#sCv8k
zW@Oc|iGCC&G6;u+#e54>UBCN}a@s_#*Ujrqn_JC`WEj7T4b1Sf(4PUmPLz49@M@K3
z;@Pa7gFbRVxXPn7N%F;D9t#}nUlkuM@Z6~VfJtXxQ8+w@(W-w!@jFbTtS(@6>b1`h
zA5bb@pmb*Fflm}BnpKz_7g^inQY@@MaQ{nK<Sai^>lZc!svKVXi|nPydWN(a>1gDY
e9MAn9&t;OfK8q!`z0Jm_ymf)=Y;I{%;*CH4c&lXq

literal 0
HcmV?d00001

diff --git a/regression/jbmc-strings/max-length-generic-array/IntegerTests.java b/regression/jbmc-strings/max-length-generic-array/IntegerTests.java
new file mode 100644
index 00000000000..017b8dc3382
--- /dev/null
+++ b/regression/jbmc-strings/max-length-generic-array/IntegerTests.java
@@ -0,0 +1,44 @@
+public class IntegerTests {
+
+    public static Boolean testMyGenSet(Integer key) {
+        if (key == null) return null;
+        MyGenSet<Integer> ms = new MyGenSet<>();
+        ms.array[0] = 101;
+        if (ms.contains(key)) return true;
+        return false;
+    }
+    
+    public static Boolean testMySet(Integer key) {
+        if (key == null) return null;
+        MySet ms = new MySet();
+        ms.array[0] = 101;
+        if (ms.contains(key)) return true;
+        return false;
+    }
+
+}
+
+class MyGenSet<E> {
+    E[] array;
+    @SuppressWarnings("unchecked")
+    MyGenSet() {
+        array = (E[]) new Object[1];
+    }
+    boolean contains(E o) {
+        if (o.equals(array[0]))
+            return true;
+        return false;
+    }
+}
+
+class MySet {
+    Integer[] array;
+    MySet() {
+        array = new Integer[1];
+    }
+    boolean contains(Integer o) {
+        if (o.equals(array[0]))
+            return true;
+        return false;
+    }
+}
diff --git a/regression/jbmc-strings/max-length-generic-array/MyGenSet.class b/regression/jbmc-strings/max-length-generic-array/MyGenSet.class
new file mode 100644
index 0000000000000000000000000000000000000000..e92e43fee856008bdc97ae12d7bab364c7cd6c44
GIT binary patch
literal 501
zcmZWl%TB^T6g|_Hr-c>~1w`YrU?Rr2Lc+$NF#%naxRBLQC!~l)`!L~C{0BBBJ`xj+
zYd^|(M_CwI%$<ABJ?FkYzh2(~?4y!~g4G1p5=f>HM^VP51j-CC?)!YokneX!{EpYh
z+#A-<1|#8w2Mj6O9eO;Be8Hggdu@W^P1ke77K3V4&j~%8TvF2LxSlwTt_Q;J@xhpo
zq%-kC?s@@3!CI_cy<o`LA$P92{AMnRThu`&tY*8hC}}N13~753`HnbpWzXD+7m6W`
zAc8R1k^AUag3e(6-%SUdLdQBxnzTDT7M?9aT29<Xd>mklj-=4(7(F7=pCV6zyc=Xm
zLNes-QY<-U?FFo+y+Qea`ULHPForDIEL5^ZXehxznS28#sie9=Iax2aU3-M4?mZ)R
kkC--7X9OyL<Q1ZCkZ=<@%BWz*e4b^Z{Z5w0%8#h<4IF-5qyPW_

literal 0
HcmV?d00001

diff --git a/regression/jbmc-strings/max-length-generic-array/MySet.class b/regression/jbmc-strings/max-length-generic-array/MySet.class
new file mode 100644
index 0000000000000000000000000000000000000000..e890519fb8ba18811c7f24a32792a41d4be83045
GIT binary patch
literal 446
zcmZutO-lk%6g_WdoY84aEwztTiwb9=glLt~CI|wnh0?-S&*>p!Hr6->{*?ZMo1hN}
z>Id|rqBAKZ)Z$*=J?EZt5AXBq?E}CbR&AJAu&|gx3Pl?lN*2l%mIP8VisVS3cv<ht
zds*$tuv0w=W7SbnO~5<|!XQ2r&@1kRfN|8nQUbYp5UR7`O<P4x+3pcZ`~5JMK{ya7
zSN?HwTLRfeEdA?Kc{|nEjs7t5)p3v*6s9+uY7h^0k|+)`uu1%h<-kJP!7^4D|8&$)
zu|WQJ>%84nJ|R=x4P}pkO0$6`Y|U+9jelYCdjyMy>>7(ViOlh}%{k$+-YbM>yhD42
z{zyQ;VV{T2z77K$oHvt2ViV~;xx}on<vl^ycVA#UAZ3j8F+pucUZKcE4ju~>i5wmB
HKTCygXD3y!

literal 0
HcmV?d00001

diff --git a/regression/jbmc-strings/max-length-generic-array/test.desc b/regression/jbmc-strings/max-length-generic-array/test.desc
new file mode 100644
index 00000000000..3862a4978b3
--- /dev/null
+++ b/regression/jbmc-strings/max-length-generic-array/test.desc
@@ -0,0 +1,19 @@
+CORE
+IntegerTests.class
+-refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMySet --cover location
+^EXIT=0$
+^SIGNAL=0$
+coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 1 .* SATISFIED
+coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 3 .* SATISFIED
+coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 4 .* SATISFIED
+coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 6 .* SATISFIED
+coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 7 .* SATISFIED
+coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 12 .* SATISFIED
+coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 13 .* SATISFIED
+coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 16 .* SATISFIED
+coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 17 .* SATISFIED
+coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 21 .* SATISFIED
+coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 19 .* SATISFIED
+coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 20 .* SATISFIED
+coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 22 .* SATISFIED
+coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 23 .* SATISFIED
diff --git a/regression/jbmc-strings/max-length-generic-array/test_gen.desc b/regression/jbmc-strings/max-length-generic-array/test_gen.desc
new file mode 100644
index 00000000000..ec123c9a16a
--- /dev/null
+++ b/regression/jbmc-strings/max-length-generic-array/test_gen.desc
@@ -0,0 +1,20 @@
+CORE
+IntegerTests.class
+-refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMyGenSet --cover location
+^EXIT=0$
+^SIGNAL=0$
+coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 1 .* SATISFIED
+coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 3 .* SATISFIED
+coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 4 .* SATISFIED
+coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 6 .* SATISFIED
+coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 7 .* SATISFIED
+coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 10 .* SATISFIED
+coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 13 .* SATISFIED
+coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 14 .* SATISFIED
+coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 17 .* SATISFIED
+coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 18 .* SATISFIED
+coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 22 .* SATISFIED
+coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 20 .* SATISFIED
+coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 21 .* SATISFIED
+coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 23 .* SATISFIED
+coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 24 .* SATISFIED

From 0ea2af6e95cec3fca943f089d17c958503786320 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 22 Feb 2018 17:26:53 +0000
Subject: [PATCH 14/22] Use string-max-input-length in tests

We should now use string-max-input-length to limit the sizes of strings
in the program.
Having string-max-length set to something too small can lead to wrong
results.
---
 regression/strings-smoke-tests/java_format2/test.desc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/regression/strings-smoke-tests/java_format2/test.desc b/regression/strings-smoke-tests/java_format2/test.desc
index 0ea5e37ca19..e4a1ea988d2 100644
--- a/regression/strings-smoke-tests/java_format2/test.desc
+++ b/regression/strings-smoke-tests/java_format2/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --verbosity 10 --string-max-length 20
+--refine-strings --verbosity 10 --string-max-input-length 20
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$

From 54fc9cca5ab52dc717a496bf7acb080f627ee3c1 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 23 Feb 2018 09:51:53 +0000
Subject: [PATCH 15/22] Add tests showing the effect on string-max-length

These tests show how the result of the solver can depend on the
string-max-input-length and string-max-length parameters.
---
 regression/jbmc-strings/max-length/Test.class | Bin 0 -> 1064 bytes
 regression/jbmc-strings/max-length/Test.java  |  37 ++++++++++++++++++
 regression/jbmc-strings/max-length/test1.desc |   6 +++
 regression/jbmc-strings/max-length/test2.desc |   6 +++
 regression/jbmc-strings/max-length/test3.desc |   6 +++
 regression/jbmc-strings/max-length/test4.desc |  11 ++++++
 6 files changed, 66 insertions(+)
 create mode 100644 regression/jbmc-strings/max-length/Test.class
 create mode 100644 regression/jbmc-strings/max-length/Test.java
 create mode 100644 regression/jbmc-strings/max-length/test1.desc
 create mode 100644 regression/jbmc-strings/max-length/test2.desc
 create mode 100644 regression/jbmc-strings/max-length/test3.desc
 create mode 100644 regression/jbmc-strings/max-length/test4.desc

diff --git a/regression/jbmc-strings/max-length/Test.class b/regression/jbmc-strings/max-length/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..0bc43cd0bdbcf889136c6b16a07dfa40f3004bb0
GIT binary patch
literal 1064
zcmZva?N8HC6vm&sb?ep@_JWKz+2nm2$P`hd5*4Q=L{JmZMEqjuno%4b={jQKf5I2V
zFMdW7Ae!JeP5hgT@wsJeF)U4QZ_hpbJ?A{9zyE$a0Wgo78oH2)B8IGnOBe|v{@}if
zQ4JwvWMoXkI3_eEOv+_SMNUH=1r^f*J>y2bZn>UabLtQ6y0KBU$^v3tAiQ8Zws%(`
zn9IKuP)fD3B@kb>9qVahd&6?qWHJfnre(feG2SgXI}LByaw^`Yz*KH|%h)xFRl}(i
zS3TEuDtFFDB)DtUGvxO>O<wmI?-ZqChT_|X?FgiEuRAj$3ud)ht+rZgxTf{kmbFFK
zthzTV3(=84Qb#x91nRhqS%Lm`g^On<JaXNdtD}f3Dz567!!;cj(5s^ly{tp>RLtwR
zjvE4rHsIODmSuYXg-*Msk=3RrG;)crX3a4TrcQRSD1W{`fq|M^DVjTOZP#*(rRV;$
z1vfVhcagMo2ij7;#EG?wELAydrk1U`?ONql)0}|U-~kI<#|ZzCF8)~}(J$@dE(G?4
zB-a$*hWQjSS~!9@kcsHw8uo(%5os6qGW7)lynxBVPpH$spd5TbU=IU@Lj<RJzey?k
zh<!)s)e*u!BrD*vQc$=LkrhUi*90`A{YWr^A%;1Oro?-G66DeCmP8AljPHM<WPwWR
ziZ9$ZlZ<~nMkI0XLnqk`RFb;Mk5e>>el{^cr7YK581zesLE-TqWK|wVcre&3<O$1=
zwhR_dLcVNpuAs~vBU)%~w03`K_6B6wU6zugG<S@oabJKGmEfV4-}62eNTy<k(D$G!
apP>Z5BGBfYd4K9rK))|1bdeGP4F3Zv9L;n9

literal 0
HcmV?d00001

diff --git a/regression/jbmc-strings/max-length/Test.java b/regression/jbmc-strings/max-length/Test.java
new file mode 100644
index 00000000000..e947169506d
--- /dev/null
+++ b/regression/jbmc-strings/max-length/Test.java
@@ -0,0 +1,37 @@
+public class Test {
+
+    static void checkMaxInputLength(String arg1, String arg2) {
+        // Filter
+        if (arg1 == null || arg2 == null)
+            return;
+
+        // The validity of this depends on string-max-input-length
+        assert arg1.length() + arg2.length() < 1_000_000;
+    }
+
+    static void checkMaxLength(String arg1, String arg2) {
+        // Filter
+        if (arg1 == null || arg2 == null)
+            return;
+
+        if(arg1.length() + arg2.length() < 4_001)
+            return;
+
+        // Act
+        String s = arg1.concat(arg2);
+
+        // When string-max-length is smaller than 4_000 this will
+        // always be the case
+        assert org.cprover.CProverString.charAt(s, 4_000) == '?';
+    }
+
+    static void main(String argv[]) {
+        // Filter
+        if (argv.length < 2)
+            return;
+
+        // Act
+        checkMaxInputLength(argv[0], argv[1]);
+        checkMaxLength(argv[0], argv[1]);
+    }
+}
diff --git a/regression/jbmc-strings/max-length/test1.desc b/regression/jbmc-strings/max-length/test1.desc
new file mode 100644
index 00000000000..1cdaf80b01e
--- /dev/null
+++ b/regression/jbmc-strings/max-length/test1.desc
@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --verbosity 10 --string-max-input-length 499999 --function Test.checkMaxInputLength
+^EXIT=0$
+^SIGNAL=0$
+assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: SUCCESS
diff --git a/regression/jbmc-strings/max-length/test2.desc b/regression/jbmc-strings/max-length/test2.desc
new file mode 100644
index 00000000000..e705d18deda
--- /dev/null
+++ b/regression/jbmc-strings/max-length/test2.desc
@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --verbosity 10 --string-max-input-length 500000 --function Test.checkMaxInputLength
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: FAILURE
diff --git a/regression/jbmc-strings/max-length/test3.desc b/regression/jbmc-strings/max-length/test3.desc
new file mode 100644
index 00000000000..ab4c3b62db5
--- /dev/null
+++ b/regression/jbmc-strings/max-length/test3.desc
@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --verbosity 10 --string-max-length 4001 --function Test.checkMaxLength
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: FAILURE
diff --git a/regression/jbmc-strings/max-length/test4.desc b/regression/jbmc-strings/max-length/test4.desc
new file mode 100644
index 00000000000..3a3ad2b15e5
--- /dev/null
+++ b/regression/jbmc-strings/max-length/test4.desc
@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --verbosity 10 --string-max-length 4000 --function Test.checkMaxLength
+^SIGNAL=0$
+--
+^EXIT=0$
+assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: SUCCESS
+--
+The solver may give an ERROR because the value of string-max-length is too
+small to give an answer about the assertion.
+So we just check that the answer is not success.
\ No newline at end of file

From c4b2434d28516ae776e1e016aa2703f214365103 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 26 Feb 2018 08:28:32 +0000
Subject: [PATCH 16/22] Use boolbvt for getting counter examples

We use this counter examples in the string solver but the formula given
there don't use arrays so it is enough to use boolbvt.
---
 src/solvers/refinement/string_refinement.cpp | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index bfcb7871f5c..ef06439d447 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -2572,14 +2572,7 @@ static optionalt<exprt> find_counter_example(
   const symbol_exprt &var)
 {
   satcheck_no_simplifiert sat_check;
-  bv_refinementt::infot info;
-  info.ns=&ns;
-  info.prop=&sat_check;
-  info.refine_arithmetic=true;
-  info.refine_arrays=true;
-  info.max_node_refinement=5;
-  info.ui=ui;
-  bv_refinementt solver(info);
+  boolbvt solver(ns, sat_check);
   solver << axiom;
 
   if(solver()==decision_proceduret::resultt::D_SATISFIABLE)

From 79c218a9b5a66f2ec12488b3c058e10aaf3163bb Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 23 Feb 2018 15:52:32 +0000
Subject: [PATCH 17/22] Ensure `get` does not concretize long strings

The function could potentially run out of memory when attempting to
concretize long strings.
Instead of trying to concretize strings for which get_array failed, we
return an array_of_exprt.
---
 src/solvers/refinement/string_refinement.cpp | 66 ++++++++++++++------
 1 file changed, 46 insertions(+), 20 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index ef06439d447..f1091b7eb6b 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -1113,15 +1113,49 @@ static optionalt<exprt> get_array(
   const array_typet ret_type(char_type, from_integer(n, index_type));
   array_exprt ret(ret_type);
 
+  if(n==0)
+    return empty_ret;
+
   if(n>max_string_length)
   {
     stream << "(sr::get_array) long string (size=" << n << "):"
            << from_expr(ns, "", arr_val) << eom;
-    return {};
   }
 
-  if(n==0)
-    return empty_ret;
+  if(arr_val.id()=="array-list")
+  {
+    DATA_INVARIANT(
+      arr_val.operands().size()%2 == 0,
+      "array-list must have even number of operands");
+    std::map<std::size_t, exprt> initial_map;
+    exprt array = array_of_exprt(
+      from_integer(CHARACTER_FOR_UNKNOWN, char_type), ret_type);
+    for(size_t i = 0; i < arr_val.operands().size(); i += 2)
+    {
+      const exprt &index = arr_val.operands()[i];
+      const auto idx = numeric_cast<std::size_t>(index);
+      if(idx.has_value() && *idx < max_string_length)
+      {
+        const exprt new_value = arr_val.operands()[i + 1];
+        array = with_exprt(array, from_integer(*idx, index_type), new_value);
+      }
+    }
+    return array;
+  }
+  else if(arr_val.id() == ID_array)
+  {
+    ret.operands().insert(
+      ret.operands().end(),
+      arr_val.operands().begin(),
+      arr_val.operands().size() >= n ? arr_val.operands().begin() + n
+                                     : arr_val.operands().end());
+    return ret;
+  }
+  else
+  {
+    stream << "get_array: not an array or array list" << eom;
+    return {};
+  }
 
   if(arr_val.id()=="array-list")
   {
@@ -2533,25 +2567,17 @@ exprt string_refinementt::get(const exprt &expr) const
         concretize_arrays_in_expression(arr_model, max_string_length, ns);
       return concretized_array;
     }
-    else
+    else if(generator.get_created_strings().count(arr))
     {
-      auto set = generator.get_created_strings();
-      if(set.find(arr) != set.end())
-      {
-        exprt length = super_get(arr.length());
-        if(const auto n = numeric_cast<std::size_t>(length))
-        {
-          exprt arr_model =
-            array_exprt(array_typet(arr.type().subtype(), length));
-          for(size_t i = 0; i < *n; i++)
-            arr_model.copy_to_operands(exprt(ID_unknown, arr.type().subtype()));
-          const exprt concretized_array =
-            concretize_arrays_in_expression(arr_model, max_string_length, ns);
-          return concretized_array;
-        }
-      }
-      return arr;
+      const exprt default_char =
+        from_integer(CHARACTER_FOR_UNKNOWN, arr.type().subtype());
+      const exprt length_expr = super_get(arr.length());
+      const array_typet type(arr.type().subtype(), length_expr);
+      const array_of_exprt array_of(default_char, type);
+      return fill_in_array_with_expr(array_of, max_string_length);
     }
+    else
+      return arr;
   }
   return supert::get(ecopy);
 }

From 6a0e9fecbc79db55277b8db54edc7be5121efe87 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 1 Mar 2018 09:59:08 +0000
Subject: [PATCH 18/22] Do not concretize past string_max_length

This is to avoid running out of memory while trying to concretize a
very long string.
---
 src/solvers/refinement/string_refinement.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index f1091b7eb6b..305939f3681 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -1478,9 +1478,12 @@ exprt fill_in_array_expr(const array_exprt &expr, std::size_t string_max_length)
   const auto &array_size_opt = numeric_cast<std::size_t>(array_type.size());
 
   if(array_size_opt && *array_size_opt > 0)
+  {
+    const std::size_t last_index = *array_size_opt <= string_max_length
+                                   ? *array_size_opt - 1 : string_max_length;
     initial_map.emplace(
-      *array_size_opt - 1,
-      from_integer(CHARACTER_FOR_UNKNOWN, array_type.subtype()));
+      last_index, from_integer(CHARACTER_FOR_UNKNOWN, array_type.subtype()));
+  }
 
   for(std::size_t i = 0; i < expr.operands().size(); ++i)
   {

From d0412d52ce8ed0ce6b79d467cfedc306eba400db Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 1 Mar 2018 13:38:54 +0000
Subject: [PATCH 19/22] Make add_lemma add guard to array accesses

This ensures we never pass formulas to the underlying solver that would
require some constraints on arrays at indexes that are negative or
greater than string-max-length.
---
 src/solvers/refinement/string_refinement.cpp | 23 ++++++++------------
 1 file changed, 9 insertions(+), 14 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 305939f3681..b48516710f7 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -943,10 +943,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   std::vector<exprt> instances =
     generate_instantiations(debug(), ns, generator, index_sets, axioms);
   for(auto &instance : instances)
-  {
-    add_guard_to_array_accesses(instance, max_string_length);
     add_lemma(instance);
-  }
 
   while((loop_bound_--)>0)
   {
@@ -1005,10 +1002,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       std::vector<exprt> instances =
         generate_instantiations(debug(), ns, generator, index_sets, axioms);
       for(auto &instance : instances)
-      {
-        add_guard_to_array_accesses(instance, max_string_length);
         add_lemma(instance);
-      }
     }
     else
     {
@@ -1032,13 +1026,14 @@ void string_refinementt::add_lemma(
   if(!seen_instances.insert(lemma).second)
     return;
 
-  current_constraints.push_back(lemma);
+  exprt lemma_copy = lemma;
+  add_guard_to_array_accesses(lemma_copy, max_string_length);
+  current_constraints.push_back(lemma_copy);
 
-  exprt simple_lemma=lemma;
   if(simplify_lemma)
-    simplify(simple_lemma, ns);
+    simplify(lemma_copy, ns);
 
-  if(simple_lemma.is_true())
+  if(lemma_copy.is_true())
   {
 #if 0
     debug() << "string_refinementt::add_lemma : tautology" << eom;
@@ -1046,11 +1041,11 @@ void string_refinementt::add_lemma(
     return;
   }
 
-  symbol_resolve.replace_expr(simple_lemma);
+  symbol_resolve.replace_expr(lemma_copy);
 
   // Replace empty arrays with array_of expression because the solver cannot
   // handle empty arrays.
-  for(auto it = simple_lemma.depth_begin(); it != simple_lemma.depth_end();)
+  for(auto it = lemma_copy.depth_begin(); it != lemma_copy.depth_end();)
   {
     if(it->id() == ID_array && it->operands().empty())
     {
@@ -1063,9 +1058,9 @@ void string_refinementt::add_lemma(
       ++it;
   }
 
-  debug() << "adding lemma " << from_expr(ns, "", simple_lemma) << eom;
+  debug() << "adding lemma " << from_expr(ns, "", lemma_copy) << eom;
 
-  prop.l_set_to_true(convert(simple_lemma));
+  prop.l_set_to_true(convert(lemma_copy));
 }
 
 /// Get a model of an array and put it in a certain form.

From d845a0a78585c90843a36224ab3b42c0477a293d Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 1 Mar 2018 13:40:46 +0000
Subject: [PATCH 20/22] Remove unecessary replace_expr

This is already done in add_lemma.
---
 src/solvers/refinement/string_refinement.cpp | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index b48516710f7..2e53bc005b4 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -895,11 +895,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       generator.fresh_symbol("not_contains_witness", witness_type);
   }
 
-  for(exprt lemma : generator.get_lemmas())
-  {
-    symbol_resolve.replace_expr(lemma);
+  for(const exprt &lemma : generator.get_lemmas())
     add_lemma(lemma);
-  }
 
   // Initial try without index set
   const auto get = [this](const exprt &expr) { return this->get(expr); };

From 569edb50bac74e4ab6058c9387b9a20f2354f711 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 1 Mar 2018 16:17:58 +0000
Subject: [PATCH 21/22] Correct bounds in instantiate method

This was not checking that the instantiate variable does not exceed the
upper bound.
---
 src/solvers/refinement/string_refinement.cpp | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 2e53bc005b4..b4d4e007371 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -2431,14 +2431,15 @@ static exprt instantiate(
     return true_exprt();
 
   const exprt r = compute_inverse_function(stream, axiom.univ_var(), val, idx);
-  implies_exprt instance(axiom.premise(), axiom.body());
+  implies_exprt instance(
+    and_exprt(
+      and_exprt(
+        binary_relation_exprt(axiom.univ_var(), ID_ge, axiom.lower_bound()),
+        binary_relation_exprt(axiom.univ_var(), ID_lt, axiom.upper_bound())),
+      axiom.premise()),
+    axiom.body());
   replace_expr(axiom.univ_var(), r, instance);
-  // We are not sure the index set contains only positive numbers
-  and_exprt bounds(
-    axiom.univ_within_bounds(),
-    binary_relation_exprt(from_integer(0, val.type()), ID_le, val));
-  replace_expr(axiom.univ_var(), r, bounds);
-  return implies_exprt(bounds, instance);
+  return instance;
 }
 
 /// Instantiates a quantified formula representing `not_contains` by

From 2a1bc921e58a838695a82cd0b1e857cc038eb438 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 1 Mar 2018 16:24:38 +0000
Subject: [PATCH 22/22] Correct instantiation of counter example

This was not adding the correct constraints on the bounds.
---
 src/solvers/refinement/string_refinement.cpp | 15 ++++-----------
 1 file changed, 4 insertions(+), 11 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index b4d4e007371..1ce7c6c7f1d 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -1947,18 +1947,11 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
         const exprt &val=v.second;
         const string_constraintt &axiom=axioms.universal[v.first];
 
-        implies_exprt instance(axiom.premise(), axiom.body());
+        implies_exprt instance(
+          and_exprt(axiom.univ_within_bounds(), axiom.premise()), axiom.body());
         replace_expr(axiom.univ_var(), val, instance);
-        // We are not sure the index set contains only positive numbers
-        exprt bounds=and_exprt(
-          axiom.univ_within_bounds(),
-          binary_relation_exprt(
-            from_integer(0, val.type()), ID_le, val));
-        replace_expr(axiom.univ_var(), val, bounds);
-        const implies_exprt counter(bounds, instance);
-
-        stream << "  -  " << from_expr(ns, "", counter) << eom;
-        lemmas.push_back(counter);
+        stream << "  -  " << from_expr(ns, "", instance) << eom;
+        lemmas.push_back(instance);
       }
 
       for(const auto &v : violated_not_contains)