From f15ea752c08a4c097bf85d7aa27104d29573d2ef Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 16 Mar 2017 14:54:57 +0000
Subject: [PATCH 01/17] Substitute array access by if-then-else expressions

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

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 1391ffd2315..d7db9a734e2 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -871,6 +871,111 @@ void string_refinementt::fill_model()
 
 /*******************************************************************\
 
+Function: string_refinementt::substitute_array_with_expr()
+
+  Inputs:
+    expr - A (possibly nested) 'with' expression on an `array_of`
+           expression
+    index - An index with which to build the equality condition
+
+ Outputs: An expression containing no 'with' expression
+
+ Purpose: Create a new expression where 'with' expressions on arrays
+          are replaced by 'if' expressions.
+          e.g. for an array access arr[x], where:
+               `arr := array_of(12) with {0:=24} with {2:=42}`
+               the constructed expression will be:
+               `index==0 ? 24 : index==2 ? 42 : 12`
+
+\*******************************************************************/
+
+exprt string_refinementt::substitute_array_with_expr
+  (exprt &expr, exprt &index) const
+{
+  if(expr.id()==ID_with)
+  {
+    with_exprt &with_expr=to_with_expr(expr);
+    return if_exprt(equal_exprt(index, with_expr.where()),
+                    with_expr.new_value(),
+                    substitute_array_with_expr(with_expr.old(), index));
+  }
+  else
+  {
+    // Only handle 'with' expressions on 'array_of' expressions.
+    assert(expr.id()==ID_array_of);
+    return to_array_of_expr(expr).what();
+  }
+}
+
+/*******************************************************************\
+
+Function: string_refinementt::substitute_array_access()
+
+  Inputs:
+    expr - an expression containing array accesses
+
+ Outputs: an expression containing no array access
+
+ Purpose: create an equivalent expression where array accesses and
+          'with' expressions are replaced by 'if' expressions.
+          e.g. for an array access arr[x], where:
+               `arr := {12, 24, 48}`
+               the constructed expression will be:
+               `index==0 ? 12 : index==1 ? 24 : 48`
+
+\*******************************************************************/
+
+exprt string_refinementt::substitute_array_access(exprt &expr) const
+{
+  for(size_t i=0; i<expr.operands().size(); ++i)
+  {
+    // TODO: only copy when necessary
+    exprt op(expr.operands()[i]);
+    expr.operands()[i]=substitute_array_access(op);
+  }
+
+  if(expr.id()==ID_index)
+  {
+    index_exprt &index_expr=to_index_expr(expr);
+
+    if(index_expr.array().id()==ID_symbol)
+    {
+      return index_expr;
+    }
+
+    if(index_expr.array().id()==ID_with)
+    {
+      exprt subst=substitute_array_with_expr(index_expr.array(),
+                                             index_expr.index());
+      return subst;
+    }
+
+    if(index_expr.array().id()==ID_array_of)
+    {
+      return to_array_of_expr(index_expr.array()).op();
+    }
+
+    assert(index_expr.array().id()==ID_array);
+    array_exprt &array_expr=to_array_expr(index_expr.array());
+
+    size_t last_index=array_expr.operands().size()-1;
+    assert(last_index>=0);
+    exprt ite=array_expr.operands()[last_index];
+
+    for(long i=last_index-1; i>=0; --i)
+    {
+      equal_exprt equals(index_expr.index(), from_integer(i, java_int_type()));
+      ite=if_exprt(equals,
+                   array_expr.operands()[i],
+                   ite);
+    }
+    return ite;
+  }
+  return expr;
+}
+
+/*******************************************************************\
+
 Function: string_refinementt::add_negation_of_constraint_to_solver
 
   Inputs: a string constraint and a solver for non string expressions
@@ -913,7 +1018,7 @@ void string_refinementt::add_negation_of_constraint_to_solver(
   and_exprt negaxiom(premise, not_exprt(axiom.body()));
 
   debug() << "(sr::check_axioms) negated axiom: " << from_expr(negaxiom) << eom;
-  solver << negaxiom;
+  solver << substitute_array_access(negaxiom);
 }
 
 /*******************************************************************\
@@ -1007,6 +1112,7 @@ bool string_refinementt::check_axioms()
         exprt premise(axiom.premise());
         exprt body(axiom.body());
         implies_exprt instance(premise, body);
+        replace_expr(symbol_resolve, instance);
         replace_expr(axiom.univ_var(), val, instance);
         debug() << "adding counter example " << from_expr(instance) << eom;
         add_lemma(instance);

From 0ef1a1fc9ab3ee4e6f2f0aafd4f3edd5bfc0a917 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 17 Mar 2017 11:48:53 +0000
Subject: [PATCH 02/17] Setting ui for temporary solver

---
 src/solvers/refinement/string_refinement.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index d7db9a734e2..06eb4b22b46 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -1058,6 +1058,7 @@ bool string_refinementt::check_axioms()
 
     satcheck_no_simplifiert sat_check;
     supert solver(ns, sat_check);
+    solver.set_ui(ui);
     add_negation_of_constraint_to_solver(axiom_in_model, solver);
 
     switch(solver())

From 4cff10e97a21cfecbee766192343add2a3a6c197 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 17 Mar 2017 12:59:51 +0000
Subject: [PATCH 03/17] Added option to the string solver for string length and
 printability

Added field in string_refinement and string_constraint_generator to
bound size of strings in the program and enforce a range on the
characters.
---
 .../refinement/string_constraint_generator.h  |  13 +-
 .../string_constraint_generator_concat.cpp    |   3 +-
 .../string_constraint_generator_main.cpp      |  56 +++++--
 src/solvers/refinement/string_refinement.cpp  | 144 ++++++++++++++----
 src/solvers/refinement/string_refinement.h    |  14 +-
 5 files changed, 184 insertions(+), 46 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index 12447e0cf04..d8f3f17326e 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -26,9 +26,17 @@ class string_constraint_generatort
   // to the axiom list.
 
   string_constraint_generatort():
-    mode(ID_unknown)
+    mode(ID_unknown),
+    max_string_length(-1),
+    force_printable_characters(false)
   { }
 
+  // Constraints on the maximal length of strings
+  int max_string_length;
+
+  // Should we add constraints on the characters
+  bool force_printable_characters;
+
   void set_mode(irep_idt _mode)
   {
     // only C and java modes supported
@@ -74,6 +82,8 @@ class string_constraint_generatort
   // Maps unresolved symbols to the string_exprt that was created for them
   std::map<irep_idt, string_exprt> unresolved_symbols;
 
+  // Set of strings that have been created by the generator
+  std::set<string_exprt> created_strings;
 
   string_exprt find_or_add_string_of_symbol(
     const symbol_exprt &sym,
@@ -100,6 +110,7 @@ class string_constraint_generatort
 
   static irep_idt extract_java_string(const symbol_exprt &s);
 
+  void add_default_axioms(const string_exprt &s);
   exprt axiom_for_is_positive_index(const exprt &x);
 
   // The following functions add axioms for the returned value
diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp
index fb8e24d5320..eb841cc5b04 100644
--- a/src/solvers/refinement/string_constraint_generator_concat.cpp
+++ b/src/solvers/refinement/string_constraint_generator_concat.cpp
@@ -35,7 +35,8 @@ string_exprt string_constraint_generatort::add_axioms_for_concat(
   // a4 : forall i<|s1|. res[i]=s1[i]
   // a5 : forall i<|s2|. res[i+|s1|]=s2[i]
 
-  res.length()=plus_exprt_with_overflow_check(s1.length(), s2.length());
+  equal_exprt a1(res.length(), plus_exprt_with_overflow_check(s1.length(), s2.length()));
+  axioms.push_back(a1);
   axioms.push_back(s1.axiom_for_is_shorter_than(res));
   axioms.push_back(s2.axiom_for_is_shorter_than(res));
 
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index e4292da542b..f081ac26f47 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -173,10 +173,11 @@ Function: string_constraint_generatort::fresh_string
 string_exprt string_constraint_generatort::fresh_string(
   const refined_string_typet &type)
 {
-  symbol_exprt length=
-    fresh_symbol("string_length", type.get_index_type());
+  symbol_exprt length=fresh_symbol("string_length", type.get_index_type());
   symbol_exprt content=fresh_symbol("string_content", type.get_content_type());
-  return string_exprt(length, content, type);
+  string_exprt str(length, content, type);
+  created_strings.insert(str);
+  return str;
 }
 
 /*******************************************************************\
@@ -246,6 +247,45 @@ string_exprt string_constraint_generatort::convert_java_string_to_string_exprt(
 
 /*******************************************************************\
 
+Function: string_constraint_generatort::add_default_constraints
+
+  Inputs:
+    s - a string expression
+
+ Outputs: a string expression that is linked to the argument through
+          axioms that are added to the list
+
+ Purpose: 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 '~'
+
+
+\*******************************************************************/
+
+void string_constraint_generatort::add_default_axioms(
+  const string_exprt &s)
+{
+  s.axiom_for_is_longer_than(from_integer(0, s.length().type()));
+  if(max_string_length>=0)
+    axioms.push_back(s.axiom_for_is_shorter_than(max_string_length));
+
+  if(force_printable_characters)
+  {
+    symbol_exprt qvar=fresh_univ_index("printable", s.length().type());
+    exprt chr=s[qvar];
+    and_exprt printable(
+      binary_relation_exprt(chr, ID_ge, from_integer(' ', chr.type())),
+      binary_relation_exprt(chr, ID_le, from_integer('~', chr.type())));
+    string_constraintt sc(qvar, s.length(), printable);
+    axioms.push_back(sc);
+  }
+}
+
+/*******************************************************************\
+
 Function: string_constraint_generatort::add_axioms_for_refined_string
 
   Inputs: an expression of refined string type
@@ -258,7 +298,6 @@ Function: string_constraint_generatort::add_axioms_for_refined_string
 
 \*******************************************************************/
 
