diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index f9d23f2b566..d9fc22be67b 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -7,7 +7,6 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 
-#include <cassert>
 #include <iostream>
 
 #include <langapi/language_util.h>
@@ -50,10 +49,12 @@ literalt arrayst::record_array_equality(
   if(!base_type_eq(op0.type(), op1.type(), ns))
   {
     prop.error() << equality.pretty() << messaget::eom;
-    throw "record_array_equality got equality without matching types";
+    DATA_INVARIANT(false, "record_array_equality got equality without matching types");
   }
 
-  assert(ns.follow(op0.type()).id()==ID_array);
+  DATA_INVARIANT(
+    ns.follow(op0.type()).id()==ID_array,
+    "record_array_equality parameter should be array-typed");
 
   array_equalities.push_back(array_equalityt());
 
@@ -109,14 +110,15 @@ void arrayst::collect_arrays(const exprt &a)
 
   if(a.id()==ID_with)
   {
-    if(a.operands().size()!=3)
-      throw "with expected to have three operands";
+    DATA_INVARIANT(
+      a.operands().size()==3,
+      "with expected to have three operands");
 
     // check types
     if(!base_type_eq(array_type, a.op0().type(), ns))
     {
       prop.error() << a.pretty() << messaget::eom;
-      throw "collect_arrays got 'with' without matching types";
+      DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
     }
 
     arrays.make_union(a, a.op0());
@@ -131,14 +133,15 @@ void arrayst::collect_arrays(const exprt &a)
   }
   else if(a.id()==ID_update) // TODO: is this obsolete?
   {
-    if(a.operands().size()!=3)
-      throw "update expected to have three operands";
+    DATA_INVARIANT(
+      a.operands().size()==3,
+      "update expected to have three operands");
 
     // check types
     if(!base_type_eq(array_type, a.op0().type(), ns))
     {
       prop.error() << a.pretty() << messaget::eom;
-      throw "collect_arrays got 'update' without matching types";
+      DATA_INVARIANT(false, "collect_arrays got 'update' without matching types");
     }
 
     arrays.make_union(a, a.op0());
@@ -155,21 +158,22 @@ void arrayst::collect_arrays(const exprt &a)
   }
   else if(a.id()==ID_if)
   {
-    if(a.operands().size()!=3)
-      throw "if expected to have three operands";
+    DATA_INVARIANT(
+      a.operands().size()==3,
+      "if expected to have three operands");
 
     // check types
     if(!base_type_eq(array_type, a.op1().type(), ns))
     {
       prop.error() << a.pretty() << messaget::eom;
-      throw "collect_arrays got if without matching types";
+      DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
     // check types
     if(!base_type_eq(array_type, a.op2().type(), ns))
     {
       prop.error() << a.pretty() << messaget::eom;
-      throw "collect_arrays got if without matching types";
+      DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
     arrays.make_union(a, a.op1());
@@ -185,9 +189,10 @@ void arrayst::collect_arrays(const exprt &a)
   }
   else if(a.id()==ID_member)
   {
-    if(to_member_expr(a).struct_op().id()!=ID_symbol)
-      throw
-        "unexpected array expression: member with `"+a.op0().id_string()+"'";
+    DATA_INVARIANT(
+      to_member_expr(a).struct_op().id()==ID_symbol,
+      ("unexpected array expression: member with `"+
+       a.op0().id_string()+"'").c_str());
   }
   else if(a.id()==ID_constant ||
           a.id()==ID_array ||
@@ -200,20 +205,24 @@ void arrayst::collect_arrays(const exprt &a)
   else if(a.id()==ID_byte_update_little_endian ||
           a.id()==ID_byte_update_big_endian)
   {
-    assert(0);
+    DATA_INVARIANT(
+      false,
+      "byte_update should be removed before collect_arrays");
   }
   else if(a.id()==ID_typecast)
   {
     // cast between array types?
-    assert(a.operands().size()==1);
+    DATA_INVARIANT(
+      a.operands().size()==1,
+      "typecast must have one operand");
 
-    if(a.op0().type().id()==ID_array)
-    {
-      arrays.make_union(a, a.op0());
-      collect_arrays(a.op0());
-    }
-    else
-      throw "unexpected array type cast from "+a.op0().type().id_string();
+    DATA_INVARIANT(
+      a.op0().type().id()==ID_array,
+      ("unexpected array type cast from "+
+       a.op0().type().id_string()).c_str());
+
+    arrays.make_union(a, a.op0());
+    collect_arrays(a.op0());
   }
   else if(a.id()==ID_index)
   {
@@ -222,7 +231,12 @@ void arrayst::collect_arrays(const exprt &a)
     collect_arrays(a.op0());
   }
   else
-    throw "unexpected array expression (collect_arrays): `"+a.id_string()+"'";
+  {
+    DATA_INVARIANT(
+      false,
+      ("unexpected array expression (collect_arrays): `"+
+       a.id_string()+"'").c_str());
+  }
 }
 
 /// adds array constraints (refine=true...lazily for the refinement loop)
@@ -364,7 +378,7 @@ void arrayst::update_index_map(std::size_t i)
     return;
 
   std::size_t root_number=arrays.find_number(i);
-  assert(root_number!=i);
+  INVARIANT(root_number!=i, "is_root_number incorrect?");
 
   index_sett &root_index_set=index_map[root_number];
   index_sett &index_set=index_map[i];
@@ -435,7 +449,9 @@ void arrayst::add_array_constraints(
     index_expr2.array()=array_equality.f2;
     index_expr2.index()=*it;
 
-    assert(index_expr1.type()==index_expr2.type());
+    DATA_INVARIANT(
+      index_expr1.type()==index_expr2.type(),
+      "array elements should all have same type");
 
     array_equalityt equal;
     equal.f1 = index_expr1;
@@ -477,12 +493,14 @@ void arrayst::add_array_constraints(
   else if(expr.id()==ID_byte_update_little_endian ||
           expr.id()==ID_byte_update_big_endian)
   {
-    assert(0);
+    INVARIANT(false, "byte_update should be removed before arrayst");
   }
   else if(expr.id()==ID_typecast)
   {
     // we got a=(type[])b
-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size()==1,
+      "typecast should have one operand");
 
     // add a[i]=b[i]
     for(index_sett::const_iterator
@@ -500,7 +518,9 @@ void arrayst::add_array_constraints(
       index_expr2.array()=expr.op0();
       index_expr2.index()=*it;
 
-      assert(index_expr1.type()==index_expr2.type());
+      DATA_INVARIANT(
+        index_expr1.type()==index_expr2.type(),
+        "array elements should all have same type");
 
       // add constraint
       lazy_constraintt lazy(lazy_typet::ARRAY_TYPECAST,
@@ -512,9 +532,12 @@ void arrayst::add_array_constraints(
   {
   }
   else
-    throw
-      "unexpected array expression (add_array_constraints): `"+
-        expr.id_string()+"'";
+  {
+    DATA_INVARIANT(
+      false,
+      ("unexpected array expression (add_array_constraints): `"+
+       expr.id_string()+"'").c_str());
+  }
 }
 
 void arrayst::add_array_constraints_with(
@@ -536,7 +559,9 @@ void arrayst::add_array_constraints_with(
     if(index_expr.type()!=value.type())
     {
       prop.error() << expr.pretty() << messaget::eom;
-      throw "index_expr and value types should match";
+      DATA_INVARIANT(
+        false,
+        "with-expression operand should match array element type");
     }
 
     lazy_constraintt lazy(
@@ -575,7 +600,9 @@ void arrayst::add_array_constraints_with(
         index_expr2.array()=expr.op0();
         index_expr2.index()=other_index;
 
-        assert(index_expr1.type()==index_expr2.type());
+        DATA_INVARIANT(
+          index_expr1.type()==index_expr2.type(),
+          "array elements should all have same type");
 
         equal_exprt equality_expr(index_expr1, index_expr2);
 
@@ -620,7 +647,9 @@ void arrayst::add_array_constraints_update(
     if(index_expr.type()!=value.type())
     {
       prop.error() << expr.pretty() << messaget::eom;
-      throw "index_expr and value types should match";
+      DATA_INVARIANT(
+        false,
+        "update operand should match array element type");
     }
 
     set_to_true(equal_exprt(index_expr, value));
@@ -657,7 +686,9 @@ void arrayst::add_array_constraints_update(
         index_expr2.array()=expr.op0();
         index_expr2.index()=other_index;
 
-        assert(index_expr1.type()==index_expr2.type());
+        DATA_INVARIANT(
+          index_expr1.type()==index_expr2.type(),
+          "array elements should all have same type");
 
         equal_exprt equality_expr(index_expr1, index_expr2);
 
@@ -693,7 +724,9 @@ void arrayst::add_array_constraints_array_of(
     index_expr.array()=expr;
     index_expr.index()=*it;
 
-    assert(base_type_eq(index_expr.type(), expr.op0().type(), ns));
+    DATA_INVARIANT(
+      base_type_eq(index_expr.type(), expr.op0().type(), ns),
+      "array_of operand type should match array element type");
 
     // add constraint
     lazy_constraintt lazy(
@@ -730,7 +763,9 @@ void arrayst::add_array_constraints_if(
     index_expr2.array()=expr.true_case();
     index_expr2.index()=*it;
 
-    assert(index_expr1.type()==index_expr2.type());
+    DATA_INVARIANT(
+      index_expr1.type()==index_expr2.type(),
+      "array elements should all have same type");
 
     // add implication
     lazy_constraintt lazy(lazy_typet::ARRAY_IF,
@@ -759,7 +794,9 @@ void arrayst::add_array_constraints_if(
     index_expr2.array()=expr.false_case();
     index_expr2.index()=*it;
 
-    assert(index_expr1.type()==index_expr2.type());
+    DATA_INVARIANT(
+      index_expr1.type()==index_expr2.type(),
+      "array elements should all have same type");
 
     // add implication
     lazy_constraintt lazy(