diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp
index cf21409ee8b..6a0715ecdb6 100644
--- a/src/solvers/refinement/bv_refinement_loop.cpp
+++ b/src/solvers/refinement/bv_refinement_loop.cpp
@@ -21,9 +21,9 @@ bv_refinementt::bv_refinementt(
   do_arithmetic_refinement(true)
 {
   // check features we need
-  assert(prop.has_set_assumptions());
-  assert(prop.has_set_to());
-  assert(prop.has_is_in_conflict());
+  PRECONDITION(prop.has_set_assumptions());
+  PRECONDITION(prop.has_set_to());
+  PRECONDITION(prop.has_is_in_conflict());
 }
 
 bv_refinementt::~bv_refinementt()
diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp
index 70faf0e600d..7b82335589a 100644
--- a/src/solvers/refinement/refine_arithmetic.cpp
+++ b/src/solvers/refinement/refine_arithmetic.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/language_util.h>
 
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/floatbv/float_utils.h>
 
 #include "bv_refinement.h"
@@ -62,7 +63,7 @@ bvt bv_refinementt::convert_mult(const exprt &expr)
 
   const typet &type=ns.follow(expr.type());
 
-  assert(operands.size()>=2);
+  PRECONDITION(operands.size()>=2);
 
   if(operands.size()>2)
     return convert_mult(make_binary(expr)); // make binary
@@ -106,7 +107,7 @@ bvt bv_refinementt::convert_div(const div_exprt &expr)
   // we catch any division
   // unless it's integer division by a constant
 
-  assert(expr.operands().size()==2);
+  PRECONDITION(expr.operands().size()==2);
 
   if(expr.op1().is_constant())
     return SUB::convert_div(expr);
@@ -124,7 +125,7 @@ bvt bv_refinementt::convert_mod(const mod_exprt &expr)
   // we catch any mod
   // unless it's integer + constant
 
-  assert(expr.operands().size()==2);
+  PRECONDITION(expr.operands().size()==2);
 
   if(expr.op1().is_constant())
     return SUB::convert_mod(expr);
@@ -152,7 +153,7 @@ void bv_refinementt::get_values(approximationt &a)
     a.op2_value=get_value(a.op2_bv);
   }
   else
-    assert(0);
+    UNREACHABLE;
 
   a.result_value=get_value(a.result_bv);
 }
@@ -170,8 +171,10 @@ void bv_refinementt::check_SAT(approximationt &a)
 
   if(type.id()==ID_floatbv)
   {
-    // these are all trinary
-    assert(a.expr.operands().size()==3);
+    // these are all ternary
+    INVARIANT(
+      a.expr.operands().size()==3,
+      string_refinement_invariantt("all floatbv typed exprs are ternary"));
 
     if(a.over_state==MAX_STATE)
       return;
@@ -203,7 +206,7 @@ void bv_refinementt::check_SAT(approximationt &a)
     else if(a.expr.id()==ID_floatbv_div)
       result/=o1;
     else
-      assert(false);
+      UNREACHABLE;
 
     if(result.pack()==a.result_value) // ok
       return;
@@ -271,9 +274,9 @@ void bv_refinementt::check_SAT(approximationt &a)
       else if(a.expr.id()==ID_floatbv_div)
         r=float_utils.div(op0, op1);
       else
-        assert(0);
+        UNREACHABLE;
 
-      assert(r.size()==res.size());
+      CHECK_RETURN(r.size()==res.size());
       bv_utils.set_equal(r, res);
     }
   }
@@ -281,7 +284,9 @@ void bv_refinementt::check_SAT(approximationt &a)
           type.id()==ID_unsignedbv)
   {
     // these are all binary
-    assert(a.expr.operands().size()==2);
+    INVARIANT(
+      a.expr.operands().size()==2,
+      string_refinement_invariantt("all (un)signedbv typed exprs are binary"));
 
     // already full interpretation?
     if(a.over_state>0)
@@ -305,7 +310,7 @@ void bv_refinementt::check_SAT(approximationt &a)
     else if(a.expr.id()==ID_mod)
       o0%=o1;
     else
-      assert(false);
+      UNREACHABLE;
 
     if(o0.pack()==a.result_value) // ok
       return;
@@ -339,21 +344,21 @@ void bv_refinementt::check_SAT(approximationt &a)
             bv_utilst::representationt::UNSIGNED);
       }
       else
-        assert(0);
+        UNREACHABLE;
 
       bv_utils.set_equal(r, a.result_bv);
     }
     else
-      assert(0);
+      UNREACHABLE;
   }
   else if(type.id()==ID_fixedbv)
   {
     // TODO: not implemented
-    assert(0);
+    TODO;
   }
   else
   {
-    assert(0);
+    UNREACHABLE;
   }
 
   status() << "Found spurious `" << a.as_string()
@@ -375,7 +380,7 @@ void bv_refinementt::check_UNSAT(approximationt &a)
   status() << "Found assumption for `" << a.as_string()
            << "' in proof (state " << a.under_state << ")" << eom;
 
-  assert(!a.under_assumptions.empty());
+  PRECONDITION(!a.under_assumptions.empty());
 
   a.under_assumptions.clear();
 
