From f99c8ff1d2306b8944a6dd10eff2ea6be4a5aeaf Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 12 Sep 2017 17:14:54 +0100
Subject: [PATCH 01/28] Replace exceptions with optional

---
 src/solvers/refinement/string_refinement.cpp | 38 ++++++++++++--------
 1 file changed, 24 insertions(+), 14 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 608b70212aa..8f403ea0897 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -33,6 +33,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <solvers/refinement/string_constraint_instantiation.h>
 #include <langapi/language_util.h>
 #include <java_bytecode/java_types.h>
+#include <util/optional.h>
 
 static bool validate(const string_refinementt::infot &info)
 {
@@ -300,19 +301,26 @@ bool string_refinementt::add_axioms_for_string_assigns(
 /// Generic case doesn't exist, specialize for different types accordingly
 /// TODO: this should go to util
 template<typename T>
-T expr_cast(const exprt&);
+optionalt<T> expr_cast(const exprt&);
 
 template<>
-std::size_t expr_cast<std::size_t>(const exprt& val_expr)
+optionalt<mp_integer> expr_cast<mp_integer>(const exprt& expr)
 {
-  mp_integer val_mb;
-  if(to_integer(val_expr, val_mb))
-    throw std::bad_cast();
-  if(!val_mb.is_long())
-    throw std::bad_cast();
-  if(val_mb<0)
-    throw std::bad_cast();
-  return val_mb.to_long();
+  mp_integer out;
+  if(to_integer(expr, out))
+    return { };
+  return out;
+}
+
+template<>
+optionalt<std::size_t> expr_cast<std::size_t>(const exprt& expr)
+{
+  if (const auto tmp=expr_cast<mp_integer>(expr))
+  {
+    if(tmp->is_long() && *tmp >= 0)
+      return tmp->to_long();
+  }
+  return { };
 }
 
 /// If the expression is of type string, then adds constants to the index set to
@@ -336,8 +344,9 @@ void string_refinementt::concretize_string(const exprt &expr)
     replace_expr(symbol_resolve, content);
     found_length[content]=length;
     const auto string_length=expr_cast<std::size_t>(length);
+    INVARIANT(string_length, "Bad integer conversion");
     INVARIANT(
-      string_length<=generator.max_string_length,
+      *string_length<=generator.max_string_length,
       string_refinement_invariantt("string length must be less than the max "
         "length"));
     if(index_set[str.content()].empty())
@@ -350,7 +359,7 @@ void string_refinementt::concretize_string(const exprt &expr)
       const exprt simple_i=simplify_expr(get(i), ns);
       mp_integer mpi_index;
       bool conversion_failure=to_integer(simple_i, mpi_index);
-      if(!conversion_failure && mpi_index>=0 && mpi_index<string_length)
+      if(!conversion_failure && mpi_index>=0 && mpi_index<*string_length)
       {
         const exprt str_i=simplify_expr(str[simple_i], ns);
         const exprt value=simplify_expr(get(str_i), ns);
@@ -896,8 +905,9 @@ exprt fill_in_array_with_expr(const exprt &expr, std::size_t string_max_length)
     const with_exprt with_expr=to_with_expr(it);
     const exprt &then_expr=with_expr.new_value();
     const auto index=expr_cast<std::size_t>(with_expr.where());
-    if(index<string_max_length)
-      initial_map.emplace(index, then_expr);
+    INVARIANT(index, "Bad integer conversion");
+    if(*index<string_max_length)
+      initial_map.emplace(*index, then_expr);
   }
 
   array_exprt result(to_array_type(expr.type()));

From c5fa708fcb7d7ce26886ef869e289d38d3117dd8 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 12 Sep 2017 17:42:57 +0100
Subject: [PATCH 02/28] Refactor integer conversions

---
 src/solvers/refinement/string_refinement.cpp | 135 +++++++++----------
 1 file changed, 62 insertions(+), 73 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 8f403ea0897..e3c9c23c627 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -35,6 +35,40 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <java_bytecode/java_types.h>
 #include <util/optional.h>
 
+/// Convert exprt to a specific type. Throw bad_cast if conversion
+/// cannot be performed
+/// Generic case doesn't exist, specialize for different types accordingly
+/// TODO: this should go to util
+template<typename T>
+optionalt<T> expr_cast(const exprt&);
+
+template<>
+optionalt<mp_integer> expr_cast<mp_integer>(const exprt& expr)
+{
+  mp_integer out;
+  if(to_integer(expr, out))
+    return { };
+  return out;
+}
+
+template<>
+optionalt<std::size_t> expr_cast<std::size_t>(const exprt& expr)
+{
+  if (const auto tmp=expr_cast<mp_integer>(expr))
+  {
+    if(tmp->is_long() && *tmp >= 0)
+      return tmp->to_long();
+  }
+  return { };
+}
+
+template<typename T>
+T expr_cast_v(const exprt& expr) {
+  const auto maybe=expr_cast<T>(expr);
+  INVARIANT(maybe, "Bad conversion");
+  return *maybe;
+}
+
 static bool validate(const string_refinementt::infot &info)
 {
   PRECONDITION(info.ns);
@@ -296,33 +330,6 @@ bool string_refinementt::add_axioms_for_string_assigns(
   return true;
 }
 
-/// Convert exprt to a specific type. Throw bad_cast if conversion
-/// cannot be performed
-/// Generic case doesn't exist, specialize for different types accordingly
-/// TODO: this should go to util
-template<typename T>
-optionalt<T> expr_cast(const exprt&);
-
-template<>
-optionalt<mp_integer> expr_cast<mp_integer>(const exprt& expr)
-{
-  mp_integer out;
-  if(to_integer(expr, out))
-    return { };
-  return out;
-}
-
-template<>
-optionalt<std::size_t> expr_cast<std::size_t>(const exprt& expr)
-{
-  if (const auto tmp=expr_cast<mp_integer>(expr))
-  {
-    if(tmp->is_long() && *tmp >= 0)
-      return tmp->to_long();
-  }
-  return { };
-}
-
 /// If the expression is of type string, then adds constants to the index set to
 /// force the solver to pick concrete values for each character, and fill the
 /// maps `found_length` and `found_content`.
@@ -343,10 +350,9 @@ void string_refinementt::concretize_string(const exprt &expr)
     exprt content=str.content();
     replace_expr(symbol_resolve, content);
     found_length[content]=length;
-    const auto string_length=expr_cast<std::size_t>(length);
-    INVARIANT(string_length, "Bad integer conversion");
+    const auto string_length=expr_cast_v<std::size_t>(length);
     INVARIANT(
-      *string_length<=generator.max_string_length,
+      string_length<=generator.max_string_length,
       string_refinement_invariantt("string length must be less than the max "
         "length"));
     if(index_set[str.content()].empty())
@@ -357,14 +363,11 @@ void string_refinementt::concretize_string(const exprt &expr)
     for(const auto &i : index_set[str.content()])
     {
       const exprt simple_i=simplify_expr(get(i), ns);
-      mp_integer mpi_index;
-      bool conversion_failure=to_integer(simple_i, mpi_index);
-      if(!conversion_failure && mpi_index>=0 && mpi_index<*string_length)
+      if(const auto index=expr_cast<std::size_t>(simple_i))
       {
         const exprt str_i=simplify_expr(str[simple_i], ns);
         const exprt value=simplify_expr(get(str_i), ns);
-        std::size_t index=mpi_index.to_long();
-        map.emplace(index, value);
+        map.emplace(*index, value);
       }
       else
       {
@@ -904,10 +907,9 @@ exprt fill_in_array_with_expr(const exprt &expr, std::size_t string_max_length)
     // statements
     const with_exprt with_expr=to_with_expr(it);
     const exprt &then_expr=with_expr.new_value();
-    const auto index=expr_cast<std::size_t>(with_expr.where());
-    INVARIANT(index, "Bad integer conversion");
-    if(*index<string_max_length)
-      initial_map.emplace(*index, then_expr);
+    const auto index=expr_cast_v<std::size_t>(with_expr.where());
+    if(index<string_max_length)
+      initial_map.emplace(index, then_expr);
   }
 
   array_exprt result(to_array_type(expr.type()));
@@ -1026,23 +1028,18 @@ static exprt negation_of_not_contains_constraint(
   const symbol_exprt &univ_var)
 {
   // If the for all is vacuously true, the negation is false.
-  exprt lbu=axiom.univ_lower_bound();
-  exprt ubu=axiom.univ_upper_bound();
+  const exprt lbu=axiom.univ_lower_bound();
+  const exprt ubu=axiom.univ_upper_bound();
   if(lbu.id()==ID_constant && ubu.id()==ID_constant)
   {
-    mp_integer lb_int, ub_int;
-    to_integer(to_constant_expr(lbu), lb_int);
-    to_integer(to_constant_expr(ubu), ub_int);
-    if(ub_int<=lb_int)
+    const auto lb_int=expr_cast<mp_integer>(lbu);
+    const auto ub_int=expr_cast<mp_integer>(ubu);
+    if(!lb_int || !ub_int || *ub_int<=*lb_int)
       return false_exprt();
   }
 
-  exprt lbe=axiom.exists_lower_bound();
-  exprt ube=axiom.exists_upper_bound();
-
-  mp_integer lbe_int, ube_int;
-  to_integer(to_constant_expr(lbe), lbe_int);
-  to_integer(to_constant_expr(ube), ube_int);
+  const auto lbe=expr_cast_v<mp_integer>(axiom.exists_lower_bound());
+  const auto ube=expr_cast_v<mp_integer>(axiom.exists_upper_bound());
 
   // If the premise is false, the implication is trivially true, so the
   // negation is false.
@@ -1056,7 +1053,7 @@ static exprt negation_of_not_contains_constraint(
   // The negated existential becomes an universal, and this is the unrolling of
   // that universal quantifier.
   std::vector<exprt> conjuncts;
-  for(mp_integer i=lbe_int; i<ube_int; ++i)
+  for(mp_integer i=lbe; i<ube; ++i)
   {
     const constant_exprt i_exprt=from_integer(i, univ_var.type());
     const equal_exprt equal_chars(
@@ -1085,10 +1082,9 @@ static exprt negation_of_constraint(const string_constraintt &axiom)
   exprt ub=axiom.upper_bound();
   if(lb.id()==ID_constant && ub.id()==ID_constant)
   {
-    mp_integer lb_int, ub_int;
-    to_integer(to_constant_expr(lb), lb_int);
-    to_integer(to_constant_expr(ub), ub_int);
-    if(ub_int<=lb_int)
+    const auto lb_int=expr_cast<mp_integer>(lb);
+    const auto ub_int=expr_cast<mp_integer>(ub);
+    if(!lb_int || !ub_int || ub_int<=lb_int)
       return false_exprt();
   }
 
@@ -1512,18 +1508,12 @@ static std::vector<exprt> sub_arrays(const exprt &array_expr)
 void string_refinementt::add_to_index_set(const exprt &s, exprt i)
 {
   simplify(i, ns);
-  if(i.id()==ID_constant)
+  if(i.id()!=ID_constant || expr_cast<size_t>(i))
   {
-    mp_integer mpi;
-    to_integer(i, mpi);
-    if(mpi<0)
-      return;
+    for(const auto &sub : sub_arrays(s))
+      if(index_set[sub].insert(i).second)
+        current_index_set[sub].insert(i);
   }
-
-  std::vector<exprt> subs=sub_arrays(s);
-  for(const auto &sub : subs)
-    if(index_set[sub].insert(i).second)
-      current_index_set[sub].insert(i);
 }
 
 void string_refinementt::initial_index_set(const string_constraintt &axiom)
@@ -1707,14 +1697,13 @@ exprt substitute_array_lists(exprt expr, size_t string_max_length)
     array_typet arr_type(char_type, infinity_exprt(char_type));
     exprt ret_expr=array_of_exprt(from_integer(0, char_type), arr_type);
 
-    for(size_t i=0; i<expr.operands().size()/2; i++)
+    for(size_t i=0; i<expr.operands().size(); i+=2)
     {
-      const exprt &index=expr.operands()[i*2];
-      const exprt &value=expr.operands()[i*2+1];
-      mp_integer index_value;
-      bool not_constant=to_integer(index, index_value);
-      if(not_constant ||
-         (index_value>=0 && index_value<string_max_length))
+      const exprt &index=expr.operands()[i];
+      const exprt &value=expr.operands()[i+1];
+      const auto index_value=expr_cast<std::size_t>(index);
+      if(!index.is_constant() ||
+         (index_value && *index_value<string_max_length))
         ret_expr=with_exprt(ret_expr, index, value);
     }
     return ret_expr;

From bf47f81c2540e20741433e48dd38e65dcda72cee Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 12 Sep 2017 18:21:55 +0100
Subject: [PATCH 03/28] Use expr_cast in string_exprt casts

---
 src/solvers/refinement/string_refinement.cpp | 76 +++++++++++---------
 1 file changed, 42 insertions(+), 34 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index e3c9c23c627..4868cba2d94 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -54,7 +54,7 @@ optionalt<mp_integer> expr_cast<mp_integer>(const exprt& expr)
 template<>
 optionalt<std::size_t> expr_cast<std::size_t>(const exprt& expr)
 {
-  if (const auto tmp=expr_cast<mp_integer>(expr))
+  if(const auto tmp=expr_cast<mp_integer>(expr))
   {
     if(tmp->is_long() && *tmp >= 0)
       return tmp->to_long();
@@ -62,6 +62,16 @@ optionalt<std::size_t> expr_cast<std::size_t>(const exprt& expr)
   return { };
 }
 
+template<>
+optionalt<string_exprt> expr_cast<string_exprt>(const exprt& expr)
+{
+  if(is_refined_string_type(expr.type()))
+  {
+    return to_string_expr(expr);
+  }
+  return { };
+}
+
 template<typename T>
 T expr_cast_v(const exprt& expr) {
   const auto maybe=expr_cast<T>(expr);
@@ -343,11 +353,10 @@ bool string_refinementt::add_axioms_for_string_assigns(
 /// last value that has been initialized.
 void string_refinementt::concretize_string(const exprt &expr)
 {
-  if(is_refined_string_type(expr.type()))
+  if(const auto str=expr_cast<string_exprt>(expr))
   {
-    const string_exprt str=to_string_expr(expr);
-    const exprt length=get(str.length());
-    exprt content=str.content();
+    const exprt length=get(str->length());
+    exprt content=str->content();
     replace_expr(symbol_resolve, content);
     found_length[content]=length;
     const auto string_length=expr_cast_v<std::size_t>(length);
@@ -355,17 +364,17 @@ void string_refinementt::concretize_string(const exprt &expr)
       string_length<=generator.max_string_length,
       string_refinement_invariantt("string length must be less than the max "
         "length"));
-    if(index_set[str.content()].empty())
+    if(index_set[str->content()].empty())
       return;
 
     std::map<std::size_t, exprt> map;
 
-    for(const auto &i : index_set[str.content()])
+    for(const auto &i : index_set[str->content()])
     {
       const exprt simple_i=simplify_expr(get(i), ns);
       if(const auto index=expr_cast<std::size_t>(simple_i))
       {
-        const exprt str_i=simplify_expr(str[simple_i], ns);
+        const exprt str_i=simplify_expr((*str)[simple_i], ns);
         const exprt value=simplify_expr(get(str_i), ns);
         map.emplace(*index, value);
       }
@@ -377,7 +386,7 @@ void string_refinementt::concretize_string(const exprt &expr)
     }
     array_exprt arr(to_array_type(content.type()));
     arr.operands()=fill_in_map_as_vector(map);
-    debug() << "Concretized " << from_expr(ns, "", str.content())
+    debug() << "Concretized " << from_expr(ns, "", str->content())
             << " = " << from_expr(ns, "", arr) << eom;
     found_content[content]=arr;
   }
@@ -399,24 +408,22 @@ void string_refinementt::concretize_results()
 /// `found_length`
 void string_refinementt::concretize_lengths()
 {
-  for(const auto &it : symbol_resolve)
+  for(const auto &pair : symbol_resolve)
   {
-    if(is_refined_string_type(it.second.type()))
+    if(const auto str=expr_cast<string_exprt>(pair.second))
     {
-      string_exprt str=to_string_expr(it.second);
-      exprt length=get(str.length());
-      exprt content=str.content();
+      exprt length=get(str->length());
+      exprt content=str->content();
       replace_expr(symbol_resolve, content);
       found_length[content]=length;
      }
   }
   for(const auto &it : generator.get_created_strings())
   {
-    if(is_refined_string_type(it.type()))
+    if(const auto str=expr_cast<string_exprt>(it))
     {
-      string_exprt str=to_string_expr(it);
-      exprt length=get(str.length());
-      exprt content=str.content();
+      exprt length=get(str->length());
+      exprt content=str->content();
       replace_expr(symbol_resolve, content);
       found_length[content]=length;
      }
@@ -794,20 +801,19 @@ void string_refinementt::debug_model()
   const std::string indent("  ");
   for(auto it : symbol_resolve)
   {
-    if(is_refined_string_type(it.second.type()))
+    if(const auto refined=expr_cast<string_exprt>(it.second))
     {
       debug() << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n";
-      string_exprt refined=to_string_expr(it.second);
       debug() << indent << indent << "in_map: "
-              << from_expr(ns, "", refined) << eom;
+              << from_expr(ns, "", *refined) << eom;
       debug() << indent << indent << "resolved: "
-              << from_expr(ns, "", refined) << eom;
-      const exprt &econtent=refined.content();
-      const exprt &elength=refined.length();
+              << from_expr(ns, "", *refined) << eom;
+      const exprt &econtent=refined->content();
+      const exprt &elength=refined->length();
 
       exprt len=supert::get(elength);
       len=simplify_expr(len, ns);
-      exprt arr=get_array(econtent, len);
+      const exprt arr=get_array(econtent, len);
       if(arr.id()==ID_array)
         debug() << indent << indent << "as_string: \""
                 << string_of_array(to_array_expr(arr)) << "\"\n";
@@ -1680,11 +1686,11 @@ std::vector<exprt> string_refinementt::instantiate_not_contains(
 /// \return an expression containing no array-list
 exprt substitute_array_lists(exprt expr, size_t string_max_length)
 {
-  for(size_t i=0; i<expr.operands().size(); ++i)
+  for(auto& operand : expr.operands())
   {
     // TODO: only copy when necessary
-    exprt op=(expr.operands()[i]);
-    expr.operands()[i]=substitute_array_lists(op, string_max_length);
+    const exprt op(operand);
+    operand=substitute_array_lists(op, string_max_length);
   }
 
   if(expr.id()=="array-list")
@@ -1729,14 +1735,16 @@ exprt string_refinementt::get(const exprt &expr) const
     if(it!=found_length.end())
       return get_array(ecopy, it->second);
   }
-  else if(is_refined_string_type(ecopy.type()) && ecopy.id()==ID_struct)
+  else if(ecopy.id()==ID_struct)
   {
-    const string_exprt &string=to_string_expr(ecopy);
-    const exprt &content=string.content();
-    const exprt &length=string.length();
+    if (const auto string=expr_cast<string_exprt>(ecopy))
+    {
+      const exprt &content=string->content();
+      const exprt &length=string->length();
 
-    const exprt arr=get_array(content, length);
-    ecopy=string_exprt(length, arr, string.type());
+      const exprt arr=get_array(content, length);
+      ecopy=string_exprt(length, arr, string->type());
+    }
   }
 
   ecopy=supert::get(ecopy);

From 317c1c6c79a2cc397d45c5a1df4e94018cbe7b6e Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 12 Sep 2017 18:39:01 +0100
Subject: [PATCH 04/28] Group bv_refinement config variables

---
 src/solvers/refinement/bv_refinement.h        | 20 +++++++++----------
 src/solvers/refinement/bv_refinement_loop.cpp |  7 ++-----
 src/solvers/refinement/refine_arithmetic.cpp  | 10 +++++-----
 src/solvers/refinement/refine_arrays.cpp      |  4 ++--
 src/solvers/refinement/string_refinement.cpp  | 17 ++--------------
 src/solvers/refinement/string_refinement.h    | 15 +++++---------
 6 files changed, 25 insertions(+), 48 deletions(-)

diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h
index 79367186b9b..0c2b5e22b3a 100644
--- a/src/solvers/refinement/bv_refinement.h
+++ b/src/solvers/refinement/bv_refinement.h
@@ -20,11 +20,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class bv_refinementt:public bv_pointerst
 {
-public:
-  struct infot
+private:
+  struct configt
   {
-    const namespacet *ns=nullptr;
-    propt *prop=nullptr;
     ui_message_handlert::uit ui=ui_message_handlert::uit::PLAIN;
     /// Max number of times we refine a formula node
     unsigned max_node_refinement=5;
@@ -33,6 +31,12 @@ class bv_refinementt:public bv_pointerst
     /// Enable arithmetic refinement
     bool refine_arithmetic=true;
   };
+public:
+  struct infot : public configt
+  {
+    const namespacet *ns=nullptr;
+    propt *prop=nullptr;
+  };
 
   explicit bv_refinementt(const infot &info);
 
@@ -103,18 +107,12 @@ class bv_refinementt:public bv_pointerst
 
   // MEMBERS
 
-  // Maximum number of times we refine a formula node
-  const unsigned max_node_refinement;
-  // Refinement toggles
-  const bool do_array_refinement;
-  const bool do_arithmetic_refinement;
   bool progress;
   std::vector<approximationt> approximations;
   bvt parent_assumptions;
-
 protected:
   // use gui format
-  ui_message_handlert::uit ui;
+  configt config_;
 };
 
 #endif // CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp
index e3ac990b3a4..8b7f373a49c 100644
--- a/src/solvers/refinement/bv_refinement_loop.cpp
+++ b/src/solvers/refinement/bv_refinement_loop.cpp
@@ -14,11 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bv_refinementt::bv_refinementt(const infot &info):
   bv_pointerst(*info.ns, *info.prop),
-  max_node_refinement(info.max_node_refinement),
-  do_array_refinement(info.refine_arrays),
-  do_arithmetic_refinement(info.refine_arithmetic),
   progress(false),
-  ui(info.ui)
+  config_(info)
 {
   // check features we need
   PRECONDITION(prop.has_set_assumptions());
@@ -44,7 +41,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve()
     status() << "BV-Refinement: iteration " << iteration << eom;
 
     // output the very same information in a structured fashion
-    if(ui==ui_message_handlert::uit::XML_UI)
+    if(config_.ui==ui_message_handlert::uit::XML_UI)
     {
       xmlt xml("refinement-iteration");
       xml.data=std::to_string(iteration);
diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp
index 2a6627a34e3..561af397486 100644
--- a/src/solvers/refinement/refine_arithmetic.cpp
+++ b/src/solvers/refinement/refine_arithmetic.cpp
@@ -38,7 +38,7 @@ void bv_refinementt::approximationt::add_under_assumption(literalt l)
 
 bvt bv_refinementt::convert_floatbv_op(const exprt &expr)
 {
-  if(!do_arithmetic_refinement)
+  if(!config_.refine_arithmetic)
     return SUB::convert_floatbv_op(expr);
 
   if(ns.follow(expr.type()).id()!=ID_floatbv ||
@@ -52,7 +52,7 @@ bvt bv_refinementt::convert_floatbv_op(const exprt &expr)
 
 bvt bv_refinementt::convert_mult(const exprt &expr)
 {
-  if(!do_arithmetic_refinement || expr.type().id()==ID_fixedbv)
+  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
     return SUB::convert_mult(expr);
 
   // we catch any multiplication
@@ -100,7 +100,7 @@ bvt bv_refinementt::convert_mult(const exprt &expr)
 
 bvt bv_refinementt::convert_div(const div_exprt &expr)
 {
-  if(!do_arithmetic_refinement || expr.type().id()==ID_fixedbv)
+  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
     return SUB::convert_div(expr);
 
   // we catch any division
@@ -118,7 +118,7 @@ bvt bv_refinementt::convert_div(const div_exprt &expr)
 
 bvt bv_refinementt::convert_mod(const mod_exprt &expr)
 {
-  if(!do_arithmetic_refinement || expr.type().id()==ID_fixedbv)
+  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
     return SUB::convert_mod(expr);
 
   // we catch any mod
@@ -228,7 +228,7 @@ void bv_refinementt::check_SAT(approximationt &a)
 
     // if(a.over_state==1) { debug() << "DISAGREEMENT!\n"; exit(1); }
 
-    if(a.over_state<max_node_refinement)
+    if(a.over_state<config_.max_node_refinement)
     {
       bvt r;
       float_utilst float_utils(prop);
diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp
index 77ddacd6584..1fa74692e10 100644
--- a/src/solvers/refinement/refine_arrays.cpp
+++ b/src/solvers/refinement/refine_arrays.cpp
@@ -29,7 +29,7 @@ void bv_refinementt::post_process_arrays()
   update_index_map(true);
 
   // we don't actually add any constraints
-  lazy_arrays=do_array_refinement;
+  lazy_arrays=config_.refine_arrays;
   add_array_constraints();
   freeze_lazy_constraints();
 }
@@ -37,7 +37,7 @@ void bv_refinementt::post_process_arrays()
 /// check whether counterexample is spurious
 void bv_refinementt::arrays_overapproximated()
 {
-  if(!do_array_refinement)
+  if(!config_.refine_arrays)
     return;
 
   unsigned nb_active=0;
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 4868cba2d94..09064bb3629 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -86,19 +86,6 @@ static bool validate(const string_refinementt::infot &info)
   return true;
 }
 
-static bv_refinementt::infot bv_refinement_info(
-  const string_refinementt::infot &in)
-{
-  bv_refinementt::infot out;
-  out.ns=in.ns;
-  out.prop=in.prop;
-  out.ui=in.ui;
-  out.max_node_refinement=in.max_node_refinement;
-  out.refine_arrays=in.refine_arrays;
-  out.refine_arithmetic=in.refine_arithmetic;
-  return out;
-}
-
 static string_constraint_generatort::infot
 generator_info(const string_refinementt::infot &in)
 {
@@ -110,7 +97,7 @@ generator_info(const string_refinementt::infot &in)
 }
 
 string_refinementt::string_refinementt(const infot &info, bool):
-  supert(bv_refinement_info(info)),
+  supert(info),
   use_counter_example(false),
   do_concretizing(info.trace),
   initial_loop_bound(info.refinement_bound),
@@ -1770,7 +1757,7 @@ bool string_refinementt::is_axiom_sat(
   info.refine_arithmetic=true;
   info.refine_arrays=true;
   info.max_node_refinement=5;
-  info.ui=ui;
+  info.ui=config_.ui;
   supert solver(info);
   solver << axiom;
 
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 50d0fcfb129..2ee26ea02b1 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -31,13 +31,8 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 
 class string_refinementt final: public bv_refinementt
 {
-public:
-  /// string_refinementt constructor arguments
-  struct infot
-  {
-    const namespacet *ns=nullptr;
-    propt *prop=nullptr;
-    ui_message_handlert::uit ui=ui_message_handlert::uit::PLAIN;
+private:
+  struct configt {
     unsigned refinement_bound=0;
     size_t string_max_length=std::numeric_limits<size_t>::max();
     /// Make non-deterministic character arrays have at least one character
@@ -46,11 +41,11 @@ class string_refinementt final: public bv_refinementt
     bool trace=false;
     /// Make non-deterministic characters printable
     bool string_printable=false;
-    unsigned max_node_refinement=5;
-    bool refine_arrays=false;
-    bool refine_arithmetic=false;
     bool use_counter_example=false;
   };
+public:
+  /// string_refinementt constructor arguments
+  struct infot:public bv_refinementt::infot, public configt { };
 
   explicit string_refinementt(const infot &);
 

From 150bab1330ad0f36aac00c3a43ca9ed43e45a7d3 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 12 Sep 2017 18:45:53 +0100
Subject: [PATCH 05/28] Group string_refinement arguments

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

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 09064bb3629..d79710942c7 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -98,11 +98,9 @@ generator_info(const string_refinementt::infot &in)
 
 string_refinementt::string_refinementt(const infot &info, bool):
   supert(info),
-  use_counter_example(false),
-  do_concretizing(info.trace),
-  initial_loop_bound(info.refinement_bound),
-  generator(generator_info(info)),
-  non_empty_string(info.string_non_empty) { }
+  config_(info),
+  loop_bound_(info.refinement_bound),
+  generator(generator_info(info)) { }
 
 string_refinementt::string_refinementt(const infot &info):
   string_refinementt(info, validate(info)) { }
@@ -560,7 +558,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   cur.clear();
   add_instantiations();
 
-  while((initial_loop_bound--)>0)
+  while((loop_bound_--)>0)
   {
     decision_proceduret::resultt res=supert::dec_solve();
 
@@ -591,7 +589,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       if(current_index_set.empty())
       {
         debug() << "current index set is empty" << eom;
-        if(do_concretizing)
+        if(config_.trace)
         {
           concretize_results();
           return resultt::D_SATISFIABLE;
@@ -1232,7 +1230,7 @@ bool string_refinementt::check_axioms()
     debug() << violated_not_contains.size()
             << " not_contains string axioms can be violated" << eom;
 
-    if(use_counter_example)
+    if(config_.use_counter_example)
     {
       // TODO: add counter examples for not_contains?
 
@@ -1757,7 +1755,7 @@ bool string_refinementt::is_axiom_sat(
   info.refine_arithmetic=true;
   info.refine_arrays=true;
   info.max_node_refinement=5;
-  info.ui=config_.ui;
+  info.ui=supert::config_.ui;
   supert solver(info);
   solver << axiom;
 
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 2ee26ea02b1..a61876b40e4 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -49,7 +49,6 @@ class string_refinementt final: public bv_refinementt
 
   explicit string_refinementt(const infot &);
 
-
   virtual std::string decision_procedure_text() const override
   {
     return "string refinement loop with "+prop.solver_text();
@@ -61,8 +60,6 @@ class string_refinementt final: public bv_refinementt
   decision_proceduret::resultt dec_solve() override;
 
 private:
-  const bool use_counter_example;
-  const bool do_concretizing;
   // Base class
   typedef bv_refinementt supert;
 
@@ -72,11 +69,9 @@ class string_refinementt final: public bv_refinementt
   string_refinementt(const infot &, bool);
   bvt convert_bool_bv(const exprt &boole, const exprt &orig);
 
-  unsigned initial_loop_bound;
-
+  const configt config_;
+  unsigned loop_bound_;
   string_constraint_generatort generator;
-
-  const bool non_empty_string;
   expr_sett nondet_arrays;
 
   // Simple constraints that have been given to the solver

From 9fff11698097f2a8af73265381ce76b328b67ddb Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 12 Sep 2017 19:00:28 +0100
Subject: [PATCH 06/28] Remove constructor boilerplate

---
 src/solvers/refinement/string_constraint_generator.h |  4 ++--
 .../refinement/string_constraint_generator_main.cpp  |  4 ++--
 src/solvers/refinement/string_refinement.cpp         | 12 +-----------
 src/solvers/refinement/string_refinement.h           |  8 ++++----
 4 files changed, 9 insertions(+), 19 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index 7a0667fb397..4e04db53d56 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -40,14 +40,14 @@ class string_constraint_generatort final
   /// Arguments pack for the string_constraint_generator constructor
   struct infot
   {
-    const namespacet *ns=nullptr;
     /// Max length of non-deterministic strings
     size_t string_max_length=std::numeric_limits<size_t>::max();
     /// Prefer printable characters in non-deterministic strings
     bool string_printable=false;
   };
 
-  explicit string_constraint_generatort(const infot& info);
+  explicit string_constraint_generatort(
+    const infot& info, const namespacet& ns);
 
   /// Axioms are of three kinds: universally quantified string constraint,
   /// not contains string constraints and simple formulas.
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index f149ef3ecf1..e6c156cd482 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -28,10 +28,10 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include <util/ssa_expr.h>
 
 string_constraint_generatort::string_constraint_generatort(
-  const string_constraint_generatort::infot& info):
+  const string_constraint_generatort::infot& info, const namespacet& ns):
   max_string_length(info.string_max_length),
   m_force_printable_characters(info.string_printable),
-  m_ns(*info.ns) { }
+  m_ns(ns) { }
 
 const std::vector<exprt> &string_constraint_generatort::get_axioms() const
 {
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index d79710942c7..664173dfc96 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -86,21 +86,11 @@ static bool validate(const string_refinementt::infot &info)
   return true;
 }
 
-static string_constraint_generatort::infot
-generator_info(const string_refinementt::infot &in)
-{
-  string_constraint_generatort::infot out;
-  out.ns=in.ns;
-  out.string_max_length=in.string_max_length;
-  out.string_printable=in.string_printable;
-  return out;
-}
-
 string_refinementt::string_refinementt(const infot &info, bool):
   supert(info),
   config_(info),
   loop_bound_(info.refinement_bound),
-  generator(generator_info(info)) { }
+  generator(info, *info.ns) { }
 
 string_refinementt::string_refinementt(const infot &info):
   string_refinementt(info, validate(info)) { }
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index a61876b40e4..d383cb66722 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -34,18 +34,18 @@ class string_refinementt final: public bv_refinementt
 private:
   struct configt {
     unsigned refinement_bound=0;
-    size_t string_max_length=std::numeric_limits<size_t>::max();
     /// Make non-deterministic character arrays have at least one character
     bool string_non_empty=false;
     /// Concretize strings after solver is finished
     bool trace=false;
-    /// Make non-deterministic characters printable
-    bool string_printable=false;
     bool use_counter_example=false;
   };
 public:
   /// string_refinementt constructor arguments
-  struct infot:public bv_refinementt::infot, public configt { };
+  struct infot:
+    public bv_refinementt::infot,
+    public string_constraint_generatort::infot,
+    public configt { };
 
   explicit string_refinementt(const infot &);
 

From 2b2a841d10e4be3e865757dbe36b9efc7044632b Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 12 Sep 2017 19:15:42 +0100
Subject: [PATCH 07/28] Convert display_index_set to a free function

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

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 664173dfc96..e21e5d84e32 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -96,29 +96,34 @@ string_refinementt::string_refinementt(const infot &info):
   string_refinementt(info, validate(info)) { }
 
 /// display the current index set, for debugging
-void string_refinementt::display_index_set()
+static void display_index_set(
+  const messaget& message,
+  const namespacet& ns,
+  const std::map<exprt, std::set<exprt>>& current_index_set,
+  const std::map<exprt, std::set<exprt>>& index_set)
 {
   std::size_t count=0;
   std::size_t count_current=0;
   for(const auto &i : index_set)
   {
     const exprt &s=i.first;
-    debug() << "IS(" << from_expr(ns, "", s) << ")=={" << eom;
+    message.debug() << "IS(" << from_expr(ns, "", s) << ")=={" << message.eom;
 
     for(auto j : i.second)
     {
-      if(current_index_set[i.first].find(j)!=current_index_set[i.first].end())
+      const auto it=current_index_set.find(i.first);
+      if(it!=current_index_set.end() && it->second.find(j)!=it->second.end())
       {
         count_current++;
-        debug() << "**";
+        message.debug() << "**";
       }
-      debug() << "  " << from_expr(ns, "", j) << ";" << eom;
+      message.debug() << "  " << from_expr(ns, "", j) << ";" << message.eom;
       count++;
     }
-    debug() << "}"  << eom;
+    message.debug() << "}"  << message.eom;
   }
-  debug() << count << " elements in index set (" << count_current
-          << " newly added)" << eom;
+  message.debug() << count << " elements in index set (" << count_current
+          << " newly added)" << message.eom;
 }
 
 /// compute the index set for all formulas, instantiate the formulas with the
@@ -592,7 +597,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         }
       }
 
-      display_index_set();
+      display_index_set(*this, ns, current_index_set, index_set);
       debug()<< "instantiating NOT_CONTAINS constraints" << eom;
       for(unsigned i=0; i<not_contains_axioms.size(); i++)
       {
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index d383cb66722..7ec8a2b539c 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -99,8 +99,6 @@ class string_refinementt final: public bv_refinementt
 
   void add_equivalence(const irep_idt & lhs, const exprt & rhs);
 
-  void display_index_set();
-
   void add_lemma(const exprt &lemma,
                  bool simplify=true,
                  bool add_to_index_set=true);

From 8e69d6d2f3f1bc66fb4c69772df73a7605262a6c Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 16:34:47 +0100
Subject: [PATCH 08/28] Make functions static

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

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index e21e5d84e32..97b876f84a3 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -35,6 +35,10 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <java_bytecode/java_types.h>
 #include <util/optional.h>
 
+static exprt instantiate(
+  const string_constraintt &axiom, const exprt &str, const exprt &val);
+exprt simplify_sum(const exprt &f);
+
 /// Convert exprt to a specific type. Throw bad_cast if conversion
 /// cannot be performed
 /// Generic case doesn't exist, specialize for different types accordingly
@@ -97,17 +101,18 @@ string_refinementt::string_refinementt(const infot &info):
 
 /// display the current index set, for debugging
 static void display_index_set(
-  const messaget& message,
+  messaget::mstreamt stream,
   const namespacet& ns,
   const std::map<exprt, std::set<exprt>>& current_index_set,
   const std::map<exprt, std::set<exprt>>& index_set)
 {
+  const auto eom = messaget::eom;
   std::size_t count=0;
   std::size_t count_current=0;
   for(const auto &i : index_set)
   {
     const exprt &s=i.first;
-    message.debug() << "IS(" << from_expr(ns, "", s) << ")=={" << message.eom;
+    stream << "IS(" << from_expr(ns, "", s) << ")=={" << eom;
 
     for(auto j : i.second)
     {
@@ -115,41 +120,53 @@ static void display_index_set(
       if(it!=current_index_set.end() && it->second.find(j)!=it->second.end())
       {
         count_current++;
-        message.debug() << "**";
+        stream << "**";
       }
-      message.debug() << "  " << from_expr(ns, "", j) << ";" << message.eom;
+      stream << "  " << from_expr(ns, "", j) << ";" << eom;
       count++;
     }
-    message.debug() << "}"  << message.eom;
+    stream << "}"  << eom;
   }
-  message.debug() << count << " elements in index set (" << count_current
-          << " newly added)" << message.eom;
+  stream << count << " elements in index set (" << count_current
+          << " newly added)" << eom;
 }
 
 /// compute the index set for all formulas, instantiate the formulas with the
 /// found indexes, and add them as lemmas.
-void string_refinementt::add_instantiations()
+
+static void display_current_index_set(
+  messaget::mstreamt &stream,
+  const namespacet &ns,
+  const std::map<exprt, std::set<exprt>> &current_index_set)
 {
-  debug() << "string_constraint_generatort::add_instantiations: "
-          << "going through the current index set:" << eom;
+  const auto eom=messaget::eom;
+  stream << "string_constraint_generatort::add_instantiations: "
+         << "going through the current index set:" << eom;
   for(const auto &i : current_index_set)
   {
     const exprt &s=i.first;
-    debug() << "IS(" << from_expr(ns, "", s) << ")=={";
+    stream << "IS(" << from_expr(ns, "", s) << ")=={";
 
     for(const auto &j : i.second)
-      debug() << from_expr(ns, "", j) << "; ";
-    debug() << "}"  << eom;
+      stream << from_expr(ns, "", j) << "; ";
+    stream << "}"  << eom;
+  }
+}
 
+static std::vector<exprt> generate_instantiations(
+  const std::map<exprt, std::set<exprt>> &current_index_set,
+  const std::vector<string_constraintt>& universal_axioms)
+{
+  std::vector<exprt> lemmas;
+  for(const auto &i : current_index_set)
+  {
     for(const auto &ua : universal_axioms)
     {
       for(const auto &j : i.second)
-      {
-        exprt lemma=instantiate(ua, s, j);
-        add_lemma(lemma);
-      }
+        lemmas.push_back(instantiate(ua, i.first, j));
     }
   }
+  return lemmas;
 }
 
 /// List the simple expressions on which the expression depends in the
@@ -381,7 +398,10 @@ void string_refinementt::concretize_results()
     concretize_string(it.second);
   for(const auto &it : generator.get_created_strings())
     concretize_string(it);
-  add_instantiations();
+  for (const auto& lemma :
+        generate_instantiations(current_index_set, universal_axioms))
+    add_lemma(lemma);
+  display_current_index_set(debug(), ns, current_index_set);
 }
 
 /// For each string whose length has been solved, add constants to the map
@@ -551,7 +571,10 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   initial_index_set(universal_axioms);
   update_index_set(cur);
   cur.clear();
-  add_instantiations();
+  for (const auto& lemma :
+         generate_instantiations(current_index_set, universal_axioms))
+    add_lemma(lemma);
+  display_current_index_set(debug(), ns, current_index_set);
 
   while((loop_bound_--)>0)
   {
@@ -579,7 +602,10 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       current_index_set.clear();
       update_index_set(cur);
       cur.clear();
-      add_instantiations();
+      for (const auto& lemma :
+            generate_instantiations(current_index_set, universal_axioms))
+        add_lemma(lemma);
+      display_current_index_set(debug(), ns, current_index_set);
 
       if(current_index_set.empty())
       {
@@ -597,7 +623,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         }
       }
 
-      display_index_set(*this, ns, current_index_set, index_set);
+      display_index_set(debug(), ns, current_index_set, index_set);
       debug()<< "instantiating NOT_CONTAINS constraints" << eom;
       for(unsigned i=0; i<not_contains_axioms.size(); i++)
       {
@@ -1254,8 +1280,7 @@ bool string_refinementt::check_axioms()
 /// \return a map where each leaf of the input is mapped to the number of times
 ///   it is added. For instance, expression $x + x - y$ would give the map x ->
 ///   2, y -> -1.
-std::map<exprt, int> string_refinementt::map_representation_of_sum(
-  const exprt &f) const
+static std::map<exprt, int> map_representation_of_sum(const exprt &f)
 {
   // number of time the leaf should be added (can be negative)
   std::map<exprt, int> elems;
@@ -1297,8 +1322,10 @@ std::map<exprt, int> string_refinementt::map_representation_of_sum(
 /// \return a expression for the sum of each element in the map a number of
 ///   times given by the corresponding integer in the map. For a map x -> 2, y
 ///   -> -1 would give an expression $x + x - y$.
-exprt string_refinementt::sum_over_map(
-  std::map<exprt, int> &m, const typet &type, bool negated) const
+static exprt sum_over_map(
+  std::map<exprt, int> &m,
+  const typet &type,
+  bool negated = false)
 {
   exprt sum=nil_exprt();
   mp_integer constants=0;
@@ -1368,7 +1395,7 @@ exprt string_refinementt::sum_over_map(
 
 /// \par parameters: an expression with only plus and minus expr
 /// \return an equivalent expression in a canonical form
-exprt string_refinementt::simplify_sum(const exprt &f) const
+exprt simplify_sum(const exprt &f)
 {
   std::map<exprt, int> map=map_representation_of_sum(f);
   return sum_over_map(map, f.type());
@@ -1381,7 +1408,7 @@ exprt string_refinementt::simplify_sum(const exprt &f) const
 ///   a function of $qvar$, i.e. the value that is necessary for qvar for f to
 ///   be equal to val. For instance, if `f` corresponds to the expression $q +
 ///   x$, `compute_inverse_function(q,v,f)` returns an expression for $v - x$.
-exprt string_refinementt::compute_inverse_function(
+static exprt compute_inverse_function(
   const exprt &qvar, const exprt &val, const exprt &f)
 {
   exprt positive, negative;
@@ -1409,8 +1436,8 @@ exprt string_refinementt::compute_inverse_function(
       string_refinement_invariantt("a proper function must have exactly one "
         "occurrences after reduction, or it canceled out, and it does not have "
         " one"));
-    debug() << "in string_refinementt::compute_inverse_function:"
-            << " warning: occurrences of qvar canceled out " << eom;
+    // debug() << "in string_refinementt::compute_inverse_function:"
+    //         << " warning: occurrences of qvar canceled out " << eom;
   }
 
   elems.erase(it);
@@ -1605,7 +1632,7 @@ class find_index_visitort: public const_expr_visitort
 /// \param [in] str: the string which must be indexed
 /// \param [in] qvar: the universal variable that must be in the index
 /// \return an index expression in `expr` on `str` containing `qvar`
-exprt find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
+static exprt find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
 {
   find_index_visitort v(str, qvar);
   expr.visit(v);
@@ -1619,7 +1646,7 @@ exprt find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
 ///   For instance, if `axiom` corresponds to $\forall q. s[q+x]='a' &&
 ///   t[q]='b'$, `instantiate(axiom,s,v)` would return an expression for
 ///   $s[v]='a' && t[v-x]='b'$.
-exprt string_refinementt::instantiate(
+static exprt instantiate(
   const string_constraintt &axiom, const exprt &str, const exprt &val)
 {
   exprt idx=find_index(axiom.body(), str, axiom.univ_var());
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 7ec8a2b539c..ea552375191 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -113,7 +113,6 @@ class string_refinementt final: public bv_refinementt
   bool add_axioms_for_string_assigns(const exprt &lhs, const exprt &rhs);
   void set_to(const exprt &expr, bool value) override;
 
-  void add_instantiations();
   void debug_model();
   bool check_axioms();
   bool is_axiom_sat(
@@ -126,9 +125,6 @@ class string_refinementt final: public bv_refinementt
   void initial_index_set(const std::vector<string_constraintt> &string_axioms);
   void add_to_index_set(const exprt &s, exprt i);
 
-  exprt instantiate(
-    const string_constraintt &axiom, const exprt &str, const exprt &val);
-
   std::vector<exprt> instantiate_not_contains(
     const string_not_contains_constraintt &axiom);
 
@@ -136,13 +132,9 @@ class string_refinementt final: public bv_refinementt
     const exprt &qvar, const exprt &val, const exprt &f);
 
   std::map<exprt, int> map_representation_of_sum(const exprt &f) const;
-  exprt sum_over_map(
-    std::map<exprt, int> &m, const typet &type, bool negated=false) const;
 
   bool is_valid_string_constraint(const string_constraintt &expr);
 
-  exprt simplify_sum(const exprt &f) const;
-
   void concretize_string(const exprt &expr);
   void concretize_results();
   void concretize_lengths();

From cfb47dbe7c5b4ba7f20c7b78c9db8f7223adbbc8 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 16:51:52 +0100
Subject: [PATCH 09/28] Remove unused functions from string_refinement header

---
 src/solvers/refinement/string_refinement.cpp | 63 ++++++++++++++++----
 src/solvers/refinement/string_refinement.h   | 41 -------------
 2 files changed, 50 insertions(+), 54 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 97b876f84a3..e09529c8715 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -35,8 +35,14 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <java_bytecode/java_types.h>
 #include <util/optional.h>
 
+static exprt substitute_array_with_expr(const exprt &expr, const exprt &index);
 static exprt instantiate(
   const string_constraintt &axiom, const exprt &str, const exprt &val);
+static bool is_char_array(const namespacet &ns, const typet &type);
+exprt substitute_array_lists(exprt expr, size_t string_max_length);
+exprt concretize_arrays_in_expression(
+  exprt expr, std::size_t string_max_length);
+
 exprt simplify_sum(const exprt &f);
 
 /// Convert exprt to a specific type. Throw bad_cast if conversion
@@ -83,6 +89,37 @@ T expr_cast_v(const exprt& expr) {
   return *maybe;
 }
 
+/// Convert index-value map to a vector of values. If a value for an
+/// index is not defined, set it to the value referenced by the next higher
+/// index. The length of the resulting vector is the key of the map's
+/// last element + 1
+/// \param index_value: map containing values of specific vector cells
+/// \return Vector containing values as described in the map
+template <typename T>
+static std::vector<T> fill_in_map_as_vector(
+  const std::map<std::size_t, T> &index_value)
+{
+  std::vector<T> result;
+  if(!index_value.empty())
+  {
+    result.resize(index_value.rbegin()->first+1);
+    for(auto it=index_value.rbegin(); it!=index_value.rend(); ++it)
+    {
+      const std::size_t index=it->first;
+      const T value=it->second;
+      const auto next=std::next(it);
+      const std::size_t leftmost_index_to_pad=
+        next!=index_value.rend()
+        ? next->first+1
+        : 0;
+      for(std::size_t j=leftmost_index_to_pad; j<=index; j++)
+        result[j]=value;
+    }
+  }
+  return result;
+}
+
+
 static bool validate(const string_refinementt::infot &info)
 {
   PRECONDITION(info.ns);
@@ -263,13 +300,14 @@ void string_refinementt::set_char_array_equality(
 /// remove functions applications and create the necessary axioms
 /// \par parameters: an expression containing function applications
 /// \return an expression containing no function application
-exprt string_refinementt::substitute_function_applications(exprt expr)
+exprt substitute_function_applications(
+  string_constraint_generatort& generator, exprt expr)
 {
   for(size_t i=0; i<expr.operands().size(); ++i)
   {
     // TODO: only copy when necessary
     exprt op(expr.operands()[i]);
-    expr.operands()[i]=substitute_function_applications(op);
+    expr.operands()[i]=substitute_function_applications(generator, op);
   }
 
   if(expr.id()==ID_function_application)
@@ -286,10 +324,10 @@ exprt string_refinementt::substitute_function_applications(exprt expr)
 /// TODO: this is only for java char array and does not work for other languages
 /// \param type: a type
 /// \return true if the given type is an array of java characters
-bool string_refinementt::is_char_array(const typet &type) const
+static bool is_char_array(const namespacet &ns, const typet &type)
 {
   if(type.id()==ID_symbol)
-    return is_char_array(ns.follow(type));
+    return is_char_array(ns, ns.follow(type));
 
   return (type.id()==ID_array && type.subtype()==java_char_type());
 }
@@ -302,7 +340,7 @@ bool string_refinementt::is_char_array(const typet &type) const
 bool string_refinementt::add_axioms_for_string_assigns(
   const exprt &lhs, const exprt &rhs)
 {
-  if(is_char_array(rhs.type()))
+  if(is_char_array(ns, rhs.type()))
   {
     set_char_array_equality(lhs, rhs);
     if(rhs.id() == ID_symbol || rhs.id() == ID_array)
@@ -444,10 +482,10 @@ void string_refinementt::set_to(const exprt &expr, bool value)
     const exprt &rhs=eq_expr.rhs();
 
     // The assignment of a string equality to false is not supported.
-    PRECONDITION(value || !is_char_array(rhs.type()));
+    PRECONDITION(value || !is_char_array(ns, rhs.type()));
     PRECONDITION(value || !is_refined_string_type(rhs.type()));
 
-    PRECONDITION(lhs.id()==ID_symbol || !is_char_array(rhs.type()));
+    PRECONDITION(lhs.id()==ID_symbol || !is_char_array(ns, rhs.type()));
     PRECONDITION(lhs.id()==ID_symbol || !is_refined_string_type(rhs.type()));
 
     // If lhs is not a symbol, let supert::set_to() handle it.
@@ -470,7 +508,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)
     debug() << "(sr::set_to) " << from_expr(ns, "", lhs)
             << " = " << from_expr(ns, "", rhs) << eom;
 
-    const exprt subst_rhs=substitute_function_applications(rhs);
+    const exprt subst_rhs=substitute_function_applications(generator, rhs);
     if(lhs.type()!=subst_rhs.type())
     {
       if(lhs.type().id()!=ID_array ||
@@ -832,7 +870,7 @@ void string_refinementt::debug_model()
     else
     {
       INVARIANT(
-        is_char_array(it.second.type()),
+        is_char_array(ns, it.second.type()),
         string_refinement_invariantt("symbol_resolve should only map to "
           "refined_strings or to char_arrays, and refined_strings are already "
           "handled"));
@@ -868,8 +906,7 @@ void string_refinementt::debug_model()
 ///   expression
 /// \param index: An index with which to build the equality condition
 /// \return An expression containing no 'with' expression
-exprt string_refinementt::substitute_array_with_expr(
-  const exprt &expr, const exprt &index) const
+static exprt substitute_array_with_expr(const exprt &expr, const exprt &index)
 {
   if(expr.id()==ID_with)
   {
@@ -941,7 +978,7 @@ exprt fill_in_array_with_expr(const exprt &expr, std::size_t string_max_length)
 ///    `arr2 := {34}`, the constructed expression will be: `g1 ? 12 : 34`
 /// \param expr: an expression containing array accesses
 /// \return an expression containing no array access
-void string_refinementt::substitute_array_access(exprt &expr) const
+static void substitute_array_access(exprt &expr)
 {
   for(auto &op : expr.operands())
     substitute_array_access(op);
@@ -1732,7 +1769,7 @@ exprt string_refinementt::get(const exprt &expr) const
 {
   exprt ecopy(expr);
   replace_expr(symbol_resolve, ecopy);
-  if(is_char_array(ecopy.type()))
+  if(is_char_array(ns, ecopy.type()))
   {
     auto it_content=found_content.find(ecopy);
     if(it_content!=found_content.end())
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index ea552375191..c5db0eded87 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -103,13 +103,7 @@ class string_refinementt final: public bv_refinementt
                  bool simplify=true,
                  bool add_to_index_set=true);
 
-  exprt substitute_function_applications(exprt expr);
-  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;
-  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);
   void set_to(const exprt &expr, bool value) override;
 
@@ -144,39 +138,4 @@ class string_refinementt final: public bv_refinementt
 
   std::string string_of_array(const array_exprt &arr);
 };
-
-exprt substitute_array_lists(exprt expr, size_t string_max_length);
-
-exprt concretize_arrays_in_expression(
-  exprt expr, std::size_t string_max_length);
-
-/// Convert index-value map to a vector of values. If a value for an
-/// index is not defined, set it to the value referenced by the next higher
-/// index. The length of the resulting vector is the key of the map's
-/// last element + 1
-/// \param index_value: map containing values of specific vector cells
-/// \return Vector containing values as described in the map
-template <typename T>
-std::vector<T> fill_in_map_as_vector(
-  const std::map<std::size_t, T> &index_value)
-{
-  std::vector<T> result;
-  if(!index_value.empty())
-  {
-    result.resize(index_value.rbegin()->first+1);
-    for(auto it=index_value.rbegin(); it!=index_value.rend(); ++it)
-    {
-      const std::size_t index=it->first;
-      const T value=it->second;
-      const auto next=std::next(it);
-      const std::size_t leftmost_index_to_pad=
-        next!=index_value.rend()
-        ? next->first+1
-        : 0;
-      for(std::size_t j=leftmost_index_to_pad; j<=index; j++)
-        result[j]=value;
-    }
-  }
-  return result;
-}
 #endif

From 01b830108d4f36add8d60ac2b3917e65baefc88b Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 16:55:49 +0100
Subject: [PATCH 10/28] static is_valid_string_constraint

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

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index e09529c8715..b5e304d39c8 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -42,6 +42,10 @@ static bool is_char_array(const namespacet &ns, const typet &type);
 exprt substitute_array_lists(exprt expr, size_t string_max_length);
 exprt concretize_arrays_in_expression(
   exprt expr, std::size_t string_max_length);
+static bool is_valid_string_constraint(
+  messaget::mstreamt& stream,
+  const namespacet& ns,
+  const string_constraintt &expr);
 
 exprt simplify_sum(const exprt &f);
 
@@ -563,12 +567,14 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     replace_expr(symbol_resolve, axiom);
     if(axiom.id()==ID_string_constraint)
     {
-      string_constraintt c=to_string_constraint(axiom);
+      string_constraintt nc_axiom=
+        to_string_constraint(axiom);
+      is_valid_string_constraint(error(), ns, nc_axiom);
       DATA_INVARIANT(
-        is_valid_string_constraint(c),
+        is_valid_string_constraint(error(), ns, nc_axiom),
         string_refinement_invariantt(
           "string constraints satisfy their invariant"));
-      universal_axioms.push_back(c);
+      universal_axioms.push_back(nc_axiom);
     }
     else if(axiom.id()==ID_string_not_contains_constraint)
     {
@@ -1938,21 +1944,24 @@ static bool universal_only_in_index(const string_constraintt &expr)
 /// \related string_constraintt
 /// \param [in] expr: the string constraint to check
 /// \return whether the constraint satisfies the invariant
-bool string_refinementt::is_valid_string_constraint(
+static bool is_valid_string_constraint(
+  messaget::mstreamt& stream,
+  const namespacet& ns,
   const string_constraintt &expr)
 {
+  const auto eom = messaget::eom;
   // Condition 1: The premise cannot contain any string indices
   const array_index_mapt premise_indices=gather_indices(expr.premise());
   if(!premise_indices.empty())
   {
-    error() << "Premise has indices: " << from_expr(ns, "", expr) << ", map: {";
+    stream << "Premise has indices: " << from_expr(ns, "", expr) << ", map: {";
     for(const auto &pair : premise_indices)
     {
-      error() << from_expr(ns, "", pair.first) << ": {";
+      stream << from_expr(ns, "", pair.first) << ": {";
       for(const auto &i : pair.second)
-        error() << from_expr(ns, "", i) <<  ", ";
+        stream << from_expr(ns, "", i) <<  ", ";
     }
-    error() << "}}" << eom;
+    stream << "}}" << eom;
     return false;
   }
 
@@ -1970,8 +1979,8 @@ bool string_refinementt::is_valid_string_constraint(
       const exprt result=simplify_expr(equals, ns);
       if(result.is_false())
       {
-        error() << "Indices not equal: " << from_expr(ns, "", expr) << ", str: "
-                << from_expr(ns, "", pair.first) << eom;
+        stream << "Indices not equal: " << from_expr(ns, "", expr) << ", str: "
+               << from_expr(ns, "", pair.first) << eom;
         return false;
       }
     }
@@ -1979,8 +1988,8 @@ bool string_refinementt::is_valid_string_constraint(
     // Condition 3: f must be linear
     if(!is_linear_arithmetic_expr(rep))
     {
-      error() << "f is not linear: " << from_expr(ns, "", expr) << ", str: "
-              << from_expr(ns, "", pair.first) << eom;
+      stream << "f is not linear: " << from_expr(ns, "", expr) << ", str: "
+             << from_expr(ns, "", pair.first) << eom;
       return false;
     }
 
@@ -1988,8 +1997,8 @@ bool string_refinementt::is_valid_string_constraint(
     // body
     if(!universal_only_in_index(expr))
     {
-      error() << "Universal variable outside of index:"
-              << from_expr(ns, "", expr) << eom;
+      stream << "Universal variable outside of index:"
+             << from_expr(ns, "", expr) << eom;
       return false;
     }
   }
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index c5db0eded87..611cd6d89e1 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -127,8 +127,6 @@ class string_refinementt final: public bv_refinementt
 
   std::map<exprt, int> map_representation_of_sum(const exprt &f) const;
 
-  bool is_valid_string_constraint(const string_constraintt &expr);
-
   void concretize_string(const exprt &expr);
   void concretize_results();
   void concretize_lengths();

From bcd6111350465963dcadcd4a8fd3aed29f5e9652 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 17:06:37 +0100
Subject: [PATCH 11/28] Static is_axiom_sat

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

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index b5e304d39c8..a01be4906cc 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -46,6 +46,12 @@ static bool is_valid_string_constraint(
   messaget::mstreamt& stream,
   const namespacet& ns,
   const string_constraintt &expr);
+static bool is_axiom_sat(
+  const namespacet& ns,
+  ui_message_handlert::uit ui,
+  const exprt &axiom,
+  const symbol_exprt& var,
+  exprt &witness);
 
 exprt simplify_sum(const exprt &f);
 
@@ -1224,7 +1230,8 @@ bool string_refinementt::check_axioms()
             << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
     exprt witness;
 
-    bool is_sat=is_axiom_sat(with_concretized_arrays, univ_var, witness);
+    bool is_sat=is_axiom_sat(
+      ns, supert::config_.ui, with_concretized_arrays, univ_var, witness);
 
     if(is_sat)
     {
@@ -1271,7 +1278,7 @@ bool string_refinementt::check_axioms()
     substitute_array_access(negaxiom);
     exprt witness;
 
-    bool is_sat=is_axiom_sat(negaxiom, univ_var, witness);
+    bool is_sat=is_axiom_sat(ns, supert::config_.ui, negaxiom, univ_var, witness);
 
     if(is_sat)
     {
@@ -1810,18 +1817,22 @@ exprt string_refinementt::get(const exprt &expr) const
 /// \param [out] witness: the witness of the satisfying assignment if one
 ///   exists. If UNSAT, then behaviour is undefined.
 /// \return: true if axiom is SAT, false if UNSAT
-bool string_refinementt::is_axiom_sat(
-  const exprt &axiom, const symbol_exprt& var, exprt &witness)
+static bool is_axiom_sat(
+  const namespacet& ns,
+  ui_message_handlert::uit ui,
+  const exprt &axiom,
+  const symbol_exprt& var,
+  exprt &witness)
 {
   satcheck_no_simplifiert sat_check;
-  supert::infot info;
+  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=supert::config_.ui;
-  supert solver(info);
+  info.ui=ui;
+  bv_refinementt solver(info);
   solver << axiom;
 
   switch(solver())
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 611cd6d89e1..9c87840b117 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -109,8 +109,6 @@ class string_refinementt final: public bv_refinementt
 
   void debug_model();
   bool check_axioms();
-  bool is_axiom_sat(
-    const exprt &axiom, const symbol_exprt& var, exprt &witness);
 
   void set_char_array_equality(const exprt &lhs, const exprt &rhs);
   void update_index_set(const exprt &formula);
@@ -122,11 +120,6 @@ class string_refinementt final: public bv_refinementt
   std::vector<exprt> instantiate_not_contains(
     const string_not_contains_constraintt &axiom);
 
-  exprt compute_inverse_function(
-    const exprt &qvar, const exprt &val, const exprt &f);
-
-  std::map<exprt, int> map_representation_of_sum(const exprt &f) const;
-
   void concretize_string(const exprt &expr);
   void concretize_results();
   void concretize_lengths();

From 666c14654c3882f886f4189734eb9065aa325342 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 18:37:32 +0100
Subject: [PATCH 12/28] make static check_axioms

---
 src/solvers/refinement/string_refinement.cpp | 150 +++++++++++++------
 src/solvers/refinement/string_refinement.h   |   3 -
 2 files changed, 104 insertions(+), 49 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index a01be4906cc..bd36f7b944b 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -22,6 +22,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <sstream>
 #include <iomanip>
 #include <stack>
+#include <functional>
 #include <ansi-c/string_constant.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_iterator.h>
@@ -36,16 +37,21 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <util/optional.h>
 
 static exprt substitute_array_with_expr(const exprt &expr, const exprt &index);
+
 static exprt instantiate(
   const string_constraintt &axiom, const exprt &str, const exprt &val);
 static bool is_char_array(const namespacet &ns, const typet &type);
+
 exprt substitute_array_lists(exprt expr, size_t string_max_length);
+
 exprt concretize_arrays_in_expression(
   exprt expr, std::size_t string_max_length);
+
 static bool is_valid_string_constraint(
   messaget::mstreamt& stream,
   const namespacet& ns,
   const string_constraintt &expr);
+
 static bool is_axiom_sat(
   const namespacet& ns,
   ui_message_handlert::uit ui,
@@ -53,6 +59,18 @@ static bool is_axiom_sat(
   const symbol_exprt& var,
   exprt &witness);
 
+static std::pair<bool, std::vector<exprt>> check_axioms(
+  const std::vector<string_constraintt> &universal_axioms,
+  const std::vector<string_not_contains_constraintt> &not_contains_axioms,
+  string_constraint_generatort &generator,
+  std::function<exprt(const exprt&)> get,
+  messaget::mstreamt &stream,
+  const namespacet &ns,
+  std::size_t max_string_length,
+  bool use_counter_example,
+  ui_message_handlert::uit ui,
+  const replace_mapt& symbol_resolve);
+
 exprt simplify_sum(const exprt &f);
 
 /// Convert exprt to a specific type. Throw bad_cast if conversion
@@ -606,8 +624,23 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   decision_proceduret::resultt res=supert::dec_solve();
   if(res==resultt::D_SATISFIABLE)
   {
-    if(!check_axioms())
+    bool success;
+    std::vector<exprt> lemmas;
+    std::tie(success, lemmas)=check_axioms(
+      universal_axioms,
+      not_contains_axioms,
+      generator,
+      [this](const exprt& expr){ return this->get(expr); },
+      debug(),
+      ns,
+      generator.max_string_length,
+      config_.use_counter_example,
+      supert::config_.ui,
+      symbol_resolve);
+    if(!success)
     {
+      for (const auto& lemma : lemmas)
+        add_lemma(lemma);
       debug() << "check_SAT: got SAT but the model is not correct" << eom;
     }
     else
@@ -630,11 +663,25 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   {
     decision_proceduret::resultt res=supert::dec_solve();
 
-    switch(res)
+    if (res == resultt::D_SATISFIABLE)
     {
-    case resultt::D_SATISFIABLE:
-      if(!check_axioms())
+      bool success;
+      std::vector<exprt> lemmas;
+      std::tie(success, lemmas)=check_axioms(
+        universal_axioms,
+        not_contains_axioms,
+        generator,
+        [this](const exprt& expr){ return this->get(expr); },
+        debug(),
+        ns,
+        generator.max_string_length,
+        config_.use_counter_example,
+        supert::config_.ui,
+        symbol_resolve);
+      if(!success)
       {
+        for (const auto& lemma : lemmas)
+          add_lemma(lemma);
         debug() << "check_SAT: got SAT but the model is not correct" << eom;
       }
       else
@@ -683,8 +730,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         for(const exprt &lemma : lemmas)
           add_lemma(lemma);
       }
-      break;
-    default:
+    } else {
       debug() << "check_SAT: default return " << static_cast<int>(res) << eom;
       return res;
     }
@@ -1188,15 +1234,26 @@ exprt concretize_arrays_in_expression(exprt expr, std::size_t string_max_length)
 
 /// return true if the current model satisfies all the axioms
 /// \return a Boolean
-bool string_refinementt::check_axioms()
+static std::pair<bool, std::vector<exprt>> check_axioms(
+  const std::vector<string_constraintt> &universal_axioms,
+  const std::vector<string_not_contains_constraintt> &not_contains_axioms,
+  string_constraint_generatort &generator,
+  std::function<exprt(const exprt&)> get,
+  messaget::mstreamt &stream,
+  const namespacet &ns,
+  std::size_t max_string_length,
+  bool use_counter_example,
+  ui_message_handlert::uit ui,
+  const replace_mapt& symbol_resolve)
 {
-  debug() << "string_refinementt::check_axioms:" << eom;
-  debug_model();
+  const auto eom = messaget::eom;
+  stream << "string_refinementt::check_axioms:" << eom;
+  // debug_model();
 
   // Maps from indexes of violated universal axiom to a witness of violation
   std::map<size_t, exprt> violated;
 
-  debug() << "string_refinement::check_axioms: " << universal_axioms.size()
+  stream << "string_refinement::check_axioms: " << universal_axioms.size()
           << " universal axioms:" << eom;
   for(size_t i=0; i<universal_axioms.size(); i++)
   {
@@ -1212,43 +1269,43 @@ bool string_refinementt::check_axioms()
 
     exprt negaxiom=negation_of_constraint(axiom_in_model);
 
-    debug() << "  "<< i << ".\n"
-            << "    - axiom:\n"
-            << "       " << from_expr(ns, "", axiom) << eom;
-    debug() << "    - axiom_in_model:\n"
-            << "       " << from_expr(ns, "", axiom_in_model) << eom;
-    debug() << "    - negated_axiom:\n"
-            << "       " << from_expr(ns, "", negaxiom) << eom;
+    stream << "  "<< i << ".\n"
+           << "    - axiom:\n"
+           << "       " << from_expr(ns, "", axiom) << eom;
+    stream << "    - axiom_in_model:\n"
+           << "       " << from_expr(ns, "", axiom_in_model) << eom;
+    stream << "    - negated_axiom:\n"
+           << "       " << from_expr(ns, "", negaxiom) << eom;
 
     exprt with_concretized_arrays=concretize_arrays_in_expression(
-      negaxiom, generator.max_string_length);
-    debug() << "    - negated_axiom_with_concretized_array_access:\n"
-            << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
+      negaxiom, max_string_length);
+    stream << "    - negated_axiom_with_concretized_array_access:\n"
+           << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
 
     substitute_array_access(with_concretized_arrays);
-    debug() << "    - negated_axiom_without_array_access:\n"
-            << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
+    stream << "    - negated_axiom_without_array_access:\n"
+           << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
     exprt witness;
 
     bool is_sat=is_axiom_sat(
-      ns, supert::config_.ui, with_concretized_arrays, univ_var, witness);
+      ns, ui, with_concretized_arrays, univ_var, witness);
 
     if(is_sat)
     {
-      debug() << "  - violated_for: "
-              << univ_var.get_identifier()
-              << " = " << from_expr(ns, "", witness) << eom;
+      stream << "  - violated_for: "
+             << univ_var.get_identifier()
+             << " = " << from_expr(ns, "", witness) << eom;
       violated[i]=witness;
     }
     else
-      debug() << "  - correct" << eom;
+      stream << "  - correct" << eom;
   }
 
   // Maps from indexes of violated not_contains axiom to a witness of violation
   std::map<std::size_t, exprt> violated_not_contains;
 
-  debug() << "there are " << not_contains_axioms.size()
-          << " not_contains axioms" << eom;
+  stream << "there are " << not_contains_axioms.size()
+         << " not_contains axioms" << eom;
   for(size_t i=0; i<not_contains_axioms.size(); i++)
   {
     const string_not_contains_constraintt &nc_axiom=not_contains_axioms[i];
@@ -1273,39 +1330,40 @@ bool string_refinementt::check_axioms()
 
     exprt negaxiom=negation_of_not_contains_constraint(
       nc_axiom_in_model, univ_var);
-    debug() << "(string_refinementt::check_axioms) Adding negated constraint: "
-            << from_expr(ns, "", negaxiom) << eom;
+    stream << "(string_refinementt::check_axioms) Adding negated constraint: "
+           << from_expr(ns, "", negaxiom) << eom;
     substitute_array_access(negaxiom);
     exprt witness;
 
-    bool is_sat=is_axiom_sat(ns, supert::config_.ui, negaxiom, univ_var, witness);
+    bool is_sat=is_axiom_sat(ns, ui, negaxiom, univ_var, witness);
 
     if(is_sat)
     {
-      debug() << "string constraint can be violated for "
-              << univ_var.get_identifier()
-              << " = " << from_expr(ns, "", witness) << eom;
+      stream << "string constraint can be violated for "
+             << univ_var.get_identifier()
+             << " = " << from_expr(ns, "", witness) << eom;
       violated_not_contains[i]=witness;
     }
   }
 
   if(violated.empty() && violated_not_contains.empty())
   {
-    debug() << "no violated property" << eom;
-    return true;
+    stream << "no violated property" << eom;
+    return { true, std::vector<exprt>() };
   }
   else
   {
-    debug() << violated.size()
-            << " universal string axioms can be violated" << eom;
-    debug() << violated_not_contains.size()
-            << " not_contains string axioms can be violated" << eom;
+    stream << violated.size()
+           << " universal string axioms can be violated" << eom;
+    stream << violated_not_contains.size()
+           << " not_contains string axioms can be violated" << eom;
 
-    if(config_.use_counter_example)
+    if(use_counter_example)
     {
       // TODO: add counter examples for not_contains?
 
       // Checking if the current solution satisfies the constraints
+      std::vector<exprt> lemmas;
       for(const auto &v : violated)
       {
         const exprt &val=v.second;
@@ -1316,14 +1374,14 @@ bool string_refinementt::check_axioms()
         implies_exprt instance(premise, body);
         replace_expr(symbol_resolve, instance);
         replace_expr(axiom.univ_var(), val, instance);
-        debug() << "adding counter example " << from_expr(ns, "", instance)
+        stream << "adding counter example " << from_expr(ns, "", instance)
                 << eom;
-        add_lemma(instance);
+        lemmas.push_back(instance);
       }
+      return { false, lemmas };
     }
-
-    return false;
   }
+  return { false, std::vector<exprt>() };
 }
 
 /// \par parameters: an expression with only addition and subtraction
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 9c87840b117..1f45b9dece5 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -97,8 +97,6 @@ class string_refinementt final: public bv_refinementt
   // Content of char arrays found during concretization
   std::map<exprt, array_exprt> found_content;
 
-  void add_equivalence(const irep_idt & lhs, const exprt & rhs);
-
   void add_lemma(const exprt &lemma,
                  bool simplify=true,
                  bool add_to_index_set=true);
@@ -108,7 +106,6 @@ class string_refinementt final: public bv_refinementt
   void set_to(const exprt &expr, bool value) override;
 
   void debug_model();
-  bool check_axioms();
 
   void set_char_array_equality(const exprt &lhs, const exprt &rhs);
   void update_index_set(const exprt &formula);

From 2eed573c17c93417f6a84c97d5c115a46f498bca Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 18:47:02 +0100
Subject: [PATCH 13/28] Static add_axioms for strings

---
 src/solvers/refinement/string_refinement.cpp | 30 ++++++++++++++++----
 src/solvers/refinement/string_refinement.h   |  1 -
 2 files changed, 24 insertions(+), 7 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index bd36f7b944b..307ecd4a1cc 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -266,8 +266,11 @@ static void depends_in_symbol_map(const exprt &expr, std::vector<exprt> &accu)
 /// \param rhs: an expression to map it to, which should be either a symbol
 ///             a string_exprt, an array_exprt, an array_of_exprt or an
 ///             if_exprt with branches of the previous kind
-void string_refinementt::add_symbol_to_symbol_map(
-  const exprt &lhs, const exprt &rhs)
+void add_symbol_to_symbol_map(
+  replace_mapt& symbol_resolve,
+  std::map<exprt, std::list<exprt>> &reverse_symbol_resolve,
+  const exprt &lhs,
+  const exprt &rhs)
 {
   PRECONDITION(lhs.id()==ID_symbol);
   PRECONDITION(rhs.id()==ID_symbol ||
@@ -373,18 +376,29 @@ bool string_refinementt::add_axioms_for_string_assigns(
     set_char_array_equality(lhs, rhs);
     if(rhs.id() == ID_symbol || rhs.id() == ID_array)
     {
-      add_symbol_to_symbol_map(lhs, rhs);
+      add_symbol_to_symbol_map(
+        symbol_resolve,
+        reverse_symbol_resolve,
+        lhs,
+        rhs);
       return false;
     }
     else if(rhs.id()==ID_nondet_symbol)
     {
       add_symbol_to_symbol_map(
-        lhs, generator.fresh_symbol("nondet_array", lhs.type()));
+        symbol_resolve,
+        reverse_symbol_resolve,
+        lhs,
+        generator.fresh_symbol("nondet_array", lhs.type()));
       return false;
     }
     else if(rhs.id()==ID_if)
     {
-      add_symbol_to_symbol_map(lhs, rhs);
+      add_symbol_to_symbol_map(
+        symbol_resolve,
+        reverse_symbol_resolve,
+        lhs,
+        rhs);
       return true;
     }
     else
@@ -396,7 +410,11 @@ bool string_refinementt::add_axioms_for_string_assigns(
   if(is_refined_string_type(rhs.type()))
   {
     exprt refined_rhs=generator.add_axioms_for_refined_string(rhs);
-    add_symbol_to_symbol_map(lhs, refined_rhs);
+    add_symbol_to_symbol_map(
+      symbol_resolve,
+      reverse_symbol_resolve,
+      lhs,
+      refined_rhs);
     return false;
   }
   // Other cases are to be handled by supert::set_to.
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 1f45b9dece5..f889ebb2c7b 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -101,7 +101,6 @@ class string_refinementt final: public bv_refinementt
                  bool simplify=true,
                  bool add_to_index_set=true);
 
-  void add_symbol_to_symbol_map(const exprt &lhs, const exprt &rhs);
   bool add_axioms_for_string_assigns(const exprt &lhs, const exprt &rhs);
   void set_to(const exprt &expr, bool value) override;
 

From 65ad3db70b1a0f94d11d7cf82654322cef298302 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 18:48:04 +0100
Subject: [PATCH 14/28] Public methods made public

---
 src/solvers/refinement/string_refinement.h | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index f889ebb2c7b..7acad3c67c3 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -50,13 +50,10 @@ class string_refinementt final: public bv_refinementt
   explicit string_refinementt(const infot &);
 
   virtual std::string decision_procedure_text() const override
-  {
-    return "string refinement loop with "+prop.solver_text();
-  }
+  { return "string refinement loop with "+prop.solver_text(); }
 
   exprt get(const exprt &expr) const override;
-
-protected:
+  void set_to(const exprt &expr, bool value) override;
   decision_proceduret::resultt dec_solve() override;
 
 private:
@@ -102,7 +99,6 @@ class string_refinementt final: public bv_refinementt
                  bool add_to_index_set=true);
 
   bool add_axioms_for_string_assigns(const exprt &lhs, const exprt &rhs);
-  void set_to(const exprt &expr, bool value) override;
 
   void debug_model();
 

From e5e1ff4b81f60e97bca59874c542ecfe1618599b Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 19:12:53 +0100
Subject: [PATCH 15/28] static index_set functions

---
 src/solvers/refinement/string_refinement.cpp | 39 ++++++++++++++++----
 src/solvers/refinement/string_refinement.h   |  3 --
 2 files changed, 31 insertions(+), 11 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 307ecd4a1cc..a6d1f5637e5 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -71,6 +71,18 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
   ui_message_handlert::uit ui,
   const replace_mapt& symbol_resolve);
 
+static void initial_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const string_constraintt &axiom);
+
+static void initial_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const std::vector<string_constraintt>  &string_axioms);
+
 exprt simplify_sum(const exprt &f);
 
 /// Convert exprt to a specific type. Throw bad_cast if conversion
@@ -669,7 +681,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     }
   }
 
-  initial_index_set(universal_axioms);
+  initial_index_set(index_set, current_index_set, ns, universal_axioms);
   update_index_set(cur);
   cur.clear();
   for (const auto& lemma :
@@ -1602,11 +1614,14 @@ static bool find_qvar(const exprt index, const symbol_exprt &qvar)
 /// add to the index set all the indices that appear in the formulas and the
 /// upper bound minus one
 /// \par parameters: a list of string constraints
-void string_refinementt::initial_index_set(
+static void initial_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
   const std::vector<string_constraintt>  &string_axioms)
 {
   for(const auto &axiom : string_axioms)
-    initial_index_set(axiom);
+    initial_index_set(index_set, current_index_set, ns, axiom);
 }
 
 /// add to the index set all the indices that appear in the formulas
@@ -1644,7 +1659,11 @@ static std::vector<exprt> sub_arrays(const exprt &array_expr)
 /// add to the index set all the indices that appear in the formula and the
 /// upper bound minus one
 /// \par parameters: a string constraint
-void string_refinementt::add_to_index_set(const exprt &s, exprt i)
+static void add_to_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const exprt &s, exprt i)
 {
   simplify(i, ns);
   if(i.id()!=ID_constant || expr_cast<size_t>(i))
@@ -1655,7 +1674,11 @@ void string_refinementt::add_to_index_set(const exprt &s, exprt i)
   }
 }
 
-void string_refinementt::initial_index_set(const string_constraintt &axiom)
+static void initial_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const string_constraintt &axiom)
 {
   symbol_exprt qvar=axiom.univ_var();
   std::list<exprt> to_process;
@@ -1675,7 +1698,7 @@ void string_refinementt::initial_index_set(const string_constraintt &axiom)
       // if cur is of the form s[i] and no quantified variable appears in i
       if(!has_quant_var)
       {
-        add_to_index_set(s, i);
+        add_to_index_set(index_set, current_index_set, ns, s, i);
       }
       else
       {
@@ -1685,7 +1708,7 @@ void string_refinementt::initial_index_set(const string_constraintt &axiom)
           axiom.upper_bound(),
           from_integer(1, axiom.upper_bound().type()));
         replace_expr(qvar, kminus1, e);
-        add_to_index_set(s, e);
+        add_to_index_set(index_set, current_index_set, ns, s, e);
       }
     }
     else
@@ -1713,7 +1736,7 @@ void string_refinementt::update_index_set(const exprt &formula)
         s.type().id()==ID_array,
         string_refinement_invariantt("index expressions must index on arrays"));
       exprt simplified=simplify_sum(i);
-      add_to_index_set(s, simplified);
+      add_to_index_set(index_set, current_index_set, ns, s, simplified);
     }
     else
     {
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 7acad3c67c3..84a7bc4a8d0 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -105,9 +105,6 @@ class string_refinementt final: public bv_refinementt
   void set_char_array_equality(const exprt &lhs, const exprt &rhs);
   void update_index_set(const exprt &formula);
   void update_index_set(const std::vector<exprt> &cur);
-  void initial_index_set(const string_constraintt &axiom);
-  void initial_index_set(const std::vector<string_constraintt> &string_axioms);
-  void add_to_index_set(const exprt &s, exprt i);
 
   std::vector<exprt> instantiate_not_contains(
     const string_not_contains_constraintt &axiom);

From a4c8cf5f9e9a788fec566084bec0da953ef3d538 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 19:21:00 +0100
Subject: [PATCH 16/28] Static index set functions

---
 src/solvers/refinement/string_refinement.cpp | 30 ++++++++++++++++----
 src/solvers/refinement/string_refinement.h   |  2 --
 2 files changed, 25 insertions(+), 7 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index a6d1f5637e5..54564ff45d3 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -85,6 +85,18 @@ static void initial_index_set(
 
 exprt simplify_sum(const exprt &f);
 
+static void update_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const std::vector<exprt> &cur);
+
+static void update_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const exprt &formula);
+
 /// Convert exprt to a specific type. Throw bad_cast if conversion
 /// cannot be performed
 /// Generic case doesn't exist, specialize for different types accordingly
@@ -682,7 +694,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   }
 
   initial_index_set(index_set, current_index_set, ns, universal_axioms);
-  update_index_set(cur);
+  update_index_set(index_set, current_index_set, ns, cur);
   cur.clear();
   for (const auto& lemma :
          generate_instantiations(current_index_set, universal_axioms))
@@ -727,7 +739,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       // and instantiating universal formulas with this indices.
       // We will then relaunch the solver with these added lemmas.
       current_index_set.clear();
-      update_index_set(cur);
+      update_index_set(index_set, current_index_set, ns, cur);
       cur.clear();
       for (const auto& lemma :
             generate_instantiations(current_index_set, universal_axioms))
@@ -1626,10 +1638,14 @@ static void initial_index_set(
 
 /// add to the index set all the indices that appear in the formulas
 /// \par parameters: a list of string constraints
-void string_refinementt::update_index_set(const std::vector<exprt> &cur)
+static void update_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const std::vector<exprt> &cur)
 {
   for(const auto &axiom : cur)
-    update_index_set(axiom);
+    update_index_set(index_set, current_index_set, ns, axiom);
 }
 
 /// An expression representing an array of characters can be in the form of an
@@ -1719,7 +1735,11 @@ static void initial_index_set(
 
 /// add to the index set all the indices that appear in the formula
 /// \par parameters: a string constraint
-void string_refinementt::update_index_set(const exprt &formula)
+static void update_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const exprt &formula)
 {
   std::list<exprt> to_process;
   to_process.push_back(formula);
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 84a7bc4a8d0..ec1e04c1231 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -103,8 +103,6 @@ class string_refinementt final: public bv_refinementt
   void debug_model();
 
   void set_char_array_equality(const exprt &lhs, const exprt &rhs);
-  void update_index_set(const exprt &formula);
-  void update_index_set(const std::vector<exprt> &cur);
 
   std::vector<exprt> instantiate_not_contains(
     const string_not_contains_constraintt &axiom);

From 918297cd0e2c35cbe91f9816d50e2eac07a3ac99 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 19:37:21 +0100
Subject: [PATCH 17/28] static concretize length

---
 src/solvers/refinement/string_refinement.cpp | 22 +++++++++++++++-----
 src/solvers/refinement/string_refinement.h   |  1 -
 2 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 54564ff45d3..625136aa5b8 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -514,7 +514,11 @@ void string_refinementt::concretize_results()
 
 /// For each string whose length has been solved, add constants to the map
 /// `found_length`
-void string_refinementt::concretize_lengths()
+void concretize_lengths(
+  std::map<exprt, exprt> &found_length,
+  std::function<exprt(const exprt&)> get,
+  const replace_mapt &symbol_resolve,
+  const std::set<string_exprt> &created_strings)
 {
   for(const auto &pair : symbol_resolve)
   {
@@ -524,9 +528,9 @@ void string_refinementt::concretize_lengths()
       exprt content=str->content();
       replace_expr(symbol_resolve, content);
       found_length[content]=length;
-     }
+    }
   }
-  for(const auto &it : generator.get_created_strings())
+  for(const auto &it : created_strings)
   {
     if(const auto str=expr_cast<string_exprt>(it))
     {
@@ -688,7 +692,11 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     else
     {
       debug() << "check_SAT: the model is correct" << eom;
-      concretize_lengths();
+      concretize_lengths(
+        found_length,
+        [](const exprt& expr){ return expr; },
+        symbol_resolve,
+        generator.get_created_strings());
       return resultt::D_SATISFIABLE;
     }
   }
@@ -729,7 +737,11 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       else
       {
         debug() << "check_SAT: the model is correct" << eom;
-        concretize_lengths();
+        concretize_lengths(
+          found_length,
+          [](const exprt& expr){ return expr; },
+          symbol_resolve,
+          generator.get_created_strings());
         return resultt::D_SATISFIABLE;
       }
 
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index ec1e04c1231..09ffbf22b45 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -109,7 +109,6 @@ class string_refinementt final: public bv_refinementt
 
   void concretize_string(const exprt &expr);
   void concretize_results();
-  void concretize_lengths();
 
   exprt get_array(const exprt &arr, const exprt &size) const;
   exprt get_array(const exprt &arr) const;

From 78303df66813f6f7f981444942abace89f01c05c Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 20:06:54 +0100
Subject: [PATCH 18/28] Static concretize strings, lengths and results

---
 src/solvers/refinement/string_refinement.cpp | 84 ++++++++++++++++----
 src/solvers/refinement/string_refinement.h   |  3 -
 2 files changed, 68 insertions(+), 19 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 625136aa5b8..a8eba1e21c6 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -456,17 +456,27 @@ bool string_refinementt::add_axioms_for_string_assigns(
 /// same value as the next index that is present in the index set.
 /// We do so by traversing the array backward, remembering the
 /// last value that has been initialized.
-void string_refinementt::concretize_string(const exprt &expr)
+static void concretize_string(
+  std::function<exprt(const exprt&)> get,
+  std::map<exprt, exprt> &found_length,
+  std::map<exprt, array_exprt> &found_content,
+  const replace_mapt &symbol_resolve,
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::size_t max_string_length,
+  messaget::mstreamt &stream,
+  const namespacet &ns,
+  const exprt &expr)
 {
   if(const auto str=expr_cast<string_exprt>(expr))
   {
+    const auto& eom=messaget::eom;
     const exprt length=get(str->length());
     exprt content=str->content();
     replace_expr(symbol_resolve, content);
     found_length[content]=length;
     const auto string_length=expr_cast_v<std::size_t>(length);
     INVARIANT(
-      string_length<=generator.max_string_length,
+      string_length<=max_string_length,
       string_refinement_invariantt("string length must be less than the max "
         "length"));
     if(index_set[str->content()].empty())
@@ -485,14 +495,14 @@ void string_refinementt::concretize_string(const exprt &expr)
       }
       else
       {
-        debug() << "concretize_string: ignoring out of bound index: "
-                << from_expr(ns, "", simple_i) << eom;
+        stream << "concretize_string: ignoring out of bound index: "
+               << from_expr(ns, "", simple_i) << eom;
       }
     }
     array_exprt arr(to_array_type(content.type()));
     arr.operands()=fill_in_map_as_vector(map);
-    debug() << "Concretized " << from_expr(ns, "", str->content())
-            << " = " << from_expr(ns, "", arr) << eom;
+    stream << "Concretized " << from_expr(ns, "", str->content())
+           << " = " << from_expr(ns, "", arr) << eom;
     found_content[content]=arr;
   }
 }
@@ -500,16 +510,44 @@ void string_refinementt::concretize_string(const exprt &expr)
 /// 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()
+std::vector<exprt> concretize_results(
+  std::function<exprt(const exprt&)> get,
+  std::map<exprt, exprt> &found_length,
+  std::map<exprt, array_exprt> &found_content,
+  const replace_mapt &symbol_resolve,
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::size_t max_string_length,
+  messaget::mstreamt &stream,
+  const namespacet &ns,
+  const std::set<string_exprt> &created_strings,
+  const std::map<exprt, std::set<exprt>>& current_index_set,
+  const std::vector<string_constraintt> &universal_axioms)
 {
-  for(const auto &it : symbol_resolve)
-    concretize_string(it.second);
-  for(const auto &it : generator.get_created_strings())
-    concretize_string(it);
-  for (const auto& lemma :
-        generate_instantiations(current_index_set, universal_axioms))
-    add_lemma(lemma);
-  display_current_index_set(debug(), ns, current_index_set);
+  for(const auto &it : symbol_resolve) {
+    concretize_string(
+      get,
+      found_length,
+      found_content,
+      symbol_resolve,
+      index_set,
+      max_string_length,
+      stream,
+      ns,
+      it.second);
+  }
+  for(const auto &expr : created_strings) {
+    concretize_string(
+      get,
+      found_length,
+      found_content,
+      symbol_resolve,
+      index_set,
+      max_string_length,
+      stream,
+      ns,
+      expr);
+  }
+  return generate_instantiations(current_index_set, universal_axioms);
 }
 
 /// For each string whose length has been solved, add constants to the map
@@ -763,7 +801,21 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         debug() << "current index set is empty" << eom;
         if(config_.trace)
         {
-          concretize_results();
+          const auto lemmas = concretize_results(
+            [this](const exprt& expr){ return this->get(expr); },
+            found_length,
+            found_content,
+            symbol_resolve,
+            index_set,
+            generator.max_string_length,
+            debug(),
+            ns,
+            generator.get_created_strings(),
+            current_index_set,
+            universal_axioms);
+          for (const auto& lemma : lemmas)
+            add_lemma(lemma);
+          display_current_index_set(debug(), ns, current_index_set);
           return resultt::D_SATISFIABLE;
         }
         else
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 09ffbf22b45..3b64f8cccd7 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -107,9 +107,6 @@ class string_refinementt final: public bv_refinementt
   std::vector<exprt> instantiate_not_contains(
     const string_not_contains_constraintt &axiom);
 
-  void concretize_string(const exprt &expr);
-  void concretize_results();
-
   exprt get_array(const exprt &arr, const exprt &size) const;
   exprt get_array(const exprt &arr) const;
 

From 229568af7cb413d793344c348511df4cd011af37 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 20:33:58 +0100
Subject: [PATCH 19/28] static Instantiate not contains

---
 src/solvers/refinement/string_refinement.cpp | 30 +++++++++++++-------
 src/solvers/refinement/string_refinement.h   |  3 --
 2 files changed, 20 insertions(+), 13 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index a8eba1e21c6..0e8ab786e01 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -97,6 +97,11 @@ static void update_index_set(
   const namespacet &ns,
   const exprt &formula);
 
+static std::vector<exprt> instantiate_not_contains(
+  const string_not_contains_constraintt &axiom,
+  const std::map<exprt, std::set<exprt>>& index_set,
+  const string_constraint_generatort &generator);
+
 /// Convert exprt to a specific type. Throw bad_cast if conversion
 /// cannot be performed
 /// Generic case doesn't exist, specialize for different types accordingly
@@ -832,7 +837,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       {
         debug()<< "constraint " << i << eom;
         const std::vector<exprt> lemmas=
-          instantiate_not_contains(not_contains_axioms[i]);
+          instantiate_not_contains(
+            not_contains_axioms[i], index_set, generator);
         for(const exprt &lemma : lemmas)
           add_lemma(lemma);
       }
@@ -1902,19 +1908,23 @@ static exprt instantiate(
 /// substituting the quantifiers and generating axioms.
 /// \param [in] axiom: the axiom to instantiate
 /// \return the lemmas produced through instantiation
-std::vector<exprt> string_refinementt::instantiate_not_contains(
-  const string_not_contains_constraintt &axiom)
+static std::vector<exprt> instantiate_not_contains(
+  const string_not_contains_constraintt &axiom,
+  const std::map<exprt, std::set<exprt>>& index_set,
+  const string_constraint_generatort &generator)
 {
   const string_exprt s0=to_string_expr(axiom.s0());
   const string_exprt s1=to_string_expr(axiom.s1());
 
-  debug() << "instantiate not contains " << from_expr(ns, "", s0) << " : "
-          << from_expr(ns, "", s1) << eom;
-  const expr_sett index_set0=index_set[s0.content()];
-  const expr_sett index_set1=index_set[s1.content()];
-
-  return ::instantiate_not_contains(
-    axiom, index_set0, index_set1, generator);
+  // debug() << "instantiate not contains " << from_expr(ns, "", s0) << " : "
+  //         << from_expr(ns, "", s1) << eom;
+  const auto& i0=index_set.find(s0.content());
+  const auto& i1=index_set.find(s1.content());
+  if (i0 != index_set.end() && i1 != index_set.end()) {
+    return ::instantiate_not_contains(
+      axiom, i0->second, i1->second, generator);
+  }
+  return { };
 }
 
 /// Replace array-lists by 'with' expressions.
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 3b64f8cccd7..cdde06f26c2 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -104,9 +104,6 @@ class string_refinementt final: public bv_refinementt
 
   void set_char_array_equality(const exprt &lhs, const exprt &rhs);
 
-  std::vector<exprt> instantiate_not_contains(
-    const string_not_contains_constraintt &axiom);
-
   exprt get_array(const exprt &arr, const exprt &size) const;
   exprt get_array(const exprt &arr) const;
 

From 7f11ccfdf04405e86e543720cadc4364cf6980d0 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 20:42:33 +0100
Subject: [PATCH 20/28] static set_char_array_equality

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

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 0e8ab786e01..b453ef64e1d 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -336,22 +336,24 @@ void add_symbol_to_symbol_map(
 
 /// add axioms if the rhs is a character array
 /// \par parameters: the rhs and lhs of an equality over character arrays
-void string_refinementt::set_char_array_equality(
-  const exprt &lhs, const exprt &rhs)
+std::vector<exprt> set_char_array_equality(const exprt &lhs, const exprt &rhs)
 {
   PRECONDITION(lhs.id()==ID_symbol);
 
   if(rhs.id()==ID_array && rhs.type().id()==ID_array)
   {
+    std::vector<exprt> lemmas;
     const typet &index_type=to_array_type(rhs.type()).size().type();
     for(size_t i=0, ilim=rhs.operands().size(); i!=ilim; ++i)
     {
       // Introduce axioms to map symbolic rhs to its char array.
       index_exprt arraycell(rhs, from_integer(i, index_type));
       equal_exprt arrayeq(arraycell, rhs.operands()[i]);
-      add_lemma(arrayeq, false);
+      lemmas.push_back(arrayeq);
     }
+    return lemmas;
   }
+  return { };
   // At least for Java (as it is currently pre-processed), we need not consider
   // other cases, because all character arrays find themselves on the rhs of an
   // equality. Note that this might not be the case for other languages.
@@ -402,7 +404,9 @@ bool string_refinementt::add_axioms_for_string_assigns(
 {
   if(is_char_array(ns, rhs.type()))
   {
-    set_char_array_equality(lhs, rhs);
+    for (const auto& lemma : set_char_array_equality(lhs, rhs))
+      add_lemma(lemma, false);
+
     if(rhs.id() == ID_symbol || rhs.id() == ID_array)
     {
       add_symbol_to_symbol_map(
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index cdde06f26c2..b8da7793933 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -102,8 +102,6 @@ class string_refinementt final: public bv_refinementt
 
   void debug_model();
 
-  void set_char_array_equality(const exprt &lhs, const exprt &rhs);
-
   exprt get_array(const exprt &arr, const exprt &size) const;
   exprt get_array(const exprt &arr) const;
 

From f5c1b2901381b02da0f4f595d6ee242c4ddefc0b Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 20:55:56 +0100
Subject: [PATCH 21/28] static get_array

---
 src/solvers/refinement/string_refinement.cpp | 51 ++++++++++++++++----
 src/solvers/refinement/string_refinement.h   |  3 --
 2 files changed, 41 insertions(+), 13 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index b453ef64e1d..8d2361628b8 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -102,6 +102,10 @@ static std::vector<exprt> instantiate_not_contains(
   const std::map<exprt, std::set<exprt>>& index_set,
   const string_constraint_generatort &generator);
 
+static exprt get_array(
+  std::function<exprt(const exprt&)> super_get,
+  const exprt &arr);
+
 /// Convert exprt to a specific type. Throw bad_cast if conversion
 /// cannot be performed
 /// Generic case doesn't exist, specialize for different types accordingly
@@ -902,10 +906,15 @@ void string_refinementt::add_lemma(
 /// \par parameters: an expression representing an array and an expression
 /// representing an integer
 /// \return an array expression or an array_of_exprt
-exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const
+static exprt get_array(
+  std::function<exprt(const exprt&)> super_get,
+  const namespacet &ns,
+  std::size_t max_string_length,
+  const exprt &arr,
+  const exprt &size)
 {
-  exprt arr_val=simplify_expr(get_array(arr), ns);
-  exprt size_val=supert::get(size);
+  exprt arr_val=simplify_expr(get_array(super_get, arr), ns);
+  exprt size_val=super_get(size);
   size_val=simplify_expr(size_val, ns);
   typet char_type=arr.type().subtype();
   typet index_type=size.type();
@@ -933,7 +942,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>generator.max_string_length)
+  if(n>max_string_length)
   {
 #if 0
     debug() << "(sr::get_array) long string (size=" << n << ")" << eom;
@@ -984,9 +993,11 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const
 /// get a model of an array of unknown size and infer the size if possible
 /// \par parameters: an expression representing an array
 /// \return an expression
-exprt string_refinementt::get_array(const exprt &arr) const
+static exprt get_array(
+  std::function<exprt(const exprt&)> super_get,
+  const exprt &arr)
 {
-  exprt arr_model=supert::get(arr);
+  exprt arr_model=super_get(arr);
   if(arr_model.id()==ID_array)
   {
     array_typet &arr_type=to_array_type(arr_model.type());
@@ -1016,6 +1027,9 @@ std::string string_refinementt::string_of_array(const array_exprt &arr)
 /// solver to constant expressions given by the current model
 void string_refinementt::debug_model()
 {
+  const auto super_get = [this](const exprt& expr) {
+    return supert::get(expr);
+  };
   const std::string indent("  ");
   for(auto it : symbol_resolve)
   {
@@ -1031,7 +1045,11 @@ void string_refinementt::debug_model()
 
       exprt len=supert::get(elength);
       len=simplify_expr(len, ns);
-      const exprt arr=get_array(econtent, len);
+      const exprt arr=get_array(
+        super_get,
+        ns,
+        generator.max_string_length,
+        econtent, len);
       if(arr.id()==ID_array)
         debug() << indent << indent << "as_string: \""
                 << string_of_array(to_array_expr(arr)) << "\"\n";
@@ -1053,7 +1071,7 @@ void string_refinementt::debug_model()
       debug() << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n";
       debug() << indent << indent << "resolved: "
               << from_expr(ns, "", arr) << "\n";
-      exprt arr_model=get_array(arr);
+      exprt arr_model=get_array(super_get, arr);
       debug() << indent << indent << "char_array: "
               << from_expr(ns, "", arr_model) << eom;
     }
@@ -1977,6 +1995,9 @@ exprt substitute_array_lists(exprt expr, size_t string_max_length)
 /// \return an expression
 exprt string_refinementt::get(const exprt &expr) const
 {
+  const auto super_get = [this](const exprt& expr) {
+    return supert::get(expr);
+  };
   exprt ecopy(expr);
   replace_expr(symbol_resolve, ecopy);
   if(is_char_array(ns, ecopy.type()))
@@ -1987,7 +2008,12 @@ exprt string_refinementt::get(const exprt &expr) const
 
     auto it=found_length.find(ecopy);
     if(it!=found_length.end())
-      return get_array(ecopy, it->second);
+      return get_array(
+        super_get,
+        ns,
+        generator.max_string_length,
+        ecopy,
+        it->second);
   }
   else if(ecopy.id()==ID_struct)
   {
@@ -1996,7 +2022,12 @@ exprt string_refinementt::get(const exprt &expr) const
       const exprt &content=string->content();
       const exprt &length=string->length();
 
-      const exprt arr=get_array(content, length);
+      const exprt arr=get_array(
+        super_get,
+        ns,
+        generator.max_string_length,
+        content,
+        length);
       ecopy=string_exprt(length, arr, string->type());
     }
   }
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index b8da7793933..f35d9e4cd2a 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -102,9 +102,6 @@ class string_refinementt final: public bv_refinementt
 
   void debug_model();
 
-  exprt get_array(const exprt &arr, const exprt &size) const;
-  exprt get_array(const exprt &arr) const;
-
   std::string string_of_array(const array_exprt &arr);
 };
 #endif

From 1531f0e1922a322f8b37f9c04c4e7971e531ee26 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 21:27:27 +0100
Subject: [PATCH 22/28] static debug_model

---
 src/solvers/refinement/string_refinement.cpp | 70 ++++++++++++--------
 src/solvers/refinement/string_refinement.h   |  4 --
 2 files changed, 42 insertions(+), 32 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 8d2361628b8..618c7da8a46 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -1011,7 +1011,7 @@ static exprt get_array(
 /// should only be used for debugging.
 /// \par parameters: a constant array expression and a integer expression
 /// \return a string
-std::string string_refinementt::string_of_array(const array_exprt &arr)
+static std::string string_of_array(const array_exprt &arr)
 {
   unsigned n;
   if(arr.type().id()!=ID_array)
@@ -1025,39 +1025,44 @@ std::string string_refinementt::string_of_array(const array_exprt &arr)
 
 /// Display part of the current model by mapping the variables created by the
 /// solver to constant expressions given by the current model
-void string_refinementt::debug_model()
+void debug_model(
+  const replace_mapt &symbol_resolve,
+  messaget::mstreamt &stream,
+  const namespacet &ns,
+  std::size_t max_string_length,
+  std::function<exprt(const exprt&)> super_get,
+  const std::vector<symbol_exprt> &boolean_symbols,
+  const std::vector<symbol_exprt> &index_symbols)
 {
-  const auto super_get = [this](const exprt& expr) {
-    return supert::get(expr);
-  };
+  const auto eom = messaget::eom;
   const std::string indent("  ");
   for(auto it : symbol_resolve)
   {
     if(const auto refined=expr_cast<string_exprt>(it.second))
     {
-      debug() << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n";
-      debug() << indent << indent << "in_map: "
-              << from_expr(ns, "", *refined) << eom;
-      debug() << indent << indent << "resolved: "
-              << from_expr(ns, "", *refined) << eom;
+      stream << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n";
+      stream << indent << indent << "in_map: "
+             << from_expr(ns, "", *refined) << eom;
+      stream << indent << indent << "resolved: "
+             << from_expr(ns, "", *refined) << eom;
       const exprt &econtent=refined->content();
       const exprt &elength=refined->length();
 
-      exprt len=supert::get(elength);
+      exprt len=super_get(elength);
       len=simplify_expr(len, ns);
       const exprt arr=get_array(
         super_get,
         ns,
-        generator.max_string_length,
+        max_string_length,
         econtent, len);
       if(arr.id()==ID_array)
-        debug() << indent << indent << "as_string: \""
-                << string_of_array(to_array_expr(arr)) << "\"\n";
+        stream << indent << indent << "as_string: \""
+               << string_of_array(to_array_expr(arr)) << "\"\n";
       else
-        debug() << indent << indent << "as_char_array: "
-                << from_expr(ns, "", arr) << "\n";
+        stream << indent << indent << "as_char_array: "
+               << from_expr(ns, "", arr) << "\n";
 
-      debug() << indent << indent << "size: " << from_expr(ns, "", len) << eom;
+      stream << indent << indent << "size: " << from_expr(ns, "", len) << eom;
     }
     else
     {
@@ -1068,25 +1073,25 @@ void string_refinementt::debug_model()
           "handled"));
       exprt arr=it.second;
       replace_expr(symbol_resolve, arr);
-      debug() << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n";
-      debug() << indent << indent << "resolved: "
+      stream << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n";
+      stream << indent << indent << "resolved: "
               << from_expr(ns, "", arr) << "\n";
       exprt arr_model=get_array(super_get, arr);
-      debug() << indent << indent << "char_array: "
-              << from_expr(ns, "", arr_model) << eom;
+      stream << indent << indent << "char_array: "
+             << from_expr(ns, "", arr_model) << eom;
     }
   }
 
-  for(const auto it : generator.get_boolean_symbols())
+  for(const auto it : boolean_symbols)
   {
-      debug() << " - " << it.get_identifier() << ": "
-              << from_expr(ns, "", supert::get(it)) << eom;
+      stream << " - " << it.get_identifier() << ": "
+             << from_expr(ns, "", super_get(it)) << eom;
   }
 
-  for(const auto it : generator.get_index_symbols())
+  for(const auto it : index_symbols)
   {
-     debug() << " - " << it.get_identifier() << ": "
-             << from_expr(ns, "", supert::get(it)) << eom;
+     stream << " - " << it.get_identifier() << ": "
+            << from_expr(ns, "", super_get(it)) << eom;
   }
 }
 
@@ -1382,7 +1387,16 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
 {
   const auto eom = messaget::eom;
   stream << "string_refinementt::check_axioms:" << eom;
-  // debug_model();
+
+  #if 0
+  debug_model(symbol_resolve,
+    stream,
+    ns,
+    max_string_length,
+    get,
+    generator.get_boolean_symbols(),
+    generator.get_index_symbols());
+  #endif
 
   // Maps from indexes of violated universal axiom to a witness of violation
   std::map<size_t, exprt> violated;
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index f35d9e4cd2a..a182afeb86f 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -99,9 +99,5 @@ class string_refinementt final: public bv_refinementt
                  bool add_to_index_set=true);
 
   bool add_axioms_for_string_assigns(const exprt &lhs, const exprt &rhs);
-
-  void debug_model();
-
-  std::string string_of_array(const array_exprt &arr);
 };
 #endif

From d03866d1f315d48276d4c41d2808af5cb8f5bf50 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 22:59:46 +0100
Subject: [PATCH 23/28] static add axioms for string assings

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

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 618c7da8a46..b300a3ea140 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -403,14 +403,17 @@ static bool is_char_array(const namespacet &ns, const typet &type)
 /// \param rhs: right and side of the equality
 /// \return true if the assignemnt needs to be handled by the parent class
 ///         via `set_to`
-bool string_refinementt::add_axioms_for_string_assigns(
-  const exprt &lhs, const exprt &rhs)
+bool add_axioms_for_string_assigns(
+  replace_mapt& symbol_resolve,
+  std::map<exprt, std::list<exprt>> &reverse_symbol_resolve,
+  string_constraint_generatort& generator,
+  messaget::mstreamt &stream,
+  const namespacet &ns,
+  const exprt &lhs,
+  const exprt &rhs)
 {
   if(is_char_array(ns, rhs.type()))
   {
-    for (const auto& lemma : set_char_array_equality(lhs, rhs))
-      add_lemma(lemma, false);
-
     if(rhs.id() == ID_symbol || rhs.id() == ID_array)
     {
       add_symbol_to_symbol_map(
@@ -440,7 +443,8 @@ bool string_refinementt::add_axioms_for_string_assigns(
     }
     else
     {
-      warning() << "ignoring char array " << from_expr(ns, "", rhs) << eom;
+      stream << "ignoring char array " << from_expr(ns, "", rhs)
+             << messaget::eom;
       return true;
     }
   }
@@ -651,8 +655,24 @@ void string_refinementt::set_to(const exprt &expr, bool value)
       }
     }
 
-    if(value && !add_axioms_for_string_assigns(lhs, subst_rhs))
-      return;
+    if(value)
+    {
+      if(is_char_array(ns, rhs.type()))
+      {
+        for (const auto& lemma : set_char_array_equality(lhs, rhs))
+          add_lemma(lemma, false);
+      }
+      const bool not_handled=add_axioms_for_string_assigns(
+        symbol_resolve,
+        reverse_symbol_resolve,
+        generator,
+        warning(),
+        ns,
+        lhs,
+        subst_rhs);
+      if (!not_handled)
+        return;
+    }
 
     // Push the substituted equality to the list of axioms to be given to
     // supert::set_to.
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index a182afeb86f..555ea4bc3de 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -97,7 +97,5 @@ class string_refinementt final: public bv_refinementt
   void add_lemma(const exprt &lemma,
                  bool simplify=true,
                  bool add_to_index_set=true);
-
-  bool add_axioms_for_string_assigns(const exprt &lhs, const exprt &rhs);
 };
 #endif

From bee20f1da5dbe6fe48665f56680e15ab0a5a739d Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Sat, 16 Sep 2017 08:59:30 +0100
Subject: [PATCH 24/28] Remove unused add_lemma parameter

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

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index b300a3ea140..d9fab2500fa 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -896,13 +896,12 @@ bvt string_refinementt::convert_bool_bv(const exprt &boole, const exprt &orig)
 /// \par parameters: a lemma and Boolean value stating whether the lemma should
 /// be added to the index set.
 void string_refinementt::add_lemma(
-  const exprt &lemma, bool _simplify, bool add_to_index_set)
+  const exprt &lemma, bool _simplify)
 {
   if(!seen_instances.insert(lemma).second)
     return;
 
-  if(add_to_index_set)
-    cur.push_back(lemma);
+  cur.push_back(lemma);
 
   exprt simple_lemma=lemma;
   if(_simplify)
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 555ea4bc3de..83957096152 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -94,8 +94,6 @@ class string_refinementt final: public bv_refinementt
   // Content of char arrays found during concretization
   std::map<exprt, array_exprt> found_content;
 
-  void add_lemma(const exprt &lemma,
-                 bool simplify=true,
-                 bool add_to_index_set=true);
+  void add_lemma(const exprt &lemma, bool simplify=true);
 };
 #endif

From 9b8a025ba03df98e6047ab466ac552a8c0be3590 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 19 Sep 2017 09:00:10 +0100
Subject: [PATCH 25/28] Fix get lambdas

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

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index d9fab2500fa..3aafec31518 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -737,6 +737,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   found_length.clear();
   found_content.clear();
 
+  const auto get = [this](const exprt& expr) { return this->get(expr); };
+
   // Initial try without index set
   decision_proceduret::resultt res=supert::dec_solve();
   if(res==resultt::D_SATISFIABLE)
@@ -747,7 +749,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       universal_axioms,
       not_contains_axioms,
       generator,
-      [this](const exprt& expr){ return this->get(expr); },
+      get,
       debug(),
       ns,
       generator.max_string_length,
@@ -765,7 +767,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       debug() << "check_SAT: the model is correct" << eom;
       concretize_lengths(
         found_length,
-        [](const exprt& expr){ return expr; },
+        get,
         symbol_resolve,
         generator.get_created_strings());
       return resultt::D_SATISFIABLE;
@@ -792,7 +794,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         universal_axioms,
         not_contains_axioms,
         generator,
-        [this](const exprt& expr){ return this->get(expr); },
+        get,
         debug(),
         ns,
         generator.max_string_length,
@@ -810,7 +812,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         debug() << "check_SAT: the model is correct" << eom;
         concretize_lengths(
           found_length,
-          [](const exprt& expr){ return expr; },
+          get,
           symbol_resolve,
           generator.get_created_strings());
         return resultt::D_SATISFIABLE;
@@ -835,7 +837,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         if(config_.trace)
         {
           const auto lemmas = concretize_results(
-            [this](const exprt& expr){ return this->get(expr); },
+            get,
             found_length,
             found_content,
             symbol_resolve,

From b544a4b98f973561faa0e8734fbca6d97ded0b6b Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 19 Sep 2017 09:15:12 +0100
Subject: [PATCH 26/28] Fix unit test build

---
 src/solvers/refinement/string_refinement.cpp   |  5 -----
 src/solvers/refinement/string_refinement.h     |  3 +++
 .../instantiate_not_contains.cpp               | 18 ++++++------------
 3 files changed, 9 insertions(+), 17 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 3aafec31518..3c34a84f4f6 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -42,11 +42,6 @@ static exprt instantiate(
   const string_constraintt &axiom, const exprt &str, const exprt &val);
 static bool is_char_array(const namespacet &ns, const typet &type);
 
-exprt substitute_array_lists(exprt expr, size_t string_max_length);
-
-exprt concretize_arrays_in_expression(
-  exprt expr, std::size_t string_max_length);
-
 static bool is_valid_string_constraint(
   messaget::mstreamt& stream,
   const namespacet& ns,
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 83957096152..632e2bb5f83 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -96,4 +96,7 @@ class string_refinementt final: public bv_refinementt
 
   void add_lemma(const exprt &lemma, bool simplify=true);
 };
+
+exprt substitute_array_lists(exprt expr, size_t string_max_length);
+exprt concretize_arrays_in_expression(exprt expr, std::size_t string_max_length);
 #endif
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 ed72dc6aa0c..a0ecd2e3f5c 100644
--- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -154,8 +154,7 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     namespacet empty_ns(symtab);
     string_constraint_generatort::infot info;
-    info.ns=&empty_ns;
-    string_constraint_generatort generator(info);
+    string_constraint_generatort generator(info, ns);
     exprt res=generator.add_axioms_for_function_application(func);
     std::string axioms;
     std::vector<string_not_contains_constraintt> nc_axioms;
@@ -242,8 +241,7 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     namespacet empty_ns(symtab);
     string_constraint_generatort::infot info;
-    info.ns=&empty_ns;
-    string_constraint_generatort generator(info);
+    string_constraint_generatort generator(info, ns);
     generator.witness[vacuous]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -301,8 +299,7 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     namespacet ns(symtab);
     string_constraint_generatort::infot info;
-    info.ns=&ns;
-    string_constraint_generatort generator(info);
+    string_constraint_generatort generator(info, ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -361,8 +358,7 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     namespacet empty_ns(symtab);
     string_constraint_generatort::infot info;
-    info.ns=&empty_ns;
-    string_constraint_generatort generator(info);
+    string_constraint_generatort generator(info, ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -423,8 +419,7 @@ SCENARIO("instantiate_not_contains",
     namespacet empty_ns(symtab);
 
     string_constraint_generatort::infot info;
-    info.ns=&empty_ns;
-    string_constraint_generatort generator(info);
+    string_constraint_generatort generator(info, ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 
@@ -483,8 +478,7 @@ SCENARIO("instantiate_not_contains",
     symbol_tablet symtab;
     namespacet empty_ns(symtab);
     string_constraint_generatort::infot info;
-    info.ns=&empty_ns;
-    string_constraint_generatort generator(info);
+    string_constraint_generatort generator(info, ns);
     generator.witness[trivial]=
       generator.fresh_symbol("w", t.witness_type());
 

From 751e8f51196a62eb64658ba1b8c90b102b54ae9f Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 19 Sep 2017 10:00:23 +0100
Subject: [PATCH 27/28] Adhere to lintage

---
 src/solvers/refinement/bv_refinement.h       |  2 +-
 src/solvers/refinement/string_refinement.cpp | 44 +++++++++++---------
 src/solvers/refinement/string_refinement.h   |  6 ++-
 3 files changed, 30 insertions(+), 22 deletions(-)

diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h
index 0c2b5e22b3a..99475efd8ad 100644
--- a/src/solvers/refinement/bv_refinement.h
+++ b/src/solvers/refinement/bv_refinement.h
@@ -32,7 +32,7 @@ class bv_refinementt:public bv_pointerst
     bool refine_arithmetic=true;
   };
 public:
-  struct infot : public configt
+  struct infot:public configt
   {
     const namespacet *ns=nullptr;
     propt *prop=nullptr;
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 3c34a84f4f6..c7b349a0b12 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -139,7 +139,8 @@ optionalt<string_exprt> expr_cast<string_exprt>(const exprt& expr)
 }
 
 template<typename T>
-T expr_cast_v(const exprt& expr) {
+T expr_cast_v(const exprt& expr)
+{
   const auto maybe=expr_cast<T>(expr);
   INVARIANT(maybe, "Bad conversion");
   return *maybe;
@@ -535,7 +536,8 @@ std::vector<exprt> concretize_results(
   const std::map<exprt, std::set<exprt>>& current_index_set,
   const std::vector<string_constraintt> &universal_axioms)
 {
-  for(const auto &it : symbol_resolve) {
+  for(const auto &it : symbol_resolve)
+  {
     concretize_string(
       get,
       found_length,
@@ -547,7 +549,8 @@ std::vector<exprt> concretize_results(
       ns,
       it.second);
   }
-  for(const auto &expr : created_strings) {
+  for(const auto &expr : created_strings)
+  {
     concretize_string(
       get,
       found_length,
@@ -654,7 +657,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)
     {
       if(is_char_array(ns, rhs.type()))
       {
-        for (const auto& lemma : set_char_array_equality(lhs, rhs))
+        for(const auto& lemma : set_char_array_equality(lhs, rhs))
           add_lemma(lemma, false);
       }
       const bool not_handled=add_axioms_for_string_assigns(
@@ -665,7 +668,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)
         ns,
         lhs,
         subst_rhs);
-      if (!not_handled)
+      if(!not_handled)
         return;
     }
 
@@ -753,7 +756,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       symbol_resolve);
     if(!success)
     {
-      for (const auto& lemma : lemmas)
+      for(const auto& lemma : lemmas)
         add_lemma(lemma);
       debug() << "check_SAT: got SAT but the model is not correct" << eom;
     }
@@ -772,8 +775,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   initial_index_set(index_set, current_index_set, ns, universal_axioms);
   update_index_set(index_set, current_index_set, ns, cur);
   cur.clear();
-  for (const auto& lemma :
-         generate_instantiations(current_index_set, universal_axioms))
+  for(const auto& lemma :
+        generate_instantiations(current_index_set, universal_axioms))
     add_lemma(lemma);
   display_current_index_set(debug(), ns, current_index_set);
 
@@ -781,7 +784,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   {
     decision_proceduret::resultt res=supert::dec_solve();
 
-    if (res == resultt::D_SATISFIABLE)
+    if(res==resultt::D_SATISFIABLE)
     {
       bool success;
       std::vector<exprt> lemmas;
@@ -798,7 +801,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         symbol_resolve);
       if(!success)
       {
-        for (const auto& lemma : lemmas)
+        for(const auto& lemma : lemmas)
           add_lemma(lemma);
         debug() << "check_SAT: got SAT but the model is not correct" << eom;
       }
@@ -821,7 +824,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       current_index_set.clear();
       update_index_set(index_set, current_index_set, ns, cur);
       cur.clear();
-      for (const auto& lemma :
+      for(const auto& lemma :
             generate_instantiations(current_index_set, universal_axioms))
         add_lemma(lemma);
       display_current_index_set(debug(), ns, current_index_set);
@@ -843,7 +846,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
             generator.get_created_strings(),
             current_index_set,
             universal_axioms);
-          for (const auto& lemma : lemmas)
+          for(const auto& lemma : lemmas)
             add_lemma(lemma);
           display_current_index_set(debug(), ns, current_index_set);
           return resultt::D_SATISFIABLE;
@@ -867,7 +870,9 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         for(const exprt &lemma : lemmas)
           add_lemma(lemma);
       }
-    } else {
+    }
+    else
+    {
       debug() << "check_SAT: default return " << static_cast<int>(res) << eom;
       return res;
     }
@@ -1923,7 +1928,8 @@ class find_index_visitort: public const_expr_visitort
 /// \param [in] str: the string which must be indexed
 /// \param [in] qvar: the universal variable that must be in the index
 /// \return an index expression in `expr` on `str` containing `qvar`
-static exprt find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
+static exprt find_index(
+  const exprt &expr, const exprt &str, const symbol_exprt &qvar)
 {
   find_index_visitort v(str, qvar);
   expr.visit(v);
@@ -1972,7 +1978,8 @@ static std::vector<exprt> instantiate_not_contains(
   //         << from_expr(ns, "", s1) << eom;
   const auto& i0=index_set.find(s0.content());
   const auto& i1=index_set.find(s1.content());
-  if (i0 != index_set.end() && i1 != index_set.end()) {
+  if(i0!=index_set.end() && i1!=index_set.end())
+  {
     return ::instantiate_not_contains(
       axiom, i0->second, i1->second, generator);
   }
@@ -2025,9 +2032,8 @@ exprt substitute_array_lists(exprt expr, size_t string_max_length)
 /// \return an expression
 exprt string_refinementt::get(const exprt &expr) const
 {
-  const auto super_get = [this](const exprt& expr) {
-    return supert::get(expr);
-  };
+  const auto super_get=[this](const exprt& expr)
+  { return supert::get(expr); };
   exprt ecopy(expr);
   replace_expr(symbol_resolve, ecopy);
   if(is_char_array(ns, ecopy.type()))
@@ -2047,7 +2053,7 @@ exprt string_refinementt::get(const exprt &expr) const
   }
   else if(ecopy.id()==ID_struct)
   {
-    if (const auto string=expr_cast<string_exprt>(ecopy))
+    if(const auto string=expr_cast<string_exprt>(ecopy))
     {
       const exprt &content=string->content();
       const exprt &length=string->length();
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 632e2bb5f83..863b4e61929 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -32,7 +32,8 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 class string_refinementt final: public bv_refinementt
 {
 private:
-  struct configt {
+  struct configt
+  {
     unsigned refinement_bound=0;
     /// Make non-deterministic character arrays have at least one character
     bool string_non_empty=false;
@@ -98,5 +99,6 @@ class string_refinementt final: public bv_refinementt
 };
 
 exprt substitute_array_lists(exprt expr, size_t string_max_length);
-exprt concretize_arrays_in_expression(exprt expr, std::size_t string_max_length);
+exprt concretize_arrays_in_expression(
+  exprt expr, std::size_t string_max_length);
 #endif

From 05d5a9be4163a0dbb6daec844dabfb5316925e09 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 19 Sep 2017 15:24:04 +0100
Subject: [PATCH 28/28] Address commenters' suggestions

---
 src/solvers/refinement/bv_refinement_loop.cpp |   2 +-
 .../refinement/string_constraint_generator.h  |   8 +-
 .../string_constraint_generator_main.cpp      |  16 +
 src/solvers/refinement/string_refinement.cpp  | 326 ++++++++----------
 src/solvers/refinement/string_refinement.h    |   8 +-
 5 files changed, 179 insertions(+), 181 deletions(-)

diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp
index 8b7f373a49c..c49875d152f 100644
--- a/src/solvers/refinement/bv_refinement_loop.cpp
+++ b/src/solvers/refinement/bv_refinement_loop.cpp
@@ -45,7 +45,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve()
     {
       xmlt xml("refinement-iteration");
       xml.data=std::to_string(iteration);
-      std::cout << xml << '\n';
+      status() << xml << '\n';
     }
 
     switch(prop_solve())
diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index 4e04db53d56..ff5b4040005 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -46,8 +46,7 @@ class string_constraint_generatort final
     bool string_printable=false;
   };
 
-  explicit string_constraint_generatort(
-    const infot& info, const namespacet& ns);
+  string_constraint_generatort(const infot& info, const namespacet& ns);
 
   /// Axioms are of three kinds: universally quantified string constraint,
   /// not contains string constraints and simple formulas.
@@ -81,6 +80,11 @@ class string_constraint_generatort final
 
   symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type);
 
+  /// remove functions applications and create the necessary axioms
+  /// \par parameters: an expression containing function applications
+  /// \return an expression containing no function application
+  exprt substitute_function_applications(const exprt& expr);
+
 private:
   symbol_exprt fresh_boolean(const irep_idt &prefix);
   string_exprt fresh_string(const refined_string_typet &type);
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index e6c156cd482..2eca6940c7b 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -628,3 +628,19 @@ exprt string_constraint_generatort::add_axioms_for_to_char_array(
   string_exprt str=get_string_expr(args(f, 1)[0]);
   return str.content();
 }
+
+exprt string_constraint_generatort::substitute_function_applications(
+  const exprt &expr)
+{
+  exprt copy=expr;
+  for(exprt &operand : copy.operands())
+    operand=substitute_function_applications(exprt(operand));
+
+  if(copy.id()==ID_function_application)
+  {
+    function_application_exprt f=to_function_application_expr(copy);
+    return this->add_axioms_for_function_application(f);
+  }
+
+  return copy;
+}
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index c7b349a0b12..483eb07ac30 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -39,32 +39,34 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 static exprt substitute_array_with_expr(const exprt &expr, const exprt &index);
 
 static exprt instantiate(
-  const string_constraintt &axiom, const exprt &str, const exprt &val);
+  messaget::mstreamt &stream,
+  const string_constraintt &axiom,
+  const exprt &str,
+  const exprt &val);
 static bool is_char_array(const namespacet &ns, const typet &type);
 
 static bool is_valid_string_constraint(
-  messaget::mstreamt& stream,
-  const namespacet& ns,
+  messaget::mstreamt &stream,
+  const namespacet &ns,
   const string_constraintt &expr);
 
-static bool is_axiom_sat(
-  const namespacet& ns,
+static optionalt<exprt> find_counter_example(
+  const namespacet &ns,
   ui_message_handlert::uit ui,
   const exprt &axiom,
-  const symbol_exprt& var,
-  exprt &witness);
+  const symbol_exprt &var);
 
 static std::pair<bool, std::vector<exprt>> check_axioms(
   const std::vector<string_constraintt> &universal_axioms,
   const std::vector<string_not_contains_constraintt> &not_contains_axioms,
   string_constraint_generatort &generator,
-  std::function<exprt(const exprt&)> get,
+  std::function<exprt(const exprt &)> get,
   messaget::mstreamt &stream,
   const namespacet &ns,
   std::size_t max_string_length,
   bool use_counter_example,
   ui_message_handlert::uit ui,
-  const replace_mapt& symbol_resolve);
+  const replace_mapt &symbol_resolve);
 
 static void initial_index_set(
   std::map<exprt, std::set<exprt>> &index_set,
@@ -93,12 +95,14 @@ static void update_index_set(
   const exprt &formula);
 
 static std::vector<exprt> instantiate_not_contains(
+  messaget::mstreamt &stream,
+  const namespacet &ns,
   const string_not_contains_constraintt &axiom,
-  const std::map<exprt, std::set<exprt>>& index_set,
+  const std::map<exprt, std::set<exprt>> &index_set,
   const string_constraint_generatort &generator);
 
 static exprt get_array(
-  std::function<exprt(const exprt&)> super_get,
+  std::function<exprt(const exprt &)> super_get,
   const exprt &arr);
 
 /// Convert exprt to a specific type. Throw bad_cast if conversion
@@ -106,10 +110,10 @@ static exprt get_array(
 /// Generic case doesn't exist, specialize for different types accordingly
 /// TODO: this should go to util
 template<typename T>
-optionalt<T> expr_cast(const exprt&);
+optionalt<T> expr_cast(const exprt &);
 
 template<>
-optionalt<mp_integer> expr_cast<mp_integer>(const exprt& expr)
+optionalt<mp_integer> expr_cast<mp_integer>(const exprt &expr)
 {
   mp_integer out;
   if(to_integer(expr, out))
@@ -118,7 +122,7 @@ optionalt<mp_integer> expr_cast<mp_integer>(const exprt& expr)
 }
 
 template<>
-optionalt<std::size_t> expr_cast<std::size_t>(const exprt& expr)
+optionalt<std::size_t> expr_cast<std::size_t>(const exprt &expr)
 {
   if(const auto tmp=expr_cast<mp_integer>(expr))
   {
@@ -129,7 +133,7 @@ optionalt<std::size_t> expr_cast<std::size_t>(const exprt& expr)
 }
 
 template<>
-optionalt<string_exprt> expr_cast<string_exprt>(const exprt& expr)
+optionalt<string_exprt> expr_cast<string_exprt>(const exprt &expr)
 {
   if(is_refined_string_type(expr.type()))
   {
@@ -139,7 +143,7 @@ optionalt<string_exprt> expr_cast<string_exprt>(const exprt& expr)
 }
 
 template<typename T>
-T expr_cast_v(const exprt& expr)
+T expr_cast_v(const exprt &expr)
 {
   const auto maybe=expr_cast<T>(expr);
   INVARIANT(maybe, "Bad conversion");
@@ -163,7 +167,7 @@ static std::vector<T> fill_in_map_as_vector(
     for(auto it=index_value.rbegin(); it!=index_value.rend(); ++it)
     {
       const std::size_t index=it->first;
-      const T value=it->second;
+      const T& value=it->second;
       const auto next=std::next(it);
       const std::size_t leftmost_index_to_pad=
         next!=index_value.rend()
@@ -196,11 +200,11 @@ string_refinementt::string_refinementt(const infot &info):
 /// display the current index set, for debugging
 static void display_index_set(
   messaget::mstreamt stream,
-  const namespacet& ns,
-  const std::map<exprt, std::set<exprt>>& current_index_set,
-  const std::map<exprt, std::set<exprt>>& index_set)
+  const namespacet &ns,
+  const std::map<exprt, std::set<exprt>> &current_index_set,
+  const std::map<exprt, std::set<exprt>> &index_set)
 {
-  const auto eom = messaget::eom;
+  const auto eom=messaget::eom;
   std::size_t count=0;
   std::size_t count_current=0;
   for(const auto &i : index_set)
@@ -222,7 +226,7 @@ static void display_index_set(
     stream << "}"  << eom;
   }
   stream << count << " elements in index set (" << count_current
-          << " newly added)" << eom;
+         << " newly added)" << eom;
 }
 
 /// compute the index set for all formulas, instantiate the formulas with the
@@ -248,8 +252,9 @@ static void display_current_index_set(
 }
 
 static std::vector<exprt> generate_instantiations(
+  messaget::mstreamt &stream,
   const std::map<exprt, std::set<exprt>> &current_index_set,
-  const std::vector<string_constraintt>& universal_axioms)
+  const std::vector<string_constraintt> &universal_axioms)
 {
   std::vector<exprt> lemmas;
   for(const auto &i : current_index_set)
@@ -257,7 +262,7 @@ static std::vector<exprt> generate_instantiations(
     for(const auto &ua : universal_axioms)
     {
       for(const auto &j : i.second)
-        lemmas.push_back(instantiate(ua, i.first, j));
+        lemmas.push_back(instantiate(stream, ua, i.first, j));
     }
   }
   return lemmas;
@@ -296,7 +301,7 @@ static void depends_in_symbol_map(const exprt &expr, std::vector<exprt> &accu)
 ///             a string_exprt, an array_exprt, an array_of_exprt or an
 ///             if_exprt with branches of the previous kind
 void add_symbol_to_symbol_map(
-  replace_mapt& symbol_resolve,
+  replace_mapt &symbol_resolve,
   std::map<exprt, std::list<exprt>> &reverse_symbol_resolve,
   const exprt &lhs,
   const exprt &rhs)
@@ -359,28 +364,6 @@ std::vector<exprt> set_char_array_equality(const exprt &lhs, const exprt &rhs)
   // equality. Note that this might not be the case for other languages.
 }
 
-/// remove functions applications and create the necessary axioms
-/// \par parameters: an expression containing function applications
-/// \return an expression containing no function application
-exprt substitute_function_applications(
-  string_constraint_generatort& generator, exprt expr)
-{
-  for(size_t i=0; i<expr.operands().size(); ++i)
-  {
-    // TODO: only copy when necessary
-    exprt op(expr.operands()[i]);
-    expr.operands()[i]=substitute_function_applications(generator, op);
-  }
-
-  if(expr.id()==ID_function_application)
-  {
-    function_application_exprt f=to_function_application_expr(expr);
-    return generator.add_axioms_for_function_application(f);
-  }
-
-  return expr;
-}
-
 /// distinguish char array from other types
 ///
 /// TODO: this is only for java char array and does not work for other languages
@@ -399,10 +382,10 @@ static bool is_char_array(const namespacet &ns, const typet &type)
 /// \param rhs: right and side of the equality
 /// \return true if the assignemnt needs to be handled by the parent class
 ///         via `set_to`
-bool add_axioms_for_string_assigns(
-  replace_mapt& symbol_resolve,
+std::pair<bool, std::vector<exprt>> add_axioms_for_string_assigns(
+  replace_mapt &symbol_resolve,
   std::map<exprt, std::list<exprt>> &reverse_symbol_resolve,
-  string_constraint_generatort& generator,
+  string_constraint_generatort &generator,
   messaget::mstreamt &stream,
   const namespacet &ns,
   const exprt &lhs,
@@ -410,14 +393,15 @@ bool add_axioms_for_string_assigns(
 {
   if(is_char_array(ns, rhs.type()))
   {
-    if(rhs.id() == ID_symbol || rhs.id() == ID_array)
+    std::vector<exprt> lemmas=set_char_array_equality(lhs, rhs);
+    if(rhs.id()==ID_symbol || rhs.id()==ID_array)
     {
       add_symbol_to_symbol_map(
         symbol_resolve,
         reverse_symbol_resolve,
         lhs,
         rhs);
-      return false;
+      return { false, std::move(lemmas) };
     }
     else if(rhs.id()==ID_nondet_symbol)
     {
@@ -426,7 +410,7 @@ bool add_axioms_for_string_assigns(
         reverse_symbol_resolve,
         lhs,
         generator.fresh_symbol("nondet_array", lhs.type()));
-      return false;
+      return { false, std::move(lemmas) };
     }
     else if(rhs.id()==ID_if)
     {
@@ -435,13 +419,13 @@ bool add_axioms_for_string_assigns(
         reverse_symbol_resolve,
         lhs,
         rhs);
-      return true;
+      return { true, std::move(lemmas) };
     }
     else
     {
       stream << "ignoring char array " << from_expr(ns, "", rhs)
              << messaget::eom;
-      return true;
+      return { true, std::move(lemmas) };
     }
   }
   if(is_refined_string_type(rhs.type()))
@@ -452,10 +436,10 @@ bool add_axioms_for_string_assigns(
       reverse_symbol_resolve,
       lhs,
       refined_rhs);
-    return false;
+    return { false, std::vector<exprt>() };
   }
   // Other cases are to be handled by supert::set_to.
-  return true;
+  return { true, std::vector<exprt>() };
 }
 
 /// If the expression is of type string, then adds constants to the index set to
@@ -470,19 +454,18 @@ bool add_axioms_for_string_assigns(
 /// We do so by traversing the array backward, remembering the
 /// last value that has been initialized.
 static void concretize_string(
-  std::function<exprt(const exprt&)> get,
+  const std::function<exprt(const exprt &)> get,
   std::map<exprt, exprt> &found_length,
   std::map<exprt, array_exprt> &found_content,
   const replace_mapt &symbol_resolve,
-  std::map<exprt, std::set<exprt>> &index_set,
-  std::size_t max_string_length,
+  const std::map<exprt, std::set<exprt>> &index_set,
+  const std::size_t max_string_length,
   messaget::mstreamt &stream,
   const namespacet &ns,
   const exprt &expr)
 {
   if(const auto str=expr_cast<string_exprt>(expr))
   {
-    const auto& eom=messaget::eom;
     const exprt length=get(str->length());
     exprt content=str->content();
     replace_expr(symbol_resolve, content);
@@ -492,12 +475,13 @@ static void concretize_string(
       string_length<=max_string_length,
       string_refinement_invariantt("string length must be less than the max "
         "length"));
-    if(index_set[str->content()].empty())
+    const auto it=index_set.find(str->content());
+    if(it==index_set.end() || it->second.empty())
       return;
 
     std::map<std::size_t, exprt> map;
 
-    for(const auto &i : index_set[str->content()])
+    for(const auto &i : it->second)
     {
       const exprt simple_i=simplify_expr(get(i), ns);
       if(const auto index=expr_cast<std::size_t>(simple_i))
@@ -509,13 +493,13 @@ static void concretize_string(
       else
       {
         stream << "concretize_string: ignoring out of bound index: "
-               << from_expr(ns, "", simple_i) << eom;
+               << from_expr(ns, "", simple_i) << messaget::eom;
       }
     }
     array_exprt arr(to_array_type(content.type()));
     arr.operands()=fill_in_map_as_vector(map);
     stream << "Concretized " << from_expr(ns, "", str->content())
-           << " = " << from_expr(ns, "", arr) << eom;
+           << "=" << from_expr(ns, "", arr) << messaget::eom;
     found_content[content]=arr;
   }
 }
@@ -524,16 +508,16 @@ static void concretize_string(
 /// to force the solver to pick concrete values for each character, and fill the
 /// map `found_length`
 std::vector<exprt> concretize_results(
-  std::function<exprt(const exprt&)> get,
+  const std::function<exprt(const exprt &)> get,
   std::map<exprt, exprt> &found_length,
   std::map<exprt, array_exprt> &found_content,
   const replace_mapt &symbol_resolve,
-  std::map<exprt, std::set<exprt>> &index_set,
-  std::size_t max_string_length,
+  const std::map<exprt, std::set<exprt>> &index_set,
+  const std::size_t max_string_length,
   messaget::mstreamt &stream,
   const namespacet &ns,
   const std::set<string_exprt> &created_strings,
-  const std::map<exprt, std::set<exprt>>& current_index_set,
+  const std::map<exprt, std::set<exprt>> &current_index_set,
   const std::vector<string_constraintt> &universal_axioms)
 {
   for(const auto &it : symbol_resolve)
@@ -562,14 +546,14 @@ std::vector<exprt> concretize_results(
       ns,
       expr);
   }
-  return generate_instantiations(current_index_set, universal_axioms);
+  return generate_instantiations(stream, current_index_set, universal_axioms);
 }
 
 /// For each string whose length has been solved, add constants to the map
 /// `found_length`
 void concretize_lengths(
   std::map<exprt, exprt> &found_length,
-  std::function<exprt(const exprt&)> get,
+  const std::function<exprt(const exprt &)> get,
   const replace_mapt &symbol_resolve,
   const std::set<string_exprt> &created_strings)
 {
@@ -633,9 +617,9 @@ void string_refinementt::set_to(const exprt &expr, bool value)
 
     // Preprocessing to remove function applications.
     debug() << "(sr::set_to) " << from_expr(ns, "", lhs)
-            << " = " << from_expr(ns, "", rhs) << eom;
+            << "=" << from_expr(ns, "", rhs) << eom;
 
-    const exprt subst_rhs=substitute_function_applications(generator, rhs);
+    const exprt subst_rhs=generator.substitute_function_applications(rhs);
     if(lhs.type()!=subst_rhs.type())
     {
       if(lhs.type().id()!=ID_array ||
@@ -655,12 +639,9 @@ void string_refinementt::set_to(const exprt &expr, bool value)
 
     if(value)
     {
-      if(is_char_array(ns, rhs.type()))
-      {
-        for(const auto& lemma : set_char_array_equality(lhs, rhs))
-          add_lemma(lemma, false);
-      }
-      const bool not_handled=add_axioms_for_string_assigns(
+      bool not_handled;
+      std::vector<exprt> lemmas;
+      std::tie(not_handled, lemmas)=add_axioms_for_string_assigns(
         symbol_resolve,
         reverse_symbol_resolve,
         generator,
@@ -668,6 +649,8 @@ void string_refinementt::set_to(const exprt &expr, bool value)
         ns,
         lhs,
         subst_rhs);
+      for(const auto &lemma : lemmas)
+        add_lemma(lemma, false);
       if(!not_handled)
         return;
     }
@@ -735,7 +718,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   found_length.clear();
   found_content.clear();
 
-  const auto get = [this](const exprt& expr) { return this->get(expr); };
+  const auto get=[this](const exprt &expr) { return this->get(expr); };
 
   // Initial try without index set
   decision_proceduret::resultt res=supert::dec_solve();
@@ -756,7 +739,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       symbol_resolve);
     if(!success)
     {
-      for(const auto& lemma : lemmas)
+      for(const auto &lemma : lemmas)
         add_lemma(lemma);
       debug() << "check_SAT: got SAT but the model is not correct" << eom;
     }
@@ -775,8 +758,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   initial_index_set(index_set, current_index_set, ns, universal_axioms);
   update_index_set(index_set, current_index_set, ns, cur);
   cur.clear();
-  for(const auto& lemma :
-        generate_instantiations(current_index_set, universal_axioms))
+  for(const auto &lemma :
+        generate_instantiations(debug(), current_index_set, universal_axioms))
     add_lemma(lemma);
   display_current_index_set(debug(), ns, current_index_set);
 
@@ -801,7 +784,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         symbol_resolve);
       if(!success)
       {
-        for(const auto& lemma : lemmas)
+        for(const auto &lemma : lemmas)
           add_lemma(lemma);
         debug() << "check_SAT: got SAT but the model is not correct" << eom;
       }
@@ -824,8 +807,9 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       current_index_set.clear();
       update_index_set(index_set, current_index_set, ns, cur);
       cur.clear();
-      for(const auto& lemma :
-            generate_instantiations(current_index_set, universal_axioms))
+      for(const auto &lemma :
+            generate_instantiations(
+              debug(), current_index_set, universal_axioms))
         add_lemma(lemma);
       display_current_index_set(debug(), ns, current_index_set);
 
@@ -834,7 +818,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         debug() << "current index set is empty" << eom;
         if(config_.trace)
         {
-          const auto lemmas = concretize_results(
+          const auto lemmas=concretize_results(
             get,
             found_length,
             found_content,
@@ -846,7 +830,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
             generator.get_created_strings(),
             current_index_set,
             universal_axioms);
-          for(const auto& lemma : lemmas)
+          for(const auto &lemma : lemmas)
             add_lemma(lemma);
           display_current_index_set(debug(), ns, current_index_set);
           return resultt::D_SATISFIABLE;
@@ -860,13 +844,13 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       }
 
       display_index_set(debug(), ns, current_index_set, index_set);
-      debug()<< "instantiating NOT_CONTAINS constraints" << eom;
+      debug() << "instantiating NOT_CONTAINS constraints" << '\n';
       for(unsigned i=0; i<not_contains_axioms.size(); i++)
       {
-        debug()<< "constraint " << i << eom;
+        debug() << "constraint " << i << '\n';
         const std::vector<exprt> lemmas=
           instantiate_not_contains(
-            not_contains_axioms[i], index_set, generator);
+            debug(), ns, not_contains_axioms[i], index_set, generator);
         for(const exprt &lemma : lemmas)
           add_lemma(lemma);
       }
@@ -898,7 +882,7 @@ bvt string_refinementt::convert_bool_bv(const exprt &boole, const exprt &orig)
 /// \par parameters: a lemma and Boolean value stating whether the lemma should
 /// be added to the index set.
 void string_refinementt::add_lemma(
-  const exprt &lemma, bool _simplify)
+  const exprt &lemma, const bool _simplify)
 {
   if(!seen_instances.insert(lemma).second)
     return;
@@ -928,9 +912,9 @@ void string_refinementt::add_lemma(
 /// representing an integer
 /// \return an array expression or an array_of_exprt
 static exprt get_array(
-  std::function<exprt(const exprt&)> super_get,
+  const std::function<exprt(const exprt &)> super_get,
   const namespacet &ns,
-  std::size_t max_string_length,
+  const std::size_t max_string_length,
   const exprt &arr,
   const exprt &size)
 {
@@ -1015,7 +999,7 @@ static exprt get_array(
 /// \par parameters: an expression representing an array
 /// \return an expression
 static exprt get_array(
-  std::function<exprt(const exprt&)> super_get,
+  const std::function<exprt(const exprt &)> super_get,
   const exprt &arr)
 {
   exprt arr_model=super_get(arr);
@@ -1050,22 +1034,21 @@ void debug_model(
   const replace_mapt &symbol_resolve,
   messaget::mstreamt &stream,
   const namespacet &ns,
-  std::size_t max_string_length,
-  std::function<exprt(const exprt&)> super_get,
+  const std::size_t max_string_length,
+  const std::function<exprt(const exprt &)> super_get,
   const std::vector<symbol_exprt> &boolean_symbols,
   const std::vector<symbol_exprt> &index_symbols)
 {
-  const auto eom = messaget::eom;
   const std::string indent("  ");
   for(auto it : symbol_resolve)
   {
     if(const auto refined=expr_cast<string_exprt>(it.second))
     {
-      stream << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n";
-      stream << indent << indent << "in_map: "
-             << from_expr(ns, "", *refined) << eom;
-      stream << indent << indent << "resolved: "
-             << from_expr(ns, "", *refined) << eom;
+      stream << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n"
+             << indent << indent << "in_map: "
+             << from_expr(ns, "", *refined) << '\n'
+             << indent << indent << "resolved: "
+             << from_expr(ns, "", *refined) << '\n';
       const exprt &econtent=refined->content();
       const exprt &elength=refined->length();
 
@@ -1083,7 +1066,7 @@ void debug_model(
         stream << indent << indent << "as_char_array: "
                << from_expr(ns, "", arr) << "\n";
 
-      stream << indent << indent << "size: " << from_expr(ns, "", len) << eom;
+      stream << indent << indent << "size: " << from_expr(ns, "", len) << '\n';
     }
     else
     {
@@ -1099,21 +1082,22 @@ void debug_model(
               << from_expr(ns, "", arr) << "\n";
       exprt arr_model=get_array(super_get, arr);
       stream << indent << indent << "char_array: "
-             << from_expr(ns, "", arr_model) << eom;
+             << from_expr(ns, "", arr_model) << '\n';
     }
   }
 
   for(const auto it : boolean_symbols)
   {
       stream << " - " << it.get_identifier() << ": "
-             << from_expr(ns, "", super_get(it)) << eom;
+             << from_expr(ns, "", super_get(it)) << '\n';
   }
 
   for(const auto it : index_symbols)
   {
      stream << " - " << it.get_identifier() << ": "
-            << from_expr(ns, "", super_get(it)) << eom;
+            << from_expr(ns, "", super_get(it)) << '\n';
   }
+  stream << messaget::eom;
 }
 
 /// Create a new expression where 'with' expressions on arrays are replaced by
@@ -1156,7 +1140,9 @@ static exprt substitute_array_with_expr(const exprt &expr, const exprt &index)
 /// \param string_max_length: bound on the length of strings
 /// \return an array expression with filled in values, or expr if it is simply
 ///   an `ARRAY_OF(x)` expression
-exprt fill_in_array_with_expr(const exprt &expr, std::size_t string_max_length)
+exprt fill_in_array_with_expr(
+  const exprt &expr,
+  const std::size_t string_max_length)
 {
   PRECONDITION(expr.type().id()==ID_array);
   PRECONDITION(expr.id()==ID_with || expr.id()==ID_array_of);
@@ -1398,15 +1384,15 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
   const std::vector<string_constraintt> &universal_axioms,
   const std::vector<string_not_contains_constraintt> &not_contains_axioms,
   string_constraint_generatort &generator,
-  std::function<exprt(const exprt&)> get,
+  std::function<exprt(const exprt &)> get,
   messaget::mstreamt &stream,
   const namespacet &ns,
   std::size_t max_string_length,
   bool use_counter_example,
   ui_message_handlert::uit ui,
-  const replace_mapt& symbol_resolve)
+  const replace_mapt &symbol_resolve)
 {
-  const auto eom = messaget::eom;
+  const auto eom=messaget::eom;
   stream << "string_refinementt::check_axioms:" << eom;
 
   #if 0
@@ -1423,7 +1409,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
   std::map<size_t, exprt> violated;
 
   stream << "string_refinement::check_axioms: " << universal_axioms.size()
-          << " universal axioms:" << eom;
+         << " universal axioms:" << eom;
   for(size_t i=0; i<universal_axioms.size(); i++)
   {
     const string_constraintt &axiom=universal_axioms[i];
@@ -1438,36 +1424,34 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
 
     exprt negaxiom=negation_of_constraint(axiom_in_model);
 
-    stream << "  "<< i << ".\n"
+    stream << "  " << i << ".\n"
            << "    - axiom:\n"
-           << "       " << from_expr(ns, "", axiom) << eom;
+           << "       " << from_expr(ns, "", axiom) << '\n';
     stream << "    - axiom_in_model:\n"
-           << "       " << from_expr(ns, "", axiom_in_model) << eom;
+           << "       " << from_expr(ns, "", axiom_in_model) << '\n';
     stream << "    - negated_axiom:\n"
-           << "       " << from_expr(ns, "", negaxiom) << eom;
+           << "       " << from_expr(ns, "", negaxiom) << '\n';
 
     exprt with_concretized_arrays=concretize_arrays_in_expression(
       negaxiom, max_string_length);
     stream << "    - negated_axiom_with_concretized_array_access:\n"
-           << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
+           << "       " << from_expr(ns, "", with_concretized_arrays) << '\n';
 
     substitute_array_access(with_concretized_arrays);
     stream << "    - negated_axiom_without_array_access:\n"
-           << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
+           << "       " << from_expr(ns, "", with_concretized_arrays) << '\n';
     exprt witness;
 
-    bool is_sat=is_axiom_sat(
-      ns, ui, with_concretized_arrays, univ_var, witness);
-
-    if(is_sat)
+    if(const auto witness=
+       find_counter_example(ns, ui, with_concretized_arrays, univ_var))
     {
       stream << "  - violated_for: "
              << univ_var.get_identifier()
-             << " = " << from_expr(ns, "", witness) << eom;
-      violated[i]=witness;
+             << "=" << from_expr(ns, "", *witness) << '\n';
+      violated[i]=*witness;
     }
     else
-      stream << "  - correct" << eom;
+      stream << "  - correct" << '\n';
   }
 
   // Maps from indexes of violated not_contains axiom to a witness of violation
@@ -1502,16 +1486,13 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
     stream << "(string_refinementt::check_axioms) Adding negated constraint: "
            << from_expr(ns, "", negaxiom) << eom;
     substitute_array_access(negaxiom);
-    exprt witness;
 
-    bool is_sat=is_axiom_sat(ns, ui, negaxiom, univ_var, witness);
-
-    if(is_sat)
+    if(const auto witness=find_counter_example(ns, ui, negaxiom, univ_var))
     {
       stream << "string constraint can be violated for "
              << univ_var.get_identifier()
-             << " = " << from_expr(ns, "", witness) << eom;
-      violated_not_contains[i]=witness;
+             << "=" << from_expr(ns, "", *witness) << eom;
+      violated_not_contains[i]=*witness;
     }
   }
 
@@ -1544,7 +1525,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
         replace_expr(symbol_resolve, instance);
         replace_expr(axiom.univ_var(), val, instance);
         stream << "adding counter example " << from_expr(ns, "", instance)
-                << eom;
+               << eom;
         lemmas.push_back(instance);
       }
       return { false, lemmas };
@@ -1602,7 +1583,7 @@ static std::map<exprt, int> map_representation_of_sum(const exprt &f)
 static exprt sum_over_map(
   std::map<exprt, int> &m,
   const typet &type,
-  bool negated = false)
+  bool negated=false)
 {
   exprt sum=nil_exprt();
   mp_integer constants=0;
@@ -1686,7 +1667,10 @@ exprt simplify_sum(const exprt &f)
 ///   be equal to val. For instance, if `f` corresponds to the expression $q +
 ///   x$, `compute_inverse_function(q,v,f)` returns an expression for $v - x$.
 static exprt compute_inverse_function(
-  const exprt &qvar, const exprt &val, const exprt &f)
+  messaget::mstreamt &stream,
+  const exprt &qvar,
+  const exprt &val,
+  const exprt &f)
 {
   exprt positive, negative;
   // number of time the element should be added (can be negative)
@@ -1713,8 +1697,8 @@ static exprt compute_inverse_function(
       string_refinement_invariantt("a proper function must have exactly one "
         "occurrences after reduction, or it canceled out, and it does not have "
         " one"));
-    // debug() << "in string_refinementt::compute_inverse_function:"
-    //         << " warning: occurrences of qvar canceled out " << eom;
+    stream << "in string_refinementt::compute_inverse_function:"
+           << " warning: occurrences of qvar canceled out " << messaget::eom;
   }
 
   elems.erase(it);
@@ -1806,10 +1790,12 @@ static void add_to_index_set(
   std::map<exprt, std::set<exprt>> &index_set,
   std::map<exprt, std::set<exprt>> &current_index_set,
   const namespacet &ns,
-  const exprt &s, exprt i)
+  const exprt &s,
+  exprt i)
 {
   simplify(i, ns);
-  if(i.id()!=ID_constant || expr_cast<size_t>(i))
+  const bool is_size_t=expr_cast<size_t>(i).has_value();
+  if(i.id()!=ID_constant || is_size_t)
   {
     for(const auto &sub : sub_arrays(s))
       if(index_set[sub].insert(i).second)
@@ -1922,7 +1908,7 @@ class find_index_visitort: public const_expr_visitort
 };
 
 /// Finds an index on `str` used in `expr` that contains `qvar`, for instance
-/// with arguments ``(str[k] == 'a')``, `str`, and `k`, the function should
+/// with arguments ``(str[k]=='a')``, `str`, and `k`, the function should
 /// return `k`.
 /// \param [in] expr: the expression to search
 /// \param [in] str: the string which must be indexed
@@ -1944,13 +1930,16 @@ static exprt find_index(
 ///   t[q]='b'$, `instantiate(axiom,s,v)` would return an expression for
 ///   $s[v]='a' && t[v-x]='b'$.
 static exprt instantiate(
-  const string_constraintt &axiom, const exprt &str, const exprt &val)
+  messaget::mstreamt &stream,
+  const string_constraintt &axiom,
+  const exprt &str,
+  const exprt &val)
 {
   exprt idx=find_index(axiom.body(), str, axiom.univ_var());
   if(idx.is_nil())
     return true_exprt();
 
-  exprt r=compute_inverse_function(axiom.univ_var(), val, idx);
+  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
@@ -1967,17 +1956,19 @@ static exprt instantiate(
 /// \param [in] axiom: the axiom to instantiate
 /// \return the lemmas produced through instantiation
 static std::vector<exprt> instantiate_not_contains(
+  messaget::mstreamt &stream,
+  const namespacet &ns,
   const string_not_contains_constraintt &axiom,
-  const std::map<exprt, std::set<exprt>>& index_set,
+  const std::map<exprt, std::set<exprt>> &index_set,
   const string_constraint_generatort &generator)
 {
   const string_exprt s0=to_string_expr(axiom.s0());
   const string_exprt s1=to_string_expr(axiom.s1());
 
-  // debug() << "instantiate not contains " << from_expr(ns, "", s0) << " : "
-  //         << from_expr(ns, "", s1) << eom;
-  const auto& i0=index_set.find(s0.content());
-  const auto& i1=index_set.find(s1.content());
+  stream << "instantiate not contains " << from_expr(ns, "", s0) << " : "
+         << from_expr(ns, "", s1) << messaget::eom;
+  const auto &i0=index_set.find(s0.content());
+  const auto &i1=index_set.find(s1.content());
   if(i0!=index_set.end() && i1!=index_set.end())
   {
     return ::instantiate_not_contains(
@@ -1995,7 +1986,7 @@ static std::vector<exprt> instantiate_not_contains(
 /// \return an expression containing no array-list
 exprt substitute_array_lists(exprt expr, size_t string_max_length)
 {
-  for(auto& operand : expr.operands())
+  for(auto &operand : expr.operands())
   {
     // TODO: only copy when necessary
     const exprt op(operand);
@@ -2032,7 +2023,7 @@ exprt substitute_array_lists(exprt expr, size_t string_max_length)
 /// \return an expression
 exprt string_refinementt::get(const exprt &expr) const
 {
-  const auto super_get=[this](const exprt& expr)
+  const auto super_get=[this](const exprt &expr)
   { return supert::get(expr); };
   exprt ecopy(expr);
   replace_expr(symbol_resolve, ecopy);
@@ -2078,15 +2069,13 @@ exprt string_refinementt::get(const exprt &expr) const
 /// in `witness`. If UNSAT, then what witness is is undefined.
 /// \param [in] axiom: the axiom to be checked
 /// \param [in] var: the variable whose evaluation will be stored in witness
-/// \param [out] witness: the witness of the satisfying assignment if one
-///   exists. If UNSAT, then behaviour is undefined.
-/// \return: true if axiom is SAT, false if UNSAT
-static bool is_axiom_sat(
-  const namespacet& ns,
-  ui_message_handlert::uit ui,
+/// \return: the witness of the satisfying assignment if one
+/// exists. If UNSAT, then behaviour is undefined.
+static optionalt<exprt> find_counter_example(
+  const namespacet &ns,
+  const ui_message_handlert::uit ui,
   const exprt &axiom,
-  const symbol_exprt& var,
-  exprt &witness)
+  const symbol_exprt &var)
 {
   satcheck_no_simplifiert sat_check;
   bv_refinementt::infot info;
@@ -2099,21 +2088,10 @@ static bool is_axiom_sat(
   bv_refinementt solver(info);
   solver << axiom;
 
-  switch(solver())
-  {
-  case decision_proceduret::resultt::D_SATISFIABLE:
-    {
-      witness=solver.get(var);
-      return true;
-    }
-  case decision_proceduret::resultt::D_UNSATISFIABLE:
-    return false;
-  case decision_proceduret::resultt::D_ERROR:
-  default:
-    INVARIANT(false, string_refinement_invariantt("failure in checking axiom"));
-    // To tell the compiler that the previous line bails
-    throw 0;
-  }
+  if(solver()==decision_proceduret::resultt::D_SATISFIABLE)
+    return solver.get(var);
+  else
+    return { };
 }
 
 /// \related string_constraintt
@@ -2220,11 +2198,11 @@ static bool universal_only_in_index(const string_constraintt &expr)
 /// \param [in] expr: the string constraint to check
 /// \return whether the constraint satisfies the invariant
 static bool is_valid_string_constraint(
-  messaget::mstreamt& stream,
-  const namespacet& ns,
+  messaget::mstreamt &stream,
+  const namespacet &ns,
   const string_constraintt &expr)
 {
-  const auto eom = messaget::eom;
+  const auto eom=messaget::eom;
   // Condition 1: The premise cannot contain any string indices
   const array_index_mapt premise_indices=gather_indices(expr.premise());
   if(!premise_indices.empty())
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 863b4e61929..b070047c582 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -34,7 +34,7 @@ class string_refinementt final: public bv_refinementt
 private:
   struct configt
   {
-    unsigned refinement_bound=0;
+    std::size_t refinement_bound=0;
     /// Make non-deterministic character arrays have at least one character
     bool string_non_empty=false;
     /// Concretize strings after solver is finished
@@ -50,7 +50,7 @@ class string_refinementt final: public bv_refinementt
 
   explicit string_refinementt(const infot &);
 
-  virtual std::string decision_procedure_text() const override
+  std::string decision_procedure_text() const override
   { return "string refinement loop with "+prop.solver_text(); }
 
   exprt get(const exprt &expr) const override;
@@ -68,7 +68,7 @@ class string_refinementt final: public bv_refinementt
   bvt convert_bool_bv(const exprt &boole, const exprt &orig);
 
   const configt config_;
-  unsigned loop_bound_;
+  std::size_t loop_bound_;
   string_constraint_generatort generator;
   expr_sett nondet_arrays;
 
@@ -98,7 +98,7 @@ class string_refinementt final: public bv_refinementt
   void add_lemma(const exprt &lemma, bool simplify=true);
 };
 
-exprt substitute_array_lists(exprt expr, size_t string_max_length);
+exprt substitute_array_lists(exprt expr, std::size_t string_max_length);
 exprt concretize_arrays_in_expression(
   exprt expr, std::size_t string_max_length);
 #endif