diff --git a/jbmc/regression/strings-smoke-tests/java_set_length/test.desc b/jbmc/regression/strings-smoke-tests/java_set_length/test.desc
index 8d8abce9a69..a94da122c23 100644
--- a/jbmc/regression/strings-smoke-tests/java_set_length/test.desc
+++ b/jbmc/regression/strings-smoke-tests/java_set_length/test.desc
@@ -8,3 +8,4 @@ test_set_length
 ^\[.*assertion.3\].* line 11.* FAILURE$
 --
 non equal types
+^warning: ignoring
diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
index c53aaa0e5f3..269534c3e36 100644
--- a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -218,7 +218,7 @@ SCENARIO(
       {ab, b, from_integer(2)}};
 
     // Generating the corresponding axioms and simplifying, recording info
-    string_constraint_generatort generator(empty_ns);
+    string_constraint_generatort generator(empty_ns, null_message_handler);
     const auto pair = generator.add_axioms_for_function_application(func);
     const string_constraintst &constraints = pair.second;
 
@@ -313,7 +313,7 @@ SCENARIO(
                                                      a_array};
 
     // Create witness for axiom
-    string_constraint_generatort generator(empty_ns);
+    string_constraint_generatort generator(empty_ns, null_message_handler);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses.emplace(vacuous, generator.fresh_symbol("w", t.witness_type()));
 
@@ -363,7 +363,7 @@ SCENARIO(
                                                      b_array};
 
     // Create witness for axiom
-    string_constraint_generatort generator(empty_ns);
+    string_constraint_generatort generator(empty_ns, null_message_handler);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
@@ -414,7 +414,7 @@ SCENARIO(
                                                      empty_array};
 
     // Create witness for axiom
-    string_constraint_generatort generator(empty_ns);
+    string_constraint_generatort generator(empty_ns, null_message_handler);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
@@ -467,7 +467,7 @@ SCENARIO(
                                                      ab_array};
 
     // Create witness for axiom
-    string_constraint_generatort generator(empty_ns);
+    string_constraint_generatort generator(empty_ns, null_message_handler);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
@@ -518,7 +518,7 @@ SCENARIO(
                                                      cd_array};
 
     // Create witness for axiom
-    string_constraint_generatort generator(empty_ns);
+    string_constraint_generatort generator(empty_ns, null_message_handler);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
     witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index 08e6c6bed47..e1673562649 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -1385,7 +1385,6 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
   goto_functionst this_interleaving;
   this_interleaving.function_map=std::move(map);
   optionst no_option;
-  null_message_handlert no_message;
 
   #if 0
   bmct bmc(no_option, symbol_table, no_message);
diff --git a/src/solvers/README.md b/src/solvers/README.md
index a601feac8b4..2a19e79f88b 100644
--- a/src/solvers/README.md
+++ b/src/solvers/README.md
@@ -461,8 +461,8 @@ This is described in more detail \link string_builtin_functiont here. \endlink
     \copybrief string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f)
     \link string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f) More... \endlink
   * `cprover_string_insert` :
-    \copybrief string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator) const
-    \link string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator) const More... \endlink
+    \copybrief string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator, message_handlert &message_handler) const
+    \link string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator, message_handlert &message_handler) const More... \endlink
   * `cprover_string_replace` :
     \copybrief string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f)
     \link string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f) More... \endlink
diff --git a/src/solvers/strings/string_builtin_function.cpp b/src/solvers/strings/string_builtin_function.cpp
index 0507281bd56..b3e08da91cc 100644
--- a/src/solvers/strings/string_builtin_function.cpp
+++ b/src/solvers/strings/string_builtin_function.cpp
@@ -101,7 +101,8 @@ optionalt<exprt> string_concat_char_builtin_functiont::eval(
 ///   * result[input.length] = character
 ///   * return_code = 0
 string_constraintst string_concat_char_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 {
   string_constraintst constraints;
   constraints.existential.push_back(length_constraint());
@@ -111,7 +112,7 @@ string_constraintst string_concat_char_builtin_functiont::constraints(
     const exprt upper_bound =
       zero_if_negative(array_pool.get_or_create_length(input));
     return string_constraintt(
-      idx, upper_bound, equal_exprt(input[idx], result[idx]));
+      idx, upper_bound, equal_exprt(input[idx], result[idx]), message_handler);
   }());
   constraints.existential.push_back(
     equal_exprt(result[array_pool.get_or_create_length(input)], character));
@@ -151,7 +152,8 @@ optionalt<exprt> string_set_char_builtin_functiont::eval(
 ///   3. forall 0 <= i < max(0, min(res.length, pos)). res[i] = str[i]
 ///   4. forall max(0, pos+1) <= i < res.length. res[i] = str[i]
 string_constraintst string_set_char_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 {
   string_constraintst constraints;
   constraints.existential.push_back(length_constraint());
@@ -169,7 +171,8 @@ string_constraintst string_set_char_builtin_functiont::constraints(
       q,
       zero_if_negative(
         minimum(array_pool.get_or_create_length(result), position)),
-      a3_body);
+      a3_body,
+      message_handler);
   }());
   constraints.universal.push_back([&] {
     const symbol_exprt q2 =
@@ -179,7 +182,8 @@ string_constraintst string_set_char_builtin_functiont::constraints(
       q2,
       zero_if_negative(plus_exprt(position, from_integer(1, position.type()))),
       zero_if_negative(array_pool.get_or_create_length(result)),
-      a4_body);
+      a4_body,
+      message_handler);
   }());
   return constraints;
 }