@@ -486,7 +491,7 @@ bv_refinementt::add_approximation(
   approximationt &a=approximations.back(); // stable!
 
   std::size_t width=boolbv_width(expr.type());
-  assert(width!=0);
+  PRECONDITION(width!=0);
 
   a.expr=expr;
   a.result_bv=prop.new_variables(width);
@@ -515,7 +520,7 @@ bv_refinementt::add_approximation(
     set_frozen(a.op2_bv);
   }
   else
-    assert(false);
+    UNREACHABLE;
 
   bv=a.result_bv;
 
diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp
index 5caee4b01bc..cbde7f1decb 100644
--- a/src/solvers/refinement/refine_arrays.cpp
+++ b/src/solvers/refinement/refine_arrays.cpp
@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/find_symbols.h>
 
 #include "bv_refinement.h"
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/sat/satcheck.h>
 
 /// generate array constraints
@@ -55,7 +56,9 @@ void bv_refinementt::arrays_overapproximated()
     if(current.id()==ID_implies)
     {
       implies_exprt imp=to_implies_expr(current);
-      assert(imp.operands().size()==2);
+      DATA_INVARIANT(
+        imp.operands().size()==2,
+        string_refinement_invariantt("implies must have two operands"));
       exprt implies_simplified=get(imp.op0());
       if(implies_simplified==false_exprt())
       {
@@ -67,7 +70,9 @@ void bv_refinementt::arrays_overapproximated()
     if(current.id()==ID_or)
     {
       or_exprt orexp=to_or_expr(current);
-      assert(orexp.operands().size()==2);
+      INVARIANT(
+        orexp.operands().size()==2,
+        string_refinement_invariantt("only treats the case of a binary or"));
       exprt o1=get(orexp.op0());
       exprt o2=get(orexp.op1());
       if(o1==true_exprt() || o2 == true_exprt())
@@ -91,7 +96,13 @@ void bv_refinementt::arrays_overapproximated()
       lazy_array_constraints.erase(it++);
       break;
     default:
-      assert(false);
+      error() << "error in array over approximation check" << eom;
+      INVARIANT(
+        false,
+        string_refinement_invariantt("error in array over approximation "
+          "check"));
+      // Placeholder to tell the compiler we bail
+      throw 0;
     }
   }
 
diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h
index c83d63cc69a..03233ab083a 100644
--- a/src/solvers/refinement/string_constraint.h
+++ b/src/solvers/refinement/string_constraint.h
@@ -22,6 +22,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 #include <langapi/language_ui.h>
 #include <solvers/refinement/bv_refinement.h>
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <util/refined_string_type.h>
 
 class string_constraintt: public exprt
@@ -103,13 +104,13 @@ class string_constraintt: public exprt
 
 extern inline const string_constraintt &to_string_constraint(const exprt &expr)
 {
-  assert(expr.id()==ID_string_constraint && expr.operands().size()==5);
+  PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5);
   return static_cast<const string_constraintt &>(expr);
 }
 
 extern inline string_constraintt &to_string_constraint(exprt &expr)
 {
-  assert(expr.id()==ID_string_constraint && expr.operands().size()==5);
+  PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5);
   return static_cast<string_constraintt &>(expr);
 }
 
@@ -173,16 +174,22 @@ class string_not_contains_constraintt: public exprt
 inline const string_not_contains_constraintt
 &to_string_not_contains_constraint(const exprt &expr)
 {
-  assert(expr.id()==ID_string_not_contains_constraint);
-  assert(expr.operands().size()==7);
+  PRECONDITION(expr.id()==ID_string_not_contains_constraint);
+  DATA_INVARIANT(
+    expr.operands().size()==7,
+    string_refinement_invariantt("string_not_contains_constraintt must have 7 "
+      "operands"));
   return static_cast<const string_not_contains_constraintt &>(expr);
 }
 
 inline string_not_contains_constraintt
 &to_string_not_contains_constraint(exprt &expr)
 {
-  assert(expr.id()==ID_string_not_contains_constraint);
-  assert(expr.operands().size()==7);
+  PRECONDITION(expr.id()==ID_string_not_contains_constraint);
+  DATA_INVARIANT(
+    expr.operands().size()==7,
+    string_refinement_invariantt("string_not_contains_constraintt must have 7 "
+      "operands"));
   return static_cast<string_not_contains_constraintt &>(expr);
 }
 
diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index a455f75ec7e..ca6ff4177de 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -317,7 +317,7 @@ class string_constraint_generatort
     const function_application_exprt &expr, size_t nb)
   {
     const function_application_exprt::argumentst &args=expr.arguments();
-    assert(args.size()==nb);
+    PRECONDITION(args.size()==nb);
     return args;
   }
 