-
 string_exprt string_constraint_generatort::add_axioms_for_refined_string(
   const exprt &string)
 {
@@ -272,15 +311,13 @@ string_exprt string_constraint_generatort::add_axioms_for_refined_string(
   {
     const symbol_exprt &sym=to_symbol_expr(string);
     string_exprt s=find_or_add_string_of_symbol(sym, type);
-    axioms.push_back(
-      s.axiom_for_is_longer_than(from_integer(0, s.length().type())));
+    add_default_axioms(s);
     return s;
   }
   else if(string.id()==ID_nondet_symbol)
   {
     string_exprt s=fresh_string(type);
-    axioms.push_back(
-      s.axiom_for_is_longer_than(from_integer(0, s.length().type())));
+    add_default_axioms(s);
     return s;
   }
   else if(string.id()==ID_if)
@@ -290,8 +327,7 @@ string_exprt string_constraint_generatort::add_axioms_for_refined_string(
   else if(string.id()==ID_struct)
   {
     const string_exprt &s=to_string_expr(string);
-    axioms.push_back(
-      s.axiom_for_is_longer_than(from_integer(0, s.length().type())));
+    add_default_axioms(s);
     return s;
   }
   else
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 06eb4b22b46..164bb32c012 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -43,7 +43,8 @@ string_refinementt::string_refinementt(
   supert(_ns, _prop),
   use_counter_example(false),
   do_concretizing(false),
-  initial_loop_bound(refinement_bound)
+  initial_loop_bound(refinement_bound),
+  non_empty_string(false)
 { }
 
 /*******************************************************************\
@@ -65,6 +66,52 @@ void string_refinementt::set_mode()
 
 /*******************************************************************\
 
+Function: string_refinementt::set_max_string_length
+
+  Inputs:
+    i - maximum length which is allowed for strings.
+        negative number means no limit
+
+ Purpose: Add constraints on the size of strings used in the
+          program.
+
+\*******************************************************************/
+
+void string_refinementt::set_max_string_length(int i)
+{
+  generator.max_string_length=i;
+}
+
+/*******************************************************************\
+
+Function: string_refinementt::set_max_string_length
+
+ Purpose: Add constraints on the size of nondet character arrays
+          to ensure they have length at least 1
+
+\*******************************************************************/
+
+void string_refinementt::enforce_non_empty_string()
+{
+  non_empty_string=true;
+}
+
+/*******************************************************************\
+
+Function: string_refinementt::enforce_printable_characters
+
+ Purpose: Add constraints on characters used in the program
+          to ensure they are printable
+
+\*******************************************************************/
+
+void string_refinementt::enforce_printable_characters()
+{
+  generator.force_printable_characters=true;
+}
+
+/*******************************************************************\
+
 Function: string_refinementt::display_index_set
 
  Purpose: display the current index set, for debugging
@@ -283,52 +330,71 @@ bool string_refinementt::add_axioms_for_string_assigns(const exprt &lhs,
 
 /*******************************************************************\
 
-Function: string_refinementt::concretize_results
+Function: string_refinementt::concretize_string
 
- Purpose: For each string whose length has been solved, add constants
+  Input:
+    expr - an expression
+
+ Purpose: 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 map `found_length`
 
 \*******************************************************************/
 
-void string_refinementt::concretize_results()
+void string_refinementt::concretize_string(const exprt &expr)
 {
-  for(const auto& it : symbol_resolve)
+  if(refined_string_typet::is_refined_string_type(expr.type()))
   {
-    if(refined_string_typet::is_refined_string_type(it.second.type()))
+    string_exprt str=to_string_expr(expr);
+    exprt length=get(str.length());
+    add_lemma(equal_exprt(str.length(), length));
+    exprt content=str.content();
+    replace_expr(symbol_resolve, content);
+    found_length[content]=length;
+    mp_integer found_length;
+    if(!to_integer(length, found_length))
     {
-      string_exprt str=to_string_expr(it.second);
-      exprt length=current_model[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))
+      assert(found_length.is_long());
+      if(found_length < 0)
       {
-        assert(found_length.is_long());
-        if(found_length < 0)
-        {
-          debug() << "concretize_results: WARNING found length is negative"
-                  << eom;
-        }
-        else
+        debug() << "concretize_results: WARNING found length is negative"
+                << eom;
+      }
+      else
+      {
+        size_t concretize_limit=found_length.to_long();
+        concretize_limit=concretize_limit>MAX_CONCRETE_STRING_SIZE?
+              MAX_CONCRETE_STRING_SIZE:concretize_limit;
+        exprt content_expr=str.content();
+        for(size_t i=0; i<concretize_limit; ++i)
         {
-          size_t concretize_limit=found_length.to_long();
-          concretize_limit=concretize_limit>MAX_CONCRETE_STRING_SIZE?
-                MAX_CONCRETE_STRING_SIZE:concretize_limit;
-          exprt content_expr=str.content();
-          replace_expr(current_model, content_expr);
-          for(size_t i=0; i<concretize_limit; ++i)
-          {
-            auto i_expr=from_integer(i, str.length().type());
-            debug() << "Concretizing " << from_expr(content_expr)
-                    << " / " << i << eom;
-            current_index_set[str.content()].insert(i_expr);
-          }
+          auto i_expr=from_integer(i, str.length().type());
+          debug() << "Concretizing " << from_expr(content_expr)
+                  << " / " << i << eom;
+          current_index_set[str.content()].insert(i_expr);
+          index_set[str.content()].insert(i_expr);
         }
       }
     }
   }
+}
+
+/*******************************************************************\
+
+Function: string_refinementt::concretize_results
+
+ Purpose: For each string whose length has been solved, add constants
+          to the index set to force the solver to pick concrete values
+          for each character, and fill the map `found_length`
+
+\*******************************************************************/
+
+void string_refinementt::concretize_results()
+{
+  for(const auto& it : symbol_resolve)
+    concretize_string(it.second);
+  for(const auto& it : generator.created_strings)
+    concretize_string(it);
   add_instantiations();
 }
 
@@ -348,7 +414,18 @@ void string_refinementt::concretize_lengths()
     if(refined_string_typet::is_refined_string_type(it.second.type()))
     {
       string_exprt str=to_string_expr(it.second);
-      exprt length=current_model[str.length()];
+      exprt length=get(str.length());
+      exprt content=str.content();
+      replace_expr(symbol_resolve, content);
+      found_length[content]=length;
+     }
+  }
+  for(const auto& it : generator.created_strings)
+  {
+    if(refined_string_typet::is_refined_string_type(it.type()))
+    {
+      string_exprt str=to_string_expr(it);
+      exprt length=get(str.length());
       exprt content=str.content();
       replace_expr(symbol_resolve, content);
       found_length[content]=length;
@@ -869,6 +946,7 @@ void string_refinementt::fill_model()
   }
 }
 
+
 /*******************************************************************\
 
 Function: string_refinementt::substitute_array_with_expr()
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 0a62a6abe7d..0163936b069 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -2,7 +2,7 @@
 
 Module: String support via creating string constraints and progressively
         instantiating the universal constraints as needed.
-	The procedure is described in the PASS paper at HVC'13:
+        The procedure is described in the PASS paper at HVC'13:
         "PASS: String Solving with Parameterized Array and Interval Automaton"
         by Guodong Li and Indradeep Ghosh
 
@@ -38,8 +38,13 @@ class string_refinementt: public bv_refinementt
   // Should we use counter examples at each iteration?
   bool use_counter_example;
 
+  // Should we concretize strings when the solver finished
   bool do_concretizing;
 
+  void set_max_string_length(int i);
+  void enforce_non_empty_string();
+  void enforce_printable_characters();
+
   virtual std::string decision_procedure_text() const override
   {
     return "string refinement loop with "+prop.solver_text();
@@ -65,6 +70,9 @@ class string_refinementt: public bv_refinementt
 
   string_constraint_generatort generator;
 
+  bool non_empty_string;
+  expr_sett nondet_arrays;
+
   // Simple constraints that have been given to the solver
   expr_sett seen_instances;
 
@@ -98,6 +106,8 @@ class string_refinementt: public bv_refinementt
   exprt substitute_function_applications(exprt expr);
   typet substitute_java_string_types(typet type);
   exprt substitute_java_strings(exprt expr);
+  exprt substitute_array_with_expr(exprt &expr, exprt &index) const;
+  exprt substitute_array_access(exprt &expr) const;
   void add_symbol_to_symbol_map(const exprt &lhs, const exprt &rhs);
   bool is_char_array(const typet &type) const;
   bool add_axioms_for_string_assigns(const exprt &lhs, const exprt &rhs);
@@ -134,8 +144,10 @@ class string_refinementt: public bv_refinementt
 
   exprt simplify_sum(const exprt &f) const;
 
+  void concretize_string(const exprt &expr);
   void concretize_results();
   void concretize_lengths();
+
   // Length of char arrays found during concretization
   std::map<exprt, exprt> found_length;
 

From 3a82a7f13837cb068e61eb556506e35f4d989a87 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 17 Mar 2017 13:08:37 +0000
Subject: [PATCH 04/17] Adding options to cbmc for parameters of the string
 solver

We add the options string-max-length, string-non-empty, and string-printable
---
 src/cbmc/cbmc_parse_options.cpp |  8 ++++++++
 src/cbmc/cbmc_parse_options.h   |  2 +-
 src/cbmc/cbmc_solvers.cpp       | 10 ++++++++++
 3 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 1f49653c644..5af90c00b79 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -320,6 +320,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("refine-strings"))
   {
     options.set_option("refine-strings", true);
+    options.set_option("string-non-empty", cmdline.isset("string-non-empty"));
+    options.set_option("string-printable", cmdline.isset("string-printable"));
+    if(cmdline.isset("string-max-length"))
+      options.set_option(
+        "string-max-length", cmdline.get_value("string-max-length"));
   }
 
   if(cmdline.isset("max-node-refinement"))
@@ -1207,6 +1212,9 @@ void cbmc_parse_optionst::help()
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
     " --refine-strings             use string refinement (experimental)\n"
+    " --string-non-empty           add constraint that strings are non empty (experimental)\n" // NOLINT(*)
+    " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
+    " --string-max-length          add constraint on the length of strings (experimental)\n" // NOLINT(*)
     " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)
     " --arrays-uf-always           always turn arrays into uninterpreted functions\n" // NOLINT(*)
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index b3225951b3b..4bdc07a6278 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -38,7 +38,7 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(no-pretty-names)(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
-  "(refine-strings)" \
+  "(refine-strings)(string-non-empty)(string-printable)(string-max-length):" \
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-loops)" \
diff --git a/src/cbmc/cbmc_solvers.cpp b/src/cbmc/cbmc_solvers.cpp
index a72546a8d0c..dace046cc17 100644
--- a/src/cbmc/cbmc_solvers.cpp
+++ b/src/cbmc/cbmc_solvers.cpp
@@ -232,6 +232,16 @@ cbmc_solverst::solvert* cbmc_solverst::get_string_refinement()
   string_refinementt *string_refinement=new string_refinementt(
     ns, *prop, MAX_NB_REFINEMENT);
   string_refinement->set_ui(ui);
+
+  string_refinement->do_concretizing=options.get_bool_option("trace");
+  if(options.get_bool_option("string-max-length"))
+    string_refinement->set_max_string_length(
+      options.get_signed_int_option("string-max-length"));
+  if(options.get_bool_option("string-non-empty"))
+    string_refinement->enforce_non_empty_string();
+  if(options.get_bool_option("string-printable"))
+    string_refinement->enforce_printable_characters();
+
   return new solvert(string_refinement, prop);
 }
 

From 6bbf1f7f65bf130cdb62477d48067db60fc63146 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 17 Mar 2017 15:40:47 +0000
Subject: [PATCH 05/17] Remove the mode option from string solver

This option is no longer requiered because the implementation is now
language independent.
---
 .../refinement/string_constraint_generator.h  | 10 --------
 .../string_constraint_generator_main.cpp      |  2 --
 src/solvers/refinement/string_refinement.cpp  | 23 -------------------
 3 files changed, 35 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index d8f3f17326e..a69f2c39ae6 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -26,7 +26,6 @@ class string_constraint_generatort
   // to the axiom list.
 
   string_constraint_generatort():
-    mode(ID_unknown),
     max_string_length(-1),
     force_printable_characters(false)
   { }
@@ -37,15 +36,6 @@ class string_constraint_generatort
   // Should we add constraints on the characters
   bool force_printable_characters;
 
-  void set_mode(irep_idt _mode)
-  {
-    // only C and java modes supported
-    assert((_mode==ID_java) || (_mode==ID_C));
-    mode=_mode;
-  }
-
-  irep_idt &get_mode() { return mode; }
-
   // Axioms are of three kinds: universally quantified string constraint,
   // not contains string constraints and simple formulas.
   std::list<exprt> axioms;
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index f081ac26f47..ddc5ab7a3a3 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -224,7 +224,6 @@ Function: string_constraint_generatort::convert_java_string_to_string_exprt
 string_exprt string_constraint_generatort::convert_java_string_to_string_exprt(
     const exprt &jls)
 {
-  assert(get_mode()==ID_java);
   assert(jls.id()==ID_struct);
 
   exprt length(to_struct_expr(jls).op1());
@@ -433,7 +432,6 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
     // TODO: This part needs some improvement.
     // Stripping the symbol name is not a very robust process.
     new_expr.function() = symbol_exprt(str_id.substr(0, pos+4));
-    assert(get_mode()==ID_java);
     new_expr.type() = refined_string_typet(java_int_type(), java_char_type());
 
     auto res_it=function_application_cache.insert(std::make_pair(new_expr,
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 164bb32c012..9fe961fb87e 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -49,23 +49,6 @@ string_refinementt::string_refinementt(
 
 /*******************************************************************\
 
-Function: string_refinementt::set_mode
-
- Purpose: determine which language should be used
-
-\*******************************************************************/
-
-void string_refinementt::set_mode()
-{
-  debug() << "initializing mode" << eom;
-  symbolt init=ns.lookup(irep_idt(CPROVER_PREFIX"initialize"));
-  irep_idt mode=init.mode;
-  debug() << "mode detected as " << mode << eom;
-  generator.set_mode(mode);
-}
-
-/*******************************************************************\
-
 Function: string_refinementt::set_max_string_length
 
   Inputs:
@@ -448,12 +431,6 @@ void string_refinementt::set_to(const exprt &expr, bool value)
 {
   assert(equality_propagation);
 
-  // TODO: remove the mode field of generator since we should be language
-  // independent.
-  // We only set the mode once.
-  if(generator.get_mode()==ID_unknown)
-    set_mode();
-
   if(expr.id()==ID_equal)
   {
     equal_exprt eq_expr=to_equal_expr(expr);

From cd010dba5a1f030d8696f27468291a03dff8db2a Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 20 Mar 2017 14:51:54 +0000
Subject: [PATCH 06/17] Setting the type for unknown values in
 substitute_array_access

Unknown values could cause type problems if we do not force the type
for them.
---
 src/solvers/refinement/string_refinement.cpp | 28 +++++++++++++++-----
 1 file changed, 22 insertions(+), 6 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 9fe961fb87e..ebcbf0f6ad5 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -950,9 +950,12 @@ exprt string_refinementt::substitute_array_with_expr
   if(expr.id()==ID_with)
   {
     with_exprt &with_expr=to_with_expr(expr);
-    return if_exprt(equal_exprt(index, with_expr.where()),
-                    with_expr.new_value(),
-                    substitute_array_with_expr(with_expr.old(), index));
+    exprt then_expr=with_expr.new_value();
+    exprt else_expr=substitute_array_with_expr(with_expr.old(), index);
+    const typet &type=then_expr.type();
+    assert(else_expr.type()==type);
+    return if_exprt(
+      equal_exprt(index, with_expr.where()), then_expr, else_expr, type);
   }
   else
   {
@@ -1015,14 +1018,27 @@ exprt string_refinementt::substitute_array_access(exprt &expr) const
 
     size_t last_index=array_expr.operands().size()-1;
     assert(last_index>=0);
+
+    const typet &char_type=index_expr.array().type().subtype();
     exprt ite=array_expr.operands()[last_index];
 
+    if(ite.type()!=char_type)
+    {
+      // We have to manualy set the type for unknown values
+      assert(ite.id()==ID_unknown);
+      ite.type()=char_type;
+    }
+
     for(long i=last_index-1; i>=0; --i)
     {
+      exprt op=array_expr.operands()[i];
+      if(op.type()!=char_type)
+      {
+        assert(op.id()==ID_unknown);
+        op.type()=char_type;
+      }
       equal_exprt equals(index_expr.index(), from_integer(i, java_int_type()));
-      ite=if_exprt(equals,
-                   array_expr.operands()[i],
-                   ite);
+      ite=if_exprt(equals, op, ite, char_type);
     }
     return ite;
   }

From 4cbc28cf5bece701b85b9e346243d5cdac64b312 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 21 Mar 2017 16:37:03 +0000
Subject: [PATCH 07/17] Adapt add_axioms_for_insert for 5 arguments #110

---
 .../string_constraint_generator_insert.cpp    | 25 +++++++++++++++----
 1 file changed, 20 insertions(+), 5 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/refinement/string_constraint_generator_insert.cpp
index cd5f4376a93..7a63279699e 100644
--- a/src/solvers/refinement/string_constraint_generator_insert.cpp
+++ b/src/solvers/refinement/string_constraint_generator_insert.cpp
@@ -40,17 +40,32 @@ Function: string_constraint_generatort::add_axioms_for_insert
 
  Outputs: a new string expression
 
- Purpose: add axioms corresponding to the StringBuilder.insert(String) java
-          function
+ Purpose: add axioms corresponding to the
+          StringBuilder.insert(int, CharSequence)
+          and StringBuilder.insert(int, CharSequence, int, int)
+          java functions
 
 \*******************************************************************/
 
 string_exprt string_constraint_generatort::add_axioms_for_insert(
   const function_application_exprt &f)
 {
-  string_exprt s1=get_string_expr(args(f, 3)[0]);
-  string_exprt s2=get_string_expr(args(f, 3)[2]);
-  return add_axioms_for_insert(s1, s2, args(f, 3)[1]);
+  assert(f.arguments().size()>=3);
+  string_exprt s1=get_string_expr(f.arguments()[0]);
+  string_exprt s2=get_string_expr(f.arguments()[2]);
+  const exprt &offset=f.arguments()[1];
+  if(f.arguments().size()==5)
+  {
+    const exprt &start=f.arguments()[3];
+    const exprt &end=f.arguments()[4];
+    string_exprt substring=add_axioms_for_substring(s2, start, end);
+    return add_axioms_for_insert(s1, substring, offset);
+  }
+  else
+  {
+    assert(f.arguments().size()==3);
+    return add_axioms_for_insert(s1, s2, offset);
+  }
 }
 
 /*******************************************************************\

From de60c68678fd24ef746b30c98c91bd44e13bf8b9 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 24 Mar 2017 14:55:14 +0000
Subject: [PATCH 08/17] Fixed linting issue in
 string_constraint_generator_concat.cpp

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

diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp
index eb841cc5b04..e6f360585bb 100644
--- a/src/solvers/refinement/string_constraint_generator_concat.cpp
+++ b/src/solvers/refinement/string_constraint_generator_concat.cpp
@@ -35,7 +35,8 @@ string_exprt string_constraint_generatort::add_axioms_for_concat(
   // a4 : forall i<|s1|. res[i]=s1[i]
   // a5 : forall i<|s2|. res[i+|s1|]=s2[i]
 
-  equal_exprt a1(res.length(), plus_exprt_with_overflow_check(s1.length(), s2.length()));
+  equal_exprt a1(
+    res.length(), plus_exprt_with_overflow_check(s1.length(), s2.length()));
   axioms.push_back(a1);
   axioms.push_back(s1.axiom_for_is_shorter_than(res));
   axioms.push_back(s2.axiom_for_is_shorter_than(res));

From 48a92f658551503dea544864f862f9835d622424 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 24 Mar 2017 16:11:03 +0000
Subject: [PATCH 09/17] Comment on the maximal length for string

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

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index ebcbf0f6ad5..93f96b1b80e 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -53,7 +53,9 @@ Function: string_refinementt::set_max_string_length
 
   Inputs:
     i - maximum length which is allowed for strings.
-        negative number means no limit
+        negative number means the strings length has no other limit
+        than the maximal integer according to the type of their
+        length, for instance 2^31-1 for Java.
 
  Purpose: Add constraints on the size of strings used in the
           program.

From 4b321b65b13722a034996248d738a5ffab309079 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 24 Mar 2017 16:15:44 +0000
Subject: [PATCH 10/17] Using max_string_length as the limit for refinement

---
 src/solvers/refinement/string_refinement.cpp | 6 +++---
 src/solvers/refinement/string_refinement.h   | 5 -----
 2 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 93f96b1b80e..6401666c792 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -348,8 +348,8 @@ void string_refinementt::concretize_string(const exprt &expr)
       else
       {
         size_t concretize_limit=found_length.to_long();
-        concretize_limit=concretize_limit>MAX_CONCRETE_STRING_SIZE?
-              MAX_CONCRETE_STRING_SIZE:concretize_limit;
+        concretize_limit=concretize_limit>generator.max_string_length?
+              generator.max_string_length:concretize_limit;
         exprt content_expr=str.content();
         for(size_t i=0; i<concretize_limit; ++i)
         {
@@ -722,7 +722,7 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const
   array_typet ret_type(char_type, from_integer(n, index_type));
   array_exprt ret(ret_type);
 
-  if(n>MAX_CONCRETE_STRING_SIZE)
+  if(n>generator.max_string_length)
   {
 #if 0
     debug() << "(sr::get_array) long string (size=" << n << ")" << eom;
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 0163936b069..745a3b53115 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -18,11 +18,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <solvers/refinement/string_constraint.h>
 #include <solvers/refinement/string_constraint_generator.h>
 
-// Defines a limit on the string witnesses we will output.
-// Longer strings are still concidered possible by the solver but
-// it will not output them.
-#define MAX_CONCRETE_STRING_SIZE 500
-
 #define MAX_NB_REFINEMENT 100
 
 class string_refinementt: public bv_refinementt

From 20450ec65a0f49a61af7160f7b3a82ba38a66700 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 24 Mar 2017 16:26:46 +0000
Subject: [PATCH 11/17] Using unsigned type for max string length

---
 src/solvers/refinement/string_constraint_generator.h | 5 +++--
 src/solvers/refinement/string_refinement.cpp         | 4 ++--
 src/solvers/refinement/string_refinement.h           | 2 +-
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index a69f2c39ae6..f87655448b9 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -13,6 +13,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
 
+#include <limits>
 #include <util/string_expr.h>
 #include <util/replace_expr.h>
 #include <util/refined_string_type.h>
@@ -26,12 +27,12 @@ class string_constraint_generatort
   // to the axiom list.
 
   string_constraint_generatort():
-    max_string_length(-1),
+    max_string_length(std::numeric_limits<unsigned int>::max()),
     force_printable_characters(false)
   { }
 
   // Constraints on the maximal length of strings
-  int max_string_length;
+  unsigned int max_string_length;
 
   // Should we add constraints on the characters
   bool force_printable_characters;
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 6401666c792..1079896796c 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -53,7 +53,7 @@ Function: string_refinementt::set_max_string_length
 
   Inputs:
     i - maximum length which is allowed for strings.
-        negative number means the strings length has no other limit
+        by default the strings length has no other limit
         than the maximal integer according to the type of their
         length, for instance 2^31-1 for Java.
 
@@ -62,7 +62,7 @@ Function: string_refinementt::set_max_string_length
 
 \*******************************************************************/
 
-void string_refinementt::set_max_string_length(int i)
+void string_refinementt::set_max_string_length(unsigned int i)
 {
   generator.max_string_length=i;
 }
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 745a3b53115..4d5caf3dd44 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -36,7 +36,7 @@ class string_refinementt: public bv_refinementt
   // Should we concretize strings when the solver finished
   bool do_concretizing;
 
-  void set_max_string_length(int i);
+  void set_max_string_length(unsigned int i);
   void enforce_non_empty_string();
   void enforce_printable_characters();
 

From a2077878955f7de9bc86b6bc05fe045bee57517f Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 24 Mar 2017 16:29:49 +0000
Subject: [PATCH 12/17] Using const ref in substitute_array_with_expr

---
 src/solvers/refinement/string_refinement.cpp | 8 ++++----
 src/solvers/refinement/string_refinement.h   | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 1079896796c..c54a48a2af3 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -946,13 +946,13 @@ Function: string_refinementt::substitute_array_with_expr()
 
 \*******************************************************************/
 
-exprt string_refinementt::substitute_array_with_expr
-  (exprt &expr, exprt &index) const
+exprt string_refinementt::substitute_array_with_expr(
+  const exprt &expr, const exprt &index) const
 {
   if(expr.id()==ID_with)
   {
-    with_exprt &with_expr=to_with_expr(expr);
-    exprt then_expr=with_expr.new_value();
+    const with_exprt &with_expr=to_with_expr(expr);
+    const exprt &then_expr=with_expr.new_value();
     exprt else_expr=substitute_array_with_expr(with_expr.old(), index);
     const typet &type=then_expr.type();
     assert(else_expr.type()==type);
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 4d5caf3dd44..80b5f7c5ed3 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -101,7 +101,7 @@ class string_refinementt: public bv_refinementt
   exprt substitute_function_applications(exprt expr);
   typet substitute_java_string_types(typet type);
   exprt substitute_java_strings(exprt expr);
-  exprt substitute_array_with_expr(exprt &expr, exprt &index) const;
+  exprt substitute_array_with_expr(const exprt &expr, const exprt &index) const;
   exprt substitute_array_access(exprt &expr) const;
   void add_symbol_to_symbol_map(const exprt &lhs, const exprt &rhs);
   bool is_char_array(const typet &type) const;

From 96cb157e9eec8c49a7cad38842e42a8938021325 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 24 Mar 2017 16:41:09 +0000
Subject: [PATCH 13/17] making substitute_array_access do in-place substitution

---
 src/solvers/refinement/string_refinement.cpp | 28 +++++++++-----------
 src/solvers/refinement/string_refinement.h   |  2 +-
 2 files changed, 14 insertions(+), 16 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index c54a48a2af3..284c3e696e8 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -985,14 +985,10 @@ Function: string_refinementt::substitute_array_access()
 
 \*******************************************************************/
 
-exprt string_refinementt::substitute_array_access(exprt &expr) const
+void string_refinementt::substitute_array_access(exprt &expr) const
 {
-  for(size_t i=0; i<expr.operands().size(); ++i)
-  {
-    // TODO: only copy when necessary
-    exprt op(expr.operands()[i]);
-    expr.operands()[i]=substitute_array_access(op);
-  }
+  for(auto &op : expr.operands())
+    substitute_array_access(op);
 
   if(expr.id()==ID_index)
   {
@@ -1000,19 +996,21 @@ exprt string_refinementt::substitute_array_access(exprt &expr) const
 
     if(index_expr.array().id()==ID_symbol)
     {
-      return index_expr;
+      expr=index_expr;
+      return;
     }
 
     if(index_expr.array().id()==ID_with)
     {
-      exprt subst=substitute_array_with_expr(index_expr.array(),
-                                             index_expr.index());
-      return subst;
+      expr=substitute_array_with_expr(
+        index_expr.array(), index_expr.index());
+      return;
     }
 
     if(index_expr.array().id()==ID_array_of)
     {
-      return to_array_of_expr(index_expr.array()).op();
+      expr=to_array_of_expr(index_expr.array()).op();
+      return;
     }
 
     assert(index_expr.array().id()==ID_array);
@@ -1042,9 +1040,8 @@ exprt string_refinementt::substitute_array_access(exprt &expr) const
       equal_exprt equals(index_expr.index(), from_integer(i, java_int_type()));
       ite=if_exprt(equals, op, ite, char_type);
     }
-    return ite;
+    expr=ite;
   }
-  return expr;
 }
 
 /*******************************************************************\
@@ -1091,7 +1088,8 @@ void string_refinementt::add_negation_of_constraint_to_solver(
   and_exprt negaxiom(premise, not_exprt(axiom.body()));
 
   debug() << "(sr::check_axioms) negated axiom: " << from_expr(negaxiom) << eom;
-  solver << substitute_array_access(negaxiom);
+  substitute_array_access(negaxiom);
+  solver << negaxiom;
 }
 
 /*******************************************************************\
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 80b5f7c5ed3..cc3f530039e 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -102,7 +102,7 @@ class string_refinementt: public bv_refinementt
   typet substitute_java_string_types(typet type);
   exprt substitute_java_strings(exprt expr);
   exprt substitute_array_with_expr(const exprt &expr, const exprt &index) const;
-  exprt substitute_array_access(exprt &expr) const;
+  void substitute_array_access(exprt &expr) const;
   void add_symbol_to_symbol_map(const exprt &lhs, const exprt &rhs);
   bool is_char_array(const typet &type) const;
   bool add_axioms_for_string_assigns(const exprt &lhs, const exprt &rhs);

From 920695a9b4ae71822d195437a5f30ef899d5463c Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 24 Mar 2017 16:26:46 +0000
Subject: [PATCH 14/17] Correcting type of max_string_length and length
 comparison functions

---
 src/solvers/refinement/string_constraint_generator.h        | 6 +++---
 src/solvers/refinement/string_constraint_generator_main.cpp | 2 +-
 src/solvers/refinement/string_refinement.cpp                | 4 ++--
 src/solvers/refinement/string_refinement.h                  | 2 +-
 src/util/string_expr.h                                      | 6 +++---
 5 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index f87655448b9..2c5216ddd6c 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -23,16 +23,16 @@ class string_constraint_generatort
 {
 public:
   // This module keeps a list of axioms. It has methods which generate
-  // string constraints for different string funcitons and add them
+  // string constraints for different string functions and add them
   // to the axiom list.
 
   string_constraint_generatort():
-    max_string_length(std::numeric_limits<unsigned int>::max()),
+    max_string_length(std::numeric_limits<unsigned long>::max()),
     force_printable_characters(false)
   { }
 
   // Constraints on the maximal length of strings
-  unsigned int max_string_length;
+  unsigned long max_string_length;
 
   // Should we add constraints on the characters
   bool force_printable_characters;
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index ddc5ab7a3a3..9e09f5ef7f3 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -268,7 +268,7 @@ void string_constraint_generatort::add_default_axioms(
   const string_exprt &s)
 {
   s.axiom_for_is_longer_than(from_integer(0, s.length().type()));
-  if(max_string_length>=0)
+  if(max_string_length!=std::numeric_limits<unsigned long>::max())
     axioms.push_back(s.axiom_for_is_shorter_than(max_string_length));
 
   if(force_printable_characters)
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 284c3e696e8..88a98fcaebc 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -347,11 +347,11 @@ void string_refinementt::concretize_string(const exprt &expr)
       }
       else
       {
-        size_t concretize_limit=found_length.to_long();
+        unsigned long concretize_limit=found_length.to_long();
         concretize_limit=concretize_limit>generator.max_string_length?
               generator.max_string_length:concretize_limit;
         exprt content_expr=str.content();
-        for(size_t i=0; i<concretize_limit; ++i)
+        for(unsigned long i=0; i<concretize_limit; ++i)
         {
           auto i_expr=from_integer(i, str.length().type());
           debug() << "Concretizing " << from_expr(content_expr)
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index cc3f530039e..1a4bc3089c3 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -61,7 +61,7 @@ class string_refinementt: public bv_refinementt
   // Base class
   typedef bv_refinementt supert;
 
-  unsigned initial_loop_bound;
+  unsigned long initial_loop_bound;
 
   string_constraint_generatort generator;
 
diff --git a/src/util/string_expr.h b/src/util/string_expr.h
index 317e3c1ee6e..ff19a8c8259 100644
--- a/src/util/string_expr.h
+++ b/src/util/string_expr.h
@@ -74,7 +74,7 @@ class string_exprt: public struct_exprt
     return binary_relation_exprt(rhs.length(), ID_lt, length());
   }
 
-  binary_relation_exprt axiom_for_is_strictly_longer_than(int i) const
+  binary_relation_exprt axiom_for_is_strictly_longer_than(mp_integer i) const
   {
     return axiom_for_is_strictly_longer_than(from_integer(i, length().type()));
   }
@@ -91,7 +91,7 @@ class string_exprt: public struct_exprt
     return binary_relation_exprt(length(), ID_le, rhs);
   }
 
-  binary_relation_exprt axiom_for_is_shorter_than(int i) const
+  binary_relation_exprt axiom_for_is_shorter_than(mp_integer i) const
   {
     return axiom_for_is_shorter_than(from_integer(i, length().type()));
   }
@@ -119,7 +119,7 @@ class string_exprt: public struct_exprt
     return equal_exprt(length(), rhs);
   }
 
-  equal_exprt axiom_for_has_length(int i) const
+  equal_exprt axiom_for_has_length(mp_integer i) const
   {
     return axiom_for_has_length(from_integer(i, length().type()));
   }

From 6a6858a03d0ba1e7a72dc405617c1ad5bae5e24e Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Sat, 25 Mar 2017 19:03:58 +0000
Subject: [PATCH 15/17] space before & sign instead of after

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

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 88a98fcaebc..e792537cb8d 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -376,9 +376,9 @@ Function: string_refinementt::concretize_results
 
 void string_refinementt::concretize_results()
 {
-  for(const auto& it : symbol_resolve)
+  for(const auto &it : symbol_resolve)
     concretize_string(it.second);
-  for(const auto& it : generator.created_strings)
+  for(const auto &it : generator.created_strings)
     concretize_string(it);
   add_instantiations();
 }
@@ -394,7 +394,7 @@ Function: string_refinementt::concretize_lengths
 
 void string_refinementt::concretize_lengths()
 {
-  for(const auto& it : symbol_resolve)
+  for(const auto &it : symbol_resolve)
   {
     if(refined_string_typet::is_refined_string_type(it.second.type()))
     {
@@ -405,7 +405,7 @@ void string_refinementt::concretize_lengths()
       found_length[content]=length;
      }
   }
-  for(const auto& it : generator.created_strings)
+  for(const auto &it : generator.created_strings)
   {
     if(refined_string_typet::is_refined_string_type(it.type()))
     {

From cb2fb78f5aa0d3d12532d29c86289f0387e3d133 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 29 Mar 2017 09:51:07 +0100
Subject: [PATCH 16/17] Putting each cbmc option on a  separate line for easy
 merging

---
 src/cbmc/cbmc_parse_options.h | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 4bdc07a6278..2c54dfc7353 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -38,7 +38,10 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(no-pretty-names)(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
-  "(refine-strings)(string-non-empty)(string-printable)(string-max-length):" \
+  "(refine-strings)" \
+  "(string-non-empty)" \
+  "(string-printable)" \
+  "(string-max-length):" \
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-loops)" \

From 6898cca08954a3c49c7a56f1f1c525f561b15e6d Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 29 Mar 2017 09:54:06 +0100
Subject: [PATCH 17/17] Correcting initial_loop_bound type

---
 src/solvers/refinement/string_refinement.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 1a4bc3089c3..cc3f530039e 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -61,7 +61,7 @@ class string_refinementt: public bv_refinementt
   // Base class
   typedef bv_refinementt supert;
 
-  unsigned long initial_loop_bound;
+  unsigned initial_loop_bound;
 
   string_constraint_generatort generator;