@@ -279,7 +283,8 @@ static exprt is_lower_case(const exprt &character)
 /// characters: `diff = 'a'-'A' = 0x20` and `is_upper_case` is true for the
 /// upper case characters of Basic Latin and Latin-1 supplement of unicode.
 string_constraintst string_to_lower_case_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 {
   // \todo for now, only characters in Basic Latin and Latin-1 supplement
   // are supported (up to 0x100), we should add others using case mapping
@@ -302,7 +307,8 @@ string_constraintst string_to_lower_case_builtin_functiont::constraints(
     return string_constraintt(
       idx,
       zero_if_negative(array_pool.get_or_create_length(result)),
-      conditional_convert);
+      conditional_convert,
+      message_handler);
   }());
   return constraints;
 }
@@ -332,9 +338,11 @@ optionalt<exprt> string_to_upper_case_builtin_functiont::eval(
 ///        is_lower_case(str[i]) ? res[i] = str[i] - 0x20 : res[i] = str[i]
 ///
 /// \param fresh_symbol: generator of fresh symbols
+/// \param message_handler: message handler
 /// \return set of constraints
 string_constraintst string_to_upper_case_builtin_functiont::constraints(
-  symbol_generatort &fresh_symbol) const
+  symbol_generatort &fresh_symbol,
+  message_handlert &message_handler) const
 {
   string_constraintst constraints;
   constraints.existential.push_back(length_constraint());
@@ -350,7 +358,8 @@ string_constraintst string_to_upper_case_builtin_functiont::constraints(
       zero_if_negative(array_pool.get_or_create_length(result)),
       equal_exprt(
         result[idx],
-        if_exprt(is_lower_case(input[idx]), converted, input[idx])));
+        if_exprt(is_lower_case(input[idx]), converted, input[idx])),
+      message_handler);
   }());
   return constraints;
 }
@@ -406,7 +415,8 @@ optionalt<exprt> string_of_int_builtin_functiont::eval(
 }
 
 string_constraintst string_of_int_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 {
   auto pair =
     generator.add_axioms_for_string_of_int_with_radix(result, arg, radix, 0);
@@ -475,7 +485,8 @@ string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(
 }
 
 string_constraintst string_builtin_function_with_no_evalt::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 {
   auto pair =
     generator.add_axioms_for_function_application(function_application);
diff --git a/src/solvers/strings/string_builtin_function.h b/src/solvers/strings/string_builtin_function.h
index 9a256f97212..566863d2593 100644
--- a/src/solvers/strings/string_builtin_function.h
+++ b/src/solvers/strings/string_builtin_function.h
@@ -102,7 +102,7 @@ class string_builtin_functiont
   /// the result of this function.
   /// This logic is implemented in add_constraints().
   virtual string_constraintst
-  constraints(string_constraint_generatort &constraint_generator) const = 0;
+  constraints(string_constraint_generatort &, message_handlert &) const = 0;
 
   /// Constraint ensuring that the length of the strings are coherent with
   /// the function call.
@@ -198,8 +198,9 @@ class string_concat_char_builtin_functiont
     return "concat_char";
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handlert) const override;
 
   exprt length_constraint() const override;
 };
@@ -235,8 +236,9 @@ class string_set_char_builtin_functiont
     return "set_char";
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override;
 
   // \todo: length_constraint is not the best possible name because we also
   // \todo: add constraint about the return code
@@ -265,8 +267,9 @@ class string_to_lower_case_builtin_functiont
     return "to_lower_case";
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override;
 
   exprt length_constraint() const override
   {
@@ -313,12 +316,15 @@ class string_to_upper_case_builtin_functiont
     return "to_upper_case";
   }
 
-  string_constraintst constraints(class symbol_generatort &fresh_symbol) const;
+  string_constraintst constraints(
+    class symbol_generatort &fresh_symbol,
+    message_handlert &message_handler) const;
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override
   {
-    return constraints(generator.fresh_symbol);
+    return constraints(generator.fresh_symbol, message_handler);
   };
 
   exprt length_constraint() const override
@@ -379,8 +385,9 @@ class string_of_int_builtin_functiont : public string_creation_builtin_functiont
     return "string_of_int";
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override;
 
   exprt length_constraint() const override;
 