diff --git a/src/solvers/refinement/string_constraint_generator_code_points.cpp b/src/solvers/refinement/string_constraint_generator_code_points.cpp
index ad44469d51e..d539e8d9e9e 100644
--- a/src/solvers/refinement/string_constraint_generator_code_points.cpp
+++ b/src/solvers/refinement/string_constraint_generator_code_points.cpp
@@ -30,7 +30,7 @@ string_exprt string_constraint_generatort::add_axioms_for_code_point(
 {
   string_exprt res=fresh_string(ref_type);
   const typet &type=code_point.type();
-  assert(type.id()==ID_signedbv);
+  PRECONDITION(type.id()==ID_signedbv);
 
   // We add axioms:
   // a1 : code_point<0x010000 => |res|=1
@@ -126,7 +126,7 @@ exprt string_constraint_generatort::add_axioms_for_code_point_at(
   const function_application_exprt &f)
 {
   typet return_type=f.type();
-  assert(return_type.id()==ID_signedbv);
+  PRECONDITION(return_type.id()==ID_signedbv);
   string_exprt str=get_string_expr(args(f, 2)[0]);
   const exprt &pos=args(f, 2)[1];
 
@@ -155,9 +155,9 @@ exprt string_constraint_generatort::add_axioms_for_code_point_before(
   const function_application_exprt &f)
 {
   const function_application_exprt::argumentst &args=f.arguments();
-  assert(args.size()==2);
+  PRECONDITION(args.size()==2);
   typet return_type=f.type();
-  assert(return_type.id()==ID_signedbv);
+  PRECONDITION(return_type.id()==ID_signedbv);
   symbol_exprt result=fresh_symbol("char", return_type);
   string_exprt str=get_string_expr(args[0]);
 
diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp
index f926147d1d4..c5021b107e3 100644
--- a/src/solvers/refinement/string_constraint_generator_comparison.cpp
+++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp
@@ -22,7 +22,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 exprt string_constraint_generatort::add_axioms_for_equals(
   const function_application_exprt &f)
 {
-  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
+  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
   symbol_exprt eq=fresh_boolean("equal");
   typecast_exprt tc_eq(eq, f.type());
 
@@ -98,7 +98,7 @@ exprt string_constraint_generatort::character_equals_ignore_case(
 exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
   const function_application_exprt &f)
 {
-  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
+  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
 
   symbol_exprt eq=fresh_boolean("equal_ignore_case");
   typecast_exprt tc_eq(eq, f.type());
@@ -207,7 +207,7 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
   //       (|s1|<|s2| &&x=|s1|) || (|s1| > |s2| &&x=|s2|) &&res=|s1|-|s2|)
   // a4 : forall i'<x. res!=0 => s1[i]=s2[i]
 
-  assert(return_type.id()==ID_signedbv);
+  PRECONDITION(return_type.id()==ID_signedbv);
 
   equal_exprt res_null=equal_exprt(res, from_integer(0, return_type));
   implies_exprt a1(res_null, s1.axiom_for_has_same_length_as(s2));
diff --git a/src/solvers/refinement/string_constraint_generator_constants.cpp b/src/solvers/refinement/string_constraint_generator_constants.cpp
index 7225a0aad00..1351a8839d4 100644
--- a/src/solvers/refinement/string_constraint_generator_constants.cpp
+++ b/src/solvers/refinement/string_constraint_generator_constants.cpp
@@ -54,8 +54,8 @@ string_exprt string_constraint_generatort::add_axioms_for_constant(
 string_exprt string_constraint_generatort::add_axioms_for_empty_string(
   const function_application_exprt &f)
 {
-  assert(f.arguments().empty());
-  assert(refined_string_typet::is_refined_string_type(f.type()));
+  PRECONDITION(f.arguments().empty());
+  PRECONDITION(refined_string_typet::is_refined_string_type(f.type()));
   const refined_string_typet &ref_type=to_refined_string_type(f.type());
   exprt size=from_integer(0, ref_type.get_index_type());
   const array_typet &content_type=ref_type.get_content_type();
@@ -74,7 +74,7 @@ string_exprt string_constraint_generatort::add_axioms_from_literal(
   const function_application_exprt &f)
 {
   const function_application_exprt::argumentst &args=f.arguments();
-  assert(args.size()==1); // Bad args to string literal?
+  PRECONDITION(args.size()==1); // Bad args to string literal?
 
   const exprt &arg=args[0];
   irep_idt sval=to_constant_expr(arg).get_value();
diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 677262092e1..33e6cc960d9 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -11,6 +11,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// Generates string constraints for the family of indexOf and lastIndexOf java
 ///   functions
 
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/refinement/string_constraint_generator.h>
 
 /// Add axioms stating that the returned value is the index within str of the
@@ -149,7 +150,10 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
     //      haystack[n+|needle|-1] != needle[|needle|-1]
     symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
     mp_integer sub_length;
-    assert(!to_integer(needle.length(), sub_length));
+    INVARIANT(
+      !to_integer(needle.length(), sub_length),
+      string_refinement_invariantt("a constant string must have constant "
+        "length"));
     exprt::operandst disjuncts;
     for(mp_integer offset=0; offset<sub_length; ++offset)
     {
@@ -263,7 +267,10 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
     //      haystack[n+|needle|-1] != needle[|needle|-1]
     symbol_exprt qvar2=fresh_univ_index("QA_index_of_string_2", index_type);
     mp_integer sub_length;
-    assert(!to_integer(needle.length(), sub_length));
+    INVARIANT(
+      !to_integer(needle.length(), sub_length),
+      string_refinement_invariantt("a constant string must have constant "
+        "length"));
     exprt::operandst disjuncts;
     for(mp_integer offset=0; offset<sub_length; ++offset)
     {
@@ -299,7 +306,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   string_exprt str=get_string_expr(args[0]);
   const exprt &c=args[1];
   const refined_string_typet &ref_type=to_refined_string_type(str.type());
-  assert(f.type()==ref_type.get_index_type());
+  PRECONDITION(f.type()==ref_type.get_index_type());
   exprt from_index;
 
   if(args.size()==2)
@@ -307,7 +314,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   else if(args.size()==3)
     from_index=args[2];
   else
-    assert(false);
+    UNREACHABLE;
 
   if(c.type().id()==ID_unsignedbv || c.type().id()==ID_signedbv)
   {
@@ -316,7 +323,10 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   }
   else
   {
-    assert(refined_string_typet::is_refined_string_type(c.type()));
+    INVARIANT(
+      refined_string_typet::is_refined_string_type(c.type()),
+      string_refinement_invariantt("c can only be a (un)signedbv or a refined "
+        "string and the (un)signedbv case is already handled"));
     string_exprt sub=get_string_expr(c);
     return add_axioms_for_index_of_string(str, sub, from_index);
   }
@@ -396,14 +406,14 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   exprt c=args[1];
   const refined_string_typet &ref_type=to_refined_string_type(str.type());
   exprt from_index;
-  assert(f.type()==ref_type.get_index_type());
+  PRECONDITION(f.type()==ref_type.get_index_type());
 
   if(args.size()==2)
     from_index=minus_exprt(str.length(), from_integer(1, str.length().type()));
   else if(args.size()==3)
     from_index=args[2];
   else
-    assert(false);
+    UNREACHABLE;
 
   if(c.type().id()==ID_unsignedbv || c.type().id()==ID_signedbv)
   {
diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/refinement/string_constraint_generator_insert.cpp
index b7a0a381bad..65ccc3b89d7 100644
--- a/src/solvers/refinement/string_constraint_generator_insert.cpp
+++ b/src/solvers/refinement/string_constraint_generator_insert.cpp
@@ -9,6 +9,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// \file
 /// Generates string constraints for the family of insert Java functions
 
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/refinement/string_constraint_generator.h>
 
 /// add axioms stating that the result correspond to the first string where we
@@ -18,7 +19,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 string_exprt string_constraint_generatort::add_axioms_for_insert(
   const string_exprt &s1, const string_exprt &s2, const exprt &offset)
 {
-  assert(offset.type()==s1.length().type());
+  PRECONDITION(offset.type()==s1.length().type());
   string_exprt pref=add_axioms_for_substring(
     s1, from_integer(0, offset.type()), offset);
   string_exprt suf=add_axioms_for_substring(s1, offset, s1.length());
@@ -34,7 +35,7 @@ string_exprt string_constraint_generatort::add_axioms_for_insert(
 string_exprt string_constraint_generatort::add_axioms_for_insert(
   const function_application_exprt &f)
 {
-  assert(f.arguments().size()>=3);
+  PRECONDITION(f.arguments().size()>=3);
   string_exprt s1=get_string_expr(f.arguments()[0]);
   string_exprt s2=get_string_expr(f.arguments()[2]);
   const exprt &offset=f.arguments()[1];
@@ -47,7 +48,10 @@ string_exprt string_constraint_generatort::add_axioms_for_insert(
   }
   else
   {
-    assert(f.arguments().size()==3);
+    INVARIANT(
+      f.arguments().size()==3,
+      string_refinement_invariantt("f must have 2 or 5 arguments and the case "
+        "of 5 arguments is already handled"));
     return add_axioms_for_insert(s1, s2, offset);
   }
 }
@@ -156,7 +160,10 @@ string_exprt string_constraint_generatort::add_axioms_for_insert_char_array(
   }
   else
   {
-    assert(f.arguments().size()==4);
+    INVARIANT(
+      f.arguments().size()==4,
+      string_refinement_invariantt("f must have 4 or 6 arguments and the case "
+        "of 6 arguments is already handled"));
     count=f.arguments()[2];
     offset=from_integer(0, count.type());
   }
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index 00b494eccaf..d697514767c 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -19,6 +19,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 #include <ansi-c/string_constant.h>
 #include <java_bytecode/java_types.h>
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/refinement/string_constraint_generator.h>
 #include <util/arith_tools.h>
 #include <util/pointer_predicates.h>
@@ -130,7 +131,7 @@ string_exprt string_constraint_generatort::fresh_string(
 /// \return a string expression
 string_exprt string_constraint_generatort::get_string_expr(const exprt &expr)
 {
-  assert(refined_string_typet::is_refined_string_type(expr.type()));
+  PRECONDITION(refined_string_typet::is_refined_string_type(expr.type()));
 
   if(expr.id()==ID_symbol)
   {
@@ -150,7 +151,7 @@ string_exprt string_constraint_generatort::get_string_expr(const exprt &expr)
 string_exprt string_constraint_generatort::convert_java_string_to_string_exprt(
     const exprt &jls)
 {
-  assert(jls.id()==ID_struct);
+  PRECONDITION(jls.id()==ID_struct);
 
   exprt length(to_struct_expr(jls).op1());
   // TODO: Add assertion on the type.
@@ -205,11 +206,11 @@ void string_constraint_generatort::add_default_axioms(
 string_exprt string_constraint_generatort::add_axioms_for_refined_string(
   const exprt &string)
 {
-  assert(refined_string_typet::is_refined_string_type(string.type()));
+  PRECONDITION(refined_string_typet::is_refined_string_type(string.type()));
   refined_string_typet type=to_refined_string_type(string.type());
 
   // Function applications should have been removed before
-  assert(string.id()!=ID_function_application);
+  PRECONDITION(string.id()!=ID_function_application);
 
   if(string.id()==ID_symbol)
   {
@@ -236,9 +237,13 @@ string_exprt string_constraint_generatort::add_axioms_for_refined_string(
   }
   else
   {
-    throw "add_axioms_for_refined_string:\n"+string.pretty()+
-      "\nwhich is not a function application, "+
-      "a symbol, a struct or an if expression";
+    INVARIANT(
+      false,
+      string_refinement_invariantt("add_axioms_for_refined_string:\n"+
+        string.pretty()+"\nwhich is not a function application, a symbol, a "+
+        "struct or an if expression"));
+    // For the compiler
+    throw 0;
   }
 }
 
@@ -248,10 +253,10 @@ string_exprt string_constraint_generatort::add_axioms_for_refined_string(
 string_exprt string_constraint_generatort::add_axioms_for_if(
   const if_exprt &expr)
 {
-  assert(
+  PRECONDITION(
     refined_string_typet::is_refined_string_type(expr.true_case().type()));
   string_exprt t=get_string_expr(expr.true_case());
-  assert(
+  PRECONDITION(
     refined_string_typet::is_refined_string_type(expr.false_case().type()));
   string_exprt f=get_string_expr(expr.false_case());
   const refined_string_typet &ref_type=to_refined_string_type(t.type());
@@ -336,7 +341,7 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
   const function_application_exprt &expr)
 {
   const exprt &name=expr.function();
-  assert(name.id()==ID_symbol);
+  PRECONDITION(name.id()==ID_symbol);
 
   const irep_idt &id=is_ssa_expr(name)?to_ssa_expr(name).get_object_name():
     to_symbol_expr(name).get_identifier();
@@ -521,7 +526,7 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
     std::string msg(
       "string_constraint_generator::function_application: unknown symbol :");
     msg+=id2string(id);
-    throw msg;
+    DATA_INVARIANT(false, string_refinement_invariantt(msg));
   }
   function_application_cache[expr]=res;
   return res;
@@ -543,7 +548,10 @@ string_exprt string_constraint_generatort::add_axioms_for_copy(
   }
   else
   {
-    assert(args.size()==3);
+    INVARIANT(
+      args.size()==3,
+      string_refinement_invariantt("f must have 1 or 3 arguments and the case "
+        "of 3 arguments is already handled"));
     string_exprt s1=get_string_expr(args[0]);
     exprt offset=args[1];
     exprt count=args[2];
@@ -583,7 +591,7 @@ exprt string_constraint_generatort::add_axioms_for_char_pointer(
   //       refinement. We need regression tests that use that function.
 
   // TODO: we do not know what to do in the other cases
-  assert(false);
+  TODO;
   return exprt();
 }
 
@@ -610,7 +618,7 @@ string_exprt string_constraint_generatort::add_axioms_from_char_array(
   const exprt &offset,
   const exprt &count)
 {
-  assert(false); // deprecated, we should use add_axioms_for_substring instead
+  UNREACHABLE; // deprecated, we should use add_axioms_for_substring instead
   const typet &char_type=to_array_type(data.type()).subtype();
   const typet &index_type=length.type();
   refined_string_typet ref_type(index_type, char_type);
@@ -622,7 +630,7 @@ string_exprt string_constraint_generatort::add_axioms_from_char_array(
 
   symbol_exprt qvar=fresh_univ_index("QA_string_of_char_array", index_type);
   exprt char_in_tab=data;
-  assert(char_in_tab.id()==ID_index);
+  PRECONDITION(char_in_tab.id()==ID_index);
   char_in_tab.op1()=plus_exprt_with_overflow_check(qvar, offset);
 
   string_constraintt a1(qvar, count, equal_exprt(str[qvar], char_in_tab));
@@ -640,7 +648,7 @@ string_exprt string_constraint_generatort::add_axioms_from_char_array(
 string_exprt string_constraint_generatort::add_axioms_from_char_array(
   const function_application_exprt &f)
 {
-  assert(false); // deprecated, we should use add_axioms_for_substring instead
+  UNREACHABLE; // deprecated, we should use add_axioms_for_substring instead
   exprt offset;
   exprt count;
   if(f.arguments().size()==4)
@@ -650,7 +658,10 @@ string_exprt string_constraint_generatort::add_axioms_from_char_array(
   }
   else
   {
-    assert(f.arguments().size()==2);
+    INVARIANT(
+      f.arguments().size()==2,
+      string_refinement_invariantt("f must have 2 or 4 arguments and the case "
+        "of 4 arguments is already handled"));
     count=f.arguments()[0];
     offset=from_integer(0, count.type());
   }
@@ -675,7 +686,7 @@ exprt string_constraint_generatort::add_axioms_for_char_literal(
   const function_application_exprt &f)
 {
   const function_application_exprt::argumentst &args=f.arguments();
-  assert(args.size()==1); // there should be exactly 1 argument to char literal
+  PRECONDITION(args.size()==1); // there should be exactly 1 arg to char literal
 
   const exprt &arg=args[0];
   // for C programs argument to char literal should be one string constant
@@ -687,12 +698,15 @@ exprt string_constraint_generatort::add_axioms_for_char_literal(
   {
     const string_constantt s=to_string_constant(arg.op0().op0().op0());
     irep_idt sval=s.get_value();
-    assert(sval.size()==1);
+    CHECK_RETURN(sval.size()==1);
     return from_integer(unsigned(sval[0]), arg.type());
   }
   else
   {
-    throw "convert_char_literal unimplemented";
+    // convert_char_literal unimplemented
+    UNIMPLEMENTED;
+    // For the compiler
+    throw 0;
   }
 }
 
diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp
index 4e2134d6388..9b8a743e022 100644
--- a/src/solvers/refinement/string_constraint_generator_testing.cpp
+++ b/src/solvers/refinement/string_constraint_generator_testing.cpp
@@ -10,6 +10,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// \file
 /// Generates string constraints for string functions that return Boolean values
 
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/refinement/string_constraint_generator.h>
 
 /// add axioms stating that the returned expression is true exactly when the
@@ -72,7 +73,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
   const function_application_exprt &f, bool swap_arguments)
 {
   const function_application_exprt::argumentst &args=f.arguments();
-  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
+  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
   string_exprt s0=get_string_expr(args[swap_arguments?1:0]);
   string_exprt s1=get_string_expr(args[swap_arguments?0:1]);
   exprt offset;
@@ -90,7 +91,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
 exprt string_constraint_generatort::add_axioms_for_is_empty(
   const function_application_exprt &f)
 {
-  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
+  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
 
   // We add axioms:
   // a1 : is_empty => |s0| = 0
@@ -113,8 +114,8 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix(
   const function_application_exprt &f, bool swap_arguments)
 {
   const function_application_exprt::argumentst &args=f.arguments();
-  assert(args.size()==2); // bad args to string issuffix?
-  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
+  PRECONDITION(args.size()==2); // bad args to string issuffix?
+  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
 
   symbol_exprt issuffix=fresh_boolean("issuffix");
   typecast_exprt tc_issuffix(issuffix, f.type());
@@ -183,7 +184,7 @@ bool string_constraint_generatort::is_constant_string(
 exprt string_constraint_generatort::add_axioms_for_contains(
   const function_application_exprt &f)
 {
-  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
+  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
   string_exprt s0=get_string_expr(args(f, 2)[0]);
   string_exprt s1=get_string_expr(args(f, 2)[1]);
   bool constant=is_constant_string(s1);
@@ -222,7 +223,10 @@ exprt string_constraint_generatort::add_axioms_for_contains(
     // If the string is constant, we can use a more efficient axiom for a4:
     // contains ==> AND_{i < |s1|} s1[i] = s0[startpos + i]
     mp_integer s1_length;
-    assert(!to_integer(s1.length(), s1_length));
+    INVARIANT(
+      !to_integer(s1.length(), s1_length),
+      string_refinement_invariantt("a constant string expression must have a "
+        "constant length"));
     exprt::operandst conjuncts;
     for(mp_integer i=0; i<s1_length; ++i)
     {
diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp
index a0010f2ec22..1e2f8d0f536 100644
--- a/src/solvers/refinement/string_constraint_generator_transformation.cpp
+++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp
@@ -11,6 +11,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// Generates string constraints for string transformations, that is, functions
 ///   taking one string and returning another
 
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/refinement/string_constraint_generator.h>
 
 /// add axioms to say that the returned string expression has length given by
@@ -69,7 +70,7 @@ string_exprt string_constraint_generatort::add_axioms_for_substring(
   const function_application_exprt &f)
 {
   const function_application_exprt::argumentst &args=f.arguments();
-  assert(args.size()>=2);
+  PRECONDITION(args.size()>=2);
   string_exprt str=get_string_expr(args[0]);
   exprt i(args[1]);
   exprt j;
@@ -79,7 +80,10 @@ string_exprt string_constraint_generatort::add_axioms_for_substring(
   }
   else
   {
-    assert(args.size()==2);
+    INVARIANT(
+      args.size()==2,
+      string_refinement_invariantt("f must have 2 or 3 arguments and the case "
+        "of 3 arguments is already handled"));
     j=str.length();
   }
   return add_axioms_for_substring(str, i, j);
@@ -96,8 +100,8 @@ string_exprt string_constraint_generatort::add_axioms_for_substring(
 {
   const refined_string_typet &ref_type=to_refined_string_type(str.type());
   const typet &index_type=ref_type.get_index_type();
-  assert(start.type()==index_type);
-  assert(end.type()==index_type);
+  PRECONDITION(start.type()==index_type);
+  PRECONDITION(end.type()==index_type);
   string_exprt res=fresh_string(ref_type);
 
   // We add axioms:
@@ -397,8 +401,8 @@ string_exprt string_constraint_generatort::add_axioms_for_delete_char_at(
 string_exprt string_constraint_generatort::add_axioms_for_delete(
   const string_exprt &str, const exprt &start, const exprt &end)
 {
-  assert(start.type()==str.length().type());
-  assert(end.type()==str.length().type());
+  PRECONDITION(start.type()==str.length().type());
+  PRECONDITION(end.type()==str.length().type());
   string_exprt str1=add_axioms_for_substring(
     str, from_integer(0, str.length().type()), start);
   string_exprt str2=add_axioms_for_substring(str, end, str.length());
diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp
index c59a20dab81..2995648dc38 100644
--- a/src/solvers/refinement/string_constraint_generator_valueof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp
@@ -11,6 +11,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// Generates string constraints for functions generating strings from other
 ///   types, in particular int, long, float, double, char, bool
 
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/refinement/string_constraint_generator.h>
 
 /// Add axioms corresponding to the String.valueOf(I) java function.
@@ -54,7 +55,7 @@ string_exprt string_constraint_generatort::add_axioms_from_bool(
   string_exprt res=fresh_string(ref_type);
   const typet &char_type=ref_type.get_char_type();
 
-  assert(b.type()==bool_typet() || b.type().id()==ID_c_bool);
+  PRECONDITION(b.type()==bool_typet() || b.type().id()==ID_c_bool);
 
   typecast_exprt eq(b, bool_typet());
 
@@ -236,7 +237,7 @@ string_exprt string_constraint_generatort::add_axioms_from_int_hex(
 {
   string_exprt res=fresh_string(ref_type);
   const typet &type=i.type();
-  assert(type.id()==ID_signedbv);
+  PRECONDITION(type.id()==ID_signedbv);
   const typet &index_type=ref_type.get_index_type();
   const typet &char_type=ref_type.get_char_type();
   exprt sixteen=from_integer(16, index_type);
@@ -350,7 +351,10 @@ string_exprt string_constraint_generatort::add_axioms_for_value_of(
   }
   else
   {
-    assert(args.size()==1);
+    INVARIANT(
+      args.size()==1,
+      string_refinement_invariantt("f can only have 1 or 3 arguments and the "
+        "case of 3 has been handled"));
     return add_axioms_for_java_char_array(args[0]);
   }
 }
@@ -429,7 +433,7 @@ exprt string_constraint_generatort::add_axioms_for_parse_int(
   const typet &char_type=ref_type.get_char_type();
   exprt minus_char=constant_char('-', char_type);
   exprt plus_char=constant_char('+', char_type);
-  assert(type.id()==ID_signedbv);
+  PRECONDITION(type.id()==ID_signedbv);
 
   exprt chr=str[0];
   exprt starts_with_minus=equal_exprt(chr, minus_char);
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index bdc33e7fe6d..8df999e1855 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -26,6 +26,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <util/simplify_expr.h>
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/string_refinement.h>
+#include <solvers/refinement/string_refinement_invariant.h>
 #include <langapi/language_util.h>
 #include <java_bytecode/java_types.h>
 
@@ -125,7 +126,7 @@ void string_refinementt::add_instantiations()
 void string_refinementt::add_symbol_to_symbol_map(
   const exprt &lhs, const exprt &rhs)
 {
-  assert(lhs.id()==ID_symbol);
+  PRECONDITION(lhs.id()==ID_symbol);
 
   // We insert the mapped value of the rhs, if it exists.
   auto it=symbol_resolve.find(rhs);
@@ -148,7 +149,7 @@ void string_refinementt::add_symbol_to_symbol_map(
 void string_refinementt::set_char_array_equality(
   const exprt &lhs, const exprt &rhs)
 {
-  assert(lhs.id()==ID_symbol);
+  PRECONDITION(lhs.id()==ID_symbol);
 
   if(rhs.id()==ID_array && rhs.type().id()==ID_array)
   {
@@ -268,10 +269,18 @@ void string_refinementt::concretize_string(const exprt &expr)
     mp_integer found_length;
     if(!to_integer(length, found_length))
     {
-      assert(found_length.is_long());
-      assert(found_length>=0);
+      INVARIANT(
+        found_length.is_long(),
+        string_refinement_invariantt("the length of a string should be a "
+          "long"));
+      INVARIANT(
+        found_length>=0,
+        string_refinement_invariantt("the length of a string should be >= 0"));
       size_t concretize_limit=found_length.to_long();
-      assert(concretize_limit<=generator.max_string_length);
+      INVARIANT(
+        concretize_limit<=generator.max_string_length,
+        string_refinement_invariantt("string length must be less than the max "
+          "length"));
       exprt content_expr=str.content();
       std::vector<exprt> result;
 
@@ -366,7 +375,10 @@ void string_refinementt::concretize_lengths()
 /// \par parameters: an expression and the value to set it to
 void string_refinementt::set_to(const exprt &expr, bool value)
 {
-  assert(equality_propagation);
+  INVARIANT(
+    equality_propagation,
+    string_refinement_invariantt("set_to should only be called when equality "
+      "propagation is enabled"));
 
   if(expr.id()==ID_equal)
   {
@@ -385,7 +397,10 @@ void string_refinementt::set_to(const exprt &expr, bool value)
     {
       error() << "string_refinementt::set_to got non-boolean operand: "
               << expr.pretty() << eom;
-      throw 0;
+      INVARIANT(
+        false,
+        string_refinement_invariantt("set_to should only be called with exprs "
+          "of type bool"));
     }
 
     // Preprocessing to remove function applications.
@@ -426,9 +441,12 @@ void string_refinementt::set_to(const exprt &expr, bool value)
     else
     {
       // TODO: Something should also be done if value is false.
-      assert(!is_char_array(eq_expr.rhs().type()));
-      assert(!refined_string_typet::is_refined_string_type(
-        eq_expr.rhs().type()));
+      INVARIANT(
+        !is_char_array(eq_expr.rhs().type()),
+        string_refinement_invariantt("set_to cannot set a char_array"));
+      INVARIANT(
+        !refined_string_typet::is_refined_string_type(eq_expr.rhs().type()),
+        string_refinement_invariantt("set_to cannot set a refined_string"));
     }
 
     non_string_axioms.push_back(std::make_pair(equal_exprt(lhs, subst_rhs),
@@ -743,7 +761,7 @@ std::string string_refinementt::string_of_array(const array_exprt &arr)
       return std::string("");
 
   exprt size_expr=to_array_type(arr.type()).size();
-  assert(size_expr.id()==ID_constant);
+  PRECONDITION(size_expr.id()==ID_constant);
   to_unsigned_integer(to_constant_expr(size_expr), n);
   std::string str(n, '?');
 
@@ -755,7 +773,7 @@ std::string string_refinementt::string_of_array(const array_exprt &arr)
     // TODO: factorize with utf16_little_endian_to_ascii
     unsigned c;
     exprt arr_i=arr.operands()[i];
-    assert(arr_i.id()==ID_constant);
+    PRECONDITION(arr_i.id()==ID_constant);
     to_unsigned_integer(to_constant_expr(arr_i), c);
     if(c<=255 && c>=32)
       result << (unsigned char) c;
@@ -796,12 +814,16 @@ void string_refinementt::fill_model()
         debug() << " = \"" << string_of_array(to_array_expr(arr))
                 << "\" (size:" << from_expr(ns, "", len) << ")"<< eom;
       else
-        debug() << " = " << from_expr(ns, "", arr) << " (size:" << from_expr(ns, "", len)
-                << ")" << eom;
+        debug() << " = " << from_expr(ns, "", arr)
+                << " (size:" << from_expr(ns, "", len) << ")" << eom;
     }
     else
     {
-      assert(is_char_array(it.second.type()));
+      INVARIANT(
+        is_char_array(it.second.type()),
+        string_refinement_invariantt("symbol_resolve should only map to "
+          "refined_strings or to char_arrays, and refined_strings are already "
+          "handled"));
       exprt arr=it.second;
       replace_expr(symbol_resolve, arr);
       replace_expr(current_model, arr);
@@ -809,7 +831,8 @@ void string_refinementt::fill_model()
       current_model[it.first]=arr_model;
 
       debug() << from_expr(ns, "", to_symbol_expr(it.first)) << "="
-              << from_expr(ns, "", arr) << " = " << from_expr(ns, "", arr_model) << "" << eom;
+              << from_expr(ns, "", arr) << " = "
+              << from_expr(ns, "", arr_model) << "" << eom;
     }
   }
 
@@ -846,14 +869,17 @@ exprt string_refinementt::substitute_array_with_expr(
     const exprt &then_expr=with_expr.new_value();
     exprt else_expr=substitute_array_with_expr(with_expr.old(), index);
     const typet &type=then_expr.type();
-    assert(else_expr.type()==type);
+    CHECK_RETURN(else_expr.type()==type);
     return if_exprt(
       equal_exprt(index, with_expr.where()), then_expr, else_expr, type);
   }
   else
   {
-    // Only handle 'with' expressions on 'array_of' expressions.
-    assert(expr.id()==ID_array_of);
+    // Only handle 'with' expressions and 'array_of' expressions.
+    INVARIANT(
+      expr.id()==ID_array_of,
+      string_refinement_invariantt("only handles 'with' and 'array_of' "
+        "expressions, and expr is 'with' is handled above"));
     return to_array_of_expr(expr).what();
   }
 }
@@ -910,10 +936,16 @@ void string_refinementt::substitute_array_access(exprt &expr) const
       return;
     }
 
-    assert(index_expr.array().id()==ID_array);
+    DATA_INVARIANT(
+      index_expr.array().id()==ID_array,
+      string_refinement_invariantt("and index expression must be on a symbol, "
+        "with, array_of, if, or array, and all cases besides array are handled "
+        "above"));
     array_exprt &array_expr=to_array_expr(index_expr.array());
 
-    assert(!array_expr.operands().empty());
+    INVARIANT(
+      !array_expr.operands().empty(),
+      string_refinement_invariantt("the array expression should not be empty"));
     size_t last_index=array_expr.operands().size()-1;
 
     const typet &char_type=index_expr.array().type().subtype();
@@ -921,8 +953,11 @@ void string_refinementt::substitute_array_access(exprt &expr) const
 
     if(ite.type()!=char_type)
     {
-      // We have to manualy set the type for unknown values
-      assert(ite.id()==ID_unknown);
+      // We have to manually set the type for unknown values
+      INVARIANT(
+        ite.id()==ID_unknown,
+        string_refinement_invariantt("the last element can only have type char "
+          "or unknown, and it is not char type"));
       ite.type()=char_type;
     }
 
@@ -934,7 +969,10 @@ void string_refinementt::substitute_array_access(exprt &expr) const
       equal_exprt equals(index_expr.index(), from_integer(i, java_int_type()));
       if(op_it->type()!=char_type)
       {
-        assert(op_it->id()==ID_unknown);
+        INVARIANT(
+          op_it->id()==ID_unknown,
+          string_refinement_invariantt("elements can only have type char or "
+            "unknown, and it is not char type"));
         op_it->type()=char_type;
       }
       ite=if_exprt(equals, *op_it, ite);
@@ -1152,7 +1190,8 @@ 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) << eom;
+        debug() << "adding counter example " << from_expr(ns, "", instance)
+                << eom;
         add_lemma(instance);
       }
     }
@@ -1306,14 +1345,20 @@ exprt string_refinementt::compute_inverse_function(
   bool neg=false;
 
   auto it=elems.find(qvar);
-  assert(it!=elems.end());
+  INVARIANT(
+    it!=elems.end(),
+    string_refinement_invariantt("a function must have an occurrence of qvar"));
   if(it->second==1 || it->second==-1)
   {
     neg=(it->second==1);
   }
   else
   {
-    assert(it->second==0);
+    INVARIANT(
+      it->second==0,
+      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;
   }
@@ -1447,7 +1492,9 @@ void string_refinementt::update_index_set(const exprt &formula)
     {
       const exprt &s=cur.op0();
       const exprt &i=cur.op1();
-      assert(s.type().id()==ID_array);
+      DATA_INVARIANT(
+        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);
     }
@@ -1594,7 +1641,10 @@ exprt string_refinementt::substitute_array_lists(exprt expr) const
 
   if(expr.id()=="array-list")
   {
-    assert(expr.operands().size()>=2);
+    DATA_INVARIANT(
+      expr.operands().size()>=2,
+      string_refinement_invariantt("array-lists must have at least two "
+        "operands"));
     typet &char_type=expr.operands()[1].type();
     array_typet arr_type(char_type, infinity_exprt(char_type));
     array_of_exprt new_arr(from_integer(0, char_type),
@@ -1665,6 +1715,8 @@ bool string_refinementt::is_axiom_sat(
   case decision_proceduret::resultt::D_UNSATISFIABLE:
     return false;
   default:
-    throw "failure in checking axiom";
+    INVARIANT(false, string_refinement_invariantt("failure in checking axiom"));
+    // To tell the compiler that the previous line bails
+    throw 0;
   }
 }
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 419ad086f84..7e534825596 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -24,6 +24,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <util/replace_expr.h>
 #include <solvers/refinement/string_constraint.h>
 #include <solvers/refinement/string_constraint_generator.h>
+#include <solvers/refinement/string_refinement_invariant.h>
 
 #define MAX_NB_REFINEMENT 100
 
@@ -198,7 +199,10 @@ void string_refinementt::pad_vector(
     // pad until we reach the next initialized index (right to left)
     while(i>leftmost_index_to_pad)
       concrete_array[(i--)-1]=last_concretized;
-    assert(i==leftmost_index_to_pad);
+    INVARIANT(
+      i==leftmost_index_to_pad,
+      string_refinement_invariantt("Loop decrements i until it is not greater "
+        " than leftmost_index_to_pad"));
     if(i>0)
       last_concretized=concrete_array[i-1];
   }
diff --git a/src/solvers/refinement/string_refinement_invariant.h b/src/solvers/refinement/string_refinement_invariant.h
new file mode 100644
index 00000000000..59f0c64cc28
--- /dev/null
+++ b/src/solvers/refinement/string_refinement_invariant.h
@@ -0,0 +1,15 @@
+/*******************************************************************\
+
+Module: Placeholder for eventual upgraded invariants.
+
+Author: Jesse Sigal, jesse.sigal@diffblue.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_INVARIANT_H
+#define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_INVARIANT_H
+
+#define string_refinement_invariantt(reason) \
+  (("string_refinement_invariantt("+std::string(reason)+")").c_str())
+
+#endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_INVARIANT_H