@@ -439,8 +446,9 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
     return {};
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override;
 
   exprt length_constraint() const override
   {
diff --git a/src/solvers/strings/string_concatenation_builtin_function.cpp b/src/solvers/strings/string_concatenation_builtin_function.cpp
index cba41fb9539..96de6af270c 100644
--- a/src/solvers/strings/string_concatenation_builtin_function.cpp
+++ b/src/solvers/strings/string_concatenation_builtin_function.cpp
@@ -73,7 +73,8 @@ string_constraint_generatort::add_axioms_for_concat_substr(
     return string_constraintt(
       idx,
       zero_if_negative(array_pool.get_or_create_length(s1)),
-      equal_exprt(s1[idx], res[idx]));
+      equal_exprt(s1[idx], res[idx]),
+      message_handler);
   }());
 
   // Axiom 3.
@@ -86,7 +87,8 @@ string_constraint_generatort::add_axioms_for_concat_substr(
     const minus_exprt upper_bound(
       array_pool.get_or_create_length(res),
       array_pool.get_or_create_length(s1));
-    return string_constraintt(idx2, zero_if_negative(upper_bound), res_eq);
+    return string_constraintt(
+      idx2, zero_if_negative(upper_bound), res_eq, message_handler);
   }());
 
   return {from_integer(0, get_return_code_type()), std::move(constraints)};
@@ -208,7 +210,8 @@ std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
 }
 
 string_constraintst string_concatenation_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 
 {
   auto pair = [&]() -> std::pair<exprt, string_constraintst> {
diff --git a/src/solvers/strings/string_concatenation_builtin_function.h b/src/solvers/strings/string_concatenation_builtin_function.h
index d21f02dd9ed..1e6e586d0e4 100644
--- a/src/solvers/strings/string_concatenation_builtin_function.h
+++ b/src/solvers/strings/string_concatenation_builtin_function.h
@@ -39,8 +39,9 @@ class string_concatenation_builtin_functiont final
     return "concat";
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override;
 
   exprt length_constraint() const override;
 };
diff --git a/src/solvers/strings/string_constraint.cpp b/src/solvers/strings/string_constraint.cpp
index 9bdef3a8813..e897dc883b3 100644
--- a/src/solvers/strings/string_constraint.cpp
+++ b/src/solvers/strings/string_constraint.cpp
@@ -11,21 +11,20 @@ Author: Diffblue Ltd.
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 
-#include <solvers/flattening/boolbv.h>
+#include <solvers/flattening/bv_pointers.h>
 #include <solvers/sat/satcheck.h>
 
 /// Runs a solver instance to verify whether an expression can only be
 /// non-negative.
 /// \param expr: the expression to check for negativity
+/// \param message_handler: message handler
 /// \return true if `expr < 0` is unsatisfiable, false otherwise
-static bool cannot_be_neg(const exprt &expr)
+static bool cannot_be_neg(const exprt &expr, message_handlert &message_handler)
 {
-  // this is an internal check, no need for user visibility
-  null_message_handlert null_message_handler;
-  satcheck_no_simplifiert sat_check(null_message_handler);
+  satcheck_no_simplifiert sat_check(message_handler);
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
-  boolbvt solver{ns, sat_check, null_message_handler};
+  bv_pointerst solver{ns, sat_check, message_handler};
   const exprt zero = from_integer(0, expr.type());
   const binary_relation_exprt non_neg(expr, ID_lt, zero);
   solver << non_neg;
@@ -36,18 +35,19 @@ string_constraintt::string_constraintt(
   const symbol_exprt &_univ_var,
   const exprt &lower_bound,
   const exprt &upper_bound,
-  const exprt &body)
+  const exprt &body,
+  message_handlert &message_handler)
   : univ_var(_univ_var),
     lower_bound(lower_bound),
     upper_bound(upper_bound),
     body(body)
 {
   INVARIANT(
-    cannot_be_neg(lower_bound),
+    cannot_be_neg(lower_bound, message_handler),
     "String constraints must have non-negative lower bound.\n" +
       lower_bound.pretty());
   INVARIANT(
-    cannot_be_neg(upper_bound),
+    cannot_be_neg(upper_bound, message_handler),
     "String constraints must have non-negative upper bound.\n" +
       upper_bound.pretty());
 }
diff --git a/src/solvers/strings/string_constraint.h b/src/solvers/strings/string_constraint.h
index 13e4e131295..4c56b03d941 100644
--- a/src/solvers/strings/string_constraint.h
+++ b/src/solvers/strings/string_constraint.h
@@ -24,6 +24,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include <util/string_expr.h>
 #include <util/union_find_replace.h>
 
+class message_handlert;
+
 ///  ### Universally quantified string constraint
 ///
 ///  This represents a universally quantified string constraint as laid out in
@@ -60,21 +62,25 @@ class string_constraintt final
   exprt upper_bound;
   exprt body;
 
-  string_constraintt() = delete;
-
   string_constraintt(
     const symbol_exprt &_univ_var,
     const exprt &lower_bound,
     const exprt &upper_bound,
-    const exprt &body);
+    const exprt &body,
+    message_handlert &message_handler);
 
   // Default bound inferior is 0
-  string_constraintt(symbol_exprt univ_var, exprt upper_bound, exprt body)
+  string_constraintt(
+    symbol_exprt univ_var,
+    exprt upper_bound,
+    exprt body,
+    message_handlert &message_handler)
     : string_constraintt(
         univ_var,
         from_integer(0, univ_var.type()),
         upper_bound,
-        body)
+        body,
+        message_handler)
   {
   }
 
diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h
index ed111538f5b..1e36064f49f 100644
--- a/src/solvers/strings/string_constraint_generator.h
+++ b/src/solvers/strings/string_constraint_generator.h
@@ -51,7 +51,9 @@ class string_constraint_generatort final
   // string constraints for different string functions and add them
   // to the axiom list.
 
-  explicit string_constraint_generatort(const namespacet &ns);
+  string_constraint_generatort(
+    const namespacet &ns,
+    message_handlert &message_handler);
 
   std::pair<exprt, string_constraintst>
   add_axioms_for_function_application(const function_application_exprt &expr);
@@ -70,6 +72,8 @@ class string_constraint_generatort final
     const function_application_exprt &expr);
 
 private:
+  message_handlert &message_handler;
+
   exprt associate_array_to_pointer(
     const exprt &return_code,
     const function_application_exprt &f);
diff --git a/src/solvers/strings/string_constraint_generator_comparison.cpp b/src/solvers/strings/string_constraint_generator_comparison.cpp
index ec5731f40d0..71ebd82bc71 100644
--- a/src/solvers/strings/string_constraint_generator_comparison.cpp
+++ b/src/solvers/strings/string_constraint_generator_comparison.cpp
@@ -55,7 +55,8 @@ string_constraint_generatort::add_axioms_for_equals(
     return string_constraintt(
       qvar,
       zero_if_negative(array_pool.get_or_create_length(s1)),
-      implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])));
+      implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])),
+      message_handler);
   }());
 
   // Axiom 3.
@@ -160,7 +161,8 @@ string_constraint_generatort::add_axioms_for_equals_ignore_case(
   const string_constraintt a2(
     qvar,
     zero_if_negative(array_pool.get_or_create_length(s1)),
-    implies_exprt(eq, constr2));
+    implies_exprt(eq, constr2),
+    message_handler);
   constraints.universal.push_back(a2);
 
   const symbol_exprt witness =
@@ -228,7 +230,8 @@ string_constraint_generatort::add_axioms_for_compare_to(
   const string_constraintt a2(
     i,
     zero_if_negative(array_pool.get_or_create_length(s1)),
-    implies_exprt(res_null, equal_exprt(s1[i], s2[i])));
+    implies_exprt(res_null, equal_exprt(s1[i], s2[i])),
+    message_handler);
   constraints.universal.push_back(a2);
 
   const symbol_exprt x = fresh_symbol("index_compare_to", index_type);
@@ -277,7 +280,8 @@ string_constraint_generatort::add_axioms_for_compare_to(
   const string_constraintt a4(
     i2,
     zero_if_negative(x),
-    implies_exprt(not_exprt(res_null), equal_exprt(s1[i2], s2[i2])));
+    implies_exprt(not_exprt(res_null), equal_exprt(s1[i2], s2[i2])),
+    message_handler);
   constraints.universal.push_back(a4);
 
   return {res, std::move(constraints)};
diff --git a/src/solvers/strings/string_constraint_generator_indexof.cpp b/src/solvers/strings/string_constraint_generator_indexof.cpp
index 19fb5ac2ee1..d4f09c421a8 100644
--- a/src/solvers/strings/string_constraint_generator_indexof.cpp
+++ b/src/solvers/strings/string_constraint_generator_indexof.cpp
@@ -71,7 +71,8 @@ string_constraint_generatort::add_axioms_for_index_of(
     n,
     lower_bound,
     zero_if_negative(index),
-    implies_exprt(contains, notequal_exprt(str[n], c)));
+    implies_exprt(contains, notequal_exprt(str[n], c)),
+    message_handler);
   constraints.universal.push_back(a4);
 
   symbol_exprt m = fresh_symbol("QA_index_of", index_type);
@@ -79,7 +80,8 @@ string_constraint_generatort::add_axioms_for_index_of(
     m,
     lower_bound,
     zero_if_negative(array_pool.get_or_create_length(str)),
-    implies_exprt(not_exprt(contains), not_exprt(equal_exprt(str[m], c))));
+    implies_exprt(not_exprt(contains), not_exprt(equal_exprt(str[m], c))),
+    message_handler);
   constraints.universal.push_back(a5);
 
   return {index, std::move(constraints)};
@@ -141,7 +143,8 @@ string_constraint_generatort::add_axioms_for_index_of_string(
     qvar,
     zero_if_negative(array_pool.get_or_create_length(needle)),
     implies_exprt(
-      contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])));
+      contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])),
+    message_handler);
   constraints.universal.push_back(a3);
 
   // string_not contains_constraintt are formulas of the form:
@@ -242,7 +245,8 @@ string_constraint_generatort::add_axioms_for_last_index_of_string(
   const string_constraintt a3(
     qvar,
     zero_if_negative(array_pool.get_or_create_length(needle)),
-    implies_exprt(contains, constr3));
+    implies_exprt(contains, constr3),
+    message_handler);
   constraints.universal.push_back(a3);
 
   // end_index is min(from_index, |str| - |substring|)
@@ -392,14 +396,16 @@ string_constraint_generatort::add_axioms_for_last_index_of(
     n,
     zero_if_negative(plus_exprt(index, index1)),
     zero_if_negative(end_index),
-    implies_exprt(contains, notequal_exprt(str[n], c)));
+    implies_exprt(contains, notequal_exprt(str[n], c)),
+    message_handler);
   constraints.universal.push_back(a4);
 
   const symbol_exprt m = fresh_symbol("QA_last_index_of2", index_type);
   const string_constraintt a5(
     m,
     zero_if_negative(end_index),
-    implies_exprt(not_exprt(contains), notequal_exprt(str[m], c)));
+    implies_exprt(not_exprt(contains), notequal_exprt(str[m], c)),
+    message_handler);
   constraints.universal.push_back(a5);
 
   return {index, std::move(constraints)};
diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp
index 36fdd378a91..a28252b6fb0 100644
--- a/src/solvers/strings/string_constraint_generator_main.cpp
+++ b/src/solvers/strings/string_constraint_generator_main.cpp
@@ -30,8 +30,10 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include <util/ssa_expr.h>
 #include <util/string_constant.h>
 
-string_constraint_generatort::string_constraint_generatort(const namespacet &ns)
-  : array_pool(fresh_symbol), ns(ns)
+string_constraint_generatort::string_constraint_generatort(
+  const namespacet &ns,
+  message_handlert &message_handler)
+  : array_pool(fresh_symbol), ns(ns), message_handler(message_handler)
 {
 }
 
@@ -142,7 +144,8 @@ string_constraintst string_constraint_generatort::add_constraint_on_characters(
     qvar,
     zero_if_negative(start),
     zero_if_negative(end),
-    interval_constraint(chr, char_range));
+    interval_constraint(chr, char_range),
+    message_handler);
   return {{}, {sc}, {}};
 }
 
diff --git a/src/solvers/strings/string_constraint_generator_testing.cpp b/src/solvers/strings/string_constraint_generator_testing.cpp
index d22f6ad6371..9fab7d39601 100644
--- a/src/solvers/strings/string_constraint_generator_testing.cpp
+++ b/src/solvers/strings/string_constraint_generator_testing.cpp
@@ -64,7 +64,8 @@ string_constraint_generatort::add_axioms_for_is_prefix(
       qvar,
       maximum(
         from_integer(0, index_type), array_pool.get_or_create_length(prefix)),
-      body);
+      body,
+      message_handler);
   }());
 
   // Axiom 3.
@@ -200,7 +201,8 @@ string_constraint_generatort::add_axioms_for_is_suffix(
   string_constraintt a2(
     qvar,
     zero_if_negative(array_pool.get_or_create_length(s0)),
-    implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])));
+    implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])),
+    message_handler);
   constraints.universal.push_back(a2);
 
   symbol_exprt witness = fresh_symbol("witness_not_suffix", index_type);
@@ -280,7 +282,8 @@ string_constraint_generatort::add_axioms_for_contains(
   string_constraintt a4(
     qvar,
     zero_if_negative(array_pool.get_or_create_length(s1)),
-    implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])));
+    implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])),
+    message_handler);
   constraints.universal.push_back(a4);
 
   const string_not_contains_constraintt a5 = {
diff --git a/src/solvers/strings/string_constraint_generator_transformation.cpp b/src/solvers/strings/string_constraint_generator_transformation.cpp
index 1c1487756f8..6d82b14307d 100644
--- a/src/solvers/strings/string_constraint_generator_transformation.cpp
+++ b/src/solvers/strings/string_constraint_generator_transformation.cpp
@@ -60,7 +60,8 @@ string_constraint_generatort::add_axioms_for_set_length(
   const string_constraintt a2(
     idx,
     zero_if_negative(minimum(array_pool.get_or_create_length(s1), k)),
-    equal_exprt(s1[idx], res[idx]));
+    equal_exprt(s1[idx], res[idx]),
+    message_handler);
   constraints.universal.push_back(a2);
 
   symbol_exprt idx2 = fresh_symbol("QA_index_set_length2", index_type);
@@ -68,7 +69,8 @@ string_constraint_generatort::add_axioms_for_set_length(
     idx2,
     zero_if_negative(array_pool.get_or_create_length(s1)),
     zero_if_negative(array_pool.get_or_create_length(res)),
-    equal_exprt(res[idx2], from_integer(0, char_type)));
+    equal_exprt(res[idx2], from_integer(0, char_type)),
+    message_handler);
   constraints.universal.push_back(a3);
 
   return {from_integer(0, get_return_code_type()), std::move(constraints)};
@@ -144,7 +146,8 @@ string_constraint_generatort::add_axioms_for_substring(
     return string_constraintt(
       idx,
       zero_if_negative(array_pool.get_or_create_length(res)),
-      equal_exprt(res[idx], str[plus_exprt(start1, idx)]));
+      equal_exprt(res[idx], str[plus_exprt(start1, idx)]),
+      message_handler);
   }());
 
   return {from_integer(0, get_return_code_type()), std::move(constraints)};
@@ -212,7 +215,7 @@ string_constraint_generatort::add_axioms_for_trim(
 
   symbol_exprt n = fresh_symbol("QA_index_trim", index_type);
   binary_relation_exprt non_print(str[n], ID_le, space_char);
-  string_constraintt a6(n, zero_if_negative(idx), non_print);
+  string_constraintt a6(n, zero_if_negative(idx), non_print, message_handler);
   constraints.universal.push_back(a6);
 
   // Axiom 7.
@@ -226,13 +229,17 @@ string_constraint_generatort::add_axioms_for_trim(
         idx, plus_exprt(array_pool.get_or_create_length(res), n2))],
       ID_le,
       space_char);
-    return string_constraintt(n2, zero_if_negative(bound), eqn2);
+    return string_constraintt(
+      n2, zero_if_negative(bound), eqn2, message_handler);
   }());
 
   symbol_exprt n3 = fresh_symbol("QA_index_trim3", index_type);
   equal_exprt eqn3(res[n3], str[plus_exprt(n3, idx)]);
   string_constraintt a8(
-    n3, zero_if_negative(array_pool.get_or_create_length(res)), eqn3);
+    n3,
+    zero_if_negative(array_pool.get_or_create_length(res)),
+    eqn3,
+    message_handler);
   constraints.universal.push_back(a8);
 
   // Axiom 9.
@@ -333,7 +340,8 @@ string_constraint_generatort::add_axioms_for_replace(
     string_constraintt a2(
       qvar,
       zero_if_negative(array_pool.get_or_create_length(res)),
-      and_exprt(case1, case2));
+      and_exprt(case1, case2),
+      message_handler);
     constraints.universal.push_back(a2);
     return {from_integer(0, f.type()), std::move(constraints)};
   }
diff --git a/src/solvers/strings/string_dependencies.cpp b/src/solvers/strings/string_dependencies.cpp
index 4b15301fad8..bb7aeab4d9a 100644
--- a/src/solvers/strings/string_dependencies.cpp
+++ b/src/solvers/strings/string_dependencies.cpp
@@ -345,8 +345,9 @@ void string_dependenciest::output_dot(std::ostream &stream) const
   stream << '}' << std::endl;
 }
 
-string_constraintst
-string_dependenciest::add_constraints(string_constraint_generatort &generator)
+string_constraintst string_dependenciest::add_constraints(
+  string_constraint_generatort &generator,
+  message_handlert &message_handler)
 {
   std::unordered_set<nodet, node_hash> test_dependencies;
   for(const auto &builtin : builtin_function_nodes)
@@ -369,7 +370,7 @@ string_dependenciest::add_constraints(string_constraint_generatort &generator)
     if(test_dependencies.count(nodet(node)))
     {
       const auto &builtin = builtin_function_nodes[node.index];
-      merge(constraints, builtin.data->constraints(generator));
+      merge(constraints, builtin.data->constraints(generator, message_handler));
     }
     else
       constraints.existential.push_back(node.data->length_constraint());
diff --git a/src/solvers/strings/string_dependencies.h b/src/solvers/strings/string_dependencies.h
index 41c8a0a2691..03a455117eb 100644
--- a/src/solvers/strings/string_dependencies.h
+++ b/src/solvers/strings/string_dependencies.h
@@ -115,8 +115,9 @@ class string_dependenciest
   /// For all builtin call on which a test (or an unsupported buitin)
   /// result depends, add the corresponding constraints. For the other builtin
   /// only add constraints on the length.
-  NODISCARD string_constraintst
-  add_constraints(string_constraint_generatort &generatort);
+  NODISCARD string_constraintst add_constraints(
+    string_constraint_generatort &generatort,
+    message_handlert &message_handler);
 
   /// Clear the content of the dependency graph
   void clear();
diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp
index 9b24668cb94..f02f75ab446 100644
--- a/src/solvers/strings/string_format_builtin_function.cpp
+++ b/src/solvers/strings/string_format_builtin_function.cpp
@@ -112,7 +112,7 @@ static exprt is_null(const array_string_exprt &string, array_poolt &array_pool)
 /// \param string_arg: format string from argument
 /// \param index_type: type for indexes in strings
 /// \param char_type: type of characters
-/// \param message: message handler for warnings
+/// \param message_handler: message handler for warnings
 /// \return String expression representing the output of String.format.
 static std::pair<array_string_exprt, string_constraintst>
 add_axioms_for_format_specifier(
@@ -121,7 +121,7 @@ add_axioms_for_format_specifier(
   const array_string_exprt &string_arg,
   const typet &index_type,
   const typet &char_type,
-  const messaget &message)
+  message_handlert &message_handler)
 {
   string_constraintst constraints;
   array_poolt &array_pool = generator.array_pool;
@@ -204,14 +204,14 @@ add_axioms_for_format_specifier(
     format_specifiert fs_lower = fs;
     fs_lower.conversion = tolower(fs.conversion);
     auto format_specifier_result = add_axioms_for_format_specifier(
-      generator, fs_lower, string_arg, index_type, char_type, message);
+      generator, fs_lower, string_arg, index_type, char_type, message_handler);
 
     const exprt return_code_upper_case =
       generator.fresh_symbol("return_code_upper_case", get_return_code_type());
     const string_to_upper_case_builtin_functiont upper_case_function(
       return_code_upper_case, res, format_specifier_result.first, array_pool);
     auto upper_case_constraints =
-      upper_case_function.constraints(generator.fresh_symbol);
+      upper_case_function.constraints(generator.fresh_symbol, message_handler);
     merge(upper_case_constraints, std::move(format_specifier_result.second));
     return {res, std::move(upper_case_constraints)};
   }
@@ -222,12 +222,15 @@ add_axioms_for_format_specifier(
   case format_specifiert::HEXADECIMAL_FLOAT:
     /// \todo Conversion of hexadecimal float is not implemented.
   case format_specifiert::DATE_TIME:
+  {
     /// \todo Conversion of date-time is not implemented
     // For all these unimplemented cases we return a non-deterministic string
+    messaget message{message_handler};
     message.warning() << "unimplemented format specifier: " << fs.conversion
                       << message.eom;
     return {array_pool.fresh_string(index_type, char_type), {}};
   }
+  }
 
   INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
 }
@@ -288,14 +291,14 @@ static exprt format_arg_from_string(
 /// \param res: string expression for the result of the format function
 /// \param s: a format string
 /// \param args: a vector of arguments
-/// \param message: message handler for warnings
+/// \param message_handler: message handler for warnings
 /// \return code, 0 on success
 static std::pair<exprt, string_constraintst> add_axioms_for_format(
   string_constraint_generatort &generator,
   const array_string_exprt &res,
   const std::string &s,
   const std::vector<array_string_exprt> &args,
-  const messaget &message)
+  message_handlert &message_handler)
 {
   string_constraintst constraints;
   array_poolt &array_pool = generator.array_pool;
@@ -336,7 +339,7 @@ static std::pair<exprt, string_constraintst> add_axioms_for_format(
       }
 
       auto result = add_axioms_for_format_specifier(
-        generator, fs, string_arg, index_type, char_type, message);
+        generator, fs, string_arg, index_type, char_type, message_handler);
       merge(constraints, std::move(result.second));
       intermediary_strings.push_back(result.first);
     }
@@ -583,20 +586,15 @@ optionalt<exprt> string_format_builtin_functiont::eval(
 }
 
 string_constraintst string_format_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 {
   // When `format_string` was not set, leave the result non-deterministic
   if(!format_string.has_value())
     return {};
 
-  null_message_handlert message_handler;
   auto result_constraint_pair = add_axioms_for_format(
-    generator,
-    result,
-    format_string.value(),
-    inputs,
-    // TODO: get rid of this argument
-    messaget{message_handler});
+    generator, result, format_string.value(), inputs, message_handler);
   INVARIANT(
     simplify_expr(result_constraint_pair.first, generator.ns).is_zero(),
     "add_axioms_for_format should return 0, meaning that formatting was"
diff --git a/src/solvers/strings/string_format_builtin_function.h b/src/solvers/strings/string_format_builtin_function.h
index f9bc8d22005..0b2d1112542 100644
--- a/src/solvers/strings/string_format_builtin_function.h
+++ b/src/solvers/strings/string_format_builtin_function.h
@@ -96,8 +96,9 @@ class string_format_builtin_functiont final : public string_builtin_functiont
     return "format";
   }
 
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override;
 
   exprt length_constraint() const override;
 
diff --git a/src/solvers/strings/string_insertion_builtin_function.cpp b/src/solvers/strings/string_insertion_builtin_function.cpp
index 9ff6017b582..62609758085 100644
--- a/src/solvers/strings/string_insertion_builtin_function.cpp
+++ b/src/solvers/strings/string_insertion_builtin_function.cpp
@@ -87,7 +87,8 @@ optionalt<exprt> string_insertion_builtin_functiont::eval(
 }
 
 string_constraintst string_insertion_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  string_constraint_generatort &generator,
+  message_handlert &message_handler) const
 {
   PRECONDITION(args.size() == 1);
   const exprt &offset = args[0];
@@ -105,7 +106,8 @@ string_constraintst string_insertion_builtin_functiont::constraints(
   // Axiom 2.
   constraints.universal.push_back([&] { // NOLINT
     const symbol_exprt i = generator.fresh_symbol("QA_insert1", index_type);
-    return string_constraintt(i, offset1, equal_exprt(result[i], input1[i]));
+    return string_constraintt(
+      i, offset1, equal_exprt(result[i], input1[i]), message_handler);
   }());
 
   // Axiom 3.
@@ -114,7 +116,8 @@ string_constraintst string_insertion_builtin_functiont::constraints(
     return string_constraintt(
       i,
       zero_if_negative(array_pool.get_or_create_length(input2)),
-      equal_exprt(result[plus_exprt(i, offset1)], input2[i]));
+      equal_exprt(result[plus_exprt(i, offset1)], input2[i]),
+      message_handler);
   }());
 
   // Axiom 4.
@@ -126,7 +129,8 @@ string_constraintst string_insertion_builtin_functiont::constraints(
       zero_if_negative(array_pool.get_or_create_length(input1)),
       equal_exprt(
         result[plus_exprt(i, array_pool.get_or_create_length(input2))],
-        input1[i]));
+        input1[i]),
+      message_handler);
   }());
 
   // return_code = 0
diff --git a/src/solvers/strings/string_insertion_builtin_function.h b/src/solvers/strings/string_insertion_builtin_function.h
index cde397ed03e..877d764aa2f 100644
--- a/src/solvers/strings/string_insertion_builtin_function.h
+++ b/src/solvers/strings/string_insertion_builtin_function.h
@@ -66,8 +66,9 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
   /// This is equivalent to
   /// `res=concat(substring(input1, 0, offset'),
   ///             concat(input2, substring(input1, offset')))`.
-  string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  string_constraintst constraints(
+    string_constraint_generatort &generator,
+    message_handlert &message_handler) const override;
 
   /// \return a constraint ensuring the length of \c result corresponds to that
   ///   of \c input1 where we inserted \c input2. That is:
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
index 634f9159f2f..67ef7564596 100644
--- a/src/solvers/strings/string_refinement.cpp
+++ b/src/solvers/strings/string_refinement.cpp
@@ -158,7 +158,7 @@ string_refinementt::string_refinementt(const infot &info, bool)
   : supert(info),
     config_(info),
     loop_bound_(info.refinement_bound),
-    generator(*info.ns)
+    generator(*info.ns, *info.message_handler)
 {
 }
 
@@ -704,7 +704,9 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 #endif
 
   log.debug() << "dec_solve: add constraints" << messaget::eom;
-  merge(constraints, dependencies.add_constraints(generator));
+  merge(
+    constraints,
+    dependencies.add_constraints(generator, log.get_message_handler()));
 
 #ifdef DEBUG
   output_equations(log.debug(), equations);
@@ -1387,7 +1389,8 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
       axiom.univ_var,
       get(axiom.lower_bound),
       get(axiom.upper_bound),
-      get(axiom.body));
+      get(axiom.body),
+      stream.message.get_message_handler());
 
     exprt negaxiom = axiom_in_model.negation();
     negaxiom = simplify_expr(negaxiom, ns);
@@ -1909,7 +1912,7 @@ static optionalt<exprt> find_counter_example(
   message_handlert &message_handler)
 {
   satcheck_no_simplifiert sat_check(message_handler);
-  boolbvt solver(ns, sat_check, message_handler);
+  bv_pointerst solver(ns, sat_check, message_handler);
   solver << axiom;
 
   if(solver() == decision_proceduret::resultt::D_SATISFIABLE)
diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp
index 172e980dbcd..3847d03101c 100644
--- a/src/xmllang/graphml.cpp
+++ b/src/xmllang/graphml.cpp
@@ -177,9 +177,9 @@ static bool build_graph(
 bool read_graphml(
   std::istream &is,
   graphmlt &dest,
-  graphmlt::node_indext &entry)
+  graphmlt::node_indext &entry,
+  message_handlert &message_handler)
 {
-  null_message_handlert message_handler;
   xmlt xml;
 
   if(parse_xml(is, "", message_handler, xml))
@@ -191,9 +191,9 @@ bool read_graphml(
 bool read_graphml(
   const std::string &filename,
   graphmlt &dest,
-  graphmlt::node_indext &entry)
+  graphmlt::node_indext &entry,
+  message_handlert &message_handler)
 {
-  null_message_handlert message_handler;
   xmlt xml;
 
   if(parse_xml(filename, message_handler, xml))
diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h
index cbdcd122828..52a78d2e85e 100644
--- a/src/xmllang/graphml.h
+++ b/src/xmllang/graphml.h
@@ -19,6 +19,8 @@ Author: Michael Tautschnig, mt@eecs.qmul.ac.uk
 #include <util/graph.h>
 #include <util/xml.h>
 
+class message_handlert;
+
 struct xml_edget
 {
   xmlt xml_node;
@@ -68,11 +70,13 @@ class graphmlt:public grapht<xml_graph_nodet>
 bool read_graphml(
   std::istream &is,
   graphmlt &dest,
-  graphmlt::node_indext &entry);
+  graphmlt::node_indext &entry,
+  message_handlert &message_handler);
 bool read_graphml(
   const std::string &filename,
   graphmlt &dest,
-  graphmlt::node_indext &entry);
+  graphmlt::node_indext &entry,
+  message_handlert &message_handler);
 
 bool write_graphml(const graphmlt &src, std::ostream &